diff options
Diffstat (limited to '')
| -rw-r--r-- | Equal.thy | 1 | ||||
| -rw-r--r-- | EqualProps.thy | 22 | ||||
| -rw-r--r-- | HoTT.thy | 1 | ||||
| -rw-r--r-- | HoTT_Base.thy | 2 | ||||
| -rw-r--r-- | Prod.thy | 1 | ||||
| -rw-r--r-- | Proj.thy | 35 | ||||
| -rw-r--r-- | Sum.thy | 3 |
7 files changed, 45 insertions, 20 deletions
@@ -9,6 +9,7 @@ theory Equal imports HoTT_Base begin + axiomatization Equal :: "[Term, Term, Term] \<Rightarrow> Term" and refl :: "Term \<Rightarrow> Term" ("(refl'(_'))" 1000) and diff --git a/EqualProps.thy b/EqualProps.thy index 2807587..cb267c6 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -22,22 +22,14 @@ definition inv :: "[Term, Term, Term] \<Rightarrow> Term" ("(1inv[_,/ _,/ _])") lemma inv_type: assumes "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x" - by (derive lems: assms unfolds: inv_def) + unfolding inv_def + by (derive lems: assms) lemma inv_comp: assumes "a : A" shows "inv[A,a,a]`refl(a) \<equiv> refl(a)" - -proof - - have "inv[A,a,a]`refl(a) \<equiv> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a)" - by (derive lems: assms unfolds: inv_def) - - also have "indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)" - by (simple lems: assms) - - finally show "inv[A,a,a]`refl(a) \<equiv> refl(a)" . -qed + unfolding inv_def by (simplify lems: assms) section \<open>Transitivity / Path composition\<close> @@ -50,6 +42,7 @@ definition rcompose :: "Term \<Rightarrow> Term" ("(1rcompose[_])") (\<lambda>x. \<^bold>\<lambda>z:A. \<^bold>\<lambda>p:(x =\<^sub>A z). indEqual[A](\<lambda>x z _. x =\<^sub>A z) (\<lambda>x. refl(x)) x z p) x y p" + text "``Natural'' composition function abbreviation, effectively equivalent to a function of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>." abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compose[_,/ _,/ _,/ _])") @@ -59,14 +52,15 @@ abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compo lemma compose_type: assumes "p : x =\<^sub>A y" and "q : y =\<^sub>A z" shows "compose[A,x,y,z]`p`q : x =\<^sub>A z" - by (derive lems: assms unfolds: rcompose_def) + unfolding rcompose_def + by (derive lems: assms) lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" - -sorry \<comment> \<open>Long and tedious proof if the Simplifier is not set up.\<close> + unfolding rcompose_def + by (simplify lems: assms) lemmas Equal_simps [intro] = inv_comp compose_comp @@ -5,7 +5,6 @@ Load all the component modules for the HoTT logic. *) theory HoTT - imports (* Basic theories *) diff --git a/HoTT_Base.thy b/HoTT_Base.thy index cfced79..60e5167 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -15,7 +15,7 @@ section \<open>Setup\<close> text "Named theorems to be used by proof methods later (see HoTT_Methods.thy). \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while -\<open>comp\<close> declares computation rules used when simplifying function application." +\<open>comp\<close> declares computation rules, which are used by the simplification method as equational rewrite rules." named_theorems wellform named_theorems comp @@ -9,6 +9,7 @@ theory Prod imports HoTT_Base begin + axiomatization Prod :: "[Term, Typefam] \<Rightarrow> Term" and lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and @@ -12,6 +12,7 @@ theory Proj Sum begin + consts fst :: "[Term, 'a] \<Rightarrow> Term" ("(1fst[/_,/ _])") snd :: "[Term, 'a] \<Rightarrow> Term" ("(1snd[/_,/ _])") @@ -49,13 +50,17 @@ text "Typing judgments and computation rules for the dependent and non-dependent lemma fst_dep_type: assumes "p : \<Sum>x:A. B x" shows "fst[A,B]`p : A" - by (derive lems: assms unfolds: fst_dep_def) + unfolding fst_dep_def + by (derive lems: assms) lemma fst_dep_comp: assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \<equiv> a" + unfolding fst_dep_def + by (simplify lems: assms) +\<comment> \<open> (* Old proof *) proof - have "fst[A,B]`(a,b) \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" by (derive lems: assms unfolds: fst_dep_def) @@ -65,8 +70,9 @@ proof - finally show "fst[A,B]`(a,b) \<equiv> a" . qed +\<close> - +\<comment> \<open> (* Old lemma *) text "In proving results about the second dependent projection function we often use the following lemma." lemma lem: @@ -77,12 +83,16 @@ proof - have "fst[A,B]`(x,y) \<equiv> x" using assms by (rule fst_dep_comp) then show "y : B (fst[A,B]`(x,y))" using assms by simp qed +\<close> lemma snd_dep_type: assumes "p : \<Sum>x:A. B x" shows "snd[A,B]`p : B (fst[A,B]`p)" + unfolding fst_dep_def snd_dep_def + by (simplify lems: assms) +\<comment> \<open> (* Old proof *) proof (derive lems: assms unfolds: snd_dep_def) show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def) @@ -90,12 +100,16 @@ proof (derive lems: assms unfolds: snd_dep_def) have "B: A \<rightarrow> U" by (wellformed jdgmt: assms) then show "y : B (fst[A, B]`(x,y))" using asm by (rule lem) qed (assumption | rule assms)+ +\<close> lemma snd_dep_comp: assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "snd[A,B]`(a,b) \<equiv> b" + unfolding snd_dep_def fst_dep_def + by (simplify lems: assms) +\<comment> \<open> (* Old proof *) proof - have "snd[A,B]`(a,b) \<equiv> indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b)" proof (derive lems: assms unfolds: snd_dep_def) @@ -115,6 +129,7 @@ proof - finally show "snd[A,B]`(a,b) \<equiv> b" . qed +\<close> text "For non-dependent projection functions:" @@ -122,13 +137,17 @@ text "For non-dependent projection functions:" lemma fst_nondep_type: assumes "p : A \<times> B" shows "fst[A,B]`p : A" - by (derive lems: assms unfolds: fst_nondep_def) + unfolding fst_nondep_def + by (derive lems: assms) lemma fst_nondep_comp: assumes "a : A" and "b : B" shows "fst[A,B]`(a,b) \<equiv> a" + unfolding fst_nondep_def + by (simplify lems: assms) +\<comment> \<open> (* Old proof *) proof - have "fst[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" by (derive lems: assms unfolds: fst_nondep_def) @@ -138,12 +157,16 @@ proof - finally show "fst[A,B]`(a,b) \<equiv> a" . qed +\<close> lemma snd_nondep_type: assumes "p : A \<times> B" shows "snd[A,B]`p : B" + unfolding snd_nondep_def + by (derive lems: assms) +\<comment> \<open> (* Old proof *) proof show "snd[A,B] : A \<times> B \<rightarrow> B" proof (derive unfolds: snd_nondep_def) @@ -151,11 +174,16 @@ proof show "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) q : B" by (derive lems: asm) qed (wellformed jdgmt: assms)+ qed (rule assms) +\<close> lemma snd_nondep_comp: assumes "a : A" and "b : B" shows "snd[A,B]`(a,b) \<equiv> b" + unfolding snd_nondep_def + by (simplify lems: assms) + +\<comment> \<open> (* Old proof *) proof - have "snd[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b)" by (derive lems: assms unfolds: snd_nondep_def) @@ -165,6 +193,7 @@ proof - finally show "snd[A,B]`(a,b) \<equiv> b" . qed +\<close> end
\ No newline at end of file @@ -9,6 +9,7 @@ theory Sum imports HoTT_Base begin + axiomatization Sum :: "[Term, Typefam] \<Rightarrow> Term" and pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and @@ -54,7 +55,7 @@ lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2 lemmas Sum_comps [comp] = Sum_comp -\<comment> \<open>Nondependent pair\<close> +text "Nondependent pair." abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_:A. B" |