diff options
Diffstat (limited to '')
-rw-r--r-- | HoTT_Methods.thy | 92 |
1 files changed, 14 insertions, 78 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index bce5123..20f3ece 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -2,8 +2,7 @@ Author: Josh Chen Date: Jun 2018 -Method setup for the HoTT library. -Relies heavily on Eisbach. +Method setup for the HoTT library. Relies heavily on Eisbach. *) theory HoTT_Methods @@ -11,14 +10,14 @@ theory HoTT_Methods "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" HoTT_Base - Equal - Prod - Sum begin + section \<open>Method setup\<close> -text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using rules declared [intro] and [elim], as well as additional provided lemmas." +text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using rules declared [intro] and [elim], as well as additional provided lemmas. + +Can also perform typechecking, and search for elements of a type." method simple uses lems = (assumption|standard|rule lems)+ @@ -33,83 +32,20 @@ method wellformed uses jdgmt = ( ) -text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations." +text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations. +\<open>wellformed\<close> uses the facts passed as \<open>lems\<close> to derive any required typing judgments. +Definitions passed as \<open>unfolds\<close> are unfolded throughout. + +Roughly speaking \<open>derive\<close> is more powerful than \<open>simple\<close>, but may fail to find a proof where \<open>simple\<close> does if it reduces too eagerly." -method derive uses lems = ( - catch \<open>unfold lems\<close> \<open>fail\<close> | - catch \<open>simple lems: lems\<close> \<open>fail\<close> | +method derive uses lems unfolds = ( + unfold unfolds | + simple lems: lems | match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> )+ -section \<open>Examples\<close> - -lemma - assumes "A : U" "B: A \<rightarrow> U" "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" - shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U" -by (simple lems: assms) - -lemma - assumes "f : \<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z" - shows - "A : U" and - "B: A \<rightarrow> U" and - "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" and - "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" -proof - - show "A : U" by (wellformed jdgmt: assms) - show "B: A \<rightarrow> U" by (wellformed jdgmt: assms) - show "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" by (wellformed jdgmt: assms) - show "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" by (wellformed jdgmt: assms) -qed - - -section \<open>Experimental methods\<close> - -text "Playing around with ML, following CTT/CTT.thy by Larry Paulson." - -lemmas forms = Prod_form Sum_form Equal_form -lemmas intros = Prod_intro Sum_intro Equal_intro -lemmas elims = Prod_elim Sum_elim Equal_elim -lemmas elements = intros elims - -ML \<open> -(* Try solving \<open>a : A\<close> by assumption provided \<open>a\<close> is rigid *) -fun test_assume_tac ctxt = let - fun is_rigid (Const(@{const_name is_of_type},_) $ a $ _) = not(is_Var (head_of a)) - | is_rigid (Const(@{const_name is_a_type},_) $ a $ _ $ _) = not(is_Var (head_of a)) - | is_rigid _ = false - in - SUBGOAL (fn (prem, i) => - if is_rigid (Logic.strip_assums_concl prem) - then assume_tac ctxt i else no_tac) - end - -fun ASSUME ctxt tf i = test_assume_tac ctxt i ORELSE tf i - -(* Solve all subgoals \<open>A : U\<close> using formation rules. *) -val form_net = Tactic.build_net @{thms forms}; -fun form_tac ctxt = - REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 form_net)); - -(* Try to prove inhabitation judgments \<open>a : A\<close> (\<open>a\<close> flexible, \<open>A\<close> rigid) by introduction rules. *) -fun intro_tac ctxt thms = - let val tac = - filt_resolve_from_net_tac ctxt 1 - (Tactic.build_net (thms @ @{thms forms} @ @{thms intros})) - in REPEAT_FIRST (ASSUME ctxt tac) end - -(*Type checking: solve \<open>a : A\<close> (\<open>a\<close> rigid, \<open>A\<close> flexible) by formation, introduction and elimination rules. *) -fun typecheck_tac ctxt thms = - let val tac = - filt_resolve_from_net_tac ctxt 3 - (Tactic.build_net (thms @ @{thms forms} @ @{thms elements})) - in REPEAT_FIRST (ASSUME ctxt tac) end -\<close> - -method_setup form = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))\<close> -method_setup intro = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intro_tac ctxt ths))\<close> -method_setup typecheck = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typecheck_tac ctxt ths))\<close> +text "Simplify function applications." end
\ No newline at end of file |