diff options
| -rw-r--r-- | Coprod.thy | 50 | ||||
| -rw-r--r-- | Empty.thy | 27 | ||||
| -rw-r--r-- | Eq.thy | 27 | ||||
| -rw-r--r-- | Equal.thy | 219 | ||||
| -rw-r--r-- | HoTT.thy | 28 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 5 | ||||
| -rw-r--r-- | More_Types.thy | 83 | ||||
| -rw-r--r-- | Nat.thy | 45 | ||||
| -rw-r--r-- | Prod.thy | 34 | ||||
| -rw-r--r-- | Unit.thy | 32 |
10 files changed, 153 insertions, 397 deletions
diff --git a/Coprod.thy b/Coprod.thy deleted file mode 100644 index b0a1ad2..0000000 --- a/Coprod.thy +++ /dev/null @@ -1,50 +0,0 @@ -(* -Title: Coprod.thy -Author: Joshua Chen -Date: 2018 - -Coproduct type -*) - -theory Coprod -imports HoTT_Base - -begin - - -axiomatization - Coprod :: "[t, t] \<Rightarrow> t" (infixr "+" 50) and - inl :: "t \<Rightarrow> t" and - inr :: "t \<Rightarrow> t" and - indCoprod :: "[t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>+)") -where - Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and - - Coprod_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl a: A + B" and - - Coprod_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr b: A + B" and - - Coprod_elim: "\<lbrakk> - u: A + B; - 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) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u" and - - Coprod_comp_inl: "\<lbrakk> - a: A; - 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) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inl a) \<equiv> c a" and - - Coprod_comp_inr: "\<lbrakk> - b: B; - 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) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b" - -lemmas Coprod_form [form] -lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim -lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr - - -end diff --git a/Empty.thy b/Empty.thy deleted file mode 100644 index ee11045..0000000 --- a/Empty.thy +++ /dev/null @@ -1,27 +0,0 @@ -(* -Title: Empty.thy -Author: Joshua Chen -Date: 2018 - -Empty type -*) - -theory Empty -imports HoTT_Base - -begin - - -axiomatization - Empty :: t ("\<zero>") and - indEmpty :: "t \<Rightarrow> t" ("(1ind\<^sub>\<zero>)") -where - Empty_form: "\<zero>: U O" and - - Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a" - -lemmas Empty_form [form] -lemmas Empty_routine [intro] = Empty_form Empty_elim - - -end @@ -54,6 +54,9 @@ method path_ind for a b p :: t = method path_ind' for C :: "[t, t, t] \<Rightarrow> t" = (rule Eq_elim[where ?C=C]; (assumption | fact)?) +syntax "_induct_over" :: "[idt, idt, idt, t] \<Rightarrow> [t, t, t] \<Rightarrow> t" ("(2{_, _, _}/ _)" 0) +translations "{x, y, p} C" \<rightleftharpoons> "\<lambda>x y p. C" + section \<open>Properties of equality\<close> @@ -180,8 +183,12 @@ qed (routine add: assms) text \<open> We use the proof of associativity of path composition to demonstrate the process of deriving proof terms. -The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the form of the proof term in the first place. +The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the correct form of the proof term in the first place. However, using proof scripts the derivation becomes quite easy; we simply give the correct form of the statements to induct over, and prove the simple subgoals returned by the prover. + +The proof is sensitive to the order of the quantifiers in the product. +In particular, changing the order causes unification to fail in the path inductions. +It seems to be good practice to order the variables in the order over which we will path-induct. \<close> declare[[pretty_pathcomp=false]] @@ -193,22 +200,22 @@ schematic_goal pathcomp_assoc: pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w] pathcomp A x z w (pathcomp A x y z p q) r" apply (quantify 3) - apply (path_ind' - "\<lambda>x y p. \<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(r: z =[A] w). + apply (path_ind' "{x, y, p} + \<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(r: z =[A] w). Eq.pathcomp A x y w p (Eq.pathcomp A y z w q r) =[x =[A] w] Eq.pathcomp A x z w (Eq.pathcomp A x y z p q) r") apply (quantify 2) - apply (path_ind' - "\<lambda>xa z q. \<Prod>(w: A). \<Prod>(r: z =[A] w). + apply (path_ind' "{xa, z, q} + \<Prod>(w: A). \<Prod>(r: z =[A] w). Eq.pathcomp A xa xa w (refl xa) (Eq.pathcomp A xa z w q r) =[xa =[A] w] Eq.pathcomp A xa z w (Eq.pathcomp A xa xa z (refl xa) q) r") apply (quantify 2) - apply (path_ind' - "\<lambda>xb w r. Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w] + apply (path_ind' "{xb, w, r} + Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w] Eq.pathcomp A xb xb w (Eq.pathcomp A xb xb xb (refl xb) (refl xb)) r") - - text \<open>\<close> - + + text \<open>And now the rest is routine.\<close> + apply (derive; (rule assms|assumption)?) apply (compute, rule assms, assumption)+ apply (elim Eq_intro, rule Eq_intro, assumption) diff --git a/Equal.thy b/Equal.thy deleted file mode 100644 index 17c1c99..0000000 --- a/Equal.thy +++ /dev/null @@ -1,219 +0,0 @@ -(******** -Isabelle/HoTT: Equality -Feb 2019 - -********) - -theory Equal -imports Prod HoTT_Methods - -begin - - -section \<open>Type definitions\<close> - -axiomatization - Eq :: "[t, t, t] \<Rightarrow> t" and - refl :: "t \<Rightarrow> t" and - indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t" - -syntax - "_Eq" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100) -translations - "a =[A] b" \<rightleftharpoons> "(CONST Eq) A a b" - -axiomatization where - Eq_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =[A] b: U i" and - - Eq_intro: "a: A \<Longrightarrow> (refl a): a =[A] a" and - - Eq_elim: "\<lbrakk> - p: x =[A] y; - a: A; - b: A; - \<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 =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f a b p : C a b p" and - - Eq_comp: "\<lbrakk> - a: A; - \<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 =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f a a (refl a) \<equiv> f a" - -lemmas Eq_form [form] -lemmas Eq_routine [intro] = Eq_form Eq_intro Eq_elim -lemmas Eq_comp [comp] - - -section \<open>Path induction\<close> - -text \<open>We set up rudimentary automation of path induction:\<close> - -method path_ind for a b p :: t = - (rule Eq_elim[where ?a=a and ?b=b and ?p=p]; (fact | assumption)?) - - -section \<open>Properties of equality\<close> - -subsection \<open>Symmetry (path inverse)\<close> - -definition inv :: "[t, t, t, t] \<Rightarrow> t" -where "inv A x y p \<equiv> indEq (\<lambda>x y. ^(y =[A] x)) (\<lambda>x. refl x) x y p" - -syntax "_inv" :: "t \<Rightarrow> t" ("~_" [1000]) - -text \<open>Pretty-printing switch for path inverse:\<close> - -ML \<open>val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\<close> - -print_translation \<open> -let fun inv_tr' ctxt [A, x, y, p] = - if Config.get ctxt pretty_inv - then Syntax.const @{syntax_const "_inv"} $ p - else @{const inv} $ A $ x $ y $ p -in - [(@{const_syntax inv}, inv_tr')] -end -\<close> - -lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A x y p: y =[A] x" -unfolding inv_def by derive - -lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv A a a (refl a) \<equiv> refl a" -unfolding inv_def by derive - -declare - inv_type [intro] - inv_comp [comp] - -subsection \<open>Transitivity (path composition)\<close> - -schematic_goal transitivity: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?p: \<Prod>z: A. y =[A]z \<rightarrow> x =[A] z" -proof (path_ind x y p, quantify_all) - fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" . -qed (routine add: assms) - -definition pathcomp :: "[t, t, t, t, t, t] \<Rightarrow> t" -where - "pathcomp A x y z p q \<equiv> - (indEq (\<lambda>x y _. \<Prod>z: A. y =[A] z \<rightarrow> x =[A] z) (\<lambda>x. \<lambda>y: A. id (x =[A] y)) x y p)`z`q" - -syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "*" 110) - -text \<open>Pretty-printing switch for path composition:\<close> - -ML \<open>val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\<close> - -print_translation \<open> -let fun pathcomp_tr' ctxt [A, x, y, z, p, q] = - if Config.get ctxt pretty_pathcomp - then Syntax.const @{syntax_const "_pathcomp"} $ p $ q - else @{const pathcomp} $ A $ x $ y $ z $ p $ q -in - [(@{const_syntax pathcomp}, pathcomp_tr')] -end -\<close> - -lemma pathcomp_type: - assumes "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z" - shows "pathcomp A x y z p q: x =[A] z" -unfolding pathcomp_def by (routine add: transitivity assms) - -lemma pathcomp_cmp: - assumes "A: U i" and "a: A" - shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a" -unfolding pathcomp_def by (derive lems: assms) - -lemmas pathcomp_type [intro] -lemmas pathcomp_comp [comp] = pathcomp_cmp - - -section \<open>Higher groupoid structure of types\<close> - -schematic_goal pathcomp_idr: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A x y y p (refl y) =[x =[A] y] p" -proof (path_ind x y p) - show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal pathcomp_idl: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A x x y (refl x) p =[x =[A] y] p" -proof (path_ind x y p) - show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal pathcomp_invr: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)" -proof (path_ind x y p) - show - "\<And>x. x: A \<Longrightarrow> refl(refl x): - pathcomp A x x x (refl x) (inv A x x (refl x)) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal pathcomp_invl: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)" -proof (path_ind x y p) - show - "\<And>x. x: A \<Longrightarrow> refl(refl x): - pathcomp A x x x (inv A x x (refl x)) (refl x) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -schematic_goal inv_involutive: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: inv A y x (inv A x y p) =[x =[A] y] p" -proof (path_ind x y p) - show "\<And>x. x: A \<Longrightarrow> refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) - -declare[[pretty_pathcomp=false]] - -schematic_goal pathcomp_assoc: - assumes "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x =[A] y" - shows - "?a: \<Prod>q: y =[A] z. \<Prod>r: z =[A] w. - pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w] - pathcomp A x z w (pathcomp A x y z p q) r" -proof (path_ind x y p) - oops - schematic_goal l: - assumes "A: U i" "x: A" "z: A" "w: A" "q: x =[A] z" - shows - "?a: \<Prod>r: z =[A] w. pathcomp A x x w (refl x) (pathcomp A y z w q r) =[x =[A] w] - pathcomp A x z w (pathcomp A x x z (refl x) q) r" - proof (path_ind x z q) - oops - schematic_goal l': - assumes "A: U i" "x: A" "w: A" "r: x =[A] w" - shows - "?a: pathcomp A x x w (refl x) (pathcomp A x x w (refl x) r) =[x =[A] w] - pathcomp A x x w (pathcomp A x x x (refl x) (refl x)) r" - proof (path_ind x w r) - show "\<And>x. x: A \<Longrightarrow> refl(refl x): - pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)) =[x =[A] x] - pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x)" - by (derive lems: assms) - qed (routine add: assms) - -(* Possible todo: - implement a custom version of schematic_goal/theorem that exports the derived proof term. -*) - -definition l'_prftm :: "[t, t, t, t] \<Rightarrow> t" -where "l'_prftm A x w r\<equiv> - indEq - (\<lambda>a b c. pathcomp A a a b (refl a) (pathcomp A a a b (refl a) c) =[a =[A] b] - pathcomp A a a b (pathcomp A a a a (refl a) (refl a)) c) - (\<lambda>x. refl (refl x)) x w r" - - -end @@ -1,44 +1,40 @@ -(* -Title: HoTT.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT +Feb 2019 -Homotopy type theory -*) +An experimental implementation of homotopy type theory. + +********) theory HoTT imports + (* Basic theories *) HoTT_Base HoTT_Methods (* Types *) -Coprod -Empty -Equal +Eq Nat Prod Sum -Unit +More_Types (* Derived definitions and properties *) -Equality Projections Univalence begin - text \<open>Rule bundles:\<close> lemmas intros = - Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro + Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Eq_intro Cprd_intro_inl Cprd_intro_inr Unit_intro lemmas elims = - Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim + Nat_elim Prod_elim Sum_elim Eq_elim Cprd_elim Unit_elim Null_elim lemmas routines = - Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine - + Nat_routine Prod_routine Sum_routine Eq_routine Cprd_routine Unit_routine Null_routine end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 099a73e..c9744e9 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -51,7 +51,7 @@ method cumulativity declares form = ( section \<open>Deriving typing judgments\<close> -method routine uses add = (rule add | assumption | rule)+ +method routine uses add = (assumption | rule add | rule)+ text \<open> The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}. @@ -65,7 +65,8 @@ The method @{theory_text derive} combines @{method routine} and @{method compute It also handles universes using @{method hierarchy} and @{method cumulativity}. \<close> -method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ +method derive uses lems = + (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ section \<open>Additional method combinators\<close> diff --git a/More_Types.thy b/More_Types.thy new file mode 100644 index 0000000..9125aca --- /dev/null +++ b/More_Types.thy @@ -0,0 +1,83 @@ +(******** +Isabelle/HoTT: Coproduct, unit, and empty types +Feb 2019 + +********) + +theory More_Types +imports HoTT_Base + +begin + + +section \<open>Coproduct type\<close> + +axiomatization + Cprd :: "[t, t] \<Rightarrow> t" (infixr "+" 50) and + inl :: "[t, t, t] \<Rightarrow> t" and + inr :: "[t, t, t] \<Rightarrow> t" and + indCprd :: "[t \<Rightarrow> t, t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t" +where + Cprd_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and + + Cprd_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl A B a: A + B" and + + Cprd_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr A B b: A + B" and + + Cprd_elim: "\<lbrakk> + u: A + B; + C: A + B \<leadsto> U i; + \<And>x. x: A \<Longrightarrow> c x: C (inl A B x); + \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d u: C u" and + + Cprd_cmp_inl: "\<lbrakk> + a: A; + C: A + B \<leadsto> U i; + \<And>x. x: A \<Longrightarrow> c x: C (inl A B x); + \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inl A B a) \<equiv> c a" and + + Cprd_cmp_inr: "\<lbrakk> + b: B; + C: A + B \<leadsto> U i; + \<And>x. x: A \<Longrightarrow> c x: C (inl A B x); + \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inr A B b) \<equiv> d b" + +lemmas Cprd_form [form] +lemmas Cprd_routine [intro] = Cprd_form Cprd_intro_inl Cprd_intro_inr Cprd_elim +lemmas Cprd_comp [comp] = Cprd_cmp_inl Cprd_cmp_inr + + +section \<open>Unit type\<close> + +axiomatization + Unit :: t and + pt :: t and + indUnit :: "[t \<Rightarrow> t, t, t] \<Rightarrow> t" +where + Unit_form: "Unit: U O" and + + Unit_intro: "pt: Unit" and + + Unit_elim: "\<lbrakk>x: Unit; c: C pt; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c x: C x" and + + Unit_cmp: "\<lbrakk>c: C Unit; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c pt \<equiv> c" + +lemmas Unit_form [form] +lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim +lemmas Unit_cmp [comp] + + +section \<open>Empty type\<close> + +axiomatization + Null :: t and + indNull :: "[t \<Rightarrow> t, t] \<Rightarrow> t" +where + Null_form: "Null: U O" and + + Null_elim: "\<lbrakk>z: Null; C: Null \<leadsto> U i\<rbrakk> \<Longrightarrow> indNull C z: C z" + +lemmas Null_form [form] +lemmas Null_routine [intro] = Null_form Null_elim + +end @@ -1,49 +1,46 @@ -(* -Title: Nat.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT: Natural numbers +Feb 2019 -Natural numbers -*) +********) theory Nat imports HoTT_Base begin - axiomatization - Nat :: t ("\<nat>") and + Nat :: t and zero :: t ("0") and succ :: "t \<Rightarrow> t" and - indNat :: "[[t, t] \<Rightarrow> t, t, t] \<Rightarrow> t" ("(1ind\<^sub>\<nat>)") + indNat :: "[t \<Rightarrow> t, [t, t] \<Rightarrow> t, t, t] \<Rightarrow> t" where - Nat_form: "\<nat>: U O" and + Nat_form: "Nat: U O" and - Nat_intro_0: "0: \<nat>" and + Nat_intro_0: "0: Nat" and - Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" and + Nat_intro_succ: "n: Nat \<Longrightarrow> succ n: Nat" and Nat_elim: "\<lbrakk> a: C 0; - n: \<nat>; - C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n" and + n: Nat; + C: Nat \<leadsto> U i; + \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> indNat C f a n: C n" and - Nat_comp_0: "\<lbrakk> + Nat_cmp_0: "\<lbrakk> a: C 0; - C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a" and + C: Nat \<leadsto> U i; + \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> indNat C f a 0 \<equiv> a" and - Nat_comp_succ: "\<lbrakk> + Nat_cmp_succ: "\<lbrakk> a: C 0; - n: \<nat>; - C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)" + n: Nat; + C: Nat \<leadsto> U i; + \<And>n c. \<lbrakk>n: Nat; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) + \<rbrakk> \<Longrightarrow> indNat C f a (succ n) \<equiv> f n (indNat C f a n)" lemmas Nat_form [form] lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim -lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ - +lemmas Nat_comps [comp] = Nat_cmp_0 Nat_cmp_succ end @@ -70,23 +70,6 @@ lemmas Prod_comp [comp] = Prod_cmp Prod_uniq lemmas Prod_cong [cong] = Prod_form_eq Prod_intro_eq -section \<open>Universal quantification\<close> - -text \<open> -It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification. - -Method @{theory_text quantify_all} converts the goal -@{text "t: \<Prod>x1: A1. ... \<Prod>xn: An. B x1 ... xn"}, -where @{term B} is not a product, to -@{text "\<And>x1 ... xn . \<lbrakk>x1: A1; ...; xn: An\<rbrakk> \<Longrightarrow> ?b x1 ... xn: B x1 ... xn"}. - -Method @{theory_text "quantify k"} does the same, but only for the first k unknowns. -\<close> - -method quantify_all = (rule Prod_intro)+ -method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close> - - section \<open>Function composition\<close> definition compose :: "[t, t, t] \<Rightarrow> t" @@ -146,4 +129,21 @@ by (derive lems: assms cong) abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x" + +section \<open>Universal quantification\<close> + +text \<open> +It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification. + +Method @{theory_text quantify_all} converts the goal +@{text "t: \<Prod>x1: A1. ... \<Prod>xn: An. B x1 ... xn"}, +where @{term B} is not a product, to +@{text "\<And>x1 ... xn . \<lbrakk>x1: A1; ...; xn: An\<rbrakk> \<Longrightarrow> ?b x1 ... xn: B x1 ... xn"}. + +Method @{theory_text "quantify k"} does the same, but only for the first k unknowns. +\<close> + +method quantify_all = (rule Prod_intro)+ +method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close> + end diff --git a/Unit.thy b/Unit.thy deleted file mode 100644 index 7c221f0..0000000 --- a/Unit.thy +++ /dev/null @@ -1,32 +0,0 @@ -(* -Title: Unit.thy -Author: Joshua Chen -Date: 2018 - -Unit type -*) - -theory Unit -imports HoTT_Base - -begin - - -axiomatization - Unit :: t ("\<one>") and - pt :: t ("\<star>") and - indUnit :: "[t, t] \<Rightarrow> t" ("(1ind\<^sub>\<one>)") -where - Unit_form: "\<one>: U O" and - - Unit_intro: "\<star>: \<one>" and - - Unit_elim: "\<lbrakk>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and - - Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c" - -lemmas Unit_form [form] -lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim -lemmas Unit_comp [comp] - -end |