diff options
Diffstat (limited to '')
-rw-r--r-- | HoTT_Methods.thy | 42 |
1 files changed, 23 insertions, 19 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 4d2174b..32e412b 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -12,23 +12,19 @@ theory HoTT_Methods begin -section \<open>Method definitions\<close> - -subsection \<open>Simple type rule proof search\<close> +section \<open>Deriving typing judgments\<close> text " - Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using the type rules declared [intro] in the respective theory files, as well as additional provided lemmas. - - Can also perform typechecking, and search for elements of a type. + \<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 simple uses lems = (assumption | rule lems | standard)+ - - -subsection \<open>Wellformedness checker\<close> +method routine uses lems = (assumption | rule lems | standard)+ text " - \<open>wellformed\<close> finds a proof of any valid typing judgment derivable from the judgments passed as \<open>lem\<close>. + \<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. + The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy. " @@ -42,14 +38,7 @@ method wellformed uses lems = match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed' jdmt: lem\<close> -subsection \<open>Derivation search\<close> - -text " Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations of judgments." - -method derive uses lems = (simple lems: lems | wellformed lems: lems)+ - - -subsection \<open>Substitution and simplification\<close> +section \<open>Substitution and simplification\<close> text "Import the \<open>subst\<close> method, used for substituting definitional equalities." @@ -64,4 +53,19 @@ text "Perform basic single-step computations:" method compute uses lems = (subst lems comp | rule lems comp) +section \<open>Derivation search\<close> + +text " Combine \<open>routine\<close>, \<open>wellformed\<close>, and \<open>compute\<close> to search for derivations of judgments." + +method derive uses lems = (routine lems: lems | compute lems: lems | wellformed lems: lems)+ + + +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>. +" + + end |