# HG changeset patch
# User wenzelm
# Date 1137880941 -3600
# Node ID 843da46f89aca5c996bd7a153613b1e02ffcf2b3
# Parent  216e3127050999a8c9952b8a013a84c5f943e612
tuned proofs;

diff -r 216e31270509 -r 843da46f89ac src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Sat Jan 21 23:02:20 2006 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Sat Jan 21 23:02:21 2006 +0100
@@ -51,7 +51,7 @@
 
 lemma LList_mono: "A \<subseteq> B \<Longrightarrow> LList A \<subseteq> LList B"
     -- {* This justifies using @{text LList} in other recursive type definitions. *}
-  by (unfold LList.defs) (blast intro!: gfp_mono)
+  unfolding LList.defs by (blast intro!: gfp_mono)
 
 consts
   LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype_Universe.item \<times> 'a) option) \<Rightarrow>
@@ -129,11 +129,11 @@
 qed
 
 lemma NIL_type: "NIL \<in> llist"
-  by (unfold llist_def) (rule LList.NIL)
+  unfolding llist_def by (rule LList.NIL)
 
 lemma CONS_type: "a \<in> range Datatype_Universe.Leaf \<Longrightarrow>
     M \<in> llist \<Longrightarrow> CONS a M \<in> llist"
-  by (unfold llist_def) (rule LList.CONS)
+  unfolding llist_def by (rule LList.CONS)
 
 lemma llistI: "x \<in> LList (range Datatype_Universe.Leaf) \<Longrightarrow> x \<in> llist"
   by (simp add: llist_def)
@@ -448,7 +448,7 @@
   def h' \<equiv> "\<lambda>x. LList_corec x f"
   then have h': "\<And>x. h' x =
       (case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h' w))"
-    by (unfold h'_def) (simp add: LList_corec)
+    unfolding h'_def by (simp add: LList_corec)
   have "(h x, h' x) \<in> {(h u, h' u) | u. True}" by blast
   then show "h x = h' x"
   proof (coinduct rule: LList_equalityI [where A = UNIV])
diff -r 216e31270509 -r 843da46f89ac src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Sat Jan 21 23:02:20 2006 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Sat Jan 21 23:02:21 2006 +0100
@@ -21,13 +21,13 @@
   by intro_classes (auto simp add: prefix_def strict_prefix_def)
 
 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
-  by (unfold prefix_def) blast
+  unfolding prefix_def by blast
 
 lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"
-  by (unfold prefix_def) blast
+  unfolding prefix_def by blast
 
 lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
-  by (unfold strict_prefix_def prefix_def) blast
+  unfolding strict_prefix_def prefix_def by blast
 
 lemma strict_prefixE' [elim?]:
   assumes lt: "xs < ys"
@@ -35,16 +35,16 @@
   shows C
 proof -
   from lt obtain us where "ys = xs @ us" and "xs \<noteq> ys"
-    by (unfold strict_prefix_def prefix_def) blast
+    unfolding strict_prefix_def prefix_def by blast
   with r show ?thesis by (auto simp add: neq_Nil_conv)
 qed
 
 lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
-  by (unfold strict_prefix_def) blast
+  unfolding strict_prefix_def by blast
 
 lemma strict_prefixE [elim?]:
     "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C"
-  by (unfold strict_prefix_def) blast
+  unfolding strict_prefix_def by blast
 
 
 subsection {* Basic properties of prefixes *}
@@ -160,17 +160,17 @@
   "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
 
 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
-  by (unfold parallel_def) blast
+  unfolding parallel_def by blast
 
 lemma parallelE [elim]:
     "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C"
-  by (unfold parallel_def) blast
+  unfolding parallel_def by blast
 
 theorem prefix_cases:
   "(xs \<le> ys ==> C) ==>
     (ys < xs ==> C) ==>
     (xs \<parallel> ys ==> C) ==> C"
-  by (unfold parallel_def strict_prefix_def) blast
+  unfolding parallel_def strict_prefix_def by blast
 
 theorem parallel_decomp:
   "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
diff -r 216e31270509 -r 843da46f89ac src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Jan 21 23:02:20 2006 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Jan 21 23:02:21 2006 +0100
@@ -291,43 +291,39 @@
   done
 
 lemma rep_multiset_induct_aux:
-  assumes "P (\<lambda>a. (0::nat))"
-    and "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
+  assumes 1: "P (\<lambda>a. (0::nat))"
+    and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
   shows "\<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
-proof -
-  note premises = prems [unfolded multiset_def]
-  show ?thesis
-    apply (unfold multiset_def)
-    apply (induct_tac n, simp, clarify)
-     apply (subgoal_tac "f = (\<lambda>a.0)")
-      apply simp
-      apply (rule premises)
-     apply (rule ext, force, clarify)
-    apply (frule setsum_SucD, clarify)
-    apply (rename_tac a)
-    apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
-     prefer 2
-     apply (rule finite_subset)
-      prefer 2
-      apply assumption
-     apply simp
-     apply blast
-    apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
-     prefer 2
-     apply (rule ext)
-     apply (simp (no_asm_simp))
-     apply (erule ssubst, rule premises, blast)
-    apply (erule allE, erule impE, erule_tac [2] mp, blast)
-    apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
-    apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
-     prefer 2
-     apply blast
-    apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
-     prefer 2
-     apply blast
-    apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
-    done
-qed
+  apply (unfold multiset_def)
+  apply (induct_tac n, simp, clarify)
+   apply (subgoal_tac "f = (\<lambda>a.0)")
+    apply simp
+    apply (rule 1)
+   apply (rule ext, force, clarify)
+  apply (frule setsum_SucD, clarify)
+  apply (rename_tac a)
+  apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
+   prefer 2
+   apply (rule finite_subset)
+    prefer 2
+    apply assumption
+   apply simp
+   apply blast
+  apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
+   prefer 2
+   apply (rule ext)
+   apply (simp (no_asm_simp))
+   apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
+  apply (erule allE, erule impE, erule_tac [2] mp, blast)
+  apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
+  apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
+   prefer 2
+   apply blast
+  apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
+   prefer 2
+   apply blast
+  apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
+  done
 
 theorem rep_multiset_induct:
   "f \<in> multiset ==> P (\<lambda>a. 0) ==>
@@ -456,19 +452,19 @@
         fix K
         assume N: "N = M0 + K"
         assume "\<forall>b. b :# K --> (b, a) \<in> r"
-	then have "M0 + K \<in> ?W"
+        then have "M0 + K \<in> ?W"
         proof (induct K)
-	  case empty
+          case empty
           from M0 show "M0 + {#} \<in> ?W" by simp
-	next
-	  case (add K x)
-	  from add.prems have "(x, a) \<in> r" by simp
+        next
+          case (add K x)
+          from add.prems have "(x, a) \<in> r" by simp
           with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
-	  moreover from add have "M0 + K \<in> ?W" by simp
+          moreover from add have "M0 + K \<in> ?W" by simp
           ultimately have "(M0 + K) + {#x#} \<in> ?W" ..
           then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc)
         qed
-	then show "N \<in> ?W" by (simp only: N)
+        then show "N \<in> ?W" by (simp only: N)
       qed
     qed
   } note tedious_reasoning = this
@@ -602,9 +598,7 @@
   le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
 
 lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
-  apply (unfold trans_def)
-  apply (blast intro: order_less_trans)
-  done
+  unfolding trans_def by (blast intro: order_less_trans)
 
 text {*
  \medskip Irreflexivity.
@@ -647,26 +641,22 @@
   by (insert mult_less_not_sym, blast)
 
 theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
-by (unfold le_multiset_def, auto)
+  unfolding le_multiset_def by auto
 
 text {* Anti-symmetry. *}
 
 theorem mult_le_antisym:
     "M <= N ==> N <= M ==> M = (N::'a::order multiset)"
-  apply (unfold le_multiset_def)
-  apply (blast dest: mult_less_not_sym)
-  done
+  unfolding le_multiset_def by (blast dest: mult_less_not_sym)
 
 text {* Transitivity. *}
 
 theorem mult_le_trans:
     "K <= M ==> M <= N ==> K <= (N::'a::order multiset)"
-  apply (unfold le_multiset_def)
-  apply (blast intro: mult_less_trans)
-  done
+  unfolding le_multiset_def by (blast intro: mult_less_trans)
 
 theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
-by (unfold le_multiset_def, auto)
+  unfolding le_multiset_def by auto
 
 text {* Partial order. *}
 
@@ -709,9 +699,8 @@
 
 lemma union_le_mono:
     "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
-  apply (unfold le_multiset_def)
-  apply (blast intro: union_less_mono union_less_mono1 union_less_mono2)
-  done
+  unfolding le_multiset_def
+  by (blast intro: union_less_mono union_less_mono1 union_less_mono2)
 
 lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)"
   apply (unfold le_multiset_def less_multiset_def)
@@ -756,7 +745,7 @@
 lemma multiset_of_append [simp]:
     "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   by (induct xs fixing: ys) (auto simp: union_ac)
-  
+
 lemma surj_multiset_of: "surj multiset_of"
   apply (unfold surj_def, rule allI)
   apply (rule_tac M=y in multiset_induct, auto)
@@ -816,10 +805,10 @@
   mset_le_def: "xs \<le># ys == (\<forall>a. count xs a \<le> count ys a)"
 
 lemma mset_le_refl[simp]: "xs \<le># xs"
-  by (unfold mset_le_def) auto
+  unfolding mset_le_def by auto
 
 lemma mset_le_trans: "\<lbrakk> xs \<le># ys; ys \<le># zs \<rbrakk> \<Longrightarrow> xs \<le># zs"
-  by (unfold mset_le_def) (fast intro: order_trans)
+  unfolding mset_le_def by (fast intro: order_trans)
 
 lemma mset_le_antisym: "\<lbrakk> xs\<le># ys; ys \<le># xs\<rbrakk> \<Longrightarrow> xs = ys"
   apply (unfold mset_le_def)
@@ -834,10 +823,10 @@
   done
 
 lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \<le># ys + zs) = (xs \<le># ys)"
-  by (unfold mset_le_def) auto
+  unfolding mset_le_def by auto
 
 lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \<le># zs + ys) = (xs \<le># ys)"
-  by (unfold mset_le_def) auto
+  unfolding mset_le_def by auto
 
 lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws"
   apply (unfold mset_le_def)
@@ -847,10 +836,10 @@
   done
 
 lemma mset_le_add_left[simp]: "xs \<le># xs + ys"
-  by (unfold mset_le_def) auto
+  unfolding mset_le_def by auto
 
 lemma mset_le_add_right[simp]: "ys \<le># xs + ys"
-  by (unfold mset_le_def) auto
+  unfolding mset_le_def by auto
 
 lemma multiset_of_remdups_le: "multiset_of (remdups x) \<le># multiset_of x"
   apply (induct x)
diff -r 216e31270509 -r 843da46f89ac src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Sat Jan 21 23:02:20 2006 +0100
+++ b/src/HOL/Library/Quotient.thy	Sat Jan 21 23:02:21 2006 +0100
@@ -64,10 +64,10 @@
   by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
-  by (unfold quot_def) blast
+  unfolding quot_def by blast
 
 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
-  by (unfold quot_def) blast
+  unfolding quot_def by blast
 
 text {*
  \medskip Abstracted equivalence classes are the canonical
@@ -83,11 +83,11 @@
   fix R assume R: "A = Abs_quot R"
   assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
-  thus ?thesis by (unfold class_def)
+  thus ?thesis unfolding class_def .
 qed
 
 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
-  by (insert quot_exhaust) blast
+  using quot_exhaust by blast
 
 
 subsection {* Equality on quotients *}
diff -r 216e31270509 -r 843da46f89ac src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Sat Jan 21 23:02:20 2006 +0100
+++ b/src/HOL/Unix/Unix.thy	Sat Jan 21 23:02:21 2006 +0100
@@ -653,11 +653,11 @@
   "can_exec root xs \<equiv> \<exists>root'. root =xs\<Rightarrow> root'"
 
 lemma can_exec_nil: "can_exec root []"
-  by (unfold can_exec_def) (blast intro: transitions.intros)
+  unfolding can_exec_def by (blast intro: transitions.intros)
 
 lemma can_exec_cons:
     "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> can_exec root' xs \<Longrightarrow> can_exec root (x # xs)"
-  by (unfold can_exec_def) (blast intro: transitions.intros)
+  unfolding can_exec_def by (blast intro: transitions.intros)
 
 text {*
   \medskip In case that we already know that a certain sequence can be
@@ -677,7 +677,7 @@
       xs_y: "r =(xs @ [y])\<Rightarrow> root''"
     by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
   from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
-    by (unfold can_exec_def) blast
+    unfolding can_exec_def by blast
   from x xs have "root =(x # xs)\<Rightarrow> root'"
     by (rule transitions.cons)
   with y show ?case by blast
@@ -913,7 +913,7 @@
   shows False
 proof -
   from inv obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
-    by (unfold invariant_def) blast
+    unfolding invariant_def by blast
   moreover
   from rmdir obtain att where
       "access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)"
@@ -1076,7 +1076,7 @@
       from inv3 lookup' and not_writable user\<^isub>1_not_root
       have "access root' path user\<^isub>1 {Writable} = None"
         by (simp add: access_def)
-      with inv1' inv2' inv3 show ?thesis by (unfold invariant_def) blast
+      with inv1' inv2' inv3 show ?thesis unfolding invariant_def by blast
     qed
   qed
 qed