Partway through changing function application syntax style.

1 files changed, 94 insertions, 98 deletions

diff --git a/scratch.thy b/scratch.thy
index ae1bdb5..b88a8fc 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,108 +3,104 @@ theory scratch
 
 begin
 
-(* Typechecking *)
-schematic_goal "\<lbrakk>A : U(i); B : U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A"
-  by derive
-
-lemma "\<zero> : U(S S S 0)"
-  by derive
-
-
-(* Simplification *)
-
-notepad begin
-
-assume asm:
-  "f`a \<equiv> g"
-  "g`b \<equiv> \<^bold>\<lambda>x:A. d"
-  "c : A"
-  "d : B"
-
-have "f`a`b`c \<equiv> d" by (simplify lems: asm)
-
-end
-
-lemma "\<lbrakk>A : U(i); a : A\<rbrakk> \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)"
-  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 simplify
-
-schematic_goal "\<lbrakk>a : A; b: A \<longrightarrow> 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 (simplify lems: assms)
-
-lemma "\<lbrakk>a : A; b : B a; B: A \<longrightarrow> U(i); \<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"
-by (simplify lems: assms)
-
-lemma
-assumes
-  "a : A"
-  "b : B a"
-  "\<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"
-  "\<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)
-
-(* Polymorphic identity function *)
+abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. (ind\<^sub>\<nat> (\<lambda>n. \<nat>) (\<lambda>n c. n) 0 n)"
+
+schematic_goal "?a : (pred`0) =\<^sub>\<nat> 0"
+apply (subst comp)
+apply (rule Nat_form)
+prefer 4 apply (subst comp)
+apply (rule Nat_form)
+apply assumption
+apply (rule Nat_intro1)
+apply (rule Equal_intro)
+apply (rule Nat_intro1)
+prefer 2 apply (rule Nat_elim)
+apply (rule Nat_form)
+apply assumption
+apply (rule Nat_intro1)
+apply assumption
+apply (rule Nat_form)
+done
+
+schematic_goal "?a : \<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n"
+apply (rule Prod_intro)
+apply (rule Nat_form)
+apply (subst comp)
+apply (rule Nat_form)
+prefer 2 apply (rule Nat_elim)
+apply (rule Nat_form)
+apply assumption
+apply (rule Nat_intro1)
+apply assumption
+apply (rule Nat_form)
+apply (rule Nat_intro2, assumption)
+apply (rule Equal_form)
+apply (rule Nat_form)
+apply (rule Nat_elim)
+apply (rule Nat_form)
+apply assumption
+apply (rule Nat_rules)+
+apply assumption+
+apply (subst comp)
+apply (rule Nat_form)
+prefer 2 apply (rule Nat_elim)
+defer
+apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+
+apply (subst Nat_comps)
+apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+
+apply (rule Equal_intro)
+apply assumption
+apply (rule Nat_form)
+done
+
+schematic_goal "?a : \<Sum>p:\<nat>\<rightarrow>\<nat>. \<Prod>n:\<nat>. (p`(succ n)) =\<^sub>\<nat> n"
+apply (rule Sum_intro)
+apply (rule Prod_form)
+apply (rule Nat_form)+
+apply (rule Prod_form)
+apply (rule Nat_form)
+apply (rule Equal_form)
+apply (rule Nat_form)
+apply (rule Prod_elim)
+apply assumption
+apply (elim Nat_intro2)
+apply assumption
+prefer 2 apply (rule Prod_intro)
+apply (rule Nat_form)
+prefer 3 apply (rule Prod_intro)
+apply (rule Nat_form)+
+prefer 3 apply (rule Nat_elim)
+back
+oops
 
-definition Id :: "Numeral \<Rightarrow> Term" where "Id n \<equiv> \<^bold>\<lambda>A:U(n). \<^bold>\<lambda>x:A. x"
 
-lemma assumes "A : U 0" and "x:A" shows "(Id 0)`A`x \<equiv> x" unfolding Id_def by (simplify lems: assms)
+(* Now try to derive pred directly *)
+schematic_goal "?a : \<Sum>pred:?A . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
+(* At some point need to perform induction *)
+apply (rule Sum_intro)
+defer
+apply (rule Sum_form)
+apply (rule Equal_form)
+apply (rule Nat_form)
+apply (rule Prod_elim)
+defer
+apply (rule Nat_intro1)+
+prefer 5 apply assumption
+prefer 4 apply (rule Prod_form)
+apply (rule Nat_form)+
+apply (rule Prod_form)
+apply (rule Nat_form)
+apply (rule Equal_form)
+apply (rule Nat_form)
+apply (rule Prod_elim)
+apply assumption
+apply (rule Nat_intro2)
+apply assumption+
+(* Now begins the hard part *)
+prefer 2 apply (rule Sum_rules)
+prefer 2 apply (rule Prod_rules)
 
 
-(* See if we can find path inverse *)
-schematic_goal "\<lbrakk>A : U(i); x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =\<^sub>A y \<rightarrow> y =\<^sub>A x"
-  apply (rule Prod_intro)
-  apply (rule Equal_elim)
-  back
-  back
-  back
-  back
-  back
-  back
-  back
-  defer
-  back
-  back
-  back
-  back
-  back
-  back
-  back
-  back
-  back
-  apply (rule Equal_form)
-  apply assumption+
-  defer
-  defer
-  apply assumption
-  defer
-  defer
-  apply (rule Equal_intro)
-  apply assumption+
-oops
 
 
 end
\ No newline at end of file