diff options
author | Josh Chen | 2018-08-16 16:11:42 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-16 16:11:42 +0200 |
commit | ca5874b8b0b60decd501bd05d0aa1913e5586d98 (patch) | |
tree | 8aad54e91d8174a4fe4d24443d5ad120612ec2e2 /Prod.thy | |
parent | ca8e7a2681c133abdd082cfa29d6994fa73f2d47 (diff) |
Prod.thy now has the correct definitional equality structure rule. Definition of function composition and properties.
Diffstat (limited to 'Prod.thy')
-rw-r--r-- | Prod.thy | 28 |
1 files changed, 11 insertions, 17 deletions
@@ -43,11 +43,15 @@ and and Prod_elim: "\<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)" and - Prod_comp: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)" + 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)" and Prod_uniq: "f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f" +and + Prod_eq: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b(x) \<equiv> b'(x); A: U(i)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b(x) \<equiv> \<^bold>\<lambda>x. b'(x)" text " + The Pure rules for \<open>\<equiv>\<close> only let us judge strict syntactic equality of object lambda expressions; Prod_eq is the actual definitional equality rule. + 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). " @@ -64,9 +68,9 @@ and 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 +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 +lemmas Prod_comps [comp] = Prod_comp Prod_uniq Prod_eq section \<open>Function composition\<close> @@ -77,23 +81,13 @@ syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 70) translations "g \<circ> f" \<rightleftharpoons> "g o f" axiomatization where - compose_type: "\<lbrakk> - g: \<Prod>x:B. C(x); + compose_def: "\<lbrakk> f: A \<rightarrow> B; - (\<Prod>x:B. C(x)): U(i); - A \<rightarrow> B: U(i) - \<rbrakk> \<Longrightarrow> g \<circ> f: \<Prod>x:A. C(f`x)" -and - compose_comp: "\<lbrakk> g: \<Prod>x:B. C(x); - f: A \<rightarrow> B; - (\<Prod>x:B. C(x)): U(i); - A \<rightarrow> B: U(i) + A \<rightarrow> B: U(i); + (\<Prod>x:B. C(x)): U(i) \<rbrakk> \<Longrightarrow> g \<circ> f \<equiv> \<^bold>\<lambda>x. g`(f`x)" -lemmas compose_rules [intro] = compose_type -lemmas compose_comps [comp] = compose_comp - section \<open>Unit type\<close> @@ -114,4 +108,4 @@ lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp lemmas Unit_comps [comp] = Unit_comp -end
\ No newline at end of file +end |