# 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 \ B \ LList A \ 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 \ ('a \ ('b Datatype_Universe.item \ 'a) option) \ @@ -129,11 +129,11 @@ qed lemma NIL_type: "NIL \ llist" - by (unfold llist_def) (rule LList.NIL) + unfolding llist_def by (rule LList.NIL) lemma CONS_type: "a \ range Datatype_Universe.Leaf \ M \ llist \ CONS a M \ llist" - by (unfold llist_def) (rule LList.CONS) + unfolding llist_def by (rule LList.CONS) lemma llistI: "x \ LList (range Datatype_Universe.Leaf) \ x \ llist" by (simp add: llist_def) @@ -448,7 +448,7 @@ def h' \ "\x. LList_corec x f" then have h': "\x. h' x = (case f x of None \ NIL | Some (z, w) \ 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) \ {(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 \ ys" - by (unfold prefix_def) blast + unfolding prefix_def by blast lemma prefixE [elim?]: "xs \ 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 \ 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 \ ys ==> xs \ ys ==> xs < (ys::'a list)" - by (unfold strict_prefix_def) blast + unfolding strict_prefix_def by blast lemma strict_prefixE [elim?]: "xs < ys ==> (xs \ ys ==> xs \ (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 \ ys == \ xs \ ys \ \ ys \ xs" lemma parallelI [intro]: "\ xs \ ys ==> \ ys \ xs ==> xs \ ys" - by (unfold parallel_def) blast + unfolding parallel_def by blast lemma parallelE [elim]: "xs \ ys ==> (\ xs \ ys ==> \ ys \ xs ==> C) ==> C" - by (unfold parallel_def) blast + unfolding parallel_def by blast theorem prefix_cases: "(xs \ ys ==> C) ==> (ys < xs ==> C) ==> (xs \ ys ==> C) ==> C" - by (unfold parallel_def strict_prefix_def) blast + unfolding parallel_def strict_prefix_def by blast theorem parallel_decomp: "xs \ ys ==> \as b bs c cs. b \ c \ xs = as @ b # bs \ 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 (\a. (0::nat))" - and "!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1))" + assumes 1: "P (\a. (0::nat))" + and 2: "!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1))" shows "\f. f \ 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 = (\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 \ a --> 0 < f x} = {x. 0 < f x}") - prefer 2 - apply blast - apply (subgoal_tac "{x. x \ a \ 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 = (\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 \ a --> 0 < f x} = {x. 0 < f x}") + prefer 2 + apply blast + apply (subgoal_tac "{x. x \ a \ 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 \ multiset ==> P (\a. 0) ==> @@ -456,19 +452,19 @@ fix K assume N: "N = M0 + K" assume "\b. b :# K --> (b, a) \ r" - then have "M0 + K \ ?W" + then have "M0 + K \ ?W" proof (induct K) - case empty + case empty from M0 show "M0 + {#} \ ?W" by simp - next - case (add K x) - from add.prems have "(x, a) \ r" by simp + next + case (add K x) + from add.prems have "(x, a) \ r" by simp with wf_hyp have "\M \ ?W. M + {#x#} \ ?W" by blast - moreover from add have "M0 + K \ ?W" by simp + moreover from add have "M0 + K \ ?W" by simp ultimately have "(M0 + K) + {#x#} \ ?W" .. then show "M0 + (K + {#x#}) \ ?W" by (simp only: union_assoc) qed - then show "N \ ?W" by (simp only: N) + then show "N \ ?W" by (simp only: N) qed qed } note tedious_reasoning = this @@ -602,9 +598,7 @@ le_multiset_def: "M' <= M == M' = M \ 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 \ M \ (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 \# ys == (\a. count xs a \ count ys a)" lemma mset_le_refl[simp]: "xs \# xs" - by (unfold mset_le_def) auto + unfolding mset_le_def by auto lemma mset_le_trans: "\ xs \# ys; ys \# zs \ \ xs \# zs" - by (unfold mset_le_def) (fast intro: order_trans) + unfolding mset_le_def by (fast intro: order_trans) lemma mset_le_antisym: "\ xs\# ys; ys \# xs\ \ xs = ys" apply (unfold mset_le_def) @@ -834,10 +823,10 @@ done lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \# ys + zs) = (xs \# ys)" - by (unfold mset_le_def) auto + unfolding mset_le_def by auto lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \# zs + ys) = (xs \# ys)" - by (unfold mset_le_def) auto + unfolding mset_le_def by auto lemma mset_le_mono_add: "\ xs \# ys; vs \# ws \ \ xs + vs \# ys + ws" apply (unfold mset_le_def) @@ -847,10 +836,10 @@ done lemma mset_le_add_left[simp]: "xs \# xs + ys" - by (unfold mset_le_def) auto + unfolding mset_le_def by auto lemma mset_le_add_right[simp]: "ys \# xs + ys" - by (unfold mset_le_def) auto + unfolding mset_le_def by auto lemma multiset_of_remdups_le: "multiset_of (remdups x) \# 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 \ x} \ quot" - by (unfold quot_def) blast + unfolding quot_def by blast lemma quotE [elim]: "R \ quot ==> (!!a. R = {x. a \ 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 \ quot" hence "\a. R = {x. a \ x}" by blast with R have "\a. A = Abs_quot {x. a \ x}" by blast - thus ?thesis by (unfold class_def) + thus ?thesis unfolding class_def . qed lemma quot_cases [cases type: quot]: "(!!a. A = \a\ ==> 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 \ \root'. root =xs\ 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 \x\ root' \ can_exec root' xs \ 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])\ 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\ root'" and y: "root' \y\ r'" - by (unfold can_exec_def) blast + unfolding can_exec_def by blast from x xs have "root =(x # xs)\ 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