diff options
| author | Josh Chen | 2019-02-23 18:57:15 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-23 18:57:15 +0100 |
| commit | 232856fbef15105f619a5c1056da2602984804df (patch) | |
| tree | fac1ffadc75dc5de325d14bd9280c5083cb156b1 /HoTT_Methods.thy | |
| parent | 0c96ce5c0b0b0948d7c5dca1634f0e0b3658b113 (diff) | |
compute method solves subgoals arising from subst
Diffstat (limited to 'HoTT_Methods.thy')
| -rw-r--r-- | HoTT_Methods.thy | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index c9744e9..ad7384d 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -2,7 +2,7 @@ Isabelle/HoTT: Proof methods Jan 2019 -Setup various proof methods and auxiliary functionality. +Set up various proof methods and auxiliary functionality. ********) @@ -23,10 +23,12 @@ ML_file "~~/src/Tools/eqsubst.ML" text \<open> Method @{theory_text compute} performs single-step simplifications, using any rules declared @{attribute comp} in the context. -Premises of the rule(s) applied are added as new subgoals. +Subgoals arising from a substitution are solved by assumption and standard rules, as well as rules passed using @{theory_text add}. + +Note that the solving is sometimes a little eager; for more manual control one should use @{method subst} directly. \<close> -method compute declares comp = (subst comp) +method compute uses add declares comp = (subst comp; (rule add | assumption | rule)?) section \<open>Handling universes\<close> @@ -51,7 +53,7 @@ method cumulativity declares form = ( section \<open>Deriving typing judgments\<close> -method routine uses add = (assumption | rule add | rule)+ +method routine uses add = (rule add | assumption | rule)+ text \<open> The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}. @@ -65,8 +67,8 @@ The method @{theory_text derive} combines @{method routine} and @{method compute It also handles universes using @{method hierarchy} and @{method cumulativity}. \<close> -method derive uses lems = - (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ +method derive uses lems declares comp = + (routine add: lems | compute add: lems comp: comp | cumulativity form: lems | hierarchy)+ section \<open>Additional method combinators\<close> |