diff options
Diffstat (limited to 'HoTT_Methods.thy')
| -rw-r--r-- | HoTT_Methods.thy | 79 |
1 files changed, 44 insertions, 35 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 32e412b..f0cee6c 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -1,46 +1,47 @@ -(* Title: HoTT/HoTT_Methods.thy - Author: Josh Chen +(* +Title: HoTT_Methods.thy +Author: Joshua Chen +Date: 2018 -Method setup for the HoTT library. Relies heavily on Eisbach. +Method setup for the HoTT logic. *) theory HoTT_Methods - imports - "HOL-Eisbach.Eisbach" - "HOL-Eisbach.Eisbach_Tools" - HoTT_Base +imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" + begin -section \<open>Deriving typing judgments\<close> +section \<open>Handling universes\<close> -text " - \<open>routine\<close> proves routine type judgments \<open>a : A\<close> using the rules declared [intro] in the respective theory files, as well as additional provided lemmas. -" +method provelt = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+) -method routine uses lems = (assumption | rule lems | standard)+ +method hierarchy = (rule U_hierarchy, provelt) -text " - \<open>wellformed'\<close> finds a proof of any valid typing judgment derivable from the judgment passed as \<open>jdmt\<close>. - If no judgment is passed, it will try to resolve with the theorems declared \<open>wellform\<close>. - \<open>wellform\<close> is like \<open>wellformed'\<close> but takes multiple judgments. +method cumulativity declares form = ( + ((elim U_cumulative' | (rule U_cumulative', rule form)), rule leq_min) | + ((elim U_cumulative | (rule U_cumulative, rule form)), provelt) +) - The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy. -" +text \<open> +Methods @{method provelt}, @{method hierarchy}, and @{method cumulativity} prove statements of the form +\<^item> \<open>n < (Suc (... (Suc n) ...))\<close>, +\<^item> \<open>U i: U (Suc (... (Suc i) ...))\<close>, and +\<^item> @{prop "A: U i \<Longrightarrow> A: U j"}, where @{prop "i \<le> j"} +respectively. +\<close> -method wellformed' uses jdmt declares wellform = - match wellform in rl: "PROP ?P" \<Rightarrow> \<open>( - catch \<open>rule rl[OF jdmt]\<close> \<open>fail\<close> | - catch \<open>wellformed' jdmt: rl[OF jdmt]\<close> \<open>fail\<close> - )\<close> -method wellformed uses lems = - match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed' jdmt: lem\<close> +section \<open>Deriving typing judgments\<close> +method routine uses add = (assumption | rule add | rule)+ -section \<open>Substitution and simplification\<close> +text \<open> +The method @{method routine} proves type judgments @{prop "a : A"} using the rules declared @{attribute intro} in the respective theory files, as well as additional provided lemmas passed using the modifier \<open>add\<close>. +\<close> -text "Import the \<open>subst\<close> method, used for substituting definitional equalities." + +section \<open>Substitution and simplification\<close> ML_file "~~/src/Tools/misc_legacy.ML" ML_file "~~/src/Tools/IsaPlanner/isand.ML" @@ -48,24 +49,32 @@ ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" ML_file "~~/src/Tools/IsaPlanner/zipper.ML" ML_file "~~/src/Tools/eqsubst.ML" -text "Perform basic single-step computations:" +\<comment> \<open>Import the @{method subst} method, used for substituting definitional equalities.\<close> + +method compute declares comp = (subst comp) -method compute uses lems = (subst lems comp | rule lems comp) +text \<open> +Method @{method 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. +\<close> section \<open>Derivation search\<close> -text " Combine \<open>routine\<close>, \<open>wellformed\<close>, and \<open>compute\<close> to search for derivations of judgments." +text \<open> +Combine @{method routine} and @{method compute} to search for derivations of judgments. +Also handle universes using @{method hierarchy} and @{method cumulativity}. +\<close> -method derive uses lems = (routine lems: lems | compute lems: lems | wellformed lems: lems)+ +method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ section \<open>Induction\<close> -text " - Placeholder section for the automation of induction, i.e. using the elimination rules. - At the moment one must directly apply them with \<open>rule X_elim\<close>. -" +text \<open> +Placeholder section for the automation of induction, i.e. using the elimination rules. +At the moment one must directly apply them with \<open>rule X_elim\<close>. +\<close> end |