Reorganize theories

1 files changed, 16 insertions, 13 deletions

diff --git a/Equal.thy b/Equal.thy
index 8c5cf29..2b49213 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -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