diff options
Diffstat (limited to 'HoTT_Methods.thy')
| -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 |