diff options
author | Josh Chen | 2019-02-17 18:34:38 +0100 |
---|---|---|
committer | Josh Chen | 2019-02-17 18:34:38 +0100 |
commit | 68aa069172933b875d70a5ef71e9db0ae685a92d (patch) | |
tree | bd1da2111e12bab878641661d91f95f66f8132cc /HoTT_Methods.thy | |
parent | 76b57317d7568f4dcd673b1b8085601c6c723355 (diff) |
Method "quantify" converts product inhabitation into Pure universal statements. Also misc. cleanups.
Diffstat (limited to '')
-rw-r--r-- | HoTT_Methods.thy | 29 |
1 files changed, 21 insertions, 8 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 088c1fa..d93680a 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -2,6 +2,8 @@ Isabelle/HoTT: Proof methods Jan 2019 +Setup various proof methods and auxiliary functionality. + ********) theory HoTT_Methods @@ -10,6 +12,25 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" begin +section \<open>More method combinators\<close> + +ML \<open> +(* Use as "repeat n tac" *) +fun repeat tac = + let + fun cparser_of parser (ctxt, toks) = parser toks ||> (fn toks => (ctxt, toks)) + in + cparser_of Args.text >> + (fn n => fn ctxt => fn facts => + SIMPLE_METHOD ( + REPEAT_DETERM_N + (the (Int.fromString n)) + (tac ctxt)) + facts) + end +\<close> + + section \<open>Substitution and simplification\<close> ML_file "~~/src/Tools/misc_legacy.ML" @@ -67,12 +88,4 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}. method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ - -section \<open>Induction\<close> - -text \<open> -Placeholder section for the automation of induction, i.e. using the type elimination rules. -At the moment one must directly apply them with @{method rule} or @{method elim}. -\<close> - end |