rcompose done

7 files changed, 105 insertions, 78 deletions

diff --git a/Equal.thy b/Equal.thy
index d910bb8..93f623f 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -15,7 +15,7 @@ section \<open>Constants and syntax\<close>
 axiomatization
   Equal :: "[Term, Term, Term] \<Rightarrow> Term" and
   refl :: "Term \<Rightarrow> Term" and
-  indEqual :: "[Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>=)")
+  indEqual :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>=)")
 
 syntax
   "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term"        ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100)
@@ -35,16 +35,16 @@ and
   Equal_elim: "\<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;
-    b: A;
+    x: A;
+    y: A;
     p: a =\<^sub>A b
-    \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(a)(b)(p) : C(a)(b)(p)"
+    \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(p) : C(x)(y)(p)"
 and
   Equal_comp: "\<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> ind\<^sub>=(f)(a)(a)(refl(a)) \<equiv> f(a)"
+    \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(refl(a)) \<equiv> f(a)"
 
 text "Admissible inference rules for equality type formation:"
 (*
@@ -56,7 +56,7 @@ and
   Equal_form_cond3: "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 [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3*)
+(*lemmas Equal_wellform [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3*)
 lemmas Equal_comps [comp] = Equal_comp
 
 
diff --git a/EqualProps.thy b/EqualProps.thy
index 9d23a99..d645fb6 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -15,20 +15,20 @@ begin
 
 section \<open>Symmetry / Path inverse\<close>
 
-definition inv :: "[Term, Term] \<Rightarrow> (Term \<Rightarrow> Term)"  ("(1inv[_,/ _])")
-  where "inv[x,y] \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) x y p"
+axiomatization inv :: "Term \<Rightarrow> Term"  ("_\<inverse>" [1000] 1000)
+  where inv_def: "inv \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) p"
 
 
 lemma inv_type:
-  assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "inv[x,y](p): y =\<^sub>A x"
+  assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x"
 unfolding inv_def
-proof
+proof (rule Equal_elim[where ?x=x and ?y=y])  \<comment> \<open>Path induction\<close>
   show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> y =\<^sub>A x: U(i)" using assms(1) ..
   show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
 qed (fact assms)+
 
 
-lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[a,a](refl(a)) \<equiv> refl(a)"
+lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)"
 unfolding inv_def
 proof
   show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
@@ -38,24 +38,66 @@ qed (fact assms)
 
 section \<open>Transitivity / Path composition\<close>
 
-text "``Raw'' composition function, of type \<open>\<Prod>x,y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close>."
+text "
+  Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>.
+"
+
+axiomatization rcompose :: Term where
+  rcompose_def: "rcompose \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p"
+
 
-definition rcompose :: "Term \<Rightarrow> Term"  ("(1rcompose[_])")
-  where "rcompose[A] \<equiv> \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:A. \<^bold>\<lambda>p:(x =\<^sub>A y). indEqual[A]
-    (\<lambda>x y _. \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)
-    (\<lambda>x. \<^bold>\<lambda>z:A. \<^bold>\<lambda>p:(x =\<^sub>A z). indEqual[A](\<lambda>x z _. x =\<^sub>A z) (\<lambda>x. refl(x)) x z p)
-    x y p"
+lemma rcompose_type:
+  assumes "A: U(i)"
+  shows "rcompose: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+unfolding rcompose_def
+proof
+  show "\<And>x. x: A \<Longrightarrow>
+    \<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+  proof
+    show "\<And>x y. \<lbrakk>x: A ; y: A\<rbrakk> \<Longrightarrow>
+       \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+    proof
+      { fix x y p assume asm: "x: A" "y: A" "p: x =\<^sub>A y"
+      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z"
+      proof (rule Equal_elim[where ?x=x and ?y=y])
+        show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)"
+        proof
+          show "\<And>x y z. \<lbrakk>x: A; y: A; z: A\<rbrakk> \<Longrightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)"
+            by (rule Prod_form Equal_form assms | assumption)+
+        qed (rule assms)
+
+        show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>z p. ind\<^sub>= refl p: \<Prod>z:A. x =\<^sub>A z \<rightarrow> x =\<^sub>A z"
+        proof
+          show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>p. ind\<^sub>= refl p: x =\<^sub>A z \<rightarrow> x =\<^sub>A z"
+          proof
+            { fix x z p assume asm: "x: A" "z: A" "p: x =\<^sub>A z"
+            show "ind\<^sub>= refl p: x =[A] z"
+            proof (rule Equal_elim[where ?x=x and ?y=z])
+              show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms)
+              show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
+            qed (fact asm)+ }
+            show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> x =\<^sub>A z: U(i)" by standard (rule assms)
+          qed
+        qed (rule assms)
+      qed (rule asm)+ }
+      show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms)
+    qed
+  qed (rule assms)
+qed (fact assms)
 
+corollary
+  assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
+  shows "rcompose`x`y`p`z`q: x =\<^sub>A z"
+  by standard+ (rule rcompose_type assms)+
 
-definition compose :: "[Term, Term, Term] \<Rightarrow> [Term, Term] \<Rightarrow> Term"  ("(1compose[ _,/ _,/ _])")
-  where "compose[x,y,z] \<equiv> \<lambda>p."
 
+axiomatization compose :: "[Term, Term] \<Rightarrow> Term"  (infixl "\<bullet>" 60) where
+  compose_comp: "\<lbrakk>
+    A: U(i);
+    x: A; y: A; z: A;
+    p: x =\<^sub>A y; q: y =\<^sub>A z
+  \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rcompose`x`y`p`z`q"
 
-lemma compose_type:
-  assumes "A : U(i)" and "x : A" and "y : A" and "z : A"
-  shows "compose[A,x,y,z] : x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
-  unfolding rcompose_def
-  by (derive lems: assms)
 
 lemma compose_comp:
   assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
diff --git a/Nat.thy b/Nat.thy
index bd2c4ca..eed9226 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -43,6 +43,7 @@ and
     \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)"
 
 lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2
+lemmas Nat_intro = Nat_intro1 Nat_intro2
 lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2
 
 
diff --git a/Prod.thy b/Prod.thy
index 5391943..76b66dd 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -14,23 +14,19 @@ section \<open>Constants and syntax\<close>
 
 axiomatization
   Prod :: "[Term, Typefam] \<Rightarrow> Term" and
-  lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
-  appl :: "[Term, Term] \<Rightarrow> Term"  ("(1_`_)" [61, 60] 60)
+  lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"  (binder "\<^bold>\<lambda>" 30) and
+  appl :: "[Term, Term] \<Rightarrow> Term"  (infixl "`" 60)
     \<comment> \<open>Application binds tighter than abstraction.\<close>
 
 syntax
   "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term"          ("(3\<Prod>_:_./ _)" 30)
-  "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(1\<^bold>\<lambda>_:_./ _)" 30)
   "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"    ("(3PROD _:_./ _)" 30)
-  "_LAMBDA_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3%%_:_./ _)" 30)
 
 text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>."
 
 translations
   "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
-  "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
   "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
-  "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
 
 text "Nondependent functions are a special case."
 
@@ -43,21 +39,20 @@ section \<open>Type rules\<close>
 axiomatization where
   Prod_form: "\<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x): U(i)"
 and
-  Prod_intro: "\<lbrakk>A: U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b(x): \<Prod>x:A. B(x)"
+  Prod_intro: "\<lbrakk>A: U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b(x): \<Prod>x:A. B(x)"
 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:A. b(x))`a \<equiv> b(a)"
+  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)"
 and
-  Prod_uniq: "f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+  Prod_uniq: "f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f"
 
 text "
   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).
 "
 
-(*
 text "
-  In addition to the usual type rules, it is a meta-theorem (*PROVE THIS!*) that whenever \<open>\<Prod>x:A. B x: U(i)\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A: U(i)\<close> and \<open>B: A \<longrightarrow> U(i)\<close>.
+  In addition to the usual type rules, it is a meta-theorem that whenever \<open>\<Prod>x:A. B x: U(i)\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A: U(i)\<close> and \<open>B: A \<longrightarrow> U(i)\<close>.
   
   That is to say, the following inference rules are admissible, and it simplifies proofs greatly to axiomatize them directly.
 "
@@ -66,12 +61,11 @@ axiomatization where
   Prod_form_cond1: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)"
 and
   Prod_form_cond2: "(\<Prod>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
-*)
 
 text "Set up the standard reasoner to use the type rules:"
 
-lemmas Prod_rules = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
-(*lemmas Prod_form_conds [intro (*elim, wellform*)] = Prod_form_cond1 Prod_form_cond2*)
+lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
+lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2
 lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 
 
diff --git a/Proj.thy b/Proj.thy
index b1c21c1..e90cd95 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -13,21 +13,23 @@ theory Proj
 begin
 
 
-abbreviation fst :: "Term \<Rightarrow> Term" where "fst \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. x)(p)"
-abbreviation snd :: "Term \<Rightarrow> Term" where "snd \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. y)(p)"
+axiomatization fst :: "Term \<Rightarrow> Term" where fst_def: "fst \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. x)(p)"
+axiomatization snd :: "Term \<Rightarrow> Term" where snd_def: "snd \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. y)(p)"
 
 text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
 
 
 lemma fst_type:
   assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A"
+unfolding fst_def
 proof
-  show "A: U(i)" using assms(1) by (rule Sum_forms)
+  show "A: U(i)" using assms(1) by (rule Sum_wellform)
 qed (fact assms | assumption)+
 
 
 lemma fst_comp:
   assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a"
+unfolding fst_def
 proof
   show "\<And>x. x: A \<Longrightarrow> x: A" .
 qed (rule assms)+
@@ -35,25 +37,27 @@ qed (rule assms)+
 
 lemma snd_type:
   assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)"
+unfolding snd_def
 proof
   show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)"
   proof -
     have "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> fst(p): A" using assms(1) by (rule fst_type)
-    with assms(1) show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (rule Sum_forms)
+    with assms(1) show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (rule Sum_wellform)
   qed
 
   fix x y
   assume asm: "x: A" "y: B(x)"
   show "y: B(fst <x,y>)"
   proof (subst fst_comp)
-    show "A: U(i)" using assms(1) by (rule Sum_forms)
-    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" using assms(1) by (rule Sum_forms)
+    show "A: U(i)" using assms(1) by (rule Sum_wellform)
+    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" using assms(1) by (rule Sum_wellform)
   qed (rule asm)+
 qed (fact assms)
 
 
 lemma snd_comp:
   assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "snd(<a,b>) \<equiv> b"
+unfolding snd_def
 proof
   show "\<And>x y. y: B(x) \<Longrightarrow> y: B(x)" .
   show "a: A" by (fact assms)
@@ -63,4 +67,7 @@ proof
 qed
 
 
+lemmas Proj_comps [intro] = fst_comp snd_comp
+
+
 end
\ No newline at end of file
diff --git a/Sum.thy b/Sum.thy
index eddb464..145c303 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -60,7 +60,7 @@ and
   Sum_form_cond2: "(\<Sum>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
 
 lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
-lemmas Sum_forms = Sum_form Sum_form_cond1 Sum_form_cond2
+lemmas Sum_wellform [wellform] = Sum_form_cond1 Sum_form_cond2
 lemmas Sum_comps [comp] = Sum_comp
 
 
diff --git a/scratch.thy b/scratch.thy
index 3141120..25d2ca7 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,66 +3,49 @@ theory scratch
 
 begin
 
-
-lemma "U(O): U(O)"
-proof (rule inhabited_implies_type)
-  show "\<nat>: U(O)" ..
-qed
-
 lemma
-  assumes "\<Sum>x:A. B(x): U(i)" "(a,b): \<Sum>x:A. B(x)"
+  assumes "\<Sum>x:A. B(x): U(i)" "<a,b>: \<Sum>x:A. B(x)"
   shows "a : A"
-proof (rule Sum_form_conds)
+proof
+oops
   
 
-abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. ind\<^sub>\<nat>(\<lambda>n c. n, 0, n)"
+abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<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_intro)
+prefer 2 apply (subst comp)
 apply (rule Nat_form)
 apply assumption
-apply (rule Nat_intro1)
+apply (rule Nat_intro)
 apply (rule Equal_intro)
-apply (rule Nat_intro1)
-prefer 2 apply (rule Nat_elim)
+apply (rule Nat_intro)
+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_intro)
+apply assumption
+prefer 2 apply (subst comp)
 apply (rule Nat_form)
 apply assumption
-apply (rule Nat_intro1)
+apply (rule Nat_intro)
+apply assumption
+apply (rule Equal_intro)
 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 (rule Nat_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"