diff options
Diffstat (limited to 'Equal.thy')
-rw-r--r-- | Equal.thy | 29 |
1 files changed, 16 insertions, 13 deletions
@@ -10,13 +10,12 @@ theory Equal begin +section \<open>Constants and syntax\<close> + axiomatization Equal :: "[Term, Term, Term] \<Rightarrow> Term" and refl :: "Term \<Rightarrow> Term" ("(refl'(_'))" 1000) and - indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(1indEqual[_])") - - -section \<open>Syntax\<close> + indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>=[_])") syntax "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) @@ -31,12 +30,6 @@ section \<open>Type rules\<close> axiomatization where Equal_form: "\<And>i A a b. \<lbrakk>A : U(i); a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U(i)" and - Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> A : U(i)" -and - Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> a : A" -and - Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> b : A" -and Equal_intro: "\<And>A a. a : A \<Longrightarrow> refl(a) : a =\<^sub>A a" and Equal_elim: "\<And>i A C f a b p. \<lbrakk> @@ -45,17 +38,27 @@ and a : A; b : A; p : a =\<^sub>A b - \<rbrakk> \<Longrightarrow> indEqual[A] C f a b p : C a b p" + \<rbrakk> \<Longrightarrow> ind\<^sub>=[A] C f a b p : C a b p" and Equal_comp: "\<And>i A C f a. \<lbrakk> \<And>x y. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U(i); \<And>x. x : A \<Longrightarrow> f x : C x x refl(x); a : A - \<rbrakk> \<Longrightarrow> indEqual[A] C f a a refl(a) \<equiv> f a" + \<rbrakk> \<Longrightarrow> ind\<^sub>=[A] C f a a refl(a) \<equiv> f a" + +text "Admissible inference rules for equality type formation:" + +axiomatization where + Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> A : U(i)" +and + Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> a : A" +and + Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> b : A" lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -lemmas Equal_form_conds [elim, wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 +lemmas Equal_form_conds [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 lemmas Equal_comps [comp] = Equal_comp + end
\ No newline at end of file |