--- 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])
--- 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"
--- 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)
--- 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 *}
--- 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