diff options
| -rw-r--r-- | Equal.thy | 154 | ||||
| -rw-r--r-- | HoTT.thy | 15 | ||||
| -rw-r--r-- | HoTT_Base.thy | 44 | ||||
| -rw-r--r-- | HoTT_Theorems.thy | 25 | ||||
| -rw-r--r-- | Prod.thy | 19 | ||||
| -rw-r--r-- | Sum.thy | 93 |
6 files changed, 215 insertions, 135 deletions
@@ -1,81 +1,85 @@ +(* Title: HoTT/Equal.thy + Author: Josh Chen + Date: Jun 2018 + +Equality type. +*) + theory Equal - imports HoTT_Base Prod + imports HoTT_Base begin -subsection \<open>Equality type\<close> - - axiomatization - Equal :: "[Term, Term, Term] \<Rightarrow> Term" - - syntax - "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 101] 100) - "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =[_]/ _)" [101, 0, 101] 100) - translations - "a =[A] b" \<rightleftharpoons> "CONST Equal A a b" - "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b" - - axiomatization - refl :: "Term \<Rightarrow> Term" ("(refl'(_'))") and - indEqual :: "[Term, [Term, Term, Term] \<Rightarrow> Term] \<Rightarrow> Term" ("(indEqual[_])") - where - Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U" - (* Should I write a permuted version \<open>\<lbrakk>A : U; b : A; a : A\<rbrakk> \<Longrightarrow> \<dots>\<close>? *) - and - Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x" - and - Equal_elim [elim]: - "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term) (b::Term) (p::Term). - \<lbrakk> \<And>x y::Term. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<rightarrow> U; - f : \<Prod>x:A. C(x)(x)(refl(x)); - a : A; - b : A; - p : a =\<^sub>A b \<rbrakk> - \<Longrightarrow> indEqual[A](C)`f`a`b`p : C(a)(b)(p)" - and - Equal_comp [simp]: - "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \<equiv> f`a" - - lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2] - - subsubsection \<open>Properties of equality\<close> - - text "Symmetry/Path inverse" - - definition inv :: "[Term, Term, Term] \<Rightarrow> Term" ("(1inv[_,/ _,/ _])") - where "inv[A,x,y] \<equiv> indEqual[A](\<lambda>x y _. y =\<^sub>A x)`(\<^bold>\<lambda>x:A. refl(x))`x`y" - - lemma inv_comp: "\<And>A a::Term. a : A \<Longrightarrow> inv[A,a,a]`refl(a) \<equiv> refl(a)" unfolding inv_def by simp - - text "Transitivity/Path composition" - - \<comment> \<open>"Raw" composition function\<close> - definition compose' :: "Term \<Rightarrow> Term" ("(1compose''[_])") - where "compose'[A] \<equiv> indEqual[A](\<lambda>x y _. \<Prod>z:A. \<Prod>q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\<lambda>x z _. x =\<^sub>A z)`(\<^bold>\<lambda>x:A. refl(x)))" - - \<comment> \<open>"Natural" composition function\<close> - abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compose[_,/ _,/ _,/ _])") - where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>q:y =\<^sub>A z. compose'[A]`x`y`p`z`q" - - (**** GOOD CANDIDATE FOR AUTOMATION ****) - lemma compose_comp: - assumes "a : A" - shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" using assms Equal_intro[OF assms] unfolding compose'_def by simp - - text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \<open>using\<close> clause in the proof. - This would likely involve something like: - 1. Recognizing that there is a function application that can be simplified. - 2. Noting that the obstruction to applying \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>. - 3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>." - - lemmas Equal_simps [simp] = inv_comp compose_comp - - subsubsection \<open>Pretty printing\<close> - - abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1_\<^sup>-\<^sup>1[_, _, _])" 500) - where "p\<^sup>-\<^sup>1[A,x,y] \<equiv> inv[A,x,y]`p" - - abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \<Rightarrow> Term" ("(1_ \<bullet>[_, _, _, _]/ _)") - where "p \<bullet>[A,x,y,z] q \<equiv> compose[A,x,y,z]`p`q" +axiomatization + Equal :: "[Term, Term, Term] \<Rightarrow> Term" and + refl :: "Term \<Rightarrow> Term" ("(refl'(_'))" 1000) and + indEqual :: "[Term, [Term, Term, Term] \<Rightarrow> Term] \<Rightarrow> Term" ("(indEqual[_])") + +syntax + "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 101] 100) + "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =[_]/ _)" [101, 0, 101] 100) +translations + "a =[A] b" \<rightleftharpoons> "CONST Equal A a b" + "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b" + +axiomatization where + Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U" + (* Should I write a permuted version \<open>\<lbrakk>A : U; b : A; a : A\<rbrakk> \<Longrightarrow> \<dots>\<close>? *) +and + Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x" +and + Equal_elim [elim]: + "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term) (b::Term) (p::Term). + \<lbrakk> \<And>x y::Term. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<rightarrow> U; + f : \<Prod>x:A. C(x)(x)(refl(x)); + a : A; + b : A; + p : a =\<^sub>A b \<rbrakk> + \<Longrightarrow> indEqual[A](C)`f`a`b`p : C(a)(b)(p)" +and + Equal_comp [simp]: + "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \<equiv> f`a" + +lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2] + +subsubsection \<open>Properties of equality\<close> + +text "Symmetry/Path inverse" + +definition inv :: "[Term, Term, Term] \<Rightarrow> Term" ("(1inv[_,/ _,/ _])") + where "inv[A,x,y] \<equiv> indEqual[A](\<lambda>x y _. y =\<^sub>A x)`(\<^bold>\<lambda>x:A. refl(x))`x`y" + +lemma inv_comp: "\<And>A a::Term. a : A \<Longrightarrow> inv[A,a,a]`refl(a) \<equiv> refl(a)" unfolding inv_def by simp + +text "Transitivity/Path composition" + +\<comment> \<open>"Raw" composition function\<close> +definition compose' :: "Term \<Rightarrow> Term" ("(1compose''[_])") + where "compose'[A] \<equiv> indEqual[A](\<lambda>x y _. \<Prod>z:A. \<Prod>q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\<lambda>x z _. x =\<^sub>A z)`(\<^bold>\<lambda>x:A. refl(x)))" + +\<comment> \<open>"Natural" composition function\<close> +abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compose[_,/ _,/ _,/ _])") + where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>q:y =\<^sub>A z. compose'[A]`x`y`p`z`q" + +(**** GOOD CANDIDATE FOR AUTOMATION ****) +lemma compose_comp: + assumes "a : A" + shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" using assms Equal_intro[OF assms] unfolding compose'_def by simp + +text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \<open>using\<close> clause in the proof. +This would likely involve something like: + 1. Recognizing that there is a function application that can be simplified. + 2. Noting that the obstruction to applying \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>. + 3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>." + +lemmas Equal_simps [simp] = inv_comp compose_comp + +subsubsection \<open>Pretty printing\<close> + +abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1_\<^sup>-\<^sup>1[_, _, _])" 500) + where "p\<^sup>-\<^sup>1[A,x,y] \<equiv> inv[A,x,y]`p" + +abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \<Rightarrow> Term" ("(1_ \<bullet>[_, _, _, _]/ _)") + where "p \<bullet>[A,x,y,z] q \<equiv> compose[A,x,y,z]`p`q" end
\ No newline at end of file diff --git a/HoTT.thy b/HoTT.thy new file mode 100644 index 0000000..405364e --- /dev/null +++ b/HoTT.thy @@ -0,0 +1,15 @@ +(* Title: HoTT/HoTT.thy + Author: Josh Chen + +Load all the component modules for the HoTT logic. +*) + +theory HoTT imports + HoTT_Base + Prod Sum + +begin + +\<comment> \<open>Maybe tactic setup can go in here?\<close> + +end
\ No newline at end of file diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9650c4c..9b422c4 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,5 +1,6 @@ (* Title: HoTT/HoTT_Base.thy Author: Josh Chen + Date: Jun 2018 Basic setup and definitions of a homotopy type theory object logic. *) @@ -9,23 +10,43 @@ theory HoTT_Base begin -section \<open>Basic definitions\<close> +section \<open>Setup\<close> -text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms. -We do not implement universes, but simply follow the informal notation in the HoTT book." +text "Set up type checking routines, proof methods etc." + + +section \<open>Metalogical definitions\<close> + +text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms. +Our implementation does not have universes, and we simply use \<open>a : U\<close> as a convenient shorthand meaning ``\<open>a\<close> is a type''." typedecl Term + section \<open>Judgments\<close> consts -is_a_type :: "Term \<Rightarrow> prop" ("(_ : U)" [0] 1000) -is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(3_ :/ _)" [0, 0] 1000) +is_a_type :: "Term \<Rightarrow> prop" ("(1_ :/ U)" [0] 1000) +is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) + + +section \<open>Type families\<close> + +text "A (one-variable) type family is a meta lambda term \<open>P :: Term \<Rightarrow> Term\<close> that further satisfies the following property." + +type_synonym Typefam = "Term \<Rightarrow> Term" + +abbreviation is_type_family :: "[Typefam, Term] \<Rightarrow> prop" ("(3_:/ _ \<rightarrow> U)") + where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P x : U)" + +text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML and is for the moment not really crucial." section \<open>Definitional equality\<close> -text "We use the Pure equality \<open>\<equiv>\<close> for definitional/judgmental equality of types and terms in our theory." +text "The Pure equality \<open>\<equiv>\<close> is used for definitional aka judgmental equality of types and terms." + +\<comment> \<open>Do these ever need to be used? theorem equal_types: assumes "A \<equiv> B" and "A : U" @@ -35,18 +56,11 @@ theorem equal_type_element: assumes "A \<equiv> B" and "x : A" shows "x : B" using assms by simp -lemmas type_equality [intro, simp] = +lemmas type_equality = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated] - - -section \<open>Type families\<close> - -text "A type family is a meta lambda term \<open>P :: Term \<Rightarrow> Term\<close> that further satisfies the following property." - -abbreviation is_type_family :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> prop" ("(3_:/ _ \<rightarrow> U)") - where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P(x) : U)" +\<close> end
\ No newline at end of file diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 95f1d0c..2c2a31d 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -1,5 +1,6 @@ theory HoTT_Theorems imports HoTT + begin text "A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified. @@ -9,8 +10,7 @@ Things that *should* be automated: \<bullet> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?" \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close> -declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=1]] - +declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]] section \<open>\<Prod> type\<close> @@ -22,17 +22,18 @@ lemma "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" .. proposition "A \<equiv> B \<Longrightarrow> \<^bold>\<lambda>x:A. x : B\<rightarrow>A" proof - - assume assm: "A \<equiv> B" - have id: "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" .. - from assm have "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp - with id show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" .. + assume "A \<equiv> B" + then have *: "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp + + have "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" .. + with * show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" by simp qed proposition "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A" proof fix a assume "a : A" - then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" .. + then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" .. qed @@ -42,7 +43,15 @@ proposition "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by text "Currying:" -lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)`a`b \<equiv> b" by simp +term "lambda A (\<lambda>x. \<^bold>\<lambda>y:B(x). y)" + +thm Prod_comp[where ?B = "\<lambda>x. \<Prod>y:B(x). B(x)"] + +lemma "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a \<equiv> \<^bold>\<lambda>y:B(a). y" +proof (rule Prod_comp[where ?B = "\<lambda>x. \<Prod>y:B(x). B(x)"]) + show "\<And>x. a : A \<Longrightarrow> x : A \<Longrightarrow> \<^bold>\<lambda>y:B x. y : B x \<rightarrow> B x" + +lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a`b \<equiv> b" by simp lemma "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). f x y)`a \<equiv> \<^bold>\<lambda>y:B(a). f a y" by simp @@ -1,5 +1,6 @@ (* Title: HoTT/Prod.thy Author: Josh Chen + Date: Jun 2018 Dependent product (function) type for the HoTT logic. *) @@ -10,8 +11,9 @@ theory Prod begin axiomatization - Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and + Prod :: "[Term, Typefam] \<Rightarrow> Term" and lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and + \<comment> \<open>Application binds tighter than abstraction.\<close> appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60) syntax @@ -29,15 +31,20 @@ translations \<comment> \<open>Type rules\<close> axiomatization where - Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U" + Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U" and - Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b(x) : B(x)) \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : \<Prod>x:A. B(x)" + Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b x : B x) \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x" and - Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> f`a : B(a)" + Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a" and - Prod_comp [simp]: "\<And>A b a. a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" + Prod_comp [simp]: "\<And>A B b a. \<lbrakk>\<And>x. x : A \<Longrightarrow> b x : B x; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" and - Prod_uniq [simp]: "\<And>A f. \<^bold>\<lambda>x:A. (f`x) \<equiv> f" + Prod_uniq [simp]: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f" + +\<comment> \<open>The funny thing about the first premises of the computation and uniqueness rules is that they introduce a variable B that doesn't actually explicitly appear in the statement of the conclusion. +In a sense, they say something like "if this condition holds for some type family B... (then we can apply the rule)". +This forces the theorem prover to search for a suitable B. Is this additional overhead necessary? +It *is* a safety check for well-formedness...\<close> text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)." @@ -1,5 +1,6 @@ (* Title: HoTT/Sum.thy Author: Josh Chen + Date: Jun 2018 Dependent sum type. *) @@ -10,9 +11,9 @@ theory Sum begin axiomatization - Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and + Sum :: "[Term, Typefam] \<Rightarrow> Term" and pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and - indSum :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" + indSum :: "[Term, Typefam, Typefam, [Term, Term] \<Rightarrow> Term] \<Rightarrow> Term" ("(1indSum[_,/ _])") syntax "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20) @@ -23,25 +24,29 @@ translations "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)" axiomatization where - Sum_form [intro]: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) : U" + Sum_form [intro]: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U" and - Sum_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> (a, b) : \<Sum>x:A. B(x)" + Sum_intro [intro]: "\<And>A B a b. \<lbrakk>B: A \<rightarrow> U; a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x" and - Sum_elim [elim]: "\<And>A B C f p. - \<lbrakk> C: \<Sum>x:A. B(x) \<rightarrow> U; - f : \<Prod>x:A. \<Prod>y:B(x). C((x,y)); - p : \<Sum>x:A. B(x) \<rbrakk> \<Longrightarrow> indSum(C)`f`p : C(p)" + Sum_elim [elim]: "\<And>A B C f p. \<lbrakk> + C: \<Sum>x:A. B x \<rightarrow> U; + \<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> (indSum[A,B] C f)`p : C p" and - Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \<equiv> f`a`b" - -text "We choose to formulate the elimination rule by using the object-level function type and function application as much as possible. -Hence only the type family \<open>C\<close> is left as a meta-level argument to the inductor indSum." + Sum_comp [simp]: "\<And>A B C f a b. \<lbrakk> + C: \<Sum>x:A. B x \<rightarrow> U; + \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y); + a : A; + b : B a + \<rbrakk> \<Longrightarrow> (indSum[A,B] C f)`(a,b) \<equiv> f a b" \<comment> \<open>Nondependent pair\<close> abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) - where "A\<times>B \<equiv> \<Sum>_:A. B" + where "A \<times> B \<equiv> \<Sum>_:A. B" + -subsubsection \<open>Projections\<close> +section \<open>Projections\<close> consts fst :: "[Term, 'a] \<Rightarrow> Term" ("(1fst[/_,/ _])") @@ -49,30 +54,56 @@ consts overloading fst_dep \<equiv> fst - snd_dep \<equiv> snd fst_nondep \<equiv> fst - snd_nondep \<equiv> snd begin - definition fst_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where - "fst_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)" - - definition snd_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where - "snd_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)" + definition fst_dep :: "[Term, Typefam] \<Rightarrow> Term" where + "fst_dep A B \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x)" definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where - "fst_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)" + "fst_nondep A B \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x)" +end + +overloading + snd_dep \<equiv> snd + snd_nondep \<equiv> snd +begin + definition snd_dep :: "[Term, Typefam] \<Rightarrow> Term" where + "snd_dep A B \<equiv> indSum[A,B] (\<lambda>p. B(fst[A,B]`p)) (\<lambda>x y. y)" definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where - "snd_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)" + "snd_nondep A B \<equiv> indSum[A, \<lambda>_. B] (\<lambda>p. B((fst A B)`p)) (\<lambda>x y. y)" end -text "Simplification rules for the projections:" - -lemma fst_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def by simp -lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by simp - -lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp -lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp +text "Simplification rules:" + +lemma fst_dep_comp: + assumes "a : A" and "b : B(a)" + shows "fst[A,B]`(a,b) \<equiv> a" +proof - + show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def using assms by simp +qed + +lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" +proof - + assume "a : A" and "b : B(a)" + then have "(a, b) : \<Sum>x:A. B(x)" .. + then show "snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by simp +qed + +lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" +proof - + assume "a : A" and "b : B" + then have "(a, b) : A \<times> B" .. + then show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp +qed + +lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" +proof - + assume "a : A" and "b : B" + then have "(a, b) : A \<times> B" .. + then show "snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp +qed + +lemmas proj_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp -lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp end
\ No newline at end of file |