diff options
| -rw-r--r-- | Prod.thy | 24 | ||||
| -rw-r--r-- | Projections.thy | 46 | ||||
| -rw-r--r-- | Sum.thy | 51 |
3 files changed, 60 insertions, 61 deletions
@@ -18,13 +18,13 @@ axiomatization \<comment> \<open>Application should bind tighter than abstraction.\<close> syntax - "_Prod" :: "[idt, t, t] \<Rightarrow> t" ("(3TT '(_: _')./ _)" 30) - "_Prod'" :: "[idt, t, t] \<Rightarrow> t" ("(3TT _: _./ _)" 30) + "_Prod" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>'(_: _')./ _)" 30) + "_Prod'" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_: _./ _)" 30) "_lam" :: "[idt, t, t] \<Rightarrow> t" ("(3\<lambda>'(_: _')./ _)" 30) "_lam'" :: "[idt, t, t] \<Rightarrow> t" ("(3\<lambda>_: _./ _)" 30) translations - "TT(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)" - "TT x: A. B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)" + "\<Prod>(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)" + "\<Prod>x: A. B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)" "\<lambda>(x: A). b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)" "\<lambda>x: A. b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)" @@ -35,25 +35,25 @@ The syntax translations above bind the variable @{term x} in the expressions @{t text \<open>Non-dependent functions are a special case:\<close> abbreviation Fun :: "[t, t] \<Rightarrow> t" (infixr "\<rightarrow>" 40) -where "A \<rightarrow> B \<equiv> TT(_: A). B" +where "A \<rightarrow> B \<equiv> \<Prod>(_: A). B" axiomatization where \<comment> \<open>Type rules\<close> - Prod_form: "\<lbrakk>A: U i; B: A \<leadsto> U i\<rbrakk> \<Longrightarrow> TT x: A. B x: U i" and + Prod_form: "\<lbrakk>A: U i; B: A \<leadsto> 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> \<lambda>x: A. b x: TT x: A. B x" and + Prod_intro: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: \<Prod>x: A. B x" and - Prod_elim: "\<lbrakk>f: TT x: A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and + Prod_elim: "\<lbrakk>f: \<Prod>x: A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and Prod_cmp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; a: A\<rbrakk> \<Longrightarrow> (\<lambda>x: A. b x)`a \<equiv> b a" and - Prod_uniq: "f: TT x: A. B x \<Longrightarrow> \<lambda>x: A. f`x \<equiv> f" and + Prod_uniq: "f: \<Prod>x: A. B x \<Longrightarrow> \<lambda>x: A. f`x \<equiv> f" and \<comment> \<open>Congruence rules\<close> Prod_form_eq: "\<lbrakk>A: U i; B: A \<leadsto> U i; C: A \<leadsto> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk> - \<Longrightarrow> TT x: A. B x \<equiv> TT x: A. C x" and + \<Longrightarrow> \<Prod>x: A. B x \<equiv> \<Prod>x: A. C x" and Prod_intro_eq: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x \<equiv> \<lambda>x: A. c x" @@ -107,14 +107,14 @@ print_translation \<open> let fun compose_tr' ctxt [A, g, f] = if Config.get ctxt pretty_compose then Syntax.const @{syntax_const "_compose"} $ g $ f - else Const ("compose", Syntax.read_typ ctxt "t \<Rightarrow> t \<Rightarrow> t") $ A $ g $ f + else @{const compose} $ A $ g $ f in [(@{const_syntax compose}, compose_tr')] end \<close> lemma compose_assoc: - assumes "A: U i" and "f: A \<rightarrow> B" and "g: B \<rightarrow> C" and "h: TT x: C. D x" + assumes "A: U i" and "f: A \<rightarrow> B" and "g: B \<rightarrow> C" and "h: \<Prod>x: C. D x" shows "compose A (compose B h g) f \<equiv> compose A h (compose A g f)" by (derive lems: assms cong) diff --git a/Projections.thy b/Projections.thy index 509402b..c819240 100644 --- a/Projections.thy +++ b/Projections.thy @@ -1,43 +1,45 @@ -(* -Title: Projections.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT: Projections +Feb 2019 -Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent sum type. -*) +Projection functions for the dependent sum type. + +********) theory Projections imports HoTT_Methods Prod Sum begin - -definition fst :: "t \<Rightarrow> t" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p" -definition snd :: "t \<Rightarrow> t" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p" +definition fst :: "[t, t] \<Rightarrow> t" where "fst A p \<equiv> indSum (\<lambda>_. A) (\<lambda>x y. x) p" lemma fst_type: - assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "fst p: A" + assumes "A: U i" and "p: \<Sum>x: A. B x" shows "fst A p: A" unfolding fst_def by (derive lems: assms) -lemma fst_comp: - assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "fst <a,b> \<equiv> a" +declare fst_type [intro] + +lemma fst_cmp: + assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "fst A <a, b> \<equiv> a" unfolding fst_def by compute (derive lems: assms) -lemma snd_type: - assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)" -unfolding snd_def proof (derive lems: assms) - show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> fst p: A" using assms(1-2) by (rule fst_type) +declare fst_cmp [comp] - fix x y assume asm: "x: A" "y: B x" - show "y: B (fst <x,y>)" by (derive lems: asm assms fst_comp) +definition snd :: "[t, t \<Rightarrow> t, t] \<Rightarrow> t" where "snd A B p \<equiv> indSum (\<lambda>p. B (fst A p)) (\<lambda>x y. y) p" + +lemma snd_type: + assumes "A: U i" and "B: A \<leadsto> U i" and "p: \<Sum>x: A. B x" shows "snd A B p: B (fst A p)" +unfolding snd_def proof (routine add: assms) + fix x y assume "x: A" and "y: B x" + with assms have [comp]: "fst A <x, y> \<equiv> x" by derive + note \<open>y: B x\<close> then show "y: B (fst A <x, y>)" by compute qed -lemma snd_comp: - assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "snd <a,b> \<equiv> b" +lemma snd_cmp: + assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "snd A B <a,b> \<equiv> b" unfolding snd_def by (derive lems: assms) lemmas Proj_types [intro] = fst_type snd_type -lemmas Proj_comps [comp] = fst_comp snd_comp - +lemmas Proj_comps [comp] = fst_cmp snd_cmp end @@ -1,59 +1,56 @@ -(* -Title: Sum.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT: Dependent sum (dependent pair) +Feb 2019 -Dependent sum type -*) +********) theory Sum imports HoTT_Base begin - axiomatization - Sum :: "[t, tf] \<Rightarrow> t" and + Sum :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and pair :: "[t, t] \<Rightarrow> t" ("(1<_,/ _>)") and - indSum :: "[[t, t] \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>\<Sum>)") + indSum :: "[t \<Rightarrow> t, [t, t] \<Rightarrow> t, t] \<Rightarrow> t" syntax - "_sum" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>_:_./ _)" 20) - "_sum_ascii" :: "[idt, t, t] \<Rightarrow> t" ("(3SUM _:_./ _)" 20) - + "_Sum" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>'(_: _')./ _)" 20) + "_Sum'" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>_: _./ _)" 20) translations - "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" - "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)" + "\<Sum>(x: A). B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" + "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" abbreviation Pair :: "[t, t] \<Rightarrow> t" (infixr "\<times>" 50) - where "A \<times> B \<equiv> \<Sum>_:A. B" + where "A \<times> B \<equiv> \<Sum>_: A. B" axiomatization where \<comment> \<open>Type rules\<close> - Sum_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x: U i" and + Sum_form: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> B x: 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" and + Sum_intro: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a, b>: \<Sum>x: A. B x" and Sum_elim: "\<lbrakk> - p: \<Sum>x:A. B x; - 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> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f p: C p" and + p: \<Sum>x: A. B x; + C: \<Sum>x: A. B x \<leadsto> U i; + \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> indSum C f p: C p" and - Sum_comp: "\<lbrakk> + Sum_cmp: "\<lbrakk> a: A; b: B a; - B: A \<longrightarrow> U i; - 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> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f <a,b> \<equiv> f a b" and + B: A \<leadsto> U i; + C: \<Sum>x: A. B x \<leadsto> U i; + \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> indSum C f <a, b> \<equiv> f a b" and \<comment> \<open>Congruence rules\<close> - Sum_form_eq: "\<lbrakk>A: U i; B: A \<longrightarrow> U i; C: A \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x \<equiv> \<Sum>x:A. C x" + Sum_form_eq: "\<lbrakk>A: U i; B: A \<leadsto> U i; C: A \<leadsto> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk> + \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. C x" lemmas Sum_form [form] lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim -lemmas Sum_comp [comp] - +lemmas Sum_comp [comp] = Sum_cmp +lemmas Sum_cong [cong] = Sum_form_eq end |