# HG changeset patch # User nipkow # Date 997098204 -7200 # Node ID ddea204de5bc54d1a98516b0c0b762749c08ceb5 # Parent 96b5b27da55ca1038f6dfe48f18318914aabd2af turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'. diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Datatype_Universe.ML --- a/src/HOL/Datatype_Universe.ML Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Datatype_Universe.ML Mon Aug 06 13:43:24 2001 +0200 @@ -80,7 +80,8 @@ (** Scons vs Atom **) -Goalw [Atom_def,Scons_def,Push_Node_def] "Scons M N ~= Atom(a)"; +Goalw [Atom_def,Scons_def,Push_Node_def,One_def] + "Scons M N ~= Atom(a)"; by (rtac notI 1); by (etac (equalityD2 RS subsetD RS UnE) 1); by (rtac singletonI 1); @@ -140,11 +141,11 @@ (** Injectiveness of Scons **) -Goalw [Scons_def] "Scons M N <= Scons M' N' ==> M<=M'"; +Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> M<=M'"; by (blast_tac (claset() addSDs [Push_Node_inject]) 1); qed "Scons_inject_lemma1"; -Goalw [Scons_def] "Scons M N <= Scons M' N' ==> N<=N'"; +Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> N<=N'"; by (blast_tac (claset() addSDs [Push_Node_inject]) 1); qed "Scons_inject_lemma2"; @@ -251,7 +252,7 @@ by (rtac ntrunc_Atom 1); qed "ntrunc_Numb"; -Goalw [Scons_def,ntrunc_def] +Goalw [Scons_def,ntrunc_def,One_def] "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"; by (safe_tac (claset() addSIs [imageI])); by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3)); @@ -265,7 +266,7 @@ (** Injection nodes **) -Goalw [In0_def] "ntrunc 1 (In0 M) = {}"; +Goalw [In0_def] "ntrunc 1' (In0 M) = {}"; by (Simp_tac 1); by (rewtac Scons_def); by (Blast_tac 1); @@ -276,7 +277,7 @@ by (Simp_tac 1); qed "ntrunc_In0"; -Goalw [In1_def] "ntrunc 1 (In1 M) = {}"; +Goalw [In1_def] "ntrunc 1' (In1 M) = {}"; by (Simp_tac 1); by (rewtac Scons_def); by (Blast_tac 1); @@ -338,7 +339,7 @@ (** Injection **) -Goalw [In0_def,In1_def] "In0(M) ~= In1(N)"; +Goalw [In0_def,In1_def,One_def] "In0(M) ~= In1(N)"; by (rtac notI 1); by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1); qed "In0_not_In1"; diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Divides.ML --- a/src/HOL/Divides.ML Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Divides.ML Mon Aug 06 13:43:24 2001 +0200 @@ -65,7 +65,7 @@ by (asm_simp_tac (simpset() addsimps [mod_geq]) 1); qed "mod_if"; -Goal "m mod 1 = (0::nat)"; +Goal "m mod 1' = 0"; by (induct_tac "m" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq]))); qed "mod_1"; @@ -387,7 +387,7 @@ (*** Further facts about div and mod ***) -Goal "m div 1 = m"; +Goal "m div 1' = m"; by (induct_tac "m" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq]))); qed "div_1"; @@ -527,12 +527,12 @@ qed "dvd_0_left_iff"; AddIffs [dvd_0_left_iff]; -Goalw [dvd_def] "1 dvd (k::nat)"; +Goalw [dvd_def] "1' dvd k"; by (Simp_tac 1); qed "dvd_1_left"; AddIffs [dvd_1_left]; -Goal "(m dvd 1) = (m = 1)"; +Goal "(m dvd 1') = (m = 1')"; by (simp_tac (simpset() addsimps [dvd_def]) 1); qed "dvd_1_iff_1"; Addsimps [dvd_1_iff_1]; diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Hoare/Examples.ML --- a/src/HOL/Hoare/Examples.ML Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Hoare/Examples.ML Mon Aug 06 13:43:24 2001 +0200 @@ -175,7 +175,7 @@ Ambiguity warnings of parser are due to := being used both for assignment and list update. *) -Goal "m - 1 < n ==> m < Suc n"; +Goal "m - 1' < n ==> m < Suc n"; by (arith_tac 1); qed "lemma"; @@ -184,7 +184,7 @@ \ geq == %A i. !k. i pivot <= A!k |] ==> \ \ |- VARS A u l.\ \ {0 < length(A::('a::order)list)} \ -\ l := 0; u := length A - 1; \ +\ l := 0; u := length A - 1'; \ \ WHILE l <= u \ \ INV {leq A l & geq A u & u (0,s'); (c0,s') -[eval]-> s1 |] ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" - IfFalse "[| (e,s) -|[eval]-> (1,s'); (c1,s') -[eval]-> s1 |] + IfFalse "[| (e,s) -|[eval]-> (1',s'); (c1,s') -[eval]-> s1 |] ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" - WhileFalse "(e,s) -|[eval]-> (1,s1) ==> (WHILE e DO c, s) -[eval]-> s1" + WhileFalse "(e,s) -|[eval]-> (1',s1) ==> (WHILE e DO c, s) -[eval]-> s1" WhileTrue "[| (e,s) -|[eval]-> (0,s1); (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |] diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Induct/Mutil.thy --- a/src/HOL/Induct/Mutil.thy Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Induct/Mutil.thy Mon Aug 06 13:43:24 2001 +0200 @@ -110,7 +110,7 @@ Diff_Int_distrib [simp] lemma tiling_domino_0_1: - "t \ tiling domino ==> card (coloured 0 \ t) = card (coloured 1 \ t)" + "t \ tiling domino ==> card (coloured 0 \ t) = card (coloured 1' \ t)" apply (erule tiling.induct) apply (drule_tac [2] domino_singletons) apply auto @@ -131,7 +131,7 @@ apply (rule notI) apply (subgoal_tac "card (coloured 0 \ (t - {(i, j)} - {(m, n)})) < - card (coloured 1 \ (t - {(i, j)} - {(m, n)}))") + card (coloured 1' \ (t - {(i, j)} - {(m, n)}))") apply (force simp only: tiling_domino_0_1) apply (simp add: tiling_domino_0_1 [symmetric]) apply (simp add: coloured_def card_Diff2_less) diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Integ/IntDef.ML --- a/src/HOL/Integ/IntDef.ML Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Integ/IntDef.ML Mon Aug 06 13:43:24 2001 +0200 @@ -326,7 +326,7 @@ by (asm_simp_tac (simpset() addsimps [zmult]) 1); qed "zmult_int0"; -Goalw [int_def] "int 1 * z = z"; +Goalw [int_def] "int 1' * z = z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zmult]) 1); qed "zmult_int1"; @@ -335,7 +335,7 @@ by (rtac ([zmult_commute, zmult_int0] MRS trans) 1); qed "zmult_int0_right"; -Goal "z * int 1 = z"; +Goal "z * int 1' = z"; by (rtac ([zmult_commute, zmult_int1] MRS trans) 1); qed "zmult_int1_right"; diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Integ/NatBin.thy --- a/src/HOL/Integ/NatBin.thy Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Integ/NatBin.thy Mon Aug 06 13:43:24 2001 +0200 @@ -18,6 +18,10 @@ "number_of v == nat (number_of v)" (*::bin=>nat ::bin=>int*) +axioms +neg_number_of_bin_pred_iff_0: + "neg (number_of (bin_pred v)) = (number_of v = (0::nat))" + use "nat_bin.ML" setup nat_bin_arith_setup end diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Integ/NatSimprocs.ML --- a/src/HOL/Integ/NatSimprocs.ML Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Integ/NatSimprocs.ML Mon Aug 06 13:43:24 2001 +0200 @@ -14,13 +14,15 @@ (*Now just instantiating n to (number_of v) does the right simplification, but with some redundant inequality tests.*) - +(* Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"; by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1); by (Asm_simp_tac 1); by (stac less_number_of_Suc 1); by (Simp_tac 1); qed "neg_number_of_bin_pred_iff_0"; +*) +val neg_number_of_bin_pred_iff_0 = thm "neg_number_of_bin_pred_iff_0"; Goal "neg (number_of (bin_minus v)) ==> \ \ Suc m - (number_of v) = m - (number_of (bin_pred v))"; diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Integ/nat_bin.ML --- a/src/HOL/Integ/nat_bin.ML Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Integ/nat_bin.ML Mon Aug 06 13:43:24 2001 +0200 @@ -495,7 +495,7 @@ by Auto_tac; val lemma1 = result(); -Goal "m+m ~= int 1 + n + n"; +Goal "m+m ~= int 1' + n + n"; by Auto_tac; by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1); by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Isar_examples/Fibonacci.thy --- a/src/HOL/Isar_examples/Fibonacci.thy Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Isar_examples/Fibonacci.thy Mon Aug 06 13:43:24 2001 +0200 @@ -29,7 +29,7 @@ consts fib :: "nat => nat" recdef fib less_than "fib 0 = 0" - "fib 1 = 1" + "fib 1' = 1" "fib (Suc (Suc x)) = fib x + fib (Suc x)" lemma [simp]: "0 < fib (Suc n)" diff -r 96b5b27da55c -r ddea204de5bc src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Library/Multiset.thy Mon Aug 06 13:43:24 2001 +0200 @@ -16,7 +16,7 @@ typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}" proof - show "(\\x. 0::nat) \\ ?multiset" by simp + show "(\x. 0::nat) \ ?multiset" by simp qed lemmas multiset_typedef [simp] = @@ -25,23 +25,23 @@ constdefs Mempty :: "'a multiset" ("{#}") - "{#} == Abs_multiset (\\a. 0)" + "{#} == Abs_multiset (\a. 0)" single :: "'a => 'a multiset" ("{#_#}") - "{#a#} == Abs_multiset (\\b. if b = a then 1 else 0)" + "{#a#} == Abs_multiset (\b. if b = a then 1' else 0)" count :: "'a multiset => 'a => nat" "count == Rep_multiset" MCollect :: "'a multiset => ('a => bool) => 'a multiset" - "MCollect M P == Abs_multiset (\\x. if P x then Rep_multiset M x else 0)" + "MCollect M P == Abs_multiset (\x. if P x then Rep_multiset M x else 0)" syntax "_Melem" :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})") translations "a :# M" == "0 < count M a" - "{#x:M. P#}" == "MCollect M (\\x. P)" + "{#x:M. P#}" == "MCollect M (\x. P)" constdefs set_of :: "'a multiset => 'a set" @@ -52,8 +52,8 @@ instance multiset :: ("term") zero .. defs (overloaded) - union_def: "M + N == Abs_multiset (\\a. Rep_multiset M a + Rep_multiset N a)" - diff_def: "M - N == Abs_multiset (\\a. Rep_multiset M a - Rep_multiset N a)" + union_def: "M + N == Abs_multiset (\a. Rep_multiset M a + Rep_multiset N a)" + diff_def: "M - N == Abs_multiset (\a. Rep_multiset M a - Rep_multiset N a)" Zero_def [simp]: "0 == {#}" size_def: "size M == setsum (count M) (set_of M)" @@ -62,16 +62,16 @@ \medskip Preservation of the representing set @{term multiset}. *} -lemma const0_in_multiset [simp]: "(\\a. 0) \\ multiset" +lemma const0_in_multiset [simp]: "(\a. 0) \ multiset" apply (simp add: multiset_def) done -lemma only1_in_multiset [simp]: "(\\b. if b = a then 1 else 0) \\ multiset" +lemma only1_in_multiset [simp]: "(\b. if b = a then 1' else 0) \ multiset" apply (simp add: multiset_def) done lemma union_preserves_multiset [simp]: - "M \\ multiset ==> N \\ multiset ==> (\\a. M a + N a) \\ multiset" + "M \ multiset ==> N \ multiset ==> (\a. M a + N a) \ multiset" apply (unfold multiset_def) apply simp apply (drule finite_UnI) @@ -80,7 +80,7 @@ done lemma diff_preserves_multiset [simp]: - "M \\ multiset ==> (\\a. M a - N a) \\ multiset" + "M \ multiset ==> (\a. M a - N a) \ multiset" apply (unfold multiset_def) apply simp apply (rule finite_subset) @@ -94,7 +94,7 @@ subsubsection {* Union *} -theorem union_empty [simp]: "M + {#} = M \\ {#} + M = M" +theorem union_empty [simp]: "M + {#} = M \ {#} + M = M" apply (simp add: union_def Mempty_def) done @@ -124,7 +124,7 @@ subsubsection {* Difference *} -theorem diff_empty [simp]: "M - {#} = M \\ {#} - M = {#}" +theorem diff_empty [simp]: "M - {#} = M \ {#} - M = {#}" apply (simp add: Mempty_def diff_def) done @@ -139,7 +139,7 @@ apply (simp add: count_def Mempty_def) done -theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" +theorem count_single [simp]: "count {#b#} a = (if b = a then 1' else 0)" apply (simp add: count_def single_def) done @@ -162,7 +162,7 @@ apply (simp add: set_of_def) done -theorem set_of_union [simp]: "set_of (M + N) = set_of M \\ set_of N" +theorem set_of_union [simp]: "set_of (M + N) = set_of M \ set_of N" apply (auto simp add: set_of_def) done @@ -170,7 +170,7 @@ apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq) done -theorem mem_set_of_iff [simp]: "(x \\ set_of M) = (x :# M)" +theorem mem_set_of_iff [simp]: "(x \ set_of M) = (x :# M)" apply (auto simp add: set_of_def) done @@ -191,7 +191,7 @@ done theorem setsum_count_Int: - "finite A ==> setsum (count N) (A \\ set_of N) = setsum (count N) A" + "finite A ==> setsum (count N) (A \ set_of N) = setsum (count N) A" apply (erule finite_induct) apply simp apply (simp add: Int_insert_left set_of_def) @@ -199,7 +199,7 @@ theorem size_union [simp]: "size (M + N::'a multiset) = size M + size N" apply (unfold size_def) - apply (subgoal_tac "count (M + N) = (\\a. count M a + count N a)") + apply (subgoal_tac "count (M + N) = (\a. count M a + count N a)") prefer 2 apply (rule ext) apply simp @@ -214,7 +214,7 @@ apply (simp add: set_of_def count_def expand_fun_eq) done -theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \\a. a :# M" +theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \a. a :# M" apply (unfold size_def) apply (drule setsum_SucD) apply auto @@ -223,11 +223,11 @@ subsubsection {* Equality of multisets *} -theorem multiset_eq_conv_count_eq: "(M = N) = (\\a. count M a = count N a)" +theorem multiset_eq_conv_count_eq: "(M = N) = (\a. count M a = count N a)" apply (simp add: count_def expand_fun_eq) done -theorem single_not_empty [simp]: "{#a#} \\ {#} \\ {#} \\ {#a#}" +theorem single_not_empty [simp]: "{#a#} \ {#} \ {#} \ {#a#}" apply (simp add: single_def Mempty_def expand_fun_eq) done @@ -235,11 +235,11 @@ apply (auto simp add: single_def expand_fun_eq) done -theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \\ N = {#})" +theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \ N = {#})" apply (auto simp add: union_def Mempty_def expand_fun_eq) done -theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \\ N = {#})" +theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \ N = {#})" apply (auto simp add: union_def Mempty_def expand_fun_eq) done @@ -252,7 +252,7 @@ done theorem union_is_single: - "(M + N = {#a#}) = (M = {#a#} \\ N={#} \\ M = {#} \\ N = {#a#})" + "(M + N = {#a#}) = (M = {#a#} \ N={#} \ M = {#} \ N = {#a#})" apply (unfold Mempty_def single_def union_def) apply (simp add: add_is_1 expand_fun_eq) apply blast @@ -260,16 +260,16 @@ theorem single_is_union: "({#a#} = M + N) = - ({#a#} = M \\ N = {#} \\ M = {#} \\ {#a#} = N)" + ({#a#} = M \ N = {#} \ M = {#} \ {#a#} = N)" apply (unfold Mempty_def single_def union_def) - apply (simp add: add_is_1 expand_fun_eq) + apply (simp add: add_is_1 one_is_add expand_fun_eq) apply (blast dest: sym) done theorem add_eq_conv_diff: "(M + {#a#} = N + {#b#}) = - (M = N \\ a = b \\ - M = N - {#a#} + {#b#} \\ N = M - {#b#} + {#a#})" + (M = N \ a = b \ + M = N - {#a#} + {#b#} \ N = M - {#b#} + {#a#})" apply (unfold single_def union_def diff_def) apply (simp (no_asm) add: expand_fun_eq) apply (rule conjI) @@ -291,7 +291,7 @@ (* val prems = Goal "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F"; -by (res_inst_tac [("a","F"),("f","\\A. if finite A then card A else 0")] +by (res_inst_tac [("a","F"),("f","\A. if finite A then card A else 0")] measure_induct 1); by (Clarify_tac 1); by (resolve_tac prems 1); @@ -320,7 +320,7 @@ lemma setsum_decr: "finite F ==> 0 < f a ==> - setsum (f (a := f a - 1)) F = (if a \\ F then setsum f F - 1 else setsum f F)" + setsum (f (a := f a - 1')) F = (if a \ F then setsum f F - 1 else setsum f F)" apply (erule finite_induct) apply auto apply (drule_tac a = a in mk_disjoint_insert) @@ -328,8 +328,8 @@ done lemma rep_multiset_induct_aux: - "P (\\a. 0) ==> (!!f b. f \\ multiset ==> P f ==> P (f (b := f b + 1))) - ==> \\f. f \\ multiset --> setsum f {x. 0 < f x} = n --> P f" + "P (\a. 0) ==> (!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1'))) + ==> \f. f \ multiset --> setsum f {x. 0 < f x} = n --> P f" proof - case antecedent note prems = this [unfolded multiset_def] @@ -338,7 +338,7 @@ apply (induct_tac n) apply simp apply clarify - apply (subgoal_tac "f = (\\a.0)") + apply (subgoal_tac "f = (\a.0)") apply simp apply (rule prems) apply (rule ext) @@ -347,14 +347,14 @@ apply (frule setsum_SucD) apply clarify apply (rename_tac a) - apply (subgoal_tac "finite {x. 0 < (f (a := f a - 1)) x}") + 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)") + 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)) @@ -363,10 +363,10 @@ apply (erule allE, erule impE, erule_tac [2] mp) apply blast apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply) - apply (subgoal_tac "{x. x \\ a --> 0 < f x} = {x. 0 < f x}") + 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}") + 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 cong: conj_cong) @@ -374,8 +374,8 @@ qed theorem rep_multiset_induct: - "f \\ multiset ==> P (\\a. 0) ==> - (!!f b. f \\ multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" + "f \ multiset ==> P (\a. 0) ==> + (!!f b. f \ multiset ==> P f ==> P (f (b := f b + 1'))) ==> P f" apply (insert rep_multiset_induct_aux) apply blast done @@ -390,7 +390,7 @@ apply (rule Rep_multiset_inverse [THEN subst]) apply (rule Rep_multiset [THEN rep_multiset_induct]) apply (rule prem1) - apply (subgoal_tac "f (b := f b + 1) = (\\a. f a + (if a = b then 1 else 0))") + apply (subgoal_tac "f (b := f b + 1') = (\a. f a + (if a = b then 1' else 0))") prefer 2 apply (simp add: expand_fun_eq) apply (erule ssubst) @@ -401,7 +401,7 @@ lemma MCollect_preserves_multiset: - "M \\ multiset ==> (\\x. if P x then M x else 0) \\ multiset" + "M \ multiset ==> (\x. if P x then M x else 0) \ multiset" apply (simp add: multiset_def) apply (rule finite_subset) apply auto @@ -413,11 +413,11 @@ apply (simp add: MCollect_preserves_multiset) done -theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \\ {x. P x}" +theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \ {x. P x}" apply (auto simp add: set_of_def) done -theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \\ P x #}" +theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \ P x #}" apply (subst multiset_eq_conv_count_eq) apply auto done @@ -427,7 +427,7 @@ theorem add_eq_conv_ex: "(M + {#a#} = N + {#b#}) = - (M = N \\ a = b \\ (\\K. M = K + {#b#} \\ N = K + {#a#}))" + (M = N \ a = b \ (\K. M = K + {#b#} \ N = K + {#a#}))" apply (auto simp add: add_eq_conv_diff) done @@ -437,41 +437,41 @@ subsubsection {* Well-foundedness *} constdefs - mult1 :: "('a \\ 'a) set => ('a multiset \\ 'a multiset) set" + mult1 :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" "mult1 r == - {(N, M). \\a M0 K. M = M0 + {#a#} \\ N = M0 + K \\ - (\\b. b :# K --> (b, a) \\ r)}" + {(N, M). \a M0 K. M = M0 + {#a#} \ N = M0 + K \ + (\b. b :# K --> (b, a) \ r)}" - mult :: "('a \\ 'a) set => ('a multiset \\ 'a multiset) set" + mult :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" "mult r == (mult1 r)\<^sup>+" -lemma not_less_empty [iff]: "(M, {#}) \\ mult1 r" +lemma not_less_empty [iff]: "(M, {#}) \ mult1 r" by (simp add: mult1_def) -lemma less_add: "(N, M0 + {#a#}) \\ mult1 r ==> - (\\M. (M, M0) \\ mult1 r \\ N = M + {#a#}) \\ - (\\K. (\\b. b :# K --> (b, a) \\ r) \\ N = M0 + K)" - (concl is "?case1 (mult1 r) \\ ?case2") +lemma less_add: "(N, M0 + {#a#}) \ mult1 r ==> + (\M. (M, M0) \ mult1 r \ N = M + {#a#}) \ + (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K)" + (concl is "?case1 (mult1 r) \ ?case2") proof (unfold mult1_def) - let ?r = "\\K a. \\b. b :# K --> (b, a) \\ r" - let ?R = "\\N M. \\a M0 K. M = M0 + {#a#} \\ N = M0 + K \\ ?r K a" + let ?r = "\K a. \b. b :# K --> (b, a) \ r" + let ?R = "\N M. \a M0 K. M = M0 + {#a#} \ N = M0 + K \ ?r K a" let ?case1 = "?case1 {(N, M). ?R N M}" - assume "(N, M0 + {#a#}) \\ {(N, M). ?R N M}" - hence "\\a' M0' K. - M0 + {#a#} = M0' + {#a'#} \\ N = M0' + K \\ ?r K a'" by simp - thus "?case1 \\ ?case2" + assume "(N, M0 + {#a#}) \ {(N, M). ?R N M}" + hence "\a' M0' K. + M0 + {#a#} = M0' + {#a'#} \ N = M0' + K \ ?r K a'" by simp + thus "?case1 \ ?case2" proof (elim exE conjE) fix a' M0' K assume N: "N = M0' + K" and r: "?r K a'" assume "M0 + {#a#} = M0' + {#a'#}" - hence "M0 = M0' \\ a = a' \\ - (\\K'. M0 = K' + {#a'#} \\ M0' = K' + {#a#})" + hence "M0 = M0' \ a = a' \ + (\K'. M0 = K' + {#a'#} \ M0' = K' + {#a#})" by (simp only: add_eq_conv_ex) thus ?thesis proof (elim disjE conjE exE) assume "M0 = M0'" "a = a'" - with N r have "?r K a \\ N = M0 + K" by simp + with N r have "?r K a \ N = M0 + K" by simp hence ?case2 .. thus ?thesis .. next fix K' @@ -485,78 +485,78 @@ qed qed -lemma all_accessible: "wf r ==> \\M. M \\ acc (mult1 r)" +lemma all_accessible: "wf r ==> \M. M \ acc (mult1 r)" proof let ?R = "mult1 r" let ?W = "acc ?R" { fix M M0 a - assume M0: "M0 \\ ?W" - and wf_hyp: "\\b. (b, a) \\ r --> (\\M \\ ?W. M + {#b#} \\ ?W)" - and acc_hyp: "\\M. (M, M0) \\ ?R --> M + {#a#} \\ ?W" - have "M0 + {#a#} \\ ?W" + assume M0: "M0 \ ?W" + and wf_hyp: "\b. (b, a) \ r --> (\M \ ?W. M + {#b#} \ ?W)" + and acc_hyp: "\M. (M, M0) \ ?R --> M + {#a#} \ ?W" + have "M0 + {#a#} \ ?W" proof (rule accI [of "M0 + {#a#}"]) fix N - assume "(N, M0 + {#a#}) \\ ?R" - hence "((\\M. (M, M0) \\ ?R \\ N = M + {#a#}) \\ - (\\K. (\\b. b :# K --> (b, a) \\ r) \\ N = M0 + K))" + assume "(N, M0 + {#a#}) \ ?R" + hence "((\M. (M, M0) \ ?R \ N = M + {#a#}) \ + (\K. (\b. b :# K --> (b, a) \ r) \ N = M0 + K))" by (rule less_add) - thus "N \\ ?W" + thus "N \ ?W" proof (elim exE disjE conjE) - fix M assume "(M, M0) \\ ?R" and N: "N = M + {#a#}" - from acc_hyp have "(M, M0) \\ ?R --> M + {#a#} \\ ?W" .. - hence "M + {#a#} \\ ?W" .. - thus "N \\ ?W" by (simp only: N) + fix M assume "(M, M0) \ ?R" and N: "N = M + {#a#}" + from acc_hyp have "(M, M0) \ ?R --> M + {#a#} \ ?W" .. + hence "M + {#a#} \ ?W" .. + thus "N \ ?W" by (simp only: N) next fix K assume N: "N = M0 + K" - assume "\\b. b :# K --> (b, a) \\ r" - have "?this --> M0 + K \\ ?W" (is "?P K") + assume "\b. b :# K --> (b, a) \ r" + have "?this --> M0 + K \ ?W" (is "?P K") proof (induct K) - from M0 have "M0 + {#} \\ ?W" by simp + from M0 have "M0 + {#} \ ?W" by simp thus "?P {#}" .. fix K x assume hyp: "?P K" show "?P (K + {#x#})" proof - assume a: "\\b. b :# (K + {#x#}) --> (b, a) \\ r" - hence "(x, a) \\ r" by simp - with wf_hyp have b: "\\M \\ ?W. M + {#x#} \\ ?W" by blast + assume a: "\b. b :# (K + {#x#}) --> (b, a) \ r" + hence "(x, a) \ r" by simp + with wf_hyp have b: "\M \ ?W. M + {#x#} \ ?W" by blast - from a hyp have "M0 + K \\ ?W" by simp - with b have "(M0 + K) + {#x#} \\ ?W" .. - thus "M0 + (K + {#x#}) \\ ?W" by (simp only: union_assoc) + from a hyp have "M0 + K \ ?W" by simp + with b have "(M0 + K) + {#x#} \ ?W" .. + thus "M0 + (K + {#x#}) \ ?W" by (simp only: union_assoc) qed qed - hence "M0 + K \\ ?W" .. - thus "N \\ ?W" by (simp only: N) + hence "M0 + K \ ?W" .. + thus "N \ ?W" by (simp only: N) qed qed } note tedious_reasoning = this assume wf: "wf r" fix M - show "M \\ ?W" + show "M \ ?W" proof (induct M) - show "{#} \\ ?W" + show "{#} \ ?W" proof (rule accI) - fix b assume "(b, {#}) \\ ?R" - with not_less_empty show "b \\ ?W" by contradiction + fix b assume "(b, {#}) \ ?R" + with not_less_empty show "b \ ?W" by contradiction qed - fix M a assume "M \\ ?W" - from wf have "\\M \\ ?W. M + {#a#} \\ ?W" + fix M a assume "M \ ?W" + from wf have "\M \ ?W. M + {#a#} \ ?W" proof induct fix a - assume "\\b. (b, a) \\ r --> (\\M \\ ?W. M + {#b#} \\ ?W)" - show "\\M \\ ?W. M + {#a#} \\ ?W" + assume "\b. (b, a) \ r --> (\M \ ?W. M + {#b#} \ ?W)" + show "\M \ ?W. M + {#a#} \ ?W" proof - fix M assume "M \\ ?W" - thus "M + {#a#} \\ ?W" + fix M assume "M \ ?W" + thus "M + {#a#} \ ?W" by (rule acc_induct) (rule tedious_reasoning) qed qed - thus "M + {#a#} \\ ?W" .. + thus "M + {#a#} \ ?W" .. qed qed @@ -578,9 +578,9 @@ text {* One direction. *} lemma mult_implies_one_step: - "trans r ==> (M, N) \\ mult r ==> - \\I J K. N = I + J \\ M = I + K \\ J \\ {#} \\ - (\\k \\ set_of K. \\j \\ set_of J. (k, j) \\ r)" + "trans r ==> (M, N) \ mult r ==> + \I J K. N = I + J \ M = I + K \ J \ {#} \ + (\k \ set_of K. \j \ set_of J. (k, j) \ r)" apply (unfold mult_def mult1_def set_of_def) apply (erule converse_trancl_induct) apply clarify @@ -592,7 +592,7 @@ apply (simp (no_asm)) apply (rule_tac x = "(K - {#a#}) + Ka" in exI) apply (simp (no_asm_simp) add: union_assoc [symmetric]) - apply (drule_tac f = "\\M. M - {#a#}" in arg_cong) + apply (drule_tac f = "\M. M - {#a#}" in arg_cong) apply (simp add: diff_union_single_conv) apply (simp (no_asm_use) add: trans_def) apply blast @@ -603,7 +603,7 @@ apply (rule conjI) apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) apply (rule conjI) - apply (drule_tac f = "\\M. M - {#a#}" in arg_cong) + apply (drule_tac f = "\M. M - {#a#}" in arg_cong) apply simp apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) apply (simp (no_asm_use) add: trans_def) @@ -617,7 +617,7 @@ apply (simp add: multiset_eq_conv_count_eq) done -lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \\a N. M = N + {#a#}" +lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \a N. M = N + {#a#}" apply (erule size_eq_Suc_imp_elem [THEN exE]) apply (drule elem_imp_eq_diff_union) apply auto @@ -625,8 +625,8 @@ lemma one_step_implies_mult_aux: "trans r ==> - \\I J K. (size J = n \\ J \\ {#} \\ (\\k \\ set_of K. \\j \\ set_of J. (k, j) \\ r)) - --> (I + K, I + J) \\ mult r" + \I J K. (size J = n \ J \ {#} \ (\k \ set_of K. \j \ set_of J. (k, j) \ r)) + --> (I + K, I + J) \ mult r" apply (induct_tac n) apply auto apply (frule size_eq_Suc_imp_eq_union) @@ -640,15 +640,15 @@ apply (rule r_into_trancl) apply (simp add: mult1_def set_of_def) apply blast - txt {* Now we know @{term "J' \\ {#}"}. *} - apply (cut_tac M = K and P = "\\x. (x, a) \\ r" in multiset_partition) - apply (erule_tac P = "\\k \\ set_of K. ?P k" in rev_mp) + txt {* Now we know @{term "J' \ {#}"}. *} + apply (cut_tac M = K and P = "\x. (x, a) \ r" in multiset_partition) + apply (erule_tac P = "\k \ set_of K. ?P k" in rev_mp) apply (erule ssubst) apply (simp add: Ball_def) apply auto apply (subgoal_tac - "((I + {# x : K. (x, a) \\ r #}) + {# x : K. (x, a) \\ r #}, - (I + {# x : K. (x, a) \\ r #}) + J') \\ mult r") + "((I + {# x : K. (x, a) \ r #}) + {# x : K. (x, a) \ r #}, + (I + {# x : K. (x, a) \ r #}) + J') \