tuned proofs;
authorwenzelm
Sat Jan 21 23:02:21 2006 +0100 (2006-01-21)
changeset 18730843da46f89ac
parent 18729 216e31270509
child 18731 3989c3c41983
tuned proofs;
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Quotient.thy
src/HOL/Unix/Unix.thy
     1.1 --- a/src/HOL/Library/Coinductive_List.thy	Sat Jan 21 23:02:20 2006 +0100
     1.2 +++ b/src/HOL/Library/Coinductive_List.thy	Sat Jan 21 23:02:21 2006 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4  
     1.5  lemma LList_mono: "A \<subseteq> B \<Longrightarrow> LList A \<subseteq> LList B"
     1.6      -- {* This justifies using @{text LList} in other recursive type definitions. *}
     1.7 -  by (unfold LList.defs) (blast intro!: gfp_mono)
     1.8 +  unfolding LList.defs by (blast intro!: gfp_mono)
     1.9  
    1.10  consts
    1.11    LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype_Universe.item \<times> 'a) option) \<Rightarrow>
    1.12 @@ -129,11 +129,11 @@
    1.13  qed
    1.14  
    1.15  lemma NIL_type: "NIL \<in> llist"
    1.16 -  by (unfold llist_def) (rule LList.NIL)
    1.17 +  unfolding llist_def by (rule LList.NIL)
    1.18  
    1.19  lemma CONS_type: "a \<in> range Datatype_Universe.Leaf \<Longrightarrow>
    1.20      M \<in> llist \<Longrightarrow> CONS a M \<in> llist"
    1.21 -  by (unfold llist_def) (rule LList.CONS)
    1.22 +  unfolding llist_def by (rule LList.CONS)
    1.23  
    1.24  lemma llistI: "x \<in> LList (range Datatype_Universe.Leaf) \<Longrightarrow> x \<in> llist"
    1.25    by (simp add: llist_def)
    1.26 @@ -448,7 +448,7 @@
    1.27    def h' \<equiv> "\<lambda>x. LList_corec x f"
    1.28    then have h': "\<And>x. h' x =
    1.29        (case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h' w))"
    1.30 -    by (unfold h'_def) (simp add: LList_corec)
    1.31 +    unfolding h'_def by (simp add: LList_corec)
    1.32    have "(h x, h' x) \<in> {(h u, h' u) | u. True}" by blast
    1.33    then show "h x = h' x"
    1.34    proof (coinduct rule: LList_equalityI [where A = UNIV])
     2.1 --- a/src/HOL/Library/List_Prefix.thy	Sat Jan 21 23:02:20 2006 +0100
     2.2 +++ b/src/HOL/Library/List_Prefix.thy	Sat Jan 21 23:02:21 2006 +0100
     2.3 @@ -21,13 +21,13 @@
     2.4    by intro_classes (auto simp add: prefix_def strict_prefix_def)
     2.5  
     2.6  lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
     2.7 -  by (unfold prefix_def) blast
     2.8 +  unfolding prefix_def by blast
     2.9  
    2.10  lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C"
    2.11 -  by (unfold prefix_def) blast
    2.12 +  unfolding prefix_def by blast
    2.13  
    2.14  lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
    2.15 -  by (unfold strict_prefix_def prefix_def) blast
    2.16 +  unfolding strict_prefix_def prefix_def by blast
    2.17  
    2.18  lemma strict_prefixE' [elim?]:
    2.19    assumes lt: "xs < ys"
    2.20 @@ -35,16 +35,16 @@
    2.21    shows C
    2.22  proof -
    2.23    from lt obtain us where "ys = xs @ us" and "xs \<noteq> ys"
    2.24 -    by (unfold strict_prefix_def prefix_def) blast
    2.25 +    unfolding strict_prefix_def prefix_def by blast
    2.26    with r show ?thesis by (auto simp add: neq_Nil_conv)
    2.27  qed
    2.28  
    2.29  lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)"
    2.30 -  by (unfold strict_prefix_def) blast
    2.31 +  unfolding strict_prefix_def by blast
    2.32  
    2.33  lemma strict_prefixE [elim?]:
    2.34      "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C"
    2.35 -  by (unfold strict_prefix_def) blast
    2.36 +  unfolding strict_prefix_def by blast
    2.37  
    2.38  
    2.39  subsection {* Basic properties of prefixes *}
    2.40 @@ -160,17 +160,17 @@
    2.41    "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
    2.42  
    2.43  lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
    2.44 -  by (unfold parallel_def) blast
    2.45 +  unfolding parallel_def by blast
    2.46  
    2.47  lemma parallelE [elim]:
    2.48      "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C"
    2.49 -  by (unfold parallel_def) blast
    2.50 +  unfolding parallel_def by blast
    2.51  
    2.52  theorem prefix_cases:
    2.53    "(xs \<le> ys ==> C) ==>
    2.54      (ys < xs ==> C) ==>
    2.55      (xs \<parallel> ys ==> C) ==> C"
    2.56 -  by (unfold parallel_def strict_prefix_def) blast
    2.57 +  unfolding parallel_def strict_prefix_def by blast
    2.58  
    2.59  theorem parallel_decomp:
    2.60    "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
     3.1 --- a/src/HOL/Library/Multiset.thy	Sat Jan 21 23:02:20 2006 +0100
     3.2 +++ b/src/HOL/Library/Multiset.thy	Sat Jan 21 23:02:21 2006 +0100
     3.3 @@ -291,43 +291,39 @@
     3.4    done
     3.5  
     3.6  lemma rep_multiset_induct_aux:
     3.7 -  assumes "P (\<lambda>a. (0::nat))"
     3.8 -    and "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
     3.9 +  assumes 1: "P (\<lambda>a. (0::nat))"
    3.10 +    and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
    3.11    shows "\<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
    3.12 -proof -
    3.13 -  note premises = prems [unfolded multiset_def]
    3.14 -  show ?thesis
    3.15 -    apply (unfold multiset_def)
    3.16 -    apply (induct_tac n, simp, clarify)
    3.17 -     apply (subgoal_tac "f = (\<lambda>a.0)")
    3.18 -      apply simp
    3.19 -      apply (rule premises)
    3.20 -     apply (rule ext, force, clarify)
    3.21 -    apply (frule setsum_SucD, clarify)
    3.22 -    apply (rename_tac a)
    3.23 -    apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
    3.24 -     prefer 2
    3.25 -     apply (rule finite_subset)
    3.26 -      prefer 2
    3.27 -      apply assumption
    3.28 -     apply simp
    3.29 -     apply blast
    3.30 -    apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
    3.31 -     prefer 2
    3.32 -     apply (rule ext)
    3.33 -     apply (simp (no_asm_simp))
    3.34 -     apply (erule ssubst, rule premises, blast)
    3.35 -    apply (erule allE, erule impE, erule_tac [2] mp, blast)
    3.36 -    apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
    3.37 -    apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
    3.38 -     prefer 2
    3.39 -     apply blast
    3.40 -    apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
    3.41 -     prefer 2
    3.42 -     apply blast
    3.43 -    apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
    3.44 -    done
    3.45 -qed
    3.46 +  apply (unfold multiset_def)
    3.47 +  apply (induct_tac n, simp, clarify)
    3.48 +   apply (subgoal_tac "f = (\<lambda>a.0)")
    3.49 +    apply simp
    3.50 +    apply (rule 1)
    3.51 +   apply (rule ext, force, clarify)
    3.52 +  apply (frule setsum_SucD, clarify)
    3.53 +  apply (rename_tac a)
    3.54 +  apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}")
    3.55 +   prefer 2
    3.56 +   apply (rule finite_subset)
    3.57 +    prefer 2
    3.58 +    apply assumption
    3.59 +   apply simp
    3.60 +   apply blast
    3.61 +  apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
    3.62 +   prefer 2
    3.63 +   apply (rule ext)
    3.64 +   apply (simp (no_asm_simp))
    3.65 +   apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
    3.66 +  apply (erule allE, erule impE, erule_tac [2] mp, blast)
    3.67 +  apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
    3.68 +  apply (subgoal_tac "{x. x \<noteq> a --> 0 < f x} = {x. 0 < f x}")
    3.69 +   prefer 2
    3.70 +   apply blast
    3.71 +  apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
    3.72 +   prefer 2
    3.73 +   apply blast
    3.74 +  apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
    3.75 +  done
    3.76  
    3.77  theorem rep_multiset_induct:
    3.78    "f \<in> multiset ==> P (\<lambda>a. 0) ==>
    3.79 @@ -456,19 +452,19 @@
    3.80          fix K
    3.81          assume N: "N = M0 + K"
    3.82          assume "\<forall>b. b :# K --> (b, a) \<in> r"
    3.83 -	then have "M0 + K \<in> ?W"
    3.84 +        then have "M0 + K \<in> ?W"
    3.85          proof (induct K)
    3.86 -	  case empty
    3.87 +          case empty
    3.88            from M0 show "M0 + {#} \<in> ?W" by simp
    3.89 -	next
    3.90 -	  case (add K x)
    3.91 -	  from add.prems have "(x, a) \<in> r" by simp
    3.92 +        next
    3.93 +          case (add K x)
    3.94 +          from add.prems have "(x, a) \<in> r" by simp
    3.95            with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
    3.96 -	  moreover from add have "M0 + K \<in> ?W" by simp
    3.97 +          moreover from add have "M0 + K \<in> ?W" by simp
    3.98            ultimately have "(M0 + K) + {#x#} \<in> ?W" ..
    3.99            then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc)
   3.100          qed
   3.101 -	then show "N \<in> ?W" by (simp only: N)
   3.102 +        then show "N \<in> ?W" by (simp only: N)
   3.103        qed
   3.104      qed
   3.105    } note tedious_reasoning = this
   3.106 @@ -602,9 +598,7 @@
   3.107    le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
   3.108  
   3.109  lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
   3.110 -  apply (unfold trans_def)
   3.111 -  apply (blast intro: order_less_trans)
   3.112 -  done
   3.113 +  unfolding trans_def by (blast intro: order_less_trans)
   3.114  
   3.115  text {*
   3.116   \medskip Irreflexivity.
   3.117 @@ -647,26 +641,22 @@
   3.118    by (insert mult_less_not_sym, blast)
   3.119  
   3.120  theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
   3.121 -by (unfold le_multiset_def, auto)
   3.122 +  unfolding le_multiset_def by auto
   3.123  
   3.124  text {* Anti-symmetry. *}
   3.125  
   3.126  theorem mult_le_antisym:
   3.127      "M <= N ==> N <= M ==> M = (N::'a::order multiset)"
   3.128 -  apply (unfold le_multiset_def)
   3.129 -  apply (blast dest: mult_less_not_sym)
   3.130 -  done
   3.131 +  unfolding le_multiset_def by (blast dest: mult_less_not_sym)
   3.132  
   3.133  text {* Transitivity. *}
   3.134  
   3.135  theorem mult_le_trans:
   3.136      "K <= M ==> M <= N ==> K <= (N::'a::order multiset)"
   3.137 -  apply (unfold le_multiset_def)
   3.138 -  apply (blast intro: mult_less_trans)
   3.139 -  done
   3.140 +  unfolding le_multiset_def by (blast intro: mult_less_trans)
   3.141  
   3.142  theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
   3.143 -by (unfold le_multiset_def, auto)
   3.144 +  unfolding le_multiset_def by auto
   3.145  
   3.146  text {* Partial order. *}
   3.147  
   3.148 @@ -709,9 +699,8 @@
   3.149  
   3.150  lemma union_le_mono:
   3.151      "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
   3.152 -  apply (unfold le_multiset_def)
   3.153 -  apply (blast intro: union_less_mono union_less_mono1 union_less_mono2)
   3.154 -  done
   3.155 +  unfolding le_multiset_def
   3.156 +  by (blast intro: union_less_mono union_less_mono1 union_less_mono2)
   3.157  
   3.158  lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)"
   3.159    apply (unfold le_multiset_def less_multiset_def)
   3.160 @@ -756,7 +745,7 @@
   3.161  lemma multiset_of_append [simp]:
   3.162      "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   3.163    by (induct xs fixing: ys) (auto simp: union_ac)
   3.164 -  
   3.165 +
   3.166  lemma surj_multiset_of: "surj multiset_of"
   3.167    apply (unfold surj_def, rule allI)
   3.168    apply (rule_tac M=y in multiset_induct, auto)
   3.169 @@ -816,10 +805,10 @@
   3.170    mset_le_def: "xs \<le># ys == (\<forall>a. count xs a \<le> count ys a)"
   3.171  
   3.172  lemma mset_le_refl[simp]: "xs \<le># xs"
   3.173 -  by (unfold mset_le_def) auto
   3.174 +  unfolding mset_le_def by auto
   3.175  
   3.176  lemma mset_le_trans: "\<lbrakk> xs \<le># ys; ys \<le># zs \<rbrakk> \<Longrightarrow> xs \<le># zs"
   3.177 -  by (unfold mset_le_def) (fast intro: order_trans)
   3.178 +  unfolding mset_le_def by (fast intro: order_trans)
   3.179  
   3.180  lemma mset_le_antisym: "\<lbrakk> xs\<le># ys; ys \<le># xs\<rbrakk> \<Longrightarrow> xs = ys"
   3.181    apply (unfold mset_le_def)
   3.182 @@ -834,10 +823,10 @@
   3.183    done
   3.184  
   3.185  lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \<le># ys + zs) = (xs \<le># ys)"
   3.186 -  by (unfold mset_le_def) auto
   3.187 +  unfolding mset_le_def by auto
   3.188  
   3.189  lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \<le># zs + ys) = (xs \<le># ys)"
   3.190 -  by (unfold mset_le_def) auto
   3.191 +  unfolding mset_le_def by auto
   3.192  
   3.193  lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws"
   3.194    apply (unfold mset_le_def)
   3.195 @@ -847,10 +836,10 @@
   3.196    done
   3.197  
   3.198  lemma mset_le_add_left[simp]: "xs \<le># xs + ys"
   3.199 -  by (unfold mset_le_def) auto
   3.200 +  unfolding mset_le_def by auto
   3.201  
   3.202  lemma mset_le_add_right[simp]: "ys \<le># xs + ys"
   3.203 -  by (unfold mset_le_def) auto
   3.204 +  unfolding mset_le_def by auto
   3.205  
   3.206  lemma multiset_of_remdups_le: "multiset_of (remdups x) \<le># multiset_of x"
   3.207    apply (induct x)
     4.1 --- a/src/HOL/Library/Quotient.thy	Sat Jan 21 23:02:20 2006 +0100
     4.2 +++ b/src/HOL/Library/Quotient.thy	Sat Jan 21 23:02:21 2006 +0100
     4.3 @@ -64,10 +64,10 @@
     4.4    by blast
     4.5  
     4.6  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
     4.7 -  by (unfold quot_def) blast
     4.8 +  unfolding quot_def by blast
     4.9  
    4.10  lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
    4.11 -  by (unfold quot_def) blast
    4.12 +  unfolding quot_def by blast
    4.13  
    4.14  text {*
    4.15   \medskip Abstracted equivalence classes are the canonical
    4.16 @@ -83,11 +83,11 @@
    4.17    fix R assume R: "A = Abs_quot R"
    4.18    assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
    4.19    with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
    4.20 -  thus ?thesis by (unfold class_def)
    4.21 +  thus ?thesis unfolding class_def .
    4.22  qed
    4.23  
    4.24  lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    4.25 -  by (insert quot_exhaust) blast
    4.26 +  using quot_exhaust by blast
    4.27  
    4.28  
    4.29  subsection {* Equality on quotients *}
     5.1 --- a/src/HOL/Unix/Unix.thy	Sat Jan 21 23:02:20 2006 +0100
     5.2 +++ b/src/HOL/Unix/Unix.thy	Sat Jan 21 23:02:21 2006 +0100
     5.3 @@ -653,11 +653,11 @@
     5.4    "can_exec root xs \<equiv> \<exists>root'. root =xs\<Rightarrow> root'"
     5.5  
     5.6  lemma can_exec_nil: "can_exec root []"
     5.7 -  by (unfold can_exec_def) (blast intro: transitions.intros)
     5.8 +  unfolding can_exec_def by (blast intro: transitions.intros)
     5.9  
    5.10  lemma can_exec_cons:
    5.11      "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> can_exec root' xs \<Longrightarrow> can_exec root (x # xs)"
    5.12 -  by (unfold can_exec_def) (blast intro: transitions.intros)
    5.13 +  unfolding can_exec_def by (blast intro: transitions.intros)
    5.14  
    5.15  text {*
    5.16    \medskip In case that we already know that a certain sequence can be
    5.17 @@ -677,7 +677,7 @@
    5.18        xs_y: "r =(xs @ [y])\<Rightarrow> root''"
    5.19      by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
    5.20    from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
    5.21 -    by (unfold can_exec_def) blast
    5.22 +    unfolding can_exec_def by blast
    5.23    from x xs have "root =(x # xs)\<Rightarrow> root'"
    5.24      by (rule transitions.cons)
    5.25    with y show ?case by blast
    5.26 @@ -913,7 +913,7 @@
    5.27    shows False
    5.28  proof -
    5.29    from inv obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
    5.30 -    by (unfold invariant_def) blast
    5.31 +    unfolding invariant_def by blast
    5.32    moreover
    5.33    from rmdir obtain att where
    5.34        "access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)"
    5.35 @@ -1076,7 +1076,7 @@
    5.36        from inv3 lookup' and not_writable user\<^isub>1_not_root
    5.37        have "access root' path user\<^isub>1 {Writable} = None"
    5.38          by (simp add: access_def)
    5.39 -      with inv1' inv2' inv3 show ?thesis by (unfold invariant_def) blast
    5.40 +      with inv1' inv2' inv3 show ?thesis unfolding invariant_def by blast
    5.41      qed
    5.42    qed
    5.43  qed