author wenzelm Tue, 13 Mar 2012 14:44:16 +0100 changeset 46900 73555abfa267 parent 46899 58110c1e02bc child 46902 8d1b9acad287
tuned proofs;
 src/ZF/Induct/Binary_Trees.thy file | annotate | diff | comparison | revisions src/ZF/Induct/Brouwer.thy file | annotate | diff | comparison | revisions src/ZF/Induct/Comb.thy file | annotate | diff | comparison | revisions src/ZF/Induct/Term.thy file | annotate | diff | comparison | revisions
```--- a/src/ZF/Induct/Binary_Trees.thy	Tue Mar 13 14:17:42 2012 +0100
+++ b/src/ZF/Induct/Binary_Trees.thy	Tue Mar 13 14:44:16 2012 +0100
@@ -123,10 +123,10 @@
*}

lemma n_leaves_reflect: "t \<in> bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"

lemma n_leaves_nodes: "t \<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
+  by (induct set: bt) simp_all

text {*
```--- a/src/ZF/Induct/Brouwer.thy	Tue Mar 13 14:17:42 2012 +0100
+++ b/src/ZF/Induct/Brouwer.thy	Tue Mar 13 14:44:16 2012 +0100
@@ -71,7 +71,7 @@
-- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
-- {* for @{text Well} to prove this. *}
apply (rule Well_unfold [THEN trans])
-  apply (simp add: Sigma_bool Pi_empty1 succ_def)
+  apply (simp add: Sigma_bool succ_def)
done

end```
```--- a/src/ZF/Induct/Comb.thy	Tue Mar 13 14:17:42 2012 +0100
+++ b/src/ZF/Induct/Comb.thy	Tue Mar 13 14:44:16 2012 +0100
@@ -114,8 +114,6 @@

inductive_cases Ap_E [elim!]: "p\<bullet>q \<in> comb"

-declare comb.intros [intro!]
-

subsection {* Results about Contraction *}

@@ -189,13 +187,13 @@
text {* Counterexample to the diamond property for @{text "-1->"}. *}

lemma KIII_contract1: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> I"
-  by (blast intro: comb.intros contract.K comb_I)
+  by (blast intro: comb_I)

lemma KIII_contract2: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I))"
-  by (unfold I_def) (blast intro: comb.intros contract.intros)
+  by (unfold I_def) (blast intro: contract.intros)

lemma KIII_contract3: "K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I)) -1-> I"
-  by (blast intro: comb.intros contract.K comb_I)
+  by (blast intro: comb_I)

lemma not_diamond_contract: "\<not> diamond(contract)"
apply (unfold diamond_def)```
```--- a/src/ZF/Induct/Term.thy	Tue Mar 13 14:17:42 2012 +0100
+++ b/src/ZF/Induct/Term.thy	Tue Mar 13 14:44:16 2012 +0100
@@ -138,8 +138,7 @@
apply (subst term_rec)
apply (assumption | rule a)+
apply (erule list.induct)