diff options
| -rw-r--r-- | Coprod.thy | 26 | ||||
| -rw-r--r-- | Equal.thy | 28 | ||||
| -rw-r--r-- | EqualProps.thy | 3 | ||||
| -rw-r--r-- | HoTT.thy | 21 | ||||
| -rw-r--r-- | HoTT_Base.thy | 1 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 5 | ||||
| -rw-r--r-- | Nat.thy | 19 | ||||
| -rw-r--r-- | Prod.thy | 24 | ||||
| -rw-r--r-- | ProdProps.thy | 3 | ||||
| -rw-r--r-- | Proj.thy | 9 | ||||
| -rw-r--r-- | Sum.thy | 36 | ||||
| -rw-r--r-- | ex/HoTT book/Ch1.thy | 3 | ||||
| -rw-r--r-- | ex/Methods.thy | 3 | ||||
| -rw-r--r-- | ex/Synthesis.thy | 7 | ||||
| -rw-r--r-- | tests/Subgoal.thy | 10 | ||||
| -rw-r--r-- | tests/Test.thy | 12 |
16 files changed, 102 insertions, 108 deletions
@@ -1,8 +1,7 @@ (* Title: HoTT/Coprod.thy Author: Josh Chen - Date: Aug 2018 -Coproduct type. +Coproduct type *) theory Coprod @@ -20,9 +19,9 @@ axiomatization where Coprod_form: "\<lbrakk>A: U(i); B: U(i)\<rbrakk> \<Longrightarrow> A + B: U(i)" and - Coprod_intro1: "\<lbrakk>a: A; B: U(i)\<rbrakk> \<Longrightarrow> inl(a): A + B" + Coprod_intro_inl: "\<lbrakk>a: A; B: U(i)\<rbrakk> \<Longrightarrow> inl(a): A + B" and - Coprod_intro2: "\<lbrakk>b: B; A: U(i)\<rbrakk> \<Longrightarrow> inr(b): A + B" + Coprod_intro_inr: "\<lbrakk>b: B; A: U(i)\<rbrakk> \<Longrightarrow> inr(b): A + B" and Coprod_elim: "\<lbrakk> C: A + B \<longrightarrow> U(i); @@ -31,14 +30,14 @@ and u: A + B \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(u) : C(u)" and - Coprod_comp1: "\<lbrakk> + Coprod_comp_inl: "\<lbrakk> C: A + B \<longrightarrow> U(i); \<And>x. x: A \<Longrightarrow> c(x): C(inl(x)); \<And>y. y: B \<Longrightarrow> d(y): C(inr(y)); a: A \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(inl(a)) \<equiv> c(a)" and - Coprod_comp2: "\<lbrakk> + Coprod_comp_inr: "\<lbrakk> C: A + B \<longrightarrow> U(i); \<And>x. x: A \<Longrightarrow> c(x): C(inl(x)); \<And>y. y: B \<Longrightarrow> d(y): C(inr(y)); @@ -49,17 +48,18 @@ and text "Admissible formation inference rules:" axiomatization where - Coprod_form_cond1: "A + B: U(i) \<Longrightarrow> A: U(i)" + Coprod_wellform1: "A + B: U(i) \<Longrightarrow> A: U(i)" and - Coprod_form_cond2: "A + B: U(i) \<Longrightarrow> B: U(i)" + Coprod_wellform2: "A + B: U(i) \<Longrightarrow> B: U(i)" -text "Rule declarations:" +text "Rule attribute declarations:" -lemmas Coprod_intro = Coprod_intro1 Coprod_intro2 -lemmas Coprod_rules [intro] = Coprod_form Coprod_intro Coprod_elim Coprod_comp1 Coprod_comp2 -lemmas Coprod_form_conds [wellform] = Coprod_form_cond1 Coprod_form_cond2 -lemmas Coprod_comps [comp] = Coprod_comp1 Coprod_comp2 +lemmas Coprod_intro = Coprod_intro_inl Coprod_intro_inr + +lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr +lemmas Coprod_wellform [wellform] = Coprod_wellform1 Coprod_wellform2 +lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_comp Coprod_elim end @@ -1,8 +1,7 @@ (* Title: HoTT/Equal.thy Author: Josh Chen - Date: Jun 2018 -Equality type. +Equality type *) theory Equal @@ -33,36 +32,35 @@ and Equal_intro: "a : A \<Longrightarrow> refl(a): a =\<^sub>A a" and Equal_elim: "\<lbrakk> - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i); - \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x); x: A; y: A; - p: x =\<^sub>A y + p: x =\<^sub>A y; + \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x); + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i) \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(p) : C(x)(y)(p)" and Equal_comp: "\<lbrakk> - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i); + a: A; \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x); - a: A + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i) \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(refl(a)) \<equiv> f(a)" text "Admissible inference rules for equality type formation:" axiomatization where - Equal_form_cond1: "a =\<^sub>A b: U(i) \<Longrightarrow> A: U(i)" + Equal_wellform1: "a =\<^sub>A b: U(i) \<Longrightarrow> A: U(i)" and - Equal_form_cond2: "a =\<^sub>A b: U(i) \<Longrightarrow> a: A" + Equal_wellform2: "a =\<^sub>A b: U(i) \<Longrightarrow> a: A" and - Equal_form_cond3: "a =\<^sub>A b: U(i) \<Longrightarrow> b: A" - + Equal_wellform3: "a =\<^sub>A b: U(i) \<Longrightarrow> b: A" -text "Rule declarations:" -lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -lemmas Equal_wellform [wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 -lemmas Equal_comps [comp] = Equal_comp +text "Rule attribute declarations:" +lemmas Equal_comp [comp] +lemmas Equal_wellform [wellform] = Equal_wellform1 Equal_wellform2 Equal_wellform3 +lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_comp Equal_elim end diff --git a/EqualProps.thy b/EqualProps.thy index 3c9b971..8b83c5b 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -1,8 +1,7 @@ (* Title: HoTT/EqualProps.thy Author: Josh Chen - Date: Aug 2018 -Properties of equality. +Properties of equality *) theory EqualProps @@ -1,7 +1,7 @@ (* Title: HoTT/HoTT.thy Author: Josh Chen -Load all the component modules for the HoTT logic. +Homotopy type theory *) theory HoTT @@ -12,15 +12,26 @@ HoTT_Base HoTT_Methods (* Types *) -Prod -Sum -Equal Coprod +Equal Nat +Prod +Sum -(* Additional properties *) +(* Derived definitions and properties *) EqualProps +ProdProps Proj begin + +lemmas form_rules = + Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form +lemmas intro_rules = + Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro +lemmas elim_rules = + Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim +lemmas routine_rules = + Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine + end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 1b8c526..a229e83 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,6 +1,5 @@ (* Title: HoTT/HoTT_Base.thy Author: Josh Chen - Date: Aug 2018 Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell. *) diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 316841d..4d2174b 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -1,6 +1,5 @@ (* Title: HoTT/HoTT_Methods.thy Author: Josh Chen - Date: Jun 2018 Method setup for the HoTT library. Relies heavily on Eisbach. *) @@ -18,7 +17,7 @@ section \<open>Method definitions\<close> subsection \<open>Simple type rule proof search\<close> text " - Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using the type rules declared [intro] and [elim] (in the respective theory files), as well as additional provided lemmas. + 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. " @@ -62,7 +61,7 @@ ML_file "~~/src/Tools/eqsubst.ML" text "Perform basic single-step computations:" -method compute uses lems = (subst lems comp) +method compute uses lems = (subst lems comp | rule lems comp) end @@ -1,8 +1,7 @@ (* Title: HoTT/Nat.thy Author: Josh Chen - Date: Aug 2018 -Natural numbers. +Natural numbers *) theory Nat @@ -20,9 +19,9 @@ axiomatization where Nat_form: "\<nat>: U(O)" and - Nat_intro1: "0: \<nat>" + Nat_intro_0: "0: \<nat>" and - Nat_intro2: "n: \<nat> \<Longrightarrow> succ(n): \<nat>" + Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ(n): \<nat>" and Nat_elim: "\<lbrakk> C: \<nat> \<longrightarrow> U(i); @@ -31,13 +30,13 @@ and n: \<nat> \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(n): C(n)" and - Nat_comp1: "\<lbrakk> + Nat_comp_0: "\<lbrakk> C: \<nat> \<longrightarrow> U(i); \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n); a: C(0) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(0) \<equiv> a" and - Nat_comp2: "\<lbrakk> + Nat_comp_succ: "\<lbrakk> C: \<nat> \<longrightarrow> U(i); \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n); a: C(0); @@ -45,11 +44,11 @@ and \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)" -text "Rule declarations:" +text "Rule attribute declarations:" -lemmas Nat_intro = Nat_intro1 Nat_intro2 -lemmas Nat_rules [intro] = Nat_form Nat_intro Nat_elim Nat_comp1 Nat_comp2 -lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 +lemmas Nat_intro = Nat_intro_0 Nat_intro_succ +lemmas Nat_comp [comp] = Nat_comp_0 Nat_comp_succ +lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_comp Nat_elim end @@ -1,8 +1,7 @@ (* Title: HoTT/Prod.thy Author: Josh Chen - Date: Aug 2018 -Dependent product (function) type. +Dependent product (function) type *) theory Prod @@ -39,11 +38,11 @@ section \<open>Type rules\<close> axiomatization where Prod_form: "\<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x): U(i)" and - Prod_intro: "\<lbrakk>A: U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b(x): \<Prod>x:A. B(x)" + Prod_intro: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b(x): B(x); A: U(i)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b(x): \<Prod>x:A. B(x)" and Prod_elim: "\<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)" and - Prod_comp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b(x): B(x); a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)" + Prod_appl: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b(x): B(x); a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)" and Prod_uniq: "f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f" and @@ -62,15 +61,16 @@ text " " axiomatization where - Prod_form_cond1: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)" + Prod_wellform1: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)" and - Prod_form_cond2: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)" + Prod_wellform2: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)" -text "Set up the standard reasoner to use the type rules:" -lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq Prod_eq -lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2 -lemmas Prod_comps [comp] = Prod_comp Prod_uniq Prod_eq +text "Rule attribute declarations---set up various methods to use the type rules." + +lemmas Prod_comp [comp] = Prod_appl Prod_uniq +lemmas Prod_wellform [wellform] = Prod_wellform1 Prod_wellform2 +lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_comp Prod_elim section \<open>Function composition\<close> @@ -96,8 +96,8 @@ and and Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c" -lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp -lemmas Unit_comps [comp] = Unit_comp +lemmas Unit_comp [comp] +lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_comp Unit_elim end diff --git a/ProdProps.thy b/ProdProps.thy index adadb29..3e51102 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -1,8 +1,7 @@ (* Title: HoTT/ProdProps.thy Author: Josh Chen - Date: Aug 2018 -Properties of the dependent product. +Properties of the dependent product *) theory ProdProps @@ -1,6 +1,5 @@ (* Title: HoTT/Proj.thy Author: Josh Chen - Date: Jun 2018 Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent sum type. *) @@ -27,7 +26,7 @@ lemma fst_comp: unfolding fst_def proof show "a: A" and "b: B(a)" by fact+ -qed (rule assms)+ +qed (simple lems: assms)+ lemma snd_type: assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)" @@ -54,10 +53,10 @@ proof qed (simple lems: assms) -text "Rule declarations:" +text "Rule attribute declarations:" -lemmas Proj_types [intro] = fst_type snd_type -lemmas Proj_comps [comp] = fst_comp snd_comp +lemmas Proj_type [intro] = fst_type snd_type +lemmas Proj_comp [comp] = fst_comp snd_comp end @@ -1,8 +1,7 @@ (* Title: HoTT/Sum.thy Author: Josh Chen - Date: Jun 2018 -Dependent sum type. +Dependent sum type *) theory Sum @@ -36,32 +35,35 @@ section \<open>Type rules\<close> axiomatization where Sum_form: "\<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x): U(i)" and - Sum_intro: "\<lbrakk>B: A \<longrightarrow> U(i); a: A; b: B(a)\<rbrakk> \<Longrightarrow> <a,b> : \<Sum>x:A. B(x)" + Sum_intro: "\<lbrakk>B: A \<longrightarrow> U(i); a: A; b: B(a)\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B(x)" and Sum_elim: "\<lbrakk> - C: \<Sum>x:A. B(x) \<longrightarrow> U(i); - \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C(<x,y>); - p : \<Sum>x:A. B(x) - \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)(p) : C(p)" (* What does writing \<lambda>x y. f(x, y) change? *) + p: \<Sum>x:A. B(x); + \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x)(y): C(<x,y>); + C: \<Sum>x:A. B(x) \<longrightarrow> U(i) + \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)(p): C(p)" (* What does writing \<lambda>x y. f(x, y) change? *) and Sum_comp: "\<lbrakk> - C: \<Sum>x:A. B(x) \<longrightarrow> U(i); - B: A \<longrightarrow> U(i); - \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C(<x,y>); a: A; - b: B(a) + b: B(a); + \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x)(y): C(<x,y>); + B: A \<longrightarrow> U(i); + C: \<Sum>x:A. B(x) \<longrightarrow> U(i) \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)(<a,b>) \<equiv> f(a)(b)" text "Admissible inference rules for sum formation:" axiomatization where - Sum_form_cond1: "(\<Sum>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)" + Sum_wellform1: "(\<Sum>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)" and - Sum_form_cond2: "(\<Sum>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)" + Sum_wellform2: "(\<Sum>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)" + + +text "Rule attribute declarations:" -lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp -lemmas Sum_wellform [wellform] = Sum_form_cond1 Sum_form_cond2 -lemmas Sum_comps [comp] = Sum_comp +lemmas Sum_comp [comp] +lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2 +lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_comp Sum_elim section \<open>Empty type\<close> @@ -74,7 +76,7 @@ where and Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)" -lemmas Empty_rules [intro] = Empty_form Empty_elim +lemmas Empty_routine [intro] = Empty_form Empty_elim end diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy index cc0adf5..d5f05dd 100644 --- a/ex/HoTT book/Ch1.thy +++ b/ex/HoTT book/Ch1.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/HoTT book/Ch1.thy Author: Josh Chen - Date: Aug 2018 A formalization of some content of Chapter 1 of the Homotopy Type Theory book. *) @@ -41,4 +40,4 @@ proof (rule Sum_elim[where ?p=p]) qed (derive lems: assms) -end
\ No newline at end of file +end diff --git a/ex/Methods.thy b/ex/Methods.thy index 871964f..415fbc3 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/Methods.thy Author: Josh Chen - Date: Aug 2018 HoTT method usage examples *) @@ -74,4 +73,4 @@ proof compute qed fact -end
\ No newline at end of file +end diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index e5a8ecf..cff9374 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/Synthesis.thy Author: Josh Chen - Date: Aug 2018 Examples of synthesis. *) @@ -33,8 +32,8 @@ text " schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n" apply compute prefer 4 apply compute -prefer 3 apply (rule Nat_rules) -apply (rule Nat_rules | assumption)+ +prefer 3 apply compute +apply (rule Nat_routine Nat_elim | assumption)+ done text " @@ -52,7 +51,7 @@ proof (simple lems: pred_type) proof compute show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0" - proof (rule Nat_comps) + proof compute show "\<nat>: U(O)" .. qed simple qed rule diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy index 4fcffad..9690013 100644 --- a/tests/Subgoal.thy +++ b/tests/Subgoal.thy @@ -13,21 +13,16 @@ lemma rpathcomp_type: shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" unfolding rpathcomp_def apply standard -prefer 2 subgoal premises 1 for x \<comment> \<open>\<open>subgoal\<close> is the proof script version of \<open>fix-assume-show\<close>.\<close> apply standard - prefer 2 subgoal premises 2 for y apply standard - prefer 2 subgoal premises 3 for p apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) \<comment> \<open>specifying \<open>?A=A\<close> is crucial here to prevent the next \<open>subgoal\<close> from binding a schematic ?A which should be instantiated to \<open>A\<close>.\<close> - prefer 2 + prefer 4 apply standard - prefer 2 apply (rule Prod_intro) - prefer 2 subgoal premises 4 for u z q apply (rule Equal_elim[where ?x=u and ?y=z]) apply (simple lems: assms 4) @@ -58,11 +53,8 @@ text " " apply (rule Prod_intro) -prefer 2 apply (rule Prod_intro) - prefer 2 apply (rule Prod_intro) - prefer 2 subgoal 123 for x y p apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) oops diff --git a/tests/Test.thy b/tests/Test.thy index 433039c..c0dc0dd 100644 --- a/tests/Test.thy +++ b/tests/Test.thy @@ -6,8 +6,8 @@ This is an old "test suite" from early implementations of the theory. It is not always guaranteed to be up to date, or reflect most recent versions of the theory. *) -theory HoTT_Test - imports HoTT +theory Test + imports "../HoTT" begin @@ -31,14 +31,14 @@ text " Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following. " -proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" using assms .. +proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" by (simple lems: assms) proposition assumes "A : U(i)" and "A \<equiv> B" shows "\<^bold>\<lambda>x. x : B \<rightarrow> A" proof - - have "A\<rightarrow>A \<equiv> B\<rightarrow>A" using assms by simp - moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" using assms(1) .. + have "A \<rightarrow> A \<equiv> B \<rightarrow> A" using assms by simp + moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (simple lems: assms) ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp qed @@ -102,7 +102,7 @@ lemma curried_type_judgment: text " - Polymorphic identity function. Trivial due to lambda expression polymorphism. + Polymorphic identity function is now trivial due to lambda expression polymorphism. (Was more involved in previous monomorphic incarnations.) " |