diff options
| author | Josh Chen | 2018-08-13 10:37:20 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-13 10:37:20 +0200 |
| commit | 962fc96123039b53b9c6946796e909fb50ec9004 (patch) | |
| tree | 16f7d456fef26b6eb549200515a274e8ed3fc388 /scratch.thy | |
| parent | 7a89ec1e72f61179767c6488177c6d12e69388c5 (diff) | |
rcompose done
Diffstat (limited to 'scratch.thy')
| -rw-r--r-- | scratch.thy | 49 |
1 files changed, 16 insertions, 33 deletions
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" |