Pre-universe implementation commit

1 files changed, 51 insertions, 20 deletions

diff --git a/scratch.thy b/scratch.thy
index 1c921bd..3f66083 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,8 +3,11 @@ theory scratch
 
 begin
 
+term "UN"
+
 (* Typechecking *)
-schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A" by simple
+schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A"
+  by derive
 
 
 (* Simplification *)
@@ -17,45 +20,73 @@ assume asm:
   "c : A"
   "d : B"
 
-have "f`a`b`c \<equiv> d" by (simp add: asm | rule comp | derive lems: asm)+
+have "f`a`b`c \<equiv> d" by (simplify lems: asm)
 
 end
 
 lemma "a : A \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)"
-  by verify_simp
+  by simplify
 
 lemma "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
-  by verify_simp
+  by simplify
+
+schematic_goal "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> ?x"
+  by rsimplify
 
 lemma
   assumes "a : A" and "\<And>x. x : A \<Longrightarrow> b x : B x"
   shows "(\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
-  by (verify_simp lems: assms)
+  by (simplify lems: assms)
 
-lemma "\<lbrakk>a : A; b : B a; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
-oops
+lemma "\<lbrakk>a : A; b : B a; B: A \<rightarrow> U; \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y\<rbrakk>
+  \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
+  by (simplify)
 
 lemma
   assumes
     "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a \<equiv> \<^bold>\<lambda>y:B a. c a y"
     "(\<^bold>\<lambda>y:B a. c a y)`b \<equiv> c a b"
   shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
-apply (simp add: assms)
-done
-
-lemmas lems =
-  Prod_comp[where ?A = "B a" and ?b = "\<lambda>b. c a b" and ?a = b]
-  Prod_comp[where ?A = A and ?b = "\<lambda>x. \<^bold>\<lambda>y:B x. c x y" and ?a = a]
+by (simplify lems: assms)
 
 lemma
-  assumes
-    "a : A"
-    "b : B a"
-    "B: A \<rightarrow> U"
-    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y"
-  shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
-apply (verify_simp lems: assms)
+assumes
+  "a : A"
+  "b : B a"
+  "B: A \<rightarrow> U"
+  "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y"
+shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
+by (simplify lems: assms)
 
+lemma
+assumes
+  "a : A"
+  "b : B a"
+  "c : C a b"
+  "B: A \<rightarrow> U"
+  "\<And>x. x : A\<Longrightarrow> C x: B x \<rightarrow> U"
+  "\<And>x y z. \<lbrakk>x : A; y : B x; z : C x y\<rbrakk> \<Longrightarrow> d x y z : D x y z"
+shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. \<^bold>\<lambda>z:C x y. d x y z)`a`b`c \<equiv> d a b c"
+by (simplify lems: assms)
+
+
+(* HERE IS HOW WE ATTEMPT TO DO PATH INDUCTION --- VERY GOOD CANDIDATE FOR THESIS SECTION *)
+
+schematic_goal "\<lbrakk>A : U; x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =\<^sub>A y \<rightarrow> y =\<^sub>A x"
+  apply (rule Prod_intro)
+  apply (rule Equal_form)
+  apply assumption+
+  apply (rule Equal_elim)
+  back
+  back
+  back
+  back
+  back
+  back
+  back
+  back back back back back back
+
+thm comp
 
 
 end
\ No newline at end of file