From 962fc96123039b53b9c6946796e909fb50ec9004 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 13 Aug 2018 10:37:20 +0200
Subject: rcompose done

---
 scratch.thy | 49 ++++++++++++++++---------------------------------
 1 file changed, 16 insertions(+), 33 deletions(-)

(limited to 'scratch.thy')

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"
-- 
cgit v1.2.3