diff --git a/thys/Compiling-Exceptions-Correctly/Exceptions.thy b/thys/Compiling-Exceptions-Correctly/Exceptions.thy --- a/thys/Compiling-Exceptions-Correctly/Exceptions.thy +++ b/thys/Compiling-Exceptions-Correctly/Exceptions.thy @@ -1,186 +1,191 @@ (* Author: Tobias Nipkow Copyright 2004 TU Muenchen *) section \Compiling exception handling\ theory Exceptions imports Main begin subsection\The source language\ datatype expr = Val int | Add expr expr | Throw | Catch expr expr primrec eval :: "expr \ int option" where "eval (Val i) = Some i" | "eval (Add x y) = (case eval x of None \ None | Some i \ (case eval y of None \ None | Some j \ Some(i+j)))" | "eval Throw = None" | "eval (Catch x h) = (case eval x of None \ eval h | Some i \ Some i)" subsection\The target language\ datatype instr = Push int | ADD | THROW | Mark nat | Unmark | Label nat | Jump nat datatype item = VAL int | HAN nat type_synonym code = "instr list" type_synonym stack = "item list" fun jump where "jump l [] = []" | "jump l (Label l' # cs) = (if l = l' then cs else jump l cs)" | "jump l (c # cs) = jump l cs" lemma size_jump1: "size (jump l cs) < Suc (size cs)" apply(induct cs) apply simp apply(case_tac a) apply auto done lemma size_jump2: "size (jump l cs) < size cs \ jump l cs = cs" apply(induct cs) apply simp apply(case_tac a) apply auto -done + done + +lemma jump_neq [simp]: "jump l cs \ Jump l # cs" + using size_jump1 [of l cs] by auto function (sequential) exec2 :: "bool \ code \ stack \ stack" where "exec2 True [] s = s" | "exec2 True (Push i#cs) s = exec2 True cs (VAL i # s)" | "exec2 True (ADD#cs) (VAL j # VAL i # s) = exec2 True cs (VAL(i+j) # s)" | "exec2 True (THROW#cs) s = exec2 False cs s" | "exec2 True (Mark l#cs) s = exec2 True cs (HAN l # s)" | "exec2 True (Unmark#cs) (v # HAN l # s) = exec2 True cs (v # s)" | "exec2 True (Label l#cs) s = exec2 True cs s" | "exec2 True (Jump l#cs) s = exec2 True (jump l cs) s" | "exec2 False cs [] = []" | "exec2 False cs (VAL i # s) = exec2 False cs s" | "exec2 False cs (HAN l # s) = exec2 True (jump l cs) s" by pat_completeness auto -termination by (relation +termination + apply (relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(b,cs,s). (cs,s))") - (auto simp add: size_jump1 size_jump2) + using size_jump2 apply(force simp add: size_jump1)+ + done abbreviation "exec \ exec2 True" abbreviation "unwind \ exec2 False" subsection\The compiler\ primrec compile :: "nat \ expr \ code * nat" where "compile l (Val i) = ([Push i], l)" | "compile l (Add x y) = (let (xs,m) = compile l x; (ys,n) = compile m y in (xs @ ys @ [ADD], n))" | "compile l Throw = ([THROW],l)" | "compile l (Catch x h) = (let (xs,m) = compile (l+2) x; (hs,n) = compile m h in (Mark l # xs @ [Unmark, Jump (l+1), Label l] @ hs @ [Label(l+1)], n))" abbreviation cmp :: "nat \ expr \ code" where "cmp l e == fst(compile l e)" primrec isFresh :: "nat \ stack \ bool" where "isFresh l [] = True" | "isFresh l (it#s) = (case it of VAL i \ isFresh l s | HAN l' \ l' < l \ isFresh l s)" definition conv :: "code \ stack \ int option \ stack" where "conv cs s io = (case io of None \ unwind cs s | Some i \ exec cs (VAL i # s))" subsection\The proofs\ text\Lemma numbers are the same as in the paper.\ declare conv_def[simp] option.splits[split] Let_def[simp] lemma 3: "(\l. c = Label l \ isFresh l s) \ unwind (c#cs) s = unwind cs s" apply(induct s) apply simp apply(auto) apply(case_tac a) apply auto apply(case_tac c) apply auto done corollary [simp]: "(!!l. c \ Label l) \ unwind (c#cs) s = unwind cs s" by(blast intro: 3) corollary [simp]: "isFresh l s \ unwind (Label l#cs) s = unwind cs s" by(blast intro: 3) lemma 5: "\ isFresh l s; l \ m \ \ isFresh m s" apply(induct s) apply simp apply(auto split:item.split) done corollary [simp]: "isFresh l s \ isFresh (Suc l) s" by(auto intro:5) lemma 6: "\l. l \ snd(compile l e)" proof(induct e) case Val thus ?case by simp next case (Add x y) from \l \ snd (compile l x)\ and \snd (compile l x) \ snd (compile (snd (compile l x)) y)\ show ?case by(simp_all add:split_def) next case Throw thus ?case by simp next case (Catch x h) from \l+2 \ snd (compile (l+2) x)\ and \snd (compile (l+2) x) \ snd (compile (snd (compile (l+2) x)) h)\ show ?case by(simp_all add:split_def) qed corollary [simp]: "l < m \ l < snd(compile m e)" using 6[where l = m and e = e] by auto corollary [simp]: "isFresh l s \ isFresh (snd(compile l e)) s" using 5 6 by blast text\Contrary to what the paper says, the proof of lemma 4 does not just need lemma 3 but also the above corollary of 5 and 6. Hence the strange order of the lemmas in our proof.\ lemma 4 [simp]: "\l cs. isFresh l s \ unwind (cmp l e @ cs) s = unwind cs s" by (induct e) (auto simp add:split_def) lemma 7 [simp]: "l < m \ jump l (cmp m e @ cs) = jump l cs" by (induct e arbitrary: m cs) (simp_all add:split_def) text\The compiler correctness theorem:\ theorem comp_corr: "\l s cs. isFresh l s \ exec (cmp l e @ cs) s = conv cs s (eval e)" by(induct e)(auto simp add:split_def) text\The specialized and more readable version (omitted in the paper):\ corollary "exec (cmp l e) [] = (case eval e of None \ [] | Some n \ [VAL n])" by (simp add: comp_corr[where cs = "[]", simplified]) end diff --git a/thys/Diophantine_Eqns_Lin_Hom/List_Vector.thy b/thys/Diophantine_Eqns_Lin_Hom/List_Vector.thy --- a/thys/Diophantine_Eqns_Lin_Hom/List_Vector.thy +++ b/thys/Diophantine_Eqns_Lin_Hom/List_Vector.thy @@ -1,687 +1,662 @@ (* Author: Florian Messner Author: Julian Parsert Author: Jonas Schöpf Author: Christian Sternagel License: LGPL *) section \Vectors as Lists of Naturals\ theory List_Vector imports Main begin (*TODO: move*) lemma lex_lengthD: "(x, y) \ lex P \ length x = length y" by (auto simp: lexord_lex) (*TODO: move*) -lemma lexI: - assumes "length ys = length xs" and "i < length xs" - and "take i xs = take i ys" and "(xs ! i, ys ! i) \ r" - shows "(xs, ys) \ lex r" -proof - - have "xs = take i xs @ xs ! i # drop (Suc i) xs" - and "ys = take i ys @ ys ! i # drop (Suc i) ys" - using assms by (metis id_take_nth_drop)+ - then show ?thesis - using assms by (auto simp: lex_def lexn_conv) -qed - -(*TODO: move*) lemma lex_take_index: assumes "(xs, ys) \ lex r" obtains i where "length ys = length xs" and "i < length xs" and "take i xs = take i ys" and "(xs ! i, ys ! i) \ r" proof - obtain n us x xs' y ys' where "(xs, ys) \ lexn r n" and "length xs = n" and "length ys = n" and "xs = us @ x # xs'" and "ys = us @ y # ys'" and "(x, y) \ r" using assms by (fastforce simp: lex_def lexn_conv) then show ?thesis by (intro that [of "length us"]) auto qed (*TODO: move*) lemma mods_with_nats: assumes "(v::nat) > w" and "(v * b) mod a = (w * b) mod a" shows "((v - w) * b) mod a = 0" by (metis add_diff_cancel_left' assms left_diff_distrib' less_imp_le mod_mult_self1_is_0 mult_le_mono1 nat_mod_eq_lemma) \ \The 0-vector of length \n\.\ abbreviation zeroes :: "nat \ nat list" where "zeroes n \ replicate n 0" lemma rep_upd_unit: assumes "x = (zeroes n)[i := a]" shows "\j < length x. (j \ i \ x ! j = 0) \ (j = i \ x ! j = a)" using assms by simp definition nonzero_iff: "nonzero xs \ (\x\set xs. x \ 0)" lemma nonzero_append [simp]: "nonzero (xs @ ys) \ nonzero xs \ nonzero ys" by (auto simp: nonzero_iff) subsection \The Inner Product\ definition dotprod :: "nat list \ nat list \ nat" (infixl "\" 70) where "xs \ ys = (\i ys = sum_list (map (\(x, y). x * y) (zip xs ys))" by (auto simp: dotprod_def sum_list_sum_nth lessThan_atLeast0) lemma dotprod_commute: assumes "length xs = length ys" shows "xs \ ys = ys \ xs" using assms by (auto simp: dotprod_def mult.commute) lemma dotprod_Nil [simp]: "[] \ [] = 0" by (simp add: dotprod_def) lemma dotprod_Cons [simp]: "(x # xs) \ (y # ys) = x * y + xs \ ys" unfolding dotprod_def and length_Cons and min_Suc_Suc and sum.lessThan_Suc_shift by auto lemma dotprod_1_right [simp]: "xs \ replicate (length xs) 1 = sum_list xs" by (induct xs) (simp_all) lemma dotprod_0_right [simp]: "xs \ zeroes (length xs) = 0" by (induct xs) (simp_all) lemma dotprod_unit [simp]: assumes "length a = n" and "k < n" shows "a \ (zeroes n)[k := zk] = a ! k * zk" using assms by (induct a arbitrary: k n) (auto split: nat.splits) lemma dotprod_gt0: assumes "length x = length y" and "\i 0 \ y ! i > 0" shows "x \ y > 0" using assms by (induct x y rule: list_induct2) (fastforce simp: nth_Cons split: nat.splits)+ lemma dotprod_gt0D: assumes "length x = length y" and "x \ y > 0" shows "\i 0 \ y ! i > 0" using assms by (induct x y rule: list_induct2) (auto simp: Ex_less_Suc2) lemma dotprod_gt0_iff [iff]: assumes "length x = length y" shows "x \ y > 0 \ (\i 0 \ y ! i > 0)" using assms and dotprod_gt0D and dotprod_gt0 by blast lemma dotprod_append: assumes "length a = length b" shows"(a @ x) \ (b @ y) = a \ b + x \ y" using assms by (induct a b rule: list_induct2) auto lemma dotprod_le_take: assumes "length a = length b" and "k \ length a" shows"take k a \ take k b \ a \ b" using assms and append_take_drop_id [of k a] and append_take_drop_id [of k b] by (metis add_right_cancel leI length_append length_drop not_add_less1 dotprod_append) lemma dotprod_le_drop: assumes "length a = length b" and "k \ length a" shows "drop k a \ drop k b \ a \ b" using assms and append_take_drop_id [of k a] and append_take_drop_id [of k b] by (metis dotprod_append length_take order_refl trans_le_add2) lemma dotprod_is_0 [simp]: assumes "length x = length y" shows "x \ y = 0 \ (\i y ! i = 0)" using assms by (metis dotprod_gt0_iff neq0_conv) lemma dotprod_eq_0_iff: assumes "length x = length a" and "0 \ set a" shows "x \ a = 0 \ (\e \ set x. e = 0)" using assms by (fastforce simp: in_set_conv_nth) lemma dotprod_eq_nonzero_iff: assumes "a \ x = b \ y" and "length x = length a" and "length y = length b" and "0 \ set a" and "0 \ set b" shows "nonzero x \ nonzero y" using assms by (auto simp: nonzero_iff) (metis dotprod_commute dotprod_eq_0_iff neq0_conv)+ lemma eq_0_iff: "xs = zeroes n \ length xs = n \ (\x\set xs. x = 0)" using in_set_replicate [of _ n 0] and replicate_eqI [of xs n 0] by auto lemma not_nonzero_iff: "\ nonzero x \ x = zeroes (length x)" by (auto simp: nonzero_iff replicate_length_same eq_0_iff) lemma neq_0_iff': "xs \ zeroes n \ length xs \ n \ (\x\set xs. x > 0)" by (auto simp: eq_0_iff) lemma dotprod_pointwise_le: assumes "length as = length xs" and "i < length as" shows "as ! i * xs ! i \ as \ xs" proof - have "as \ xs = (\i y = x * sum_list y" proof - have "x * (\iiThe Pointwise Order on Vectors\ definition less_eq :: "nat list \ nat list \ bool" ("_/ \\<^sub>v _" [51, 51] 50) where "xs \\<^sub>v ys \ length xs = length ys \ (\i ys ! i)" definition less :: "nat list \ nat list \ bool" ("_/ <\<^sub>v _" [51, 51] 50) where "xs <\<^sub>v ys \ xs \\<^sub>v ys \ \ ys \\<^sub>v xs" interpretation order_vec: order less_eq less by (standard, auto simp add: less_def less_eq_def dual_order.antisym nth_equalityI) (force) lemma less_eqI [intro?]: "length xs = length ys \ \i ys ! i \ xs \\<^sub>v ys" by (auto simp: less_eq_def) lemma le0 [simp, intro]: "zeroes (length xs) \\<^sub>v xs" by (simp add: less_eq_def) lemma le_list_update [simp]: assumes "xs \\<^sub>v ys" and "i < length ys" and "z \ ys ! i" shows "xs[i := z] \\<^sub>v ys" using assms by (auto simp: less_eq_def nth_list_update) lemma le_Cons: "x # xs \\<^sub>v y # ys \ x \ y \ xs \\<^sub>v ys" by (auto simp add: less_eq_def nth_Cons split: nat.splits) lemma zero_less: assumes "nonzero x" shows "zeroes (length x) <\<^sub>v x" using assms and eq_0_iff order_vec.dual_order.strict_iff_order by (auto simp: nonzero_iff) lemma le_append: assumes "length xs = length vs" shows "xs @ ys \\<^sub>v vs @ ws \ xs \\<^sub>v vs \ ys \\<^sub>v ws" using assms by (auto simp: less_eq_def nth_append) (metis add.commute add_diff_cancel_left' nat_add_left_cancel_less not_add_less2) lemma less_Cons: "(x # xs) <\<^sub>v (y # ys) \ length xs = length ys \ (x \ y \ xs <\<^sub>v ys \ x < y \ xs \\<^sub>v ys)" by (simp add: less_def less_eq_def All_less_Suc2) (auto dest: leD) lemma le_length [dest]: assumes "xs \\<^sub>v ys" shows "length xs = length ys" using assms by (simp add: less_eq_def) lemma less_length [dest]: assumes "x <\<^sub>v y" shows "length x = length y" using assms by (auto simp: less_def) lemma less_append: assumes "xs <\<^sub>v vs " and "ys \\<^sub>v ws" shows "xs @ ys <\<^sub>v vs @ ws" proof - have "length xs = length vs" using assms by blast then show ?thesis using assms by (induct xs vs rule: list_induct2) (auto simp: less_Cons le_append le_length) qed lemma less_appendD: assumes "xs @ ys <\<^sub>v vs @ ws" and "length xs = length vs" shows "xs <\<^sub>v vs \ ys <\<^sub>v ws" by (auto) (metis (no_types, lifting) assms le_append order_vec.order.strict_iff_order) lemma less_append_cases: assumes "xs @ ys <\<^sub>v vs @ ws" and "length xs = length vs" obtains "xs <\<^sub>v vs" and "ys \\<^sub>v ws" | "xs \\<^sub>v vs" and "ys <\<^sub>v ws" using assms and that by (metis le_append less_appendD order_vec.order.strict_implies_order) lemma less_append_swap: assumes "x @ y <\<^sub>v u @ v" and "length x = length u" shows "y @ x <\<^sub>v v @ u" using assms(2, 1) by (induct x u rule: list_induct2) (auto simp: order_vec.order.strict_iff_order le_Cons le_append le_length) lemma le_sum_list_less: assumes "xs \\<^sub>v ys" and "sum_list xs < sum_list ys" shows "xs <\<^sub>v ys" proof - have "length xs = length ys" and "\i ys ! i" using assms by (auto simp: less_eq_def) then show ?thesis using \sum_list xs < sum_list ys\ by (induct xs ys rule: list_induct2) (auto simp: less_Cons All_less_Suc2 less_eq_def) qed lemma dotprod_le_right: assumes "v \\<^sub>v w" and "length b = length w" shows "b \ v \ b \ w" using assms by (auto simp: dotprod_def less_eq_def intro: sum_mono) lemma dotprod_pointwise_le_right: assumes "length z = length u" and "length u = length v" and "\i v ! i" shows "z \ u \ z \ v" using assms by (intro dotprod_le_right) (auto intro: less_eqI) lemma dotprod_le_left: assumes "v \\<^sub>v w" and "length b = length w" shows "v \ b \ w \ b " using assms by (simp add: dotprod_le_right dotprod_commute le_length) lemma dotprod_le: assumes "x \\<^sub>v u" and "y \\<^sub>v v" and "length y = length x" and "length v = length u" shows "x \ y \ u \ v" using assms by (metis dotprod_le_left dotprod_le_right le_length le_trans) lemma dotprod_less_left: assumes "length b = length w" and "0 \ set b" and "v <\<^sub>v w" shows "v \ b < w \ b" proof - have "length v = length w" using assms using less_eq_def order_vec.order.strict_implies_order by blast then show ?thesis using assms proof (induct v w arbitrary: b rule: list_induct2) case (Cons x xs y ys) then show ?case by (cases b) (auto simp: less_Cons add_mono_thms_linordered_field dotprod_le_left) qed simp qed lemma le_append_swap: assumes "length y = length v" and "x @ y \\<^sub>v w @ v" shows "y @ x \\<^sub>v v @ w" proof - have "length w = length x" using assms by auto with assms show ?thesis by (induct y v arbitrary: x w rule: list_induct2) (auto simp: le_Cons le_append) qed lemma le_append_swap_iff: assumes "length y = length v" shows "y @ x \\<^sub>v v @ w \ x @ y \\<^sub>v w @ v" using assms and le_append_swap by (auto) (metis (no_types, lifting) add_left_imp_eq le_length length_append) lemma unit_less: assumes "i < n" and "x <\<^sub>v (zeroes n)[i := b]" shows "x ! i < b \ (\j i \ x ! j = 0)" proof show "x ! i < b" using assms less_def by fastforce next have "x \\<^sub>v (zeroes n)[i := b]" by (simp add: assms order_vec.less_imp_le) then show "\j i \ x ! j = 0" by (auto simp: less_eq_def) qed lemma le_sum_list_mono: assumes "xs \\<^sub>v ys" shows "sum_list xs \ sum_list ys" using assms and sum_list_mono [of "[0..\<^sub>v y" and "sum_list u < sum_list y" shows "\ii y ! i" using \u \\<^sub>v y\ by (auto simp: less_eq_def) then show ?thesis using \sum_list u < sum_list y\ by (induct u y rule: list_induct2) (force simp: Ex_less_Suc2 All_less_Suc2)+ qed lemma less_vec_sum_list_less: assumes "v <\<^sub>v w" shows "sum_list v < sum_list w" using assms proof - have "length v = length w" using assms less_eq_def less_imp_le by blast then show ?thesis using assms proof (induct v w rule: list_induct2) case (Cons x xs y ys) then show ?case using length_replicate less_Cons order_vec.order.strict_iff_order by force qed simp qed definition maxne0 :: "nat list \ nat list \ nat" where "maxne0 x a = (if length x = length a \ (\i 0) then Max {a ! i | i. i < length a \ x ! i \ 0} else 0)" lemma maxne0_le_Max: "maxne0 x a \ Max (set a)" by (auto simp: maxne0_def nonzero_iff in_set_conv_nth) simp lemma maxne0_Nil [simp]: "maxne0 [] as = 0" "maxne0 xs [] = 0" by (auto simp: maxne0_def) lemma maxne0_Cons [simp]: "maxne0 (x # xs) (a # as) = (if length xs = length as then (if x = 0 then maxne0 xs as else max a (maxne0 xs as)) else 0)" proof - let ?a = "a # as" and ?x = "x # xs" have eq: "{?a ! i | i. i < length ?a \ ?x ! i \ 0} = (if x > 0 then {a} else {}) \ {as ! i | i. i < length as \ xs ! i \ 0}" by (auto simp: nth_Cons split: nat.splits) (metis Suc_pred)+ show ?thesis unfolding maxne0_def and eq by (auto simp: less_Suc_eq_0_disj nth_Cons' intro: Max_insert2) qed lemma maxne0_times_sum_list_gt_dotprod: assumes "length b = length ys" shows "maxne0 ys b * sum_list ys \ b \ ys" using assms apply (induct b ys rule: list_induct2) apply (auto simp: max_def ring_distribs add_mono_thms_linordered_semiring(1)) by (meson leI le_trans mult_less_cancel2 nat_less_le) lemma max_times_sum_list_gt_dotprod: assumes "length b = length ys" shows "Max (set b) * sum_list ys \ b \ ys" proof - have "\ e \ set b . Max (set b) \ e" by simp then have "replicate (length ys) (Max (set b)) \ ys \ b \ ys" (is "?rep \ _") by (metis assms dotprod_pointwise_le_right dotprod_commute length_replicate nth_mem nth_replicate) moreover have "Max (set b) * sum_list ys = ?rep" using replicate_dotprod [of ys _ "Max (set b)"] by auto ultimately show ?thesis by (simp add: assms) qed lemma maxne0_mono: assumes "y \\<^sub>v x" shows "maxne0 y a \ maxne0 x a" proof (cases "length y = length a") case True have "length y = length x" using assms by (auto) then show ?thesis using assms and True proof (induct y x arbitrary: a rule: list_induct2) case (Cons x xs y ys) then show ?case by (cases a) (force simp: less_eq_def All_less_Suc2 le_max_iff_disj)+ qed simp next case False then show ?thesis using assms by (auto simp: maxne0_def) qed lemma all_leq_Max: assumes "x \\<^sub>v y" and "x \ []" shows "\xi \ set x. xi \ Max (set y)" by (metis (no_types, lifting) List.finite_set Max_ge_iff assms in_set_conv_nth length_0_conv less_eq_def set_empty) lemma le_not_less_replicate: "\x\set xs. x \ b \ \ xs <\<^sub>v replicate (length xs) b \ xs = replicate (length xs) b" by (induct xs) (auto simp: less_Cons) lemma le_replicateI: "\x\set xs. x \ b \ xs \\<^sub>v replicate (length xs) b" by (induct xs) (auto simp: le_Cons) lemma le_take: assumes "x \\<^sub>v y" and "i \ length x" shows "take i x \\<^sub>v take i y" using assms by (auto simp: less_eq_def) lemma wf_less: "wf {(x, y). x <\<^sub>v y}" proof - have "wf (measure sum_list)" .. moreover have "{(x, y). x <\<^sub>v y} \ measure sum_list" by (auto simp: less_vec_sum_list_less) ultimately show "wf {(x, y). x <\<^sub>v y}" by (rule wf_subset) qed subsection \Pointwise Subtraction\ definition vdiff :: "nat list \ nat list \ nat list" (infixl "-\<^sub>v" 65) where "w -\<^sub>v v = map (\i. w ! i - v ! i) [0 ..< length w]" lemma vdiff_Nil [simp]: "[] -\<^sub>v [] = []" by (simp add: vdiff_def) lemma upt_Cons_conv: assumes "j < n" shows "[j.. Suc) [m ..< n]" by (fold list.map_comp [of f "Suc" "[m ..< n]"]) (simp add: map_Suc_upt) lemma vdiff_Cons [simp]: "(x # xs) -\<^sub>v (y # ys) = (x - y) # (xs -\<^sub>v ys)" by (simp add: vdiff_def upt_Cons_conv [OF zero_less_Suc] map_upt_Suc del: upt_Suc) lemma vdiff_alt_def: assumes "length w = length v" shows "w -\<^sub>v v = map (\(x, y). x - y) (zip w v)" using assms by (induct rule: list_induct2) simp_all lemma vdiff_dotprod_distr: assumes "length b = length w" and "v \\<^sub>v w" shows "(w -\<^sub>v v) \ b = w \ b - v \ b" proof - have "length v = length w" and "\i w ! i" using assms less_eq_def by auto then show ?thesis using \length b = length w\ proof (induct v w arbitrary: b rule: list_induct2) case (Cons x xs y ys) then show ?case by (cases b) (auto simp: All_less_Suc2 diff_mult_distrib dotprod_commute dotprod_pointwise_le_right) qed simp qed lemma sum_list_vdiff_distr [simp]: assumes "v \\<^sub>v u" shows "sum_list (u -\<^sub>v v) = sum_list u - sum_list v" by (metis (no_types, lifting) assms diff_zero dotprod_1_right length_map length_replicate length_upt less_eq_def vdiff_def vdiff_dotprod_distr) lemma vdiff_le: assumes "v \\<^sub>v w" and "length v = length x" shows "v -\<^sub>v x \\<^sub>v w" using assms by (auto simp add: less_eq_def vdiff_def) lemma mods_with_vec: assumes "v <\<^sub>v w" and "0 \ set b" and "length b = length w" and "(v \ b) mod a = (w \ b) mod a" shows "((w -\<^sub>v v) \ b) mod a = 0" proof - have *: "v \ b < w \ b" using dotprod_less_left and assms by blast have "v \\<^sub>v w" using assms by auto from vdiff_dotprod_distr [OF assms(3) this] have "((w -\<^sub>v v) \ b) mod a = (w \ b - v \ b) mod a " by simp also have "... = 0 mod a" using mods_with_nats [of "v \ b" "w \ b" "1" a, OF *] assms by auto finally show ?thesis by simp qed lemma mods_with_vec_2: assumes "v <\<^sub>v w" and "0 \ set b" and "length b = length w" and "(b \ v) mod a = (b \ w) mod a" shows "(b \ (w -\<^sub>v v)) mod a = 0" by (metis (no_types, lifting) assms diff_zero dotprod_commute length_map length_upt less_eq_def order_vec.less_imp_le mods_with_vec vdiff_def) subsection \The Lexicographic Order on Vectors\ abbreviation lex_less_than ("_/ <\<^sub>l\<^sub>e\<^sub>x _" [51, 51] 50) where "xs <\<^sub>l\<^sub>e\<^sub>x ys \ (xs, ys) \ lex less_than" definition rlex (infix "<\<^sub>r\<^sub>l\<^sub>e\<^sub>x" 50) where "xs <\<^sub>r\<^sub>l\<^sub>e\<^sub>x ys \ rev xs <\<^sub>l\<^sub>e\<^sub>x rev ys" lemma rev_le [simp]: "rev xs \\<^sub>v rev ys \ xs \\<^sub>v ys" proof - { fix i assume i: "i < length ys" and [simp]: "length xs = length ys" and "\i < length ys. rev xs ! i \ rev ys ! i" then have "rev xs ! (length ys - i - 1) \ rev ys ! (length ys - i - 1)" by auto then have "xs ! i \ ys ! i" using i by (auto simp: rev_nth) } then show ?thesis by (auto simp: less_eq_def rev_nth) qed lemma rev_less [simp]: "rev xs <\<^sub>v rev ys \ xs <\<^sub>v ys" by (simp add: less_def) lemma less_imp_lex: assumes "xs <\<^sub>v ys" shows "xs <\<^sub>l\<^sub>e\<^sub>x ys" proof - have "length ys = length xs" using assms by auto then show ?thesis using assms by (induct rule: list_induct2) (auto simp: less_Cons) qed lemma less_imp_rlex: assumes "xs <\<^sub>v ys" shows "xs <\<^sub>r\<^sub>l\<^sub>e\<^sub>x ys" using assms and less_imp_lex [of "rev xs" "rev ys"] by (simp add: rlex_def) lemma lex_not_sym: assumes "xs <\<^sub>l\<^sub>e\<^sub>x ys" shows "\ ys <\<^sub>l\<^sub>e\<^sub>x xs" proof assume "ys <\<^sub>l\<^sub>e\<^sub>x xs" then obtain i where "i < length xs" and "take i xs = take i ys" and "ys ! i < xs ! i" by (elim lex_take_index) auto moreover obtain j where "j < length xs" and "length ys = length xs" and "take j xs = take j ys" and "xs ! j < ys ! j" using assms by (elim lex_take_index) auto ultimately show False by (metis le_antisym nat_less_le nat_neq_iff nth_take) qed lemma rlex_not_sym: assumes "xs <\<^sub>r\<^sub>l\<^sub>e\<^sub>x ys" shows "\ ys <\<^sub>r\<^sub>l\<^sub>e\<^sub>x xs" proof assume ass: "ys <\<^sub>r\<^sub>l\<^sub>e\<^sub>x xs" then obtain i where "i < length xs" and "take i xs = take i ys" and "ys ! i > xs ! i" using assms lex_not_sym rlex_def by blast moreover obtain j where "j < length xs" and "length ys = length xs" and "take j xs = take j ys" and "xs ! j > ys ! j" using assms rlex_def ass lex_not_sym by blast ultimately show False by (metis leD nat_less_le nat_neq_iff nth_take) qed lemma lex_trans: assumes "x <\<^sub>l\<^sub>e\<^sub>x y" and "y <\<^sub>l\<^sub>e\<^sub>x z" shows "x <\<^sub>l\<^sub>e\<^sub>x z" -proof - - from assms obtain i and j where "length y = length x" and "length z = length x" - and "i < length x" and "j < length x" - and "take i x = take i y" and "take j y = take j z" - and "x ! i < y ! i" and "y ! j < z ! j" by (fastforce elim!: lex_take_index) - then show ?thesis - apply (intro lexI [where i = "min i j"]) - apply (auto) - apply (metis min.commute take_take) - apply (auto simp: min_def) - apply (metis dual_order.order_iff_strict dual_order.trans not_le nth_take) - by (metis not_less nth_take) -qed + using assms by (auto simp: antisym_def intro: transD [OF lex_transI]) lemma rlex_trans: assumes "x <\<^sub>r\<^sub>l\<^sub>e\<^sub>x y" and "y <\<^sub>r\<^sub>l\<^sub>e\<^sub>x z" shows "x <\<^sub>r\<^sub>l\<^sub>e\<^sub>x z" using assms lex_trans rlex_def by blast lemma lex_append_rightD: assumes "xs @ us <\<^sub>l\<^sub>e\<^sub>x ys @ vs" and "length xs = length ys" and "\ xs <\<^sub>l\<^sub>e\<^sub>x ys" shows "ys = xs \ us <\<^sub>l\<^sub>e\<^sub>x vs" using assms(2,1,3) - by (induct xs ys rule: list_induct2) simp_all + by (induct xs ys rule: list_induct2) auto lemma rlex_Cons: "x # xs <\<^sub>r\<^sub>l\<^sub>e\<^sub>x y # ys \ xs <\<^sub>r\<^sub>l\<^sub>e\<^sub>x ys \ ys = xs \ x < y" (is "?A = ?B") by (cases "length ys = length xs") (auto simp: rlex_def intro: lex_append_rightI lex_append_leftI dest: lex_append_rightD lex_lengthD) lemma rlex_irrefl: "\ x <\<^sub>r\<^sub>l\<^sub>e\<^sub>x x" by (induct x) (auto simp: rlex_def dest: lex_append_rightD) subsection \Code Equations\ fun exists2 where "exists2 d P [] [] \ False" | "exists2 d P (x#xs) (y#ys) \ P x y \ exists2 d P xs ys" | "exists2 d P _ _ \ d" lemma not_le_code [code_unfold]: "\ xs \\<^sub>v ys \ exists2 True (>) xs ys" by (induct "True" "(>) :: nat \ nat \ bool" xs ys rule: exists2.induct) (auto simp: le_Cons) end diff --git a/thys/LTL_to_GBA/LTL_to_GBA.thy b/thys/LTL_to_GBA/LTL_to_GBA.thy --- a/thys/LTL_to_GBA/LTL_to_GBA.thy +++ b/thys/LTL_to_GBA/LTL_to_GBA.thy @@ -1,3224 +1,3233 @@ section \LTL to GBA translation\ (* Author: Alexander Schimpf Modified by Peter Lammich **) theory LTL_to_GBA imports CAVA_Base.CAVA_Base LTL.LTL CAVA_Automata.Automata begin subsection \Statistics\ code_printing code_module Gerth_Statistics \ (SML) \ structure Gerth_Statistics = struct val active = Unsynchronized.ref false val data = Unsynchronized.ref (0,0,0) fun is_active () = !active fun set_data num_states num_init num_acc = ( active := true; data := (num_states, num_init, num_acc) ) fun to_string () = let val (num_states, num_init, num_acc) = !data in "Num states: " ^ IntInf.toString (num_states) ^ "\n" ^ " Num initial: " ^ IntInf.toString num_init ^ "\n" ^ " Num acc-classes: " ^ IntInf.toString num_acc ^ "\n" end val _ = Statistics.register_stat ("Gerth LTL_to_GBA",is_active,to_string) end \ code_reserved SML Gerth_Statistics consts stat_set_data_int :: "integer \ integer \ integer \ unit" code_printing constant stat_set_data_int \ (SML) "Gerth'_Statistics.set'_data" definition "stat_set_data ns ni na \ stat_set_data_int (integer_of_nat ns) (integer_of_nat ni) (integer_of_nat na)" lemma [autoref_rules]: "(stat_set_data,stat_set_data) \ nat_rel \ nat_rel \ nat_rel \ unit_rel" by auto abbreviation "stat_set_data_nres ns ni na \ RETURN (stat_set_data ns ni na)" lemma discard_stat_refine[refine]: "m1\m2 \ stat_set_data_nres ns ni na \ m1 \ m2" by simp_all subsection \Preliminaries\ text \Some very special lemmas for reasoning about the nres-monad\ lemma SPEC_rule_nested2: "\m \ SPEC P; \r1 r2. P (r1, r2) \ g (r1, r2) \ SPEC P\ \ m \ SPEC (\r'. g r' \ SPEC P)" by (simp add: pw_le_iff) blast lemma SPEC_rule_param2: assumes "f x \ SPEC (P x)" and "\r1 r2. (P x) (r1, r2) \ (P x') (r1, r2)" shows "f x \ SPEC (P x')" using assms by (simp add: pw_le_iff) lemma SPEC_rule_weak: assumes "f x \ SPEC (Q x)" and "f x \ SPEC (P x)" and "\r1 r2. \(Q x) (r1, r2); (P x) (r1, r2)\ \ (P x') (r1, r2)" shows "f x \ SPEC (P x')" using assms by (simp add: pw_le_iff) lemma SPEC_rule_weak_nested2: "\f \ SPEC Q; f \ SPEC P; \r1 r2. \Q (r1, r2); P (r1, r2)\ \ g (r1, r2) \ SPEC P\ \ f \ SPEC (\r'. g r' \ SPEC P)" by (simp add: pw_le_iff) blast subsection \Creation of States\ text \ In this section, the first part of the algorithm, which creates the states of the automaton, is formalized. \ (* FIXME: Abstraktion über node_name *) type_synonym node_name = nat type_synonym 'a frml = "'a ltlr" type_synonym 'a interprt = "'a set word" record 'a node = name :: node_name incoming :: "node_name set" new :: "'a frml set" old :: "'a frml set" "next" :: "'a frml set" context begin fun new1 where "new1 (\ and\<^sub>r \) = {\,\}" | "new1 (\ U\<^sub>r \) = {\}" | "new1 (\ R\<^sub>r \) = {\}" | "new1 (\ or\<^sub>r \) = {\}" | "new1 _ = {}" fun next1 where "next1 (X\<^sub>r \) = {\}" | "next1 (\ U\<^sub>r \) = {\ U\<^sub>r \}" | "next1 (\ R\<^sub>r \) = {\ R\<^sub>r \}" | "next1 _ = {}" fun new2 where "new2 (\ U\<^sub>r \) = {\}" | "new2 (\ R\<^sub>r \) = {\, \}" | "new2 (\ or\<^sub>r \) = {\}" | "new2 _ = {}" (* FIXME: Abstraction over concrete definition *) definition "expand_init \ 0" definition "expand_new_name \ Suc" lemma expand_new_name_expand_init: "expand_init < expand_new_name nm" by (auto simp add:expand_init_def expand_new_name_def) lemma expand_new_name_step[intro]: fixes n :: "'a node" shows "name n < expand_new_name (name n)" by (auto simp add:expand_new_name_def) lemma expand_new_name__less_zero[intro]: "0 < expand_new_name nm" proof - from expand_new_name_expand_init have "expand_init < expand_new_name nm" by auto then show ?thesis by (metis gr0I less_zeroE) qed abbreviation "upd_incoming_f n \ (\n'. if (old n' = old n \ next n' = next n) then n'\ incoming := incoming n \ incoming n' \ else n' )" definition "upd_incoming n ns \ ((upd_incoming_f n) ` ns)" lemma upd_incoming__elem: assumes "nd\upd_incoming n ns" shows "nd\ns \ (\nd'\ns. nd = nd'\ incoming := incoming n \ incoming nd' \ \ old nd' = old n \ next nd' = next n)" proof - obtain nd' where "nd'\ns" and nd_eq: "nd = upd_incoming_f n nd'" using assms unfolding upd_incoming_def by blast then show ?thesis by auto qed lemma upd_incoming__ident_node: assumes "nd\upd_incoming n ns" and "nd\ns" shows "incoming n \ incoming nd \ \ (old nd = old n \ next nd = next n)" proof (rule ccontr) assume "\ ?thesis" then have nsubset: "\ (incoming n \ incoming nd)" and old_next_eq: "old nd = old n \ next nd = next n" by auto moreover obtain nd' where "nd'\ns" and nd_eq: "nd = upd_incoming_f n nd'" using assms unfolding upd_incoming_def by blast { assume "old nd' = old n \ next nd' = next n" with nd_eq have "nd = nd'\incoming := incoming n \ incoming nd'\" by auto with nsubset have "False" by auto } moreover { assume "\ (old nd' = old n \ next nd' = next n)" with nd_eq old_next_eq have "False" by auto } ultimately show "False" by fast qed lemma upd_incoming__ident: assumes "\n\ns. P n" and "\n. \n\ns; P n\ \ (\v. P (n\ incoming := v \))" shows "\n\upd_incoming n ns. P n" proof fix nd v let ?f = "\n'. if (old n' = old n \ next n' = next n) then n'\ incoming := incoming n \ incoming n' \ else n'" assume "nd\upd_incoming n ns" then obtain nd' where "nd'\ns" and nd_eq: "nd = ?f nd'" unfolding upd_incoming_def by blast { assume "old nd' = old n \ next nd' = next n" then obtain v where "nd = nd'\ incoming := v \" using nd_eq by auto with assms \nd'\ns\ have "P nd" by auto } then show "P nd" using nd_eq \nd'\ns\ assms by auto qed lemma name_upd_incoming_f[simp]: "name (upd_incoming_f n x) = name x" by auto lemma name_upd_incoming[simp]: "name ` (upd_incoming n ns) = name ` ns" (is "?lhs = ?rhs") unfolding upd_incoming_def proof safe fix x assume "x\ns" then have "upd_incoming_f n x \ (\n'. local.upd_incoming_f n n') ` ns" by auto then have "name (upd_incoming_f n x) \ name ` (\n'. local.upd_incoming_f n n') ` ns" by blast then show "name x \ name ` (\n'. local.upd_incoming_f n n') ` ns" by simp qed auto abbreviation expand_body where "expand_body \ (\expand (n,ns). if new n = {} then ( if (\n'\ns. old n' = old n \ next n' = next n) then RETURN (name n, upd_incoming n ns) else expand ( \ name=expand_new_name (name n), incoming={name n}, new=next n, old={}, next={} \, {n} \ ns) ) else do { \ \ SPEC (\x. x\(new n)); let n = n\ new := new n - {\} \; if (\q. \ = prop\<^sub>r(q) \ \ = nprop\<^sub>r(q)) then (if (not\<^sub>r \) \ old n then RETURN (name n, ns) else expand (n\ old := {\} \ old n \, ns)) else if \ = true\<^sub>r then expand (n\ old := {\} \ old n \, ns) else if \ = false\<^sub>r then RETURN (name n, ns) else if (\\ \. (\ = \ and\<^sub>r \) \ (\ = X\<^sub>r \)) then expand ( n\ new := new1 \ \ new n, old := {\} \ old n, next := next1 \ \ next n \, ns) else do { (nm, nds) \ expand ( n\ new := new1 \ \ new n, old := {\} \ old n, next := next1 \ \ next n \, ns); expand (n\ name := nm, new := new2 \ \ new n, old := {\} \ old n \, nds) } } )" lemma expand_body_mono: "trimono expand_body" by refine_mono definition expand :: "('a node \ ('a node set)) \ (node_name \ 'a node set) nres" where "expand \ REC expand_body" lemma REC_rule_old: (* TODO: Adapt proofs below, have fun with subgoal 27 ...*) fixes x::"'x" assumes M: "trimono body" assumes I0: "\ x" assumes IS: "\f x. \ \x. \ x \ f x \ M x; \ x; f \ REC body \ \ body f x \ M x" shows "REC body x \ M x" by (rule REC_rule_arb[where pre="\_. \" and M="\_. M", OF assms]) lemma expand_rec_rule: assumes I0: "\ x" assumes IS: "\f x. \ \x. f x \ expand x; \x. \ x \ f x \ M x; \ x \ \ expand_body f x \ M x" shows "expand x \ M x" unfolding expand_def apply (rule REC_rule_old[where \="\"]) apply (rule expand_body_mono) apply (rule I0) apply (rule IS[unfolded expand_def]) apply (blast dest: le_funD) apply blast apply blast done abbreviation "expand_assm_incoming n_ns \ (\nm\incoming (fst n_ns). name (fst n_ns) > nm) \ 0 < name (fst n_ns) \ (\q\snd n_ns. name (fst n_ns) > name q \ (\nm\incoming q. name (fst n_ns) > nm))" abbreviation "expand_rslt_incoming nm_nds \ (\q\snd nm_nds. (fst nm_nds > name q \ (\nm'\incoming q. fst nm_nds > nm')))" abbreviation "expand_rslt_name n_ns nm_nds \ (name (fst n_ns) \ fst nm_nds \ name ` (snd n_ns) \ name ` (snd nm_nds)) \ name ` (snd nm_nds) = name ` (snd n_ns) \ name ` {nd\snd nm_nds. name nd \ name (fst n_ns)}" abbreviation "expand_name_ident nds \ (\q\nds. \!q'\nds. name q = name q')" abbreviation "expand_assm_exist \ n_ns \ {\. \\. \ U\<^sub>r \ \ old (fst n_ns) \ \ \\<^sub>r \} \ new (fst n_ns) \ old (fst n_ns) \ (\\\new (fst n_ns). \ \\<^sub>r \) \ (\\\old (fst n_ns). \ \\<^sub>r \) \ (\\\next (fst n_ns). \ \\<^sub>r X\<^sub>r \)" abbreviation "expand_rslt_exist__node_prop \ n nd \ incoming n \ incoming nd \ (\\\old nd. \ \\<^sub>r \) \ (\\\next nd. \ \\<^sub>r X\<^sub>r \) \ {\. \\. \ U\<^sub>r \ \ old nd \ \ \\<^sub>r \} \ old nd" abbreviation "expand_rslt_exist \ n_ns nm_nds \ (\nd\snd nm_nds. expand_rslt_exist__node_prop \ (fst n_ns) nd)" abbreviation "expand_rslt_exist_eq__node n nd \ name n = name nd \ old n = old nd \ next n = next nd \ incoming n \ incoming nd" abbreviation "expand_rslt_exist_eq n_ns nm_nds \ (\n\snd n_ns. \nd\snd nm_nds. expand_rslt_exist_eq__node n nd)" lemma expand_name_propag: assumes "expand_assm_incoming n_ns \ expand_name_ident (snd n_ns)" (is "?Q n_ns") shows "expand n_ns \ SPEC (\r. expand_rslt_incoming r \ expand_rslt_name n_ns r \ expand_name_ident (snd r))" (is "expand _ \ SPEC (?P n_ns)") using assms proof (rule_tac expand_rec_rule[where \="?Q"], simp, intro refine_vcg, goal_cases) case prems: (1 _ _ n ns) then have Q: "?Q (n, ns)" by fast let ?nds = "upd_incoming n ns" from prems have "\q\?nds. name q < name n" by (rule_tac upd_incoming__ident) auto moreover have "\q\?nds. \nm'\incoming q. nm' < name n" (is "\q\_. ?sg q") proof fix q assume q_in:"q\?nds" show "?sg q" proof (cases "q\ns") case True with prems show ?thesis by auto next case False with upd_incoming__elem[OF q_in] obtain nd' where nd'_def:"nd'\ns \ q = nd'\incoming := incoming n \ incoming nd'\" by blast { fix nm' assume "nm'\incoming q" moreover { assume "nm'\incoming n" with Q have "nm' < name n" by auto } moreover { assume "nm'\incoming nd'" with Q nd'_def have "nm' < name n" by auto } ultimately have "nm' < name n" using nd'_def by auto } then show ?thesis by fast qed qed moreover have "expand_name_ident ?nds" proof (rule upd_incoming__ident, goal_cases) case 1 show ?case proof fix q assume "q\ns" with Q have "\!q'\ns. name q = name q'" by auto then obtain q' where "q'\ns" and "name q = name q'" and q'_all: "\q''\ns. name q' = name q'' \ q' = q''" by auto let ?q' = "upd_incoming_f n q'" have P_a: "?q'\?nds \ name q = name ?q'" using \q'\ns\ \name q = name q'\ q'_all unfolding upd_incoming_def by auto have P_all: "\q''\?nds. name ?q' = name q'' \ ?q' = q''" proof(clarify) fix q'' assume "q''\?nds" and q''_name_eq: "name ?q' = name q''" { assume "q''\ns" with upd_incoming__elem[OF \q''\?nds\] obtain nd'' where "nd''\ns" and q''_is: "q'' = nd''\incoming := incoming n \ incoming nd''\ \ old nd'' = old n \ next nd'' = next n" by auto then have "name nd'' = name q'" using q''_name_eq by (cases "old q' = old n \ next q' = next n") auto with \nd''\ns\ q'_all have "nd'' = q'" by auto then have "?q' = q''" using q''_is by simp } moreover { assume "q''\ns" moreover have "name q' = name q''" using q''_name_eq by (cases "old q' = old n \ next q' = next n") auto moreover then have "incoming n \ incoming q'' \ incoming q'' = incoming n \ incoming q''" by auto ultimately have "?q' = q''" using upd_incoming__ident_node[OF \q''\?nds\] q'_all by auto } ultimately show "?q' = q''" by fast qed show "\!q'\upd_incoming n ns. name q = name q'" proof(rule ex1I[of _ ?q'], goal_cases) case 1 then show ?case using P_a by simp next case 2 then show ?case using P_all unfolding P_a[THEN conjunct2, THEN sym] by blast qed qed qed simp ultimately show ?case using prems by auto next case prems: (2 f x n ns) then have step: "\x. ?Q x \ f x \ SPEC (?P x)" by simp from prems have Q: "?Q (n, ns)" by auto show ?case unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_param2[where P = "?P"], rule_tac step, goal_cases) case 1 with expand_new_name_step[of n] show ?case using Q by (auto elim: order_less_trans[rotated]) next case prems': (2 _ nds) then have "name ` ns \ name ` nds" by auto with expand_new_name_step[of n] show ?case using prems' by auto qed next case 3 then show ?case by auto next case prems: (4 f) then have step: "\x. ?Q x \ f x \ SPEC (?P x)" by simp_all with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (5 f) then have step: "\x. ?Q x \ f x \ SPEC (?P x)" by simp_all from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case 6 then show ?case by auto next case prems: (7 f) then have step: "\x. ?Q x \ f x \ SPEC (?P x)" by simp_all from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have Q: "?Q (n, ns)" and step: "\x. ?Q x \ f x \ SPEC (?P x)" by simp_all show ?case using goal_assms Q unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_nested2, goal_cases) case 1 then show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (2 nm nds) then have P_x: "(name n \ nm \ name ` ns \ name ` nds) \ name ` nds = name ` ns \ name ` {nd\nds. name nd \ name n}" (is "_ \ ?nodes_eq nds ns (name n)") by auto show ?case proof (rule_tac SPEC_rule_param2[where P = "?P"], goal_cases) case 1 with prems show ?case by (rule_tac step) auto next case prems': (2 nm' nds') then have "\q\nds'. name q < nm' \ (\nm''\incoming q. nm'' < nm')" by auto moreover have "?nodes_eq nds ns (name n)" and "?nodes_eq nds' nds nm" and "name n \ nm" using prems' P_x by auto then have "?nodes_eq nds' ns (name n)" by auto then have "expand_rslt_name (n, ns) (nm', nds')" using prems' P_x subset_trans[of "name ` ns" "name ` nds"] by auto ultimately show ?case using prems' by auto qed qed qed lemmas expand_name_propag__incoming = SPEC_rule_conjunct1[OF expand_name_propag] lemmas expand_name_propag__name = SPEC_rule_conjunct1[OF SPEC_rule_conjunct2[OF expand_name_propag]] lemmas expand_name_propag__name_ident = SPEC_rule_conjunct2[OF SPEC_rule_conjunct2[OF expand_name_propag]] lemma expand_rslt_exist_eq: shows "expand n_ns \ SPEC (expand_rslt_exist_eq n_ns)" (is "_ \ SPEC (?P n_ns)") proof (rule_tac expand_rec_rule[where \="\_. True"], simp, intro refine_vcg, goal_cases) case prems: (1 f x n ns) let ?r = "(name n, upd_incoming n ns)" have "expand_rslt_exist_eq (n, ns) ?r" unfolding snd_conv proof fix n' assume "n'\ns" { assume "old n' = old n \ next n' = next n" with \n'\ns\ have "n'\ incoming := incoming n \ incoming n' \ \ upd_incoming n ns" unfolding upd_incoming_def by auto } moreover { assume "\ (old n' = old n \ next n' = next n)" with \n'\ns\ have "n' \ upd_incoming n ns" unfolding upd_incoming_def by auto } ultimately show "\nd\upd_incoming n ns. expand_rslt_exist_eq__node n' nd" by force qed with prems show ?case by auto next case prems: (2 f) then have step: "\x. f x \ SPEC (?P x)" by simp with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case 3 then show ?case by auto next case prems: (4 f) then have step: "\x. f x \ SPEC (?P x)" by simp with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (5 f) then have step: "\x. f x \ SPEC (?P x)" by simp with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case 6 then show ?case by auto next case prems: (7 f) then have step: "\x. f x \ SPEC (?P x)" by simp with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (8 f x n ns) then have step: "\x. f x \ SPEC (?P x)" by simp show ?case proof (rule_tac SPEC_rule_nested2, goal_cases) case 1 with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case (2 nm nds) with prems have P_x: "?P (n, ns) (nm, nds)" by fast show ?case unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_param2[where P = "?P"], goal_cases) case 1 then show ?case by (rule_tac step) next case prems': (2 nm' nds') { fix n' assume "n'\ns" with P_x obtain nd where "nd\nds" and n'_split: "expand_rslt_exist_eq__node n' nd" by auto with prems' obtain nd' where "nd'\nds'" and "expand_rslt_exist_eq__node nd nd'" by auto then have "\nd'\nds'. expand_rslt_exist_eq__node n' nd'" using n'_split subset_trans[of "incoming n'"] by auto } then have "expand_rslt_exist_eq (n, ns) (nm', nds')" by auto with prems show ?case by auto qed qed qed lemma expand_prop_exist: "expand n_ns \ SPEC (\r. expand_assm_exist \ n_ns \ expand_rslt_exist \ n_ns r)" (is "_ \ SPEC (?P n_ns)") proof (rule_tac expand_rec_rule[where \="\_. True"], simp, intro refine_vcg, goal_cases) case prems: (1 f x n ns) let ?nds = "upd_incoming n ns" let ?r = "(name n, ?nds)" { assume Q: "expand_assm_exist \ (n, ns)" note \\n'\ns. old n' = old n \ next n' = next n\ then obtain n' where "n'\ns" and assm_eq: "old n' = old n \ next n' = next n" by auto let ?nd = "n'\ incoming := incoming n \ incoming n'\" have "?nd \ ?nds" using \n'\ns\ assm_eq unfolding upd_incoming_def by auto moreover have "incoming n \ incoming ?nd" by auto moreover have "expand_rslt_exist__node_prop \ n ?nd" using Q assm_eq \new n = {}\ by simp ultimately have "expand_rslt_exist \ (n, ns) ?r" unfolding fst_conv snd_conv by blast } with prems show ?case by auto next case prems: (2 f x n ns) then have step: "\x. f x \ SPEC (?P x)" and f_sup: "\x. f x \ expand x" by auto show ?case unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_weak[where Q = "expand_rslt_exist_eq"], goal_cases) case 1 then show ?case by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq) next case 2 then show ?case by (rule_tac step) next case prems': (3 nm nds) then have "name ` ns \ name ` nds" by auto moreover { assume assm_ex: "expand_assm_exist \ (n, ns)" with prems' obtain nd where "nd\nds" and "expand_rslt_exist_eq__node n nd" by force+ then have "expand_rslt_exist__node_prop \ n nd" using assm_ex \new n = {}\ by auto then have "expand_rslt_exist \ (n, ns) (nm, nds)" using \nd\nds\ by auto } ultimately show ?case using expand_new_name_step[of n] prems' by auto qed next case prems: (3 f x n ns \) { assume "expand_assm_exist \ (n, ns)" with prems have "\ \\<^sub>r \" and "\ \\<^sub>r not\<^sub>r \" by (metis (no_types, lifting) fstI node.select_convs(4) node.surjective node.update_convs(3))+ then have False by simp } with prems show ?case by auto next case prems: (4 f x n ns \) then have goal_assms: "\ \ new n \ (\q. \ = prop\<^sub>r(q) \ \ = nprop\<^sub>r(q))" and step: "\x. f x \ SPEC (?P x)" by simp_all show ?case using goal_assms unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases) case prems': (1 nm nds) { assume "expand_assm_exist \ (n, ns)" with prems' have "expand_rslt_exist \ (n, ns) (nm, nds)" by auto } then show ?case by auto qed next case prems: (5 f x n ns \) then have goal_assms: "\ \ new n \ \ = true\<^sub>r" and step: "\x. f x \ SPEC (?P x)" by simp_all show ?case using goal_assms unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases) case prems': (1 nm nds) { assume "expand_assm_exist \ (n, ns)" with prems' have "expand_rslt_exist \ (n, ns) (nm, nds)" by auto } then show ?case by auto qed next case prems: (6 f x n ns \) { assume "expand_assm_exist \ (n, ns)" with prems have "\ \\<^sub>r false\<^sub>r" by auto } with prems show ?case by auto next case prems: (7 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ and\<^sub>r \ \ \ = X\<^sub>r \)" and step: "\x. f x \ SPEC (?P x)" by simp_all show ?case using goal_assms unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases) case prems': (1 nm nds) { assume "expand_assm_exist \ (n, ns)" with prems' have "expand_rslt_exist \ (n, ns) (nm, nds)" by auto } then show ?case by auto qed next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have step: "\x. f x \ SPEC (?P x)" and f_sup: "\x. f x \ expand x" by auto let ?x1 = "(n\new := new n - {\}, new := new1 \ \ new (n\new := new n - {\}\), old := {\} \ old n, next := next1 \ \ next n\, ns)" let ?new1_assm_sel = "\\. (case \ of \ U\<^sub>r \ => \ | \ R\<^sub>r \ \ \ | \ or\<^sub>r \ \ \)" { assume new1_assm: "\ (\ \\<^sub>r (?new1_assm_sel \))" then have ?case using goal_assms unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_nested2, goal_cases) case prems': 1 then show ?case proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases) case prems'': (1 nm nds) { assume "expand_assm_exist \ (n, ns)" with prems'' have "expand_assm_exist \ ?x1" unfolding fst_conv proof (cases \, goal_cases) case \: (8 \ \) then have "\ \\<^sub>r \ U\<^sub>r \" by fast then have "\ \\<^sub>r \" and "\ \\<^sub>r X\<^sub>r (\ U\<^sub>r \)" using \ ltlr_expand_Until[of \ \ \] by auto with \ show ?case by auto next case \: (9 \ \) then have *: "\ \\<^sub>r \ R\<^sub>r \" by fast with \ have "\ \\<^sub>r \" and "\ \\<^sub>r X\<^sub>r (\ R\<^sub>r \)" using ltlr_expand_Release[of \ \ \] by auto with \ * show ?case by auto qed auto with prems'' have "expand_rslt_exist \ (n, ns) (nm, nds)" by force } with prems'' show ?case by auto qed next case prems': (2 nm nds) then have P_x: "?P (n, ns) (nm, nds)" by fast show ?case unfolding case_prod_unfold proof (rule_tac SPEC_rule_weak[where P = "?P" and Q = "expand_rslt_exist_eq"], goal_cases) case 1 then show ?case by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq) next case 2 then show ?case by (rule_tac step) next case prems'': (3 nm' nds') { assume "expand_assm_exist \ (n, ns)" with P_x have "expand_rslt_exist \ (n, ns) (nm, nds)" by simp then obtain nd where nd: "nd\nds" "expand_rslt_exist__node_prop \ n nd" using goal_assms by auto with prems'' obtain nd' where "nd'\nds'" and "expand_rslt_exist_eq__node nd nd'" by force with nd have "expand_rslt_exist__node_prop \ n nd'" using subset_trans[of "incoming n" "incoming nd"] by auto then have "expand_rslt_exist \ (n,ns) (nm', nds')" using \nd'\nds'\ goal_assms by auto } then show ?case by fast qed qed } moreover { assume new1_assm: "\ \\<^sub>r (?new1_assm_sel \)" let ?x2f = "\(nm::node_name, nds::'a node set). ( n\new := new n - {\}, name := nm, new := new2 \ \ new (n\new := new n - {\}\), old := {\} \ old n\, nds)" have P_x: "f ?x1 \ SPEC (?P ?x1)" by (rule step) moreover { fix r :: "node_name \ 'a node set" let ?x2 = "?x2f r" assume assm: "(?P ?x1) r" have "f ?x2 \ SPEC (?P (n, ns))" unfolding case_prod_unfold fst_conv proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases) case prems': (1 nm' nds') { assume "expand_assm_exist \ (n, ns)" with new1_assm goal_assms have "expand_assm_exist \ ?x2" proof (cases r, cases \, goal_cases) case prems'': (9 _ _ \ \) then have *: "\ \\<^sub>r \ R\<^sub>r \" unfolding fst_conv by fast with ltlr_expand_Release[of \ \ \] have "\ \\<^sub>r \" by auto with prems'' * show ?case by auto qed auto with prems' have "expand_rslt_exist \ ?x2 (nm', nds')" unfolding case_prod_unfold fst_conv snd_conv by fast then have "expand_rslt_exist \ (n, ns) (nm', nds')" by (cases r, auto) } then show ?case by simp qed } then have "SPEC (?P ?x1) \ SPEC (\r. (case r of (nm, nds) => f (?x2f (nm, nds))) \ SPEC (?P (n, ns)))" using goal_assms by (rule_tac SPEC_rule) force finally have ?case unfolding case_prod_unfold \x = (n, ns)\ by simp } ultimately show ?case by fast qed text \Termination proof\ definition expand\<^sub>T :: "('a node \ ('a node set)) \ (node_name \ 'a node set) nres" where "expand\<^sub>T n_ns \ REC\<^sub>T expand_body n_ns" abbreviation "old_next_pair n \ (old n, next n)" abbreviation "old_next_limit \ \ Pow (subfrmlsr \) \ Pow (subfrmlsr \)" lemma old_next_limit_finite: "finite (old_next_limit \)" using subfrmlsr_finite by auto definition "expand_ord \ \ inv_image (finite_psupset (old_next_limit \) <*lex*> less_than) (\(n, ns). (old_next_pair ` ns, size_set (new n)))" lemma expand_ord_wf[simp]: "wf (expand_ord \)" using finite_psupset_wf[OF old_next_limit_finite] unfolding expand_ord_def by auto abbreviation "expand_inv_node \ n \ finite (new n) \ finite (old n) \ finite (next n) \ (new n) \ (old n) \ (next n) \ subfrmlsr \" abbreviation "expand_inv_result \ ns \ finite ns \ (\n'\ns. (new n') \ (old n') \ (next n') \ subfrmlsr \)" definition "expand_inv \ n_ns \ (case n_ns of (n, ns) \ expand_inv_node \ n \ expand_inv_result \ ns)" lemma new1_less_sum: "size_set (new1 \) < size_set {\}" proof (cases \) case (And_ltlr \ \) thus ?thesis by (cases "\ = \"; simp) qed (simp_all) lemma new2_less_sum: "size_set (new2 \) < size_set {\}" proof (cases \) case (Release_ltlr \ \) thus ?thesis by (cases "\ = \"; simp) qed (simp_all) lemma new1_finite[intro]: "finite (new1 \)" by (cases \) auto lemma new1_subset_frmls: "\ \ new1 \ \ \ \ subfrmlsr \" by (cases \) auto lemma new2_finite[intro]: "finite (new2 \)" by (cases \) auto lemma new2_subset_frmls: "\ \ new2 \ \ \ \ subfrmlsr \" by (cases \) auto lemma next1_finite[intro]: "finite (next1 \)" by (cases \) auto lemma next1_subset_frmls: "\ \ next1 \ \ \ \ subfrmlsr \" by (cases \) auto +text \Expanding the new-style lexorder\ +lemma expand_ord_iff: "((a,b),(c,d)) \ expand_ord \ + \ ((old_next_pair ` b, old_next_pair ` d) \ finite_psupset (old_next_limit \) + \ old_next_pair ` b = old_next_pair ` d \ (\x\new a. Suc (2 * size x)) < (\x\new c. Suc (2 * size x)))" +apply (simp add: expand_ord_def) + apply (auto simp: finite_psupset_def) + apply (metis (mono_tags, lifting) image_iff)+ + done + lemma expand_inv_impl[intro!]: assumes "expand_inv \ (n, ns)" and newn: "\ \ new n" and "old_next_pair ` ns \ old_next_pair ` ns'" and "expand_inv_result \ ns'" and "(n' = n\ new := new n - {\}, old := {\} \ old n \) \ (n' = n\ new := new1 \ \ (new n - {\}), old := {\} \ old n, next := next1 \ \ next n \) \ (n' = n\ name := nm, new := new2 \ \ (new n - {\}), old := {\} \ old n \)" (is "?case1 \ ?case2 \ ?case3") shows "((n', ns'), (n, ns))\expand_ord \ \ expand_inv \ (n', ns')" (is "?concl1 \ ?concl2") proof from assms consider ?case1 | ?case2 | ?case3 by blast then show ?concl1 proof cases case n'def: 1 with assms show ?thesis - unfolding expand_ord_def expand_inv_def finite_psupset_def + unfolding expand_ord_iff expand_inv_def finite_psupset_def apply (cases "old_next_pair ` ns \ old_next_pair ` ns'") - apply simp_all - apply auto [1] - apply (metis (no_types, lifting) add_Suc diff_Suc_less psubsetI sum.remove sum_diff1_nat zero_less_Suc) + apply (simp_all add: psubset_eq) + apply blast + apply (metis (no_types, lifting) add_Suc diff_Suc_less sum.remove sum_diff1_nat zero_less_Suc) done next case n'def: 2 have \innew: "\ \ new n" and fin_new: "finite (new n)" using assms unfolding expand_inv_def by auto then have "size_set (new n - {\}) = size_set (new n) - size_set {\}" using size_set_diff by fastforce moreover from fin_new sum_Un_nat[OF new1_finite _, of "new n - {\}" size \] have "size_set (new n') \ size_set (new1 \) + size_set (new n - {\})" unfolding n'def by (simp add: new1_finite sum_Un_nat) moreover have sum_leq: "size_set (new n) \ size_set {\}" using \innew sum_mono2[OF fin_new, of "{\}"] by blast ultimately have "size_set (new n') < size_set (new n)" using new1_less_sum[of \] by auto with assms show ?thesis - unfolding expand_ord_def finite_psupset_def by auto + unfolding expand_ord_iff finite_psupset_def by auto next case n'def: 3 have \innew: "\ \ new n" and fin_new: "finite (new n)" using assms unfolding expand_inv_def by auto from \innew sum_diff1_nat[of size "new n" \] have "size_set (new n - {\}) = size_set (new n) - size_set {\}" using size_set_diff[of "new n" "{\}"] by fastforce moreover from fin_new sum_Un_nat[OF new2_finite _, of "new n - {\}" size \] have "size_set (new n') \ size_set (new2 \) + size_set (new n - {\})" unfolding n'def by (simp add: new2_finite sum_Un_nat) moreover have sum_leq:"size_set (new n) \ size_set {\}" using \innew sum_mono2[OF fin_new, of "{\}"] by blast ultimately have "size_set (new n') < size_set (new n)" using new2_less_sum[of \] sum_leq by auto with assms show ?thesis - unfolding expand_ord_def finite_psupset_def by auto + unfolding expand_ord_iff finite_psupset_def by auto qed next have "new1 \ \ subfrmlsr \" and "new2 \ \ subfrmlsr \" and "next1 \ \ subfrmlsr \" using assms subfrmlsr_subset[OF new1_subset_frmls[of _ \]] subfrmlsr_subset[of \ \, OF rev_subsetD[of _ "new n"]] subfrmlsr_subset[OF new2_subset_frmls[of _ \]] subfrmlsr_subset[OF next1_subset_frmls[of _ \]] unfolding expand_inv_def (* This proof is merely a speed optimization. A single force+ does the job, but takes very long *) apply - apply (clarsimp split: prod.splits) apply (metis in_mono new1_subset_frmls) apply (clarsimp split: prod.splits) apply (metis new2_subset_frmls rev_subsetD) apply (clarsimp split: prod.splits) apply (metis in_mono next1_subset_frmls) done with assms show ?concl2 unfolding expand_inv_def by auto qed lemma expand_term_prop_help: assumes "((n', ns'), (n, ns))\expand_ord \ \ expand_inv \ (n', ns')" and assm_rule: "\expand_inv \ (n', ns'); ((n', ns'), n, ns) \ expand_ord \\ \ f (n', ns') \ SPEC P" shows "f (n', ns') \ SPEC P" using assms by (rule_tac assm_rule) auto lemma expand_inv_upd_incoming: assumes "expand_inv \ (n, ns)" shows "expand_inv_result \ (upd_incoming n ns)" using assms unfolding expand_inv_def upd_incoming_def by force lemma upd_incoming_eq_old_next_pair: "old_next_pair ` ns = old_next_pair ` (upd_incoming n ns)" (is "?A = ?B") proof show "?A \ ?B" proof fix x let ?f = "\n'. n'\incoming := incoming n \ incoming n'\" assume "x \ ?A" then obtain n' where "n' \ ns" and xeq: "x = (old n', next n')" by auto have "x \ (old_next_pair ` (\n'. n'\incoming := incoming n \ incoming n'\) ` (ns \ {n' \ ns. old n' = old n \ next n' = next n})) \ (old_next_pair ` (ns \ {n' \ ns. old n' \ old n \ next n' \ next n}))" proof (cases "old n' = old n \ next n' = next n") case True with \n' \ ns\ have "?f n' \ ?f ` (ns \ {n'\ns. old n' = old n \ next n' = next n})" (is "_ \ ?C") by auto then have "old_next_pair (?f n') \ old_next_pair ` ?C" by (rule_tac imageI) auto with xeq have "x\old_next_pair ` ?C" by auto then show ?thesis by blast next case False with \n' \ ns\ xeq have "x \ old_next_pair ` (ns \ {n'\ns. old n' \ old n \ next n' \ next n})" by auto then show ?thesis by blast qed then show "x \ ?B" using \x \ ?A\ unfolding upd_incoming_def by auto qed show "?B \ ?A" unfolding upd_incoming_def by (force intro:imageI) qed lemma expand_term_prop: "expand_inv \ n_ns \ expand\<^sub>T n_ns \ SPEC (\(_, nds). old_next_pair ` snd n_ns\old_next_pair `nds \ expand_inv_result \ nds)" (is "_ \ _ \ SPEC (?P n_ns)") unfolding expand\<^sub>T_def apply (rule_tac RECT_rule[where pre="\(n, ns). expand_inv \ (n, ns)" and V="expand_ord \"]) apply (refine_mono) apply simp apply simp proof (intro refine_vcg, goal_cases) case prems: (1 _ _ n ns) have "old_next_pair ` ns \ old_next_pair ` (upd_incoming n ns)" by (rule equalityD1[OF upd_incoming_eq_old_next_pair]) with prems show ?case using expand_inv_upd_incoming[of \ n ns] by auto next case prems: (2 expand x n ns) let ?n' = "\ name = expand_new_name (name n), incoming = {name n}, new = next n, old = {}, next = {}\" let ?ns' = "{n} \ ns" from prems have SPEC_sub:"SPEC (?P (?n', ?ns')) \ SPEC (?P x)" by (rule_tac SPEC_rule) auto from prems have "old_next_pair n \ old_next_pair ` ns" by auto then have "old_next_pair ` ns \ old_next_pair ` (insert n ns)" by auto moreover from prems have "expand_inv \ (n, ns)" by simp ultimately have "((?n', ?ns'), (n, ns)) \ expand_ord \" - by (auto simp add: expand_ord_def finite_psupset_def expand_inv_def) + by (auto simp add: expand_ord_iff finite_psupset_def expand_inv_def) moreover from prems have "expand_inv \ (?n', ?ns')" unfolding expand_inv_def by auto ultimately have "expand (?n', ?ns') \ SPEC (?P (?n', ?ns'))" using prems by fast with SPEC_sub show ?case by (rule_tac order_trans) fast+ next case 3 then show ?case by (auto simp add:expand_inv_def) next case 4 then show ?case apply (rule_tac expand_term_prop_help[OF expand_inv_impl]) apply (simp add: expand_inv_def)+ apply force done next case 5 then show ?case apply (rule_tac expand_term_prop_help[OF expand_inv_impl]) apply (simp add: expand_inv_def)+ apply force done next case 6 then show ?case by (simp add: expand_inv_def) next case 7 then show ?case apply (rule_tac expand_term_prop_help[OF expand_inv_impl]) apply (simp add: expand_inv_def)+ apply force done next case prems: (8 f x a b xa) let ?n' = "a\ new := new1 xa \ (new a - {xa}), old := insert xa (old a), next := next1 xa \ next a\" let ?n'' = "\nm. a\ name := nm, new := new2 xa \ (new a - {xa}), old := insert xa (old a)\" have step:"((?n', b), (a, b)) \ expand_ord \ \ expand_inv \ (?n', b)" using prems by (rule_tac expand_inv_impl) (auto simp add: expand_inv_def) with prems have assm1: "f (?n', b) \ SPEC (?P (a, b))" by auto moreover { fix nm::node_name and nds::"'a node set" assume assm1: "old_next_pair ` b \ old_next_pair ` nds" and assm2: "expand_inv_result \ nds" with prems step have "((?n'' nm, nds), (a, b)) \ expand_ord \ \ expand_inv \ (?n'' nm, nds)" by (rule_tac expand_inv_impl) auto with prems have "f (?n'' nm, nds) \ SPEC (?P (?n'' nm, nds))" by auto moreover have "SPEC (?P (?n'' nm, nds)) \ SPEC (?P (a, b))" using assm2 subset_trans[OF assm1] by auto ultimately have "f (?n'' nm, nds) \ SPEC (?P (a, b))" by (rule order_trans) } then have assm2: "SPEC (?P (a, b)) \ SPEC (\r. (case r of (nm, nds) \ f (?n'' nm, nds)) \ SPEC (?P (a, b)))" by (rule_tac SPEC_rule) auto from prems order_trans[OF assm1 assm2] show ?case by auto qed lemma expand_eq_expand\<^sub>T: assumes inv: "expand_inv \ n_ns" shows "expand\<^sub>T n_ns = expand n_ns" unfolding expand\<^sub>T_def expand_def apply (rule RECT_eq_REC) unfolding expand\<^sub>T_def[symmetric] using expand_term_prop[OF inv] apply auto done lemma expand_nofail: assumes inv: "expand_inv \ n_ns" shows "nofail (expand\<^sub>T n_ns)" using expand_term_prop[OF inv] by (simp add: pw_le_iff) lemma [intro!]: "expand_inv \ ( \ name = expand_new_name expand_init, incoming = {expand_init}, new = {\}, old = {}, next = {} \, {})" by (auto simp add: expand_inv_def) definition create_graph :: "'a frml \ 'a node set nres" where "create_graph \ \ do { (_, nds) \ expand ( \ name = expand_new_name expand_init, incoming = {expand_init}, new = {\}, old = {}, next = {} \::'a node, {}::'a node set); RETURN nds }" (* "expand_eq_expand\<^sub>T" *) definition create_graph\<^sub>T :: "'a frml \ 'a node set nres" where "create_graph\<^sub>T \ \ do { (_, nds) \ expand\<^sub>T ( \ name = expand_new_name expand_init, incoming = {expand_init}, new = {\}, old = {}, next = {} \::'a node, {}::'a node set); RETURN nds }" lemma create_graph_eq_create_graph\<^sub>T: "create_graph \ = create_graph\<^sub>T \" unfolding create_graph\<^sub>T_def create_graph_def unfolding eq_iff proof (standard, goal_cases) case 1 then show ?case by refine_mono (unfold expand_def expand\<^sub>T_def, rule REC_le_RECT) next case 2 then show ?case by (refine_mono, rule expand_eq_expand\<^sub>T[unfolded eq_iff, THEN conjunct1]) auto qed lemma create_graph_finite: "create_graph \ \ SPEC finite" unfolding create_graph_def expand_def apply (intro refine_vcg) apply (rule_tac order_trans) apply (rule_tac REC_le_RECT) apply (fold expand\<^sub>T_def) apply (rule_tac order_trans[OF expand_term_prop]) apply auto[1] apply (rule_tac SPEC_rule) apply auto done lemma create_graph_nofail: "nofail (create_graph \)" by (rule_tac pwD1[OF create_graph_finite]) auto abbreviation "create_graph_rslt_exist \ nds \ \nd\nds. expand_init\incoming nd \ (\\\old nd. \ \\<^sub>r \) \ (\\\next nd. \ \\<^sub>r X\<^sub>r \) \ {\. \\. \ U\<^sub>r \ \ old nd \ \ \\<^sub>r \} \ old nd" lemma L4_7: assumes "\ \\<^sub>r \" shows "create_graph \ \ SPEC (create_graph_rslt_exist \)" using assms unfolding create_graph_def by (intro refine_vcg, rule_tac order_trans, rule_tac expand_prop_exist) ( auto simp add:expand_new_name_expand_init) lemma expand_incoming_name_exist: assumes "name (fst n_ns) > expand_init \ (\nm\incoming (fst n_ns). nm \ expand_init \ nm\name ` (snd n_ns)) \ expand_assm_incoming n_ns \ expand_name_ident (snd n_ns)" (is "?Q n_ns") and "\nd\snd n_ns. name nd > expand_init \ (\nm\incoming nd. nm \ expand_init \ nm\name ` (snd n_ns))" (is "?P (snd n_ns)") shows "expand n_ns \ SPEC (\nm_nds. ?P (snd nm_nds))" using assms apply (rule_tac expand_rec_rule[where \="\n_ns. ?Q n_ns \ ?P (snd n_ns)"]) apply simp apply (intro refine_vcg) proof goal_cases case (1 f x n ns) then show ?case proof (simp, clarify, goal_cases) case prems: (1 _ _ nd) { assume "nd\ns" with prems have ?case by auto } moreover { assume "nd\ns" with upd_incoming__elem[OF \nd\upd_incoming n ns\] obtain nd' where "nd'\ns" and "nd = nd'\incoming := incoming n \ incoming nd'\ \ old nd' = old n \ next nd' = next n" by auto with prems have ?case by auto } ultimately show ?case by fast qed next case (2 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x. ?P (snd x))" and QP: "?Q (n, ns) \ ?P ns" and f_sup: "\x. f x \ expand x" by auto show ?case unfolding \x = (n, ns)\ using QP expand_new_name_expand_init proof (rule_tac step, goal_cases) case prems: 1 then have name_less: "name n < expand_new_name (name n)" by auto moreover from prems name_less have "\nm\incoming n. nm < expand_new_name (name n)" by auto moreover from prems name_less have **: "\q\ns. name q < expand_new_name (name n) \ (\nm\incoming q. nm < expand_new_name (name n))" by force moreover from QP have "\!q'. (q' = n \ q' \ ns) \ name n = name q'" by force moreover have "\q\ns. \!q'. (q' = n \ q' \ ns) \ name q = name q' " using QP by auto ultimately show ?case using prems by simp qed next case 3 then show ?case by simp next case 4 then show ?case by simp next case 5 then show ?case by simp next case 6 then show ?case by simp next case 7 then show ?case by simp next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto with prems have QP: "?Q (n, ns) \ ?P ns" and step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x'. ?P (snd x'))" and f_sup: "\x. f x \ expand x" by auto let ?x = "(n\new := new n - {\}, new := new1 \ \ new (n\new := new n - {\}\), old := {\} \ old (n\new := new n - {\}\), next := next1 \ \ next (n\new := new n - {\}\)\, ns)" let ?props = "\x r. expand_rslt_incoming r \ expand_rslt_name x r \ expand_name_ident (snd r)" show ?case using goal_assms QP unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases) case 1 then show ?case by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) simp next case 2 then show ?case by (rule_tac SPEC_rule_param2[where P = "\x r. ?P (snd r)"], rule_tac step) auto next case (3 nm nds) then show ?case proof (rule_tac SPEC_rule_weak[where P = "\x r. ?P (snd r)" and Q = "\x r. expand_rslt_exist_eq x r \ ?props x r"], goal_cases) case 1 then show ?case by (rule_tac SPEC_rule_conjI, rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq, rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) force next case 2 then show ?case by (rule_tac SPEC_rule_param2[where P = "\x r. ?P (snd r)"], rule_tac step) force next case (3 nm' nds') then show ?case by simp qed qed qed lemma create_graph__incoming_name_exist: "create_graph \ \ SPEC (\nds. \nd\nds. expand_init < name nd \ (\nm\incoming nd. nm \ expand_init \ nm\name ` nds))" unfolding create_graph_def by (intro refine_vcg, rule_tac order_trans, rule_tac expand_incoming_name_exist) ( auto simp add:expand_new_name_expand_init) abbreviation "expand_rslt_all__ex_equiv \ nd nds \ (\nd'\nds. name nd \ incoming nd' \ (\\\old nd'. suffix 1 \ \\<^sub>r \) \ (\\\next nd'. suffix 1 \ \\<^sub>r X\<^sub>r \) \ {\. \\. \ U\<^sub>r \ \ old nd' \ suffix 1 \ \\<^sub>r \} \ old nd')" abbreviation "expand_rslt_all \ n_ns nm_nds \ (\nd\snd nm_nds. name nd \ name ` (snd n_ns) \ (\\\old nd. \ \\<^sub>r \) \ (\\\next nd. \ \\<^sub>r X\<^sub>r \) \ expand_rslt_all__ex_equiv \ nd (snd nm_nds))" lemma expand_prop_all: assumes "expand_assm_incoming n_ns \ expand_name_ident (snd n_ns)" (is "?Q n_ns") shows "expand n_ns \ SPEC (expand_rslt_all \ n_ns)" (is "_ \ SPEC (?P n_ns)") using assms apply (rule_tac expand_rec_rule[where \="?Q"]) apply simp apply (intro refine_vcg) proof goal_cases case 1 then show ?case by (simp, rule_tac upd_incoming__ident) simp_all next case (2 f x n ns) then have step: "\x. ?Q x \ f x \ SPEC (?P x)" and Q: "?Q (n, ns)" and f_sup: "\x. f x \ expand x" by auto let ?x = "(\name = expand_new_name (name n), incoming = {name n}, new = next n, old = {}, next = {}\, {n} \ ns)" from Q have name_le: "name n < expand_new_name (name n)" by auto show ?case unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_weak[where Q = "\p r. (expand_assm_exist (suffix 1 \) ?x \ expand_rslt_exist (suffix 1 \) ?x r) \ expand_rslt_exist_eq p r \ (expand_name_ident (snd r))"], goal_cases) case 1 then show ?case proof (rule_tac SPEC_rule_conjI, rule_tac order_trans, rule_tac f_sup, rule_tac expand_prop_exist, rule_tac SPEC_rule_conjI, rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq, rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag__name_ident, goal_cases) case 1 then show ?case using Q name_le by force qed next case 2 then show ?case using Q name_le by (rule_tac step) force next case prems: (3 nm nds) then obtain n' where "n'\nds" and eq_node: "expand_rslt_exist_eq__node n n'" by auto with prems have ex1_name: "\!q\nds. name n = name q" by auto then have nds_eq: "nds = {n'} \ {x \ nds. name n \ name x}" using eq_node \n'\nds\ by blast have name_notin: "name n \ name ` ns" using Q by auto from prems have P_x: "expand_rslt_all \ ?x (nm, nds)" by fast show ?case unfolding snd_conv proof clarify fix nd assume "nd \ nds" and name_img: "name nd \ name ` ns" and nd_old_equiv: "\\\old nd. \ \\<^sub>r \" and nd_next_equiv: "\\\next nd. \ \\<^sub>r X\<^sub>r \" show "expand_rslt_all__ex_equiv \ nd nds" proof (cases "name nd = name n") case True with nds_eq eq_node \nd\nds\ have "nd = n'" by auto with prems(1)[THEN conjunct1, simplified] nd_old_equiv nd_next_equiv eq_node show ?thesis by simp next case False with name_img \nd \ nds\ nd_old_equiv nd_next_equiv P_x show ?thesis by simp qed qed qed next case 3 then show ?case by auto next case prems: (4 f) then have step: "\x. ?Q x \ f x \ SPEC (?P x)" by simp from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (5 f) then have step: "\x. ?Q x \ f x \ SPEC (?P x)" by simp from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case 6 then show ?case by auto next case prems: (7 f) then have step: "\x. ?Q x \ f x \ SPEC (?P x)" by simp from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have Q: "?Q (n, ns)" and step: "\x. ?Q x \ f x \ SPEC (?P x)" and f_sup: "\x. f x \ expand x" by auto let ?x = "(n\new := new n - {\}, new := new1 \ \ new (n\new := new n - {\}\), old := {\} \ old (n\new := new n - {\}\), next := next1 \ \ next (n\new := new n - {\}\) \, ns)" let ?props = "\x r. expand_rslt_incoming r \ expand_rslt_name x r \ expand_name_ident (snd r)" show ?case using goal_assms Q unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases) case 1 then show ?case by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) simp next case 2 then show ?case by (rule_tac SPEC_rule_param2[where P = "?P"], rule_tac step) auto next case prems: (3 nm nds) then show ?case proof (rule_tac SPEC_rule_weak[where P = "?P" and Q = "\x r. expand_rslt_exist_eq x r \ ?props x r"], goal_cases) case 1 then show ?case by (rule_tac SPEC_rule_conjI, rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq, rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) auto next case 2 then show ?case by (rule_tac SPEC_rule_param2[where P = "?P"], rule_tac step) auto next case prems': (3 nm' nds') then have P_x: "?P (n, ns) (nm, nds)" and P_x': "?P (n, nds) (nm', nds')" by simp_all show ?case unfolding snd_conv proof clarify fix nd assume "nd\nds'" and name_nd_notin: "name nd \ name ` ns" and old_equiv: "\\\old nd. \ \\<^sub>r \" and next_equiv: "\\\next nd. \ \\<^sub>r X\<^sub>r \" show "expand_rslt_all__ex_equiv \ nd nds'" proof (cases "name nd \ name ` nds") case True then obtain n' where "n' \ nds" and "name nd = name n'" by auto with prems' obtain nd' where "nd'\nds'" and nd'_eq: "expand_rslt_exist_eq__node n' nd'" by auto moreover from prems' have "\q\nds'. \!q'\nds'. name q = name q'" by simp ultimately have "nd' = nd" using \name nd = name n'\ \nd \ nds'\ by auto with nd'_eq have n'_eq: "expand_rslt_exist_eq__node n' nd" by simp then have "name n'\name ` ns" and "\\\old n'. \ \\<^sub>r \" and "\\\next n'. \ \\<^sub>r X\<^sub>r \" using name_nd_notin old_equiv next_equiv \n' \ nds\ by auto then have "expand_rslt_all__ex_equiv \ n' nds" (is "\nd'\nds. ?sthm n' nd'") using P_x \n' \ nds\ unfolding snd_conv by blast then obtain sucnd where sucnd: "sucnd\nds" and sthm: "?sthm n' sucnd" by blast moreover from prems' sucnd sthm obtain sucnd' where "sucnd'\nds'" and sucnd'_eq: "expand_rslt_exist_eq__node sucnd sucnd'" by auto ultimately have "?sthm n' sucnd'" by auto then show ?thesis using \sucnd' \ nds'\ unfolding \name nd = name n'\ by blast next case False with \nd \ nds'\ P_x' old_equiv next_equiv show ?thesis unfolding snd_conv by blast qed qed qed qed qed abbreviation "create_graph_rslt_all \ nds \ \q\nds. (\\\old q. \ \\<^sub>r \) \ (\\\next q. \ \\<^sub>r X\<^sub>r \) \ (\q'\nds. name q \ incoming q' \ (\\\old q'. suffix 1 \ \\<^sub>r \) \ (\\\next q'. suffix 1 \ \\<^sub>r X\<^sub>r \) \ {\. \\. \ U\<^sub>r \ \ old q' \ suffix 1 \ \\<^sub>r \} \ old q')" lemma L4_5: "create_graph \ \ SPEC (create_graph_rslt_all \)" unfolding create_graph_def apply (refine_vcg expand_prop_all) apply (auto simp add:expand_new_name_expand_init) done subsection \Creation of GBA\ text \This section formalizes the second part of the algorithm, that creates the actual generalized B\"uchi automata from the set of nodes.\ definition create_gba_from_nodes :: "'a frml \ 'a node set \ ('a node, 'a set) gba_rec" where "create_gba_from_nodes \ qs \ \ g_V = qs, g_E = {(q, q'). q\qs \ q'\qs \ name q\incoming q'}, g_V0 = {q\qs. expand_init\incoming q}, gbg_F = {{q\qs. \ U\<^sub>r \\old q \ \\old q}|\ \. \ U\<^sub>r \ \ subfrmlsr \}, gba_L = \q l. q\qs \ {p. prop\<^sub>r(p)\old q}\l \ {p. nprop\<^sub>r(p)\old q} \ l = {} \" end locale create_gba_from_nodes_precond = fixes \ :: "'a ltlr" fixes qs :: "'a node set" assumes res: "inres (create_graph \) qs" begin lemma finite_qs[simp, intro!]: "finite qs" using res create_graph_finite by (auto simp add: pw_le_iff) lemma create_gba_from_nodes__invar: "gba (create_gba_from_nodes \ qs)" using [[simproc finite_Collect]] apply unfold_locales apply (auto intro!: finite_vimageI subfrmlsr_finite injI simp: create_gba_from_nodes_def) done sublocale gba: gba "create_gba_from_nodes \ qs" by (rule create_gba_from_nodes__invar) lemma create_gba_from_nodes__fin: "finite (g_V (create_gba_from_nodes \ qs))" unfolding create_gba_from_nodes_def by auto lemma create_gba_from_nodes__ipath: "ipath gba.E r \ (\i. r i \qs \ name (r i)\incoming (r (Suc i)))" unfolding create_gba_from_nodes_def ipath_def by auto lemma create_gba_from_nodes__is_run: "gba.is_run r \ expand_init \ incoming (r 0) \ (\i. r i\qs \ name (r i)\incoming (r (Suc i)))" unfolding gba.is_run_def apply (simp add: create_gba_from_nodes__ipath) apply (auto simp: create_gba_from_nodes_def) done context begin abbreviation "auto_run_j j \ q \ (\\\old q. suffix j \ \\<^sub>r \) \ (\\\next q. suffix j \ \\<^sub>r X\<^sub>r \) \ {\. \\. \ U\<^sub>r \ \ old q \ suffix j \ \\<^sub>r \} \ old q" fun auto_run :: "['a interprt, 'a node set] \ 'a node word" where "auto_run \ nds 0 = (SOME q. q\nds \ expand_init \ incoming q \ auto_run_j 0 \ q)" | "auto_run \ nds (Suc k) = (SOME q'. q'\nds \ name (auto_run \ nds k) \ incoming q' \ auto_run_j (Suc k) \ q')" (* TODO: Remove. Only special instance of more generic principle lemma create_graph_comb: assumes "\x. inres (create_graph \) x \ P x" shows "create_graph \\SPEC P" using create_graph_nofail assms by (auto simp add: pw_le_iff refine_pw_simps) *) lemma run_propag_on_create_graph: assumes "ipath gba.E \" shows "\ k\qs \ name (\ k)\incoming (\ (k+1))" using assms by (auto simp: create_gba_from_nodes__ipath) lemma expand_false_propag: assumes "false\<^sub>r \ old (fst n_ns) \ (\nd\snd n_ns. false\<^sub>r \ old nd)" (is "?Q n_ns") shows "expand n_ns \ SPEC (\nm_nds. \nd\snd nm_nds. false\<^sub>r \ old nd)" using assms proof (rule_tac expand_rec_rule[where \="?Q"], simp, intro refine_vcg, goal_cases) case 1 then show ?case by (simp, rule_tac upd_incoming__ident) auto next case 8 then show ?case by (rule_tac SPEC_rule_nested2) auto qed auto lemma false_propag_on_create_graph: "create_graph \ \ SPEC (\nds. \nd\nds. false\<^sub>r \ old nd)" unfolding create_graph_def by (intro refine_vcg, rule_tac order_trans, rule_tac expand_false_propag) auto lemma expand_and_propag: assumes "\ and\<^sub>r \ \ old (fst n_ns) \ {\, \} \ old (fst n_ns) \ new (fst n_ns)" (is "?Q n_ns") and "\nd\snd n_ns. \ and\<^sub>r \ \ old nd \ {\, \} \ old nd" (is "?P (snd n_ns)") shows "expand n_ns \ SPEC (\nm_nds. ?P (snd nm_nds))" using assms proof (rule_tac expand_rec_rule[where \="\x. ?Q x \ ?P (snd x)"], simp, intro refine_vcg, goal_cases) case 1 then show ?case by (simp, rule_tac upd_incoming__ident) auto next case prems: (4 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x'. ?P (snd x'))" by simp with prems show ?case by (rule_tac step) auto next case prems: (5 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x'. ?P (snd x'))" by simp with prems show ?case by (rule_tac step) auto next case (6 f x n ns) then show ?case by auto next case prems: (7 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x'. ?P (snd x'))" by simp with prems show ?case by (rule_tac step) auto next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ \ (\q. \ = prop\<^sub>r(q) \ \ = nprop\<^sub>r(q)) \ \ \ true\<^sub>r \ \ \ false\<^sub>r \ \ (\\ \. \ = \ and\<^sub>r \ \ \ = X\<^sub>r \) \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have QP: "?Q (n, ns) \ ?P ns" and step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x'. ?P (snd x'))" by simp_all show ?case using goal_assms QP unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_nested2, goal_cases) case 1 then show ?case by (rule_tac step) auto next case 2 then show ?case by (rule_tac step) auto qed qed auto lemma and_propag_on_create_graph: "create_graph \ \ SPEC (\nds. \nd\nds. \ and\<^sub>r \ \ old nd \ {\, \} \ old nd)" unfolding create_graph_def by (intro refine_vcg, rule_tac order_trans, rule_tac expand_and_propag) auto lemma expand_or_propag: assumes "\ or\<^sub>r \ \ old (fst n_ns) \ {\, \} \ (old (fst n_ns) \ new (fst n_ns)) \ {}" (is "?Q n_ns") and "\nd\snd n_ns. \ or\<^sub>r \ \ old nd \ {\, \} \ old nd \ {}" (is "?P (snd n_ns)") shows "expand n_ns \ SPEC (\nm_nds. ?P (snd nm_nds))" using assms proof (rule_tac expand_rec_rule[where \="\x. ?Q x \ ?P (snd x)"], simp, intro refine_vcg, goal_cases) case 1 then show ?case by (simp, rule_tac upd_incoming__ident) auto next case prems: (4 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x'. ?P (snd x'))" by simp with prems show ?case by (rule_tac step) auto next case prems: (5 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x'. ?P (snd x'))" by simp with prems show ?case by (rule_tac step) auto next case (6 f x n ns) then show ?case by auto next case prems: (7 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x'. ?P (snd x'))" by simp with prems show ?case by (rule_tac step) auto next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ \ (\q. \ = prop\<^sub>r(q) \ \ = nprop\<^sub>r(q)) \ \ \ true\<^sub>r \ \ \ false\<^sub>r \ \ (\\ \. \ = \ and\<^sub>r \ \ \ = X\<^sub>r \) \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have QP: "?Q (n, ns) \ ?P ns" and step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\x'. ?P (snd x'))" by simp_all show ?case using goal_assms QP unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_nested2, goal_cases) case 1 then show ?case by (rule_tac step) auto next case 2 then show ?case by (rule_tac step) auto qed qed auto lemma or_propag_on_create_graph: "create_graph \ \ SPEC (\nds. \nd\nds. \ or\<^sub>r \ \ old nd \ {\, \} \ old nd \ {})" unfolding create_graph_def by (intro refine_vcg, rule_tac order_trans, rule_tac expand_or_propag) auto abbreviation "next_propag__assm \ n_ns \ (X\<^sub>r \ \ old (fst n_ns) \ \ \ next (fst n_ns)) \ (\nd\snd n_ns. X\<^sub>r \ \ old nd \ name nd \ incoming (fst n_ns) \ \ \ old (fst n_ns) \ new (fst n_ns))" abbreviation "next_propag__rslt \ ns \ \nd\ns. \nd'\ns. X\<^sub>r \ \ old nd \ name nd \ incoming nd' \ \ \ old nd'" lemma expand_next_propag: fixes n_ns :: "_ \ 'a node set" assumes "next_propag__assm \ n_ns \ next_propag__rslt \ (snd n_ns) \ expand_assm_incoming n_ns \ expand_name_ident (snd n_ns)" (is "?Q n_ns") shows "expand n_ns \ SPEC (\r. next_propag__rslt \ (snd r))" (is "_ \ SPEC ?P") using assms proof (rule_tac expand_rec_rule[where \="?Q"], simp, intro refine_vcg, goal_cases) case (1 f x n ns) then show ?case proof (simp, rule_tac upd_incoming__ident, goal_cases) case prems: 1 { fix nd :: "'a node" and nd' :: "'a node" assume "nd\ns" and nd'_elem: "nd'\upd_incoming n ns" have "\ \ old nd'" if *: "X\<^sub>r \ \ old nd" and **: "name nd \ incoming nd'" proof (cases "nd'\ns") case True with prems * ** show ?thesis using \nd\ns\ by auto next case False with upd_incoming__elem[of nd' n ns] nd'_elem * ** obtain nd'' where "nd''\ns" and nd'_eq: "nd' = nd''\incoming := incoming n \ incoming nd''\" and old_eq: "old nd'' = old n" by auto have "\ \ old nd'" proof (cases "name nd \ incoming n") case True with prems * \nd\ns\ have "\ \ old n" by auto then show ?thesis using nd'_eq old_eq by simp next case False then have "name nd \ incoming nd''" using \name nd \incoming nd'\ nd'_eq by simp then show ?thesis unfolding nd'_eq using \nd\ns\ \nd''\ns\ * prems by auto qed then show ?thesis by auto qed } then show ?case by auto next case 2 then show ?case by simp qed next case prems: (2 f x n ns) then have step: "\x. ?Q x \ f x \ SPEC ?P" and f_sup: "\x. f x \ expand x" by auto from prems have Q: "?Q (n, ns)" by auto from Q have name_le: "name n < expand_new_name (name n)" by auto let ?x' = "(\name = expand_new_name (name n), incoming = {name n}, new = next n, old = {}, next = {}\, {n} \ ns)" have Q'1: "expand_assm_incoming ?x'\ expand_name_ident (snd ?x')" using \new n = {}\ Q[THEN conjunct2, THEN conjunct2] name_le by force have Q'2: "next_propag__assm \ ?x' \ next_propag__rslt \ (snd ?x')" using Q \new n = {}\ by auto show ?case using \new n = {}\ unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_weak[where Q = "\_ r. expand_name_ident (snd r)" and P = "\_. ?P"], goal_cases) case 1 then show ?case using Q'1 by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag__name_ident) auto next case 2 then show ?case using Q'1 Q'2 by (rule_tac step) simp next case (3 nm nds) then show ?case by simp qed next case 3 then show ?case by auto next case prems: (4 f) then have step: "\x. ?Q x \ f x \ SPEC ?P" by simp from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (5 f) then have step: "\x. ?Q x \ f x \ SPEC ?P" by simp from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case 6 then show ?case by auto next case prems: (7 f) then have step: "\x. ?Q x \ f x \ SPEC ?P" by simp from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have Q: "?Q (n, ns)" and step: "\x. ?Q x \ f x \ SPEC ?P" and f_sup: "\x. f x \ expand x" by auto let ?x = "(n\new := new n - {\}, new := new1 \ \ new (n\new := new n - {\}\), old := {\} \ old (n\new := new n - {\}\), next := next1 \ \ next (n\new := new n - {\}\) \, ns)" let ?props = "\x r. expand_rslt_exist_eq x r \ expand_rslt_incoming r \ expand_rslt_name x r \ expand_name_ident (snd r)" show ?case using goal_assms Q unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases) case 1 then show ?case by (rule_tac SPEC_rule_conjI, rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq, rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) simp+ next case 2 then show ?case by (rule_tac SPEC_rule_param2[where P = "\_. ?P"], rule_tac step) auto next case prems': (3 nm nds) let ?x' = "(n\new := new n - {\}, name := fst (nm, nds), new := new2 \ \ new (n\new := new n - {\}\), old := {\} \ old (n\new := new n - {\}\)\, nds)" from prems' show ?case proof (rule_tac step, goal_cases) case prems'': 1 then have "expand_assm_incoming ?x'" by auto moreover from prems'' have nds_ident: "expand_name_ident (snd ?x')" by simp moreover have "X\<^sub>r \ \ old (fst ?x') \ \\next (fst ?x')" using Q[THEN conjunct1] goal_assms by auto moreover from prems'' have "next_propag__rslt \ (snd ?x')" by simp moreover from prems'' have name_nds_eq: "name ` nds = name ` ns \ name ` {nd\nds. name nd \ name n}" by auto have "\nd\nds. (X\<^sub>r \ \ old nd \ name nd \ incoming (fst ?x')) \ \\old (fst ?x')\new (fst ?x')" (is "\nd\nds. ?assm (fst ?x') nd \ ?concl (fst ?x') nd") proof fix nd assume "nd\nds" { assume loc_assm: "name nd\name ` ns" then obtain n' where n': "n'\ns" "name n' = name nd" by auto moreover from prems'' n' obtain nd' where "nd'\nds" and n'_nd'_eq: "expand_rslt_exist_eq__node n' nd'" by auto ultimately have "nd = nd'" using nds_ident \nd\nds\ loc_assm by auto moreover from prems'' have "?assm n n' \ ?concl n n'" using \n'\ns\ by auto ultimately have "?assm (fst ?x') nd \ ?concl (fst ?x') nd" using n'_nd'_eq by auto } moreover { assume "name nd\name ` ns" with name_nds_eq \nd\nds\ have "name nd \ name n" by auto with prems'' have "\ (?assm (fst ?x') nd)" by auto } ultimately show "?assm (fst ?x') nd \ ?concl (fst ?x') nd" by auto qed ultimately show ?case by simp qed qed qed lemma next_propag_on_create_graph: "create_graph \ \ SPEC (\nds. \n\nds. \n'\nds. X\<^sub>r \\old n \ name n\incoming n' \ \\old n')" unfolding create_graph_def apply (refine_vcg expand_next_propag) apply (auto simp add:expand_new_name_expand_init) done abbreviation "release_propag__assm \ \ n_ns \ (\ R\<^sub>r \ \ old (fst n_ns) \ {\, \}\old (fst n_ns)\new (fst n_ns) \ (\\old (fst n_ns)\new (fst n_ns)) \ \ R\<^sub>r \ \ next (fst n_ns)) \ (\nd\snd n_ns. \ R\<^sub>r \ \ old nd \ name nd \ incoming (fst n_ns) \ {\, \}\old nd \ (\\old nd \ \ R\<^sub>r \ \ old (fst n_ns)\new (fst n_ns)))" abbreviation "release_propag__rslt \ \ ns \ \nd\ns. \nd'\ns. \ R\<^sub>r \ \ old nd \ name nd \ incoming nd' \ {\, \}\old nd \ (\\old nd \ \ R\<^sub>r \ \ old nd')" lemma expand_release_propag: fixes n_ns :: "_ \ 'a node set" assumes "release_propag__assm \ \ n_ns \ release_propag__rslt \ \ (snd n_ns) \ expand_assm_incoming n_ns \ expand_name_ident (snd n_ns)" (is "?Q n_ns") shows "expand n_ns \ SPEC (\r. release_propag__rslt \ \ (snd r))" (is "_ \ SPEC ?P") using assms proof (rule_tac expand_rec_rule[where \="?Q"], simp, intro refine_vcg, goal_cases) case (1 f x n ns) then show ?case proof (simp, rule_tac upd_incoming__ident, goal_cases) case prems: 1 { fix nd :: "'a node" and nd' :: "'a node" let ?V_prop = "\ R\<^sub>r \ \ old nd \ name nd \ incoming nd' \ {\, \} \ old nd \ \ \ old nd \ \ R\<^sub>r \ \ old nd'" assume "nd\ns" and nd'_elem: "nd'\upd_incoming n ns" { assume "nd'\ns" with prems have ?V_prop using \nd\ns\ by auto } moreover { assume "nd'\ns" and V_in_nd: "\ R\<^sub>r \ \ old nd" and "name nd \incoming nd'" with upd_incoming__elem[of nd' n ns] nd'_elem obtain nd'' where "nd''\ns" and nd'_eq: "nd' = nd''\incoming := incoming n \ incoming nd''\" and old_eq: "old nd'' = old n" by auto { assume "name nd \ incoming n" with prems V_in_nd \nd\ns\ have "{\, \} \ old nd \ \ \ old nd \ \ R\<^sub>r \ \ old n" by auto then have "{\, \} \ old nd \ \ \ old nd \ \ R\<^sub>r \ \ old nd'" using nd'_eq old_eq by simp } moreover { assume "name nd \ incoming n" then have "name nd \ incoming nd''" using \name nd \incoming nd'\ nd'_eq by simp then have "{\, \} \ old nd \ \ \ old nd \ \ R\<^sub>r \ \ old nd'" unfolding nd'_eq using prems \nd\ns\ \nd''\ns\ V_in_nd by auto } ultimately have "{\, \} \ old nd \ \ \ old nd \ \ R\<^sub>r \ \ old nd'" by fast } ultimately have ?V_prop by auto } then show ?case by auto next case 2 then show ?case by simp qed next case prems: (2 f x n ns) then have step: "\x. ?Q x \ f x \ SPEC ?P" and f_sup: "\x. f x \ expand x" by auto from prems have Q: "?Q (n, ns)" by auto from Q have name_le: "name n < expand_new_name (name n)" by auto let ?x' = "(\name = expand_new_name (name n), incoming = {name n}, new = next n, old = {}, next = {}\, {n} \ ns)" have Q'1: "expand_assm_incoming ?x'\ expand_name_ident (snd ?x')" using \new n = {}\ Q[THEN conjunct2, THEN conjunct2] name_le by force have Q'2: "release_propag__assm \ \ ?x' \ release_propag__rslt \ \ (snd ?x')" using Q \new n = {}\ by auto show ?case using \new n = {}\ unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_weak[where Q = "\_ r. expand_name_ident (snd r)" and P = "\_. ?P"], goal_cases) case 1 then show ?case using Q'1 by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag__name_ident) auto next case 2 then show ?case using Q'1 Q'2 by (rule_tac step) simp next case (3 nm nds) then show ?case by simp qed next case 3 then show ?case by auto next case prems: (4 f x n ns \) then have goal_assms: "\ \ new n \ (\q. \ = prop\<^sub>r(q) \ \ = nprop\<^sub>r(q))" by simp from prems have step: "\x. ?Q x \ f x \ SPEC ?P" and Q: "?Q (n, ns)" by simp_all show ?case using Q goal_assms by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (5 f x n ns \) then have goal_assms: "\ \ new n \ \ = true\<^sub>r" by simp from prems have step: "\x. ?Q x \ f x \ SPEC ?P" and Q: "?Q (n, ns)" by simp_all show ?case using Q goal_assms by (rule_tac SPEC_rule_param2, rule_tac step) auto next case 6 then show ?case by auto next case prems: (7 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ and\<^sub>r \ \ \ = X\<^sub>r \)" by simp from prems have step: "\x. ?Q x \ f x \ SPEC ?P" and Q: "?Q (n, ns)" by simp_all show ?case using Q goal_assms by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have Q: "?Q (n, ns)" and step: "\x. ?Q x \ f x \ SPEC ?P" and f_sup: "\x. f x \ expand x" by auto let ?x = "(n\new := new n - {\}, new := new1 \ \ new (n\new := new n - {\}\), old := {\} \ old (n\new := new n - {\}\), next := next1 \ \ next (n\new := new n - {\}\) \, ns)" let ?props = "\x r. expand_rslt_exist_eq x r \ expand_rslt_incoming r \ expand_rslt_name x r \ expand_name_ident (snd r)" show ?case using goal_assms Q unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases) case 1 then show ?case by (rule_tac SPEC_rule_conjI, rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq, rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) simp+ next case 2 then show ?case by (rule_tac SPEC_rule_param2[where P = "\_. ?P"], rule_tac step) auto next case prems': (3 nm nds) let ?x' = "(n\new := new n - {\}, name := fst (nm, nds), new := new2 \ \ new (n\new := new n - {\}\), old := {\} \ old (n\new := new n - {\}\)\, nds)" from prems' show ?case proof (rule_tac step, goal_cases) case prems'': 1 then have "expand_assm_incoming ?x'" by auto moreover from prems'' have nds_ident: "expand_name_ident (snd ?x')" by simp moreover have "(\ R\<^sub>r \ \ old (fst ?x') \ ({\, \}\old (fst ?x') \ new (fst ?x') \ (\\old (fst ?x')\new (fst ?x') \ \ R\<^sub>r \ \ next (fst ?x'))))" using Q[THEN conjunct1] goal_assms by auto moreover from prems'' have "release_propag__rslt \ \ (snd ?x')" by simp moreover from prems'' have name_nds_eq: "name ` nds = name ` ns \ name ` {nd\nds. name nd \ name n}" by auto have "\nd\nds. (\ R\<^sub>r \ \ old nd \ name nd \ incoming (fst ?x')) \ ({\, \}\old nd \ (\\old nd \ \ R\<^sub>r \ \old (fst ?x')\new (fst ?x')))" (is "\nd\nds. ?assm (fst ?x') nd \ ?concl (fst ?x') nd") proof fix nd assume "nd\nds" { assume loc_assm: "name nd\name ` ns" then obtain n' where n': "n'\ns" "name n' = name nd" by auto with prems'' obtain nd' where "nd'\nds" and n'_nd'_eq: "expand_rslt_exist_eq__node n' nd'" by auto with n' have "nd = nd'" using nds_ident \nd\nds\ loc_assm by auto moreover from prems'' have "?assm n n' \ ?concl n n'" using \n'\ns\ by auto ultimately have "?assm (fst ?x') nd \ ?concl (fst ?x') nd" using n'_nd'_eq by auto } moreover { assume "name nd\name ` ns" with name_nds_eq \nd\nds\ have "name nd \ name n" by auto with prems'' have "\ (?assm (fst ?x') nd)" by auto } ultimately show "?assm (fst ?x') nd \ ?concl (fst ?x') nd" by auto qed ultimately show ?case by simp qed qed qed lemma release_propag_on_create_graph: "create_graph \ \ SPEC (\nds. \n\nds. \n'\nds. \ R\<^sub>r \\old n \ name n\incoming n' \ ({\, \}\old n \ \\old n \ \ R\<^sub>r \\old n'))" unfolding create_graph_def apply (refine_vcg expand_release_propag) by (auto simp add:expand_new_name_expand_init) abbreviation "until_propag__assm f g n_ns \ (f U\<^sub>r g \ old (fst n_ns) \ (g\old (fst n_ns)\new (fst n_ns) \ (f\old (fst n_ns)\new (fst n_ns) \ f U\<^sub>r g \ next (fst n_ns)))) \ (\nd\snd n_ns. f U\<^sub>r g \ old nd \ name nd \ incoming (fst n_ns) \ (g\old nd \ (f\old nd \ f U\<^sub>r g \old (fst n_ns)\new (fst n_ns))))" abbreviation "until_propag__rslt f g ns \ \n\ns. \nd\ns. f U\<^sub>r g \ old n \ name n \ incoming nd \ (g \ old n \ (f\old n \ f U\<^sub>r g \ old nd))" lemma expand_until_propag: fixes n_ns :: "_ \ 'a node set" assumes "until_propag__assm \ \ n_ns \ until_propag__rslt \ \ (snd n_ns) \ expand_assm_incoming n_ns \ expand_name_ident (snd n_ns)" (is "?Q n_ns") shows "expand n_ns \ SPEC (\r. until_propag__rslt \ \ (snd r))" (is "_ \ SPEC ?P") using assms proof (rule_tac expand_rec_rule[where \="?Q"], simp, intro refine_vcg, goal_cases) case prems: (1 f x n ns) then show ?case proof (simp, rule_tac upd_incoming__ident, goal_cases) case prems': 1 { fix nd :: "'a node" and nd' :: "'a node" let ?U_prop = "\ U\<^sub>r \ \ old nd \ name nd \ incoming nd' \ \ \ old nd \ \ \ old nd \ \ U\<^sub>r \ \ old nd'" assume "nd\ns" and nd'_elem: "nd'\upd_incoming n ns" { assume "nd'\ns" with prems' have ?U_prop using \nd\ns\ by auto } moreover { assume "nd'\ns" and U_in_nd: "\ U\<^sub>r \ \ old nd" and "name nd \incoming nd'" with upd_incoming__elem[of nd' n ns] nd'_elem obtain nd'' where "nd''\ns" and nd'_eq: "nd' = nd''\incoming := incoming n \ incoming nd''\" and old_eq: "old nd'' = old n" by auto { assume "name nd \ incoming n" with prems' U_in_nd \nd\ns\ have "\ \ old nd \ \ \ old nd \ \ U\<^sub>r \ \ old n" by auto then have "\ \ old nd \ \ \ old nd \ \ U\<^sub>r \ \ old nd'" using nd'_eq old_eq by simp } moreover { assume "name nd \ incoming n" then have "name nd \ incoming nd''" using \name nd \incoming nd'\ nd'_eq by simp then have "\ \ old nd \ \ \ old nd \ \ U\<^sub>r \ \ old nd'" unfolding nd'_eq using prems' \nd\ns\ \nd''\ns\ U_in_nd by auto } ultimately have "\ \ old nd \ \ \ old nd \ \ U\<^sub>r \ \ old nd'" by fast } ultimately have ?U_prop by auto } then show ?case by auto next case 2 then show ?case by simp qed next case prems: (2 f x n ns) then have step: "\x. ?Q x \ f x \ SPEC ?P" and f_sup: "\x. f x \ expand x" by auto from prems have Q: "?Q (n, ns)" by auto from Q have name_le: "name n < expand_new_name (name n)" by auto let ?x' = "(\name = expand_new_name (name n), incoming = {name n}, new = next n, old = {}, next = {}\, {n} \ ns)" have Q'1: "expand_assm_incoming ?x'\ expand_name_ident (snd ?x')" using \new n = {}\ Q[THEN conjunct2, THEN conjunct2] name_le by force have Q'2: "until_propag__assm \ \ ?x' \ until_propag__rslt \ \ (snd ?x')" using Q \new n = {}\ by auto show ?case using \new n = {}\ unfolding \x = (n, ns)\ proof (rule_tac SPEC_rule_weak[where Q = "\_ r. expand_name_ident (snd r)" and P = "\_. ?P"], goal_cases) case 1 then show ?case using Q'1 by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag__name_ident) auto next case 2 then show ?case using Q'1 Q'2 by (rule_tac step) simp next case (3 nm nds) then show ?case by simp qed next case 3 then show ?case by auto next case prems: (4 f) then have step: "\x. ?Q x \ f x \ SPEC ?P" by simp_all from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (5 f) then have step: "\x. ?Q x \ f x \ SPEC ?P" by simp_all from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case 6 then show ?case by auto next case prems: (7 f) then have step: "\x. ?Q x \ f x \ SPEC ?P" by simp_all from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have Q: "?Q (n, ns)" and step: "\x. ?Q x \ f x \ SPEC ?P" and f_sup: "\x. f x \ expand x" by auto let ?x = "(n\new := new n - {\}, new := new1 \ \ new (n\new := new n - {\}\), old := {\} \ old (n\new := new n - {\}\), next := next1 \ \ next (n\new := new n - {\}\) \, ns)" let ?props = "\x r. expand_rslt_exist_eq x r \ expand_rslt_incoming r \ expand_rslt_name x r \ expand_name_ident (snd r)" show ?case using goal_assms Q unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases) case 1 then show ?case by (rule_tac SPEC_rule_conjI, rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq, rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) simp+ next case 2 then show ?case by (rule_tac SPEC_rule_param2[where P = "\_. ?P"], rule_tac step) auto next case prems: (3 nm nds) let ?x' = "(n\new := new n - {\}, name := fst (nm, nds), new := new2 \ \ new (n\new := new n - {\}\), old := {\} \ old (n\new := new n - {\}\)\, nds)" from prems show ?case proof (rule_tac step, goal_cases) case prems': 1 then have "expand_assm_incoming ?x'" by auto moreover from prems' have nds_ident: "expand_name_ident (snd ?x')" by simp moreover have "(\ U\<^sub>r \ \ old (fst ?x') \ (\\old (fst ?x')\new (fst ?x') \ (\\old (fst ?x')\new (fst ?x') \ \ U\<^sub>r \ \ next (fst ?x'))))" using Q[THEN conjunct1] goal_assms by auto moreover from prems' have "until_propag__rslt \ \ (snd ?x')" by simp moreover from prems' have name_nds_eq: "name ` nds = name ` ns \ name ` {nd\nds. name nd \ name n}" by auto have "\nd\nds. (\ U\<^sub>r \ \ old nd \ name nd \ incoming (fst ?x')) \ (\\old nd \ (\\old nd \ \ U\<^sub>r \ \old (fst ?x')\new (fst ?x')))" (is "\nd\nds. ?assm (fst ?x') nd \ ?concl (fst ?x') nd") proof fix nd assume "nd\nds" { assume loc_assm: "name nd\name ` ns" then obtain n' where n': "n'\ns" "name n' = name nd" by auto moreover from prems' n' obtain nd' where "nd'\nds" and n'_nd'_eq: "expand_rslt_exist_eq__node n' nd'" by auto ultimately have "nd = nd'" using nds_ident \nd\nds\ loc_assm by auto moreover from prems' have "?assm n n' \ ?concl n n'" using \n'\ns\ by auto ultimately have "?assm (fst ?x') nd \ ?concl (fst ?x') nd" using n'_nd'_eq by auto } moreover { assume "name nd\name ` ns" with name_nds_eq \nd\nds\ have "name nd \ name n" by auto with prems' have "\ (?assm (fst ?x') nd)" by auto } ultimately show "?assm (fst ?x') nd \ ?concl (fst ?x') nd" by auto qed ultimately show ?case by simp qed qed qed lemma until_propag_on_create_graph: "create_graph \ \ SPEC (\nds. \n\nds. \n'\nds. \ U\<^sub>r \\old n \ name n\incoming n' \ (\\old n \ \\old n \ \ U\<^sub>r \\old n'))" unfolding create_graph_def apply (refine_vcg expand_until_propag) by (auto simp add:expand_new_name_expand_init) definition all_subfrmls :: "'a node \ 'a frml set" where "all_subfrmls n \ \(subfrmlsr ` (new n \ old n \ next n))" lemma all_subfrmls__UnionD: assumes "(\x\A. subfrmlsr x) \ B" and "x\A" and "y\subfrmlsr x" shows "y\B" proof - note subfrmlsr_id[of x] also have "subfrmlsr x \ (\x\A. subfrmlsr x)" using assms by auto finally show ?thesis using assms by auto qed lemma expand_all_subfrmls_propag: assumes "all_subfrmls (fst n_ns) \ B \ (\nd\snd n_ns. all_subfrmls nd \ B)" (is "?Q n_ns") shows "expand n_ns \ SPEC (\r. \nd\snd r. all_subfrmls nd \ B)" (is "_ \ SPEC ?P") using assms proof (rule_tac expand_rec_rule[where \="?Q"], simp, intro refine_vcg, goal_cases) case 1 then show ?case proof (simp, rule_tac upd_incoming__ident, goal_cases) case 1 then show ?case by auto next case 2 then show ?case by (simp add: all_subfrmls_def) qed next case 2 then show ?case by (auto simp add: all_subfrmls_def) next case 3 then show ?case by (auto simp add: all_subfrmls_def) next case prems: (4 f) then have step: "\x. ?Q x \ f x \ SPEC ?P" by simp_all from prems show ?case by (rule_tac step) (auto simp add: all_subfrmls_def) next case prems: (5 f _ n ns \) then have goal_assms: "\ \ new n \ \ = true\<^sub>r" by simp from prems have step: "\x. ?Q x \ f x \ SPEC ?P" and Q: "?Q (n, ns)" by simp_all show ?case using Q goal_assms by (rule_tac step) (auto dest: all_subfrmls__UnionD simp add: all_subfrmls_def) next case 6 then show ?case by auto next case prems: (7 f x n ns \) then have goal_assms: "\ \ new n \ (\\ \. \ = \ and\<^sub>r \ \ \ = X\<^sub>r \)" by simp from prems have step: "\x. ?Q x \ f x \ SPEC ?P" and Q: "?Q (n, ns)" by simp_all show ?case using Q goal_assms by (rule_tac step) (auto dest: all_subfrmls__UnionD simp add: all_subfrmls_def) next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ \ (\q. \ = prop\<^sub>r(q) \ \ = nprop\<^sub>r(q)) \ \ \ true\<^sub>r \ \ \ false\<^sub>r \ \ (\\ \. \ = \ and\<^sub>r \ \ \ = X\<^sub>r \) \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have Q: "?Q (n, ns)" and step: "\x. ?Q x \ f x \ SPEC ?P" by simp_all show ?case using goal_assms Q unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_nested2, goal_cases) case 1 then show ?case by (rule_tac step) (auto dest: all_subfrmls__UnionD simp: all_subfrmls_def) next case 2 then show ?case by (rule_tac step) (auto dest: all_subfrmls__UnionD simp: all_subfrmls_def) qed qed lemma old_propag_on_create_graph: "create_graph \ \ SPEC (\nds. \n\nds. old n \ subfrmlsr \)" unfolding create_graph_def by (intro refine_vcg, rule_tac order_trans, rule_tac expand_all_subfrmls_propag[where B = "subfrmlsr \"]) (force simp add:all_subfrmls_def expand_new_name_expand_init)+ lemma L4_2__aux: assumes run: "ipath gba.E \" and "\ U\<^sub>r \ \ old (\ 0)" and "\j. (\i, \ U\<^sub>r \} \ old (\ i)) \ \ \ old (\ j)" shows "\i. {\, \ U\<^sub>r \} \ old (\ i) \ \ \ old (\ i)" proof - have "\i, \ U\<^sub>r \} \ old (\ i)" (is "?sbthm j") for j proof (induct j) show "?sbthm 0" by auto next fix k assume step: "?sbthm k" then have \_k_prop: "\ \ old (\ k) \ \ k\qs \ \ (Suc k)\qs \ name (\ k) \ incoming (\ (Suc k))" using assms run_propag_on_create_graph[OF run] by auto with inres_SPEC[OF res until_propag_on_create_graph[where \ = \ and \ = \]] have "{\, \ U\<^sub>r \} \ old (\ k)" (is "?subsetthm") proof (cases k) assume "k = 0" with assms \_k_prop inres_SPEC[OF res until_propag_on_create_graph[where \ = \ and \ = \]] show ?subsetthm by auto next fix l assume "k = Suc l" then have "{\, \ U\<^sub>r \}\old (\ l) \ \\old (\ l) \ \ l\qs \ \ k\qs \ name (\ l)\incoming (\ k)" using step assms run_propag_on_create_graph[OF run] by auto with inres_SPEC[OF res until_propag_on_create_graph[where \ = \ and \ = \]] have "\ U\<^sub>r \\old (\ k)" by auto with \_k_prop inres_SPEC[OF res until_propag_on_create_graph[where \ = \ and \ = \]] show ?subsetthm by auto qed with step show "?sbthm (Suc k)" by (metis less_SucE) qed with assms show ?thesis by auto qed lemma L4_2a: assumes "ipath gba.E \" and "\ U\<^sub>r \ \ old (\ 0)" shows "(\i. {\, \ U\<^sub>r \} \ old (\ i) \ \ \ old (\ i)) \ (\j. (\i, \ U\<^sub>r \} \ old (\ i)) \ \ \ old (\ j))" (is "?A \ ?B") proof (rule disjCI) assume "\ ?B" then show ?A using assms by (rule_tac L4_2__aux) blast+ qed lemma L4_2b: assumes run: "ipath gba.E \" and "\ U\<^sub>r \ \ old (\ 0)" and ACC: "gba.is_acc \" shows "\j. (\i, \ U\<^sub>r \} \ old (\ i)) \ \ \ old (\ j)" proof (rule ccontr) assume "\ ?thesis" then have contr: "\i. {\, \ U\<^sub>r \}\old(\ i) \ \\old(\ i)" using assms L4_2a[of \ \ \] by blast define S where "S = {q \ qs. \ U\<^sub>r \ \ old q \ \ \ old q}" from assms inres_SPEC[OF res old_propag_on_create_graph] create_gba_from_nodes__ipath have "\ U\<^sub>r \ \ subfrmlsr \" by (metis assms(2) subsetD) then have "S\gbg_F(create_gba_from_nodes \ qs)" unfolding S_def create_gba_from_nodes_def by auto with ACC have 1: "\\<^sub>\i. \ i \ S" unfolding gba.is_acc_def by blast from INFM_EX[OF 1] obtain k where "\ k \ qs" and "\ U\<^sub>r \ \ old (\ k) \ \ \ old (\ k)" unfolding S_def by auto moreover have "{\, \ U\<^sub>r \}\old(\ k) \ \\old(\ k)" using contr by auto ultimately show False by auto qed lemma L4_2c: assumes run: "ipath gba.E \" and "\ R\<^sub>r \ \ old (\ 0)" shows "\i. \ \ old (\ i) \ (\j \ old (\ j))" proof - have "{\, \ R\<^sub>r \} \ old (\ i) \ (\j \ old (\ j))" (is "?thm i") for i proof (induct i) case 0 have "\ 0\qs \ \ 1\qs \ name (\ 0) \ incoming (\ 1)" using create_gba_from_nodes__ipath assms by auto then show ?case using assms inres_SPEC[OF res release_propag_on_create_graph, of \ \] by auto next case (Suc k) note \?thm k\ moreover { assume "{\, \ R\<^sub>r \} \ old (\ k)" moreover have "\ k\qs \ \ (Suc k)\qs \ name (\ k) \ incoming (\ (Suc k))" using create_gba_from_nodes__ipath assms by auto ultimately have "\ \ old (\ k) \ \ R\<^sub>r \ \ old (\ (Suc k))" using assms inres_SPEC[OF res release_propag_on_create_graph, of \ \] by auto moreover { assume "\ \ old (\ k)" then have ?case by blast } moreover { assume "\ R\<^sub>r \ \ old (\ (Suc k))" moreover have "\ (Suc k)\qs \ \ (Suc (Suc k))\qs \ name (\ (Suc k)) \ incoming (\ (Suc (Suc k)))" using create_gba_from_nodes__ipath assms by auto ultimately have ?case using assms inres_SPEC[OF res release_propag_on_create_graph, of \ \] by auto } ultimately have ?case by fast } moreover { assume "\j \ old (\ j)" then have ?case by auto } ultimately show ?case by auto qed then show ?thesis by auto qed lemma L4_8': assumes "ipath gba.E \" (is "?inf_run \") and "gba.is_acc \" (is "?gbarel_accept \") and "\i. gba.L (\ i) (\ i)" (is "?lgbarel_accept \ \") and "\ \ old (\ 0)" shows "\ \\<^sub>r \" using assms proof (induct \ arbitrary: \ \) case True_ltlr show ?case by auto next case False_ltlr then show ?case using inres_SPEC[OF res false_propag_on_create_graph] create_gba_from_nodes__ipath by (metis) next case (Prop_ltlr p) then show ?case unfolding create_gba_from_nodes_def by auto next case (Nprop_ltlr p) then show ?case unfolding create_gba_from_nodes_def by auto next case (And_ltlr \ \) then show ?case using inres_SPEC[OF res and_propag_on_create_graph, of \ \] create_gba_from_nodes__ipath by (metis insert_subset semantics_ltlr.simps(5)) next case (Or_ltlr \ \) then have "\ \ old (\ 0) \ \ \ old (\ 0)" using inres_SPEC[OF res or_propag_on_create_graph, of \ \] create_gba_from_nodes__ipath by (metis (full_types) Int_empty_left Int_insert_left_if0) moreover have "\ \\<^sub>r \" if "\ \ old (\ 0)" using Or_ltlr that by auto moreover have "\ \\<^sub>r \" if "\ \ old (\ 0)" using Or_ltlr that by auto ultimately show ?case by auto next case (Next_ltlr \) with create_gba_from_nodes__ipath[of \] have "\ 0 \ qs \ \ 1 \ qs \ name (\ 0) \ incoming (\ 1)" by auto with inres_SPEC[OF res next_propag_on_create_graph, of \] have "\\old (suffix 1 \ 0)" using Next_ltlr by auto moreover have "?inf_run (suffix 1 \)" and "?gbarel_accept (suffix 1 \)" and "?lgbarel_accept (suffix 1 \) (suffix 1 \ )" using Next_ltlr create_gba_from_nodes__ipath apply - apply (metis ipath_suffix) apply (auto simp del: suffix_nth) [] (* FIXME: "\a. suffix i \ a" is unfolded, but "suffix i \" is not! *) apply auto done ultimately show ?case using Next_ltlr by simp next case (Until_ltlr \ \) then have "\j. (\i, \ U\<^sub>r \} \ old (\ i)) \ \ \ old (\ j)" using L4_2b by auto then obtain j where \_pre: "\i, \ U\<^sub>r \} \ old (\ i)" and "\ \ old (suffix j \ 0)" by auto moreover have "?inf_run (suffix j \)" and "?gbarel_accept (suffix j \)" and "?lgbarel_accept (suffix j \) (suffix j \)" unfolding limit_suffix using Until_ltlr create_gba_from_nodes__ipath apply - apply (metis ipath_suffix) apply (auto simp del: suffix_nth) [] (* FIXME: "\a. suffix i \ a" is unfolded, but "suffix i \" is not! *) apply auto done ultimately have "suffix j \ \\<^sub>r \" using Until_ltlr by simp moreover { fix i assume "i < j" have "?inf_run (suffix i \)" and "?gbarel_accept (suffix i \)" and "?lgbarel_accept (suffix i \) (suffix i \ )" unfolding limit_suffix using Until_ltlr create_gba_from_nodes__ipath apply - apply (metis ipath_suffix) apply (auto simp del: suffix_nth) [] (* FIXME: "\a. suffix i \ a" is unfolded, but "suffix i \" is not! *) apply auto done moreover have "\\old (suffix i \ 0)" using \_pre \i by auto ultimately have "suffix i \ \\<^sub>r \" using Until_ltlr by simp } ultimately show ?case by auto next case (Release_ltlr \ \) { fix i assume "\ \ old (\ i) \ (\j \ old (\ j))" moreover { assume *: "\ \ old (\ i)" have "?inf_run (suffix i \)" and "?gbarel_accept (suffix i \)" and "?lgbarel_accept (suffix i \) (suffix i \ )" unfolding limit_suffix using Release_ltlr create_gba_from_nodes__ipath apply - apply (metis ipath_suffix) apply (auto simp del: suffix_nth) [] (* FIXME: "\a. suffix i \ a" is unfolded, but "suffix i \" is not! *) apply auto done with * have "suffix i \ \\<^sub>r \" using Release_ltlr by auto } moreover { assume "\j \ old (\ j)" then obtain j where "j \ old (\ j)" by auto moreover have "?inf_run (suffix j \)" and "?gbarel_accept (suffix j \)" and "?lgbarel_accept (suffix j \) (suffix j \ )" unfolding limit_suffix using Release_ltlr create_gba_from_nodes__ipath apply - apply (metis ipath_suffix) apply (auto simp del: suffix_nth) [] (* FIXME: "\a. suffix i \ a" is unfolded, but "suffix i \" is not! *) apply auto done ultimately have "suffix j \ \\<^sub>r \" using Release_ltlr by auto then have "\j \\<^sub>r \" using \j by auto } ultimately have "suffix i \ \\<^sub>r \ \ (\j \\<^sub>r \)" by auto } then show ?case using Release_ltlr L4_2c by auto qed lemma L4_8: assumes "gba.is_acc_run \" and "\i. gba.L (\ i) (\ i)" and "\ \ old (\ 0)" shows "\ \\<^sub>r \" using assms unfolding gba.is_acc_run_def gba.is_run_def using L4_8' by blast lemma expand_expand_init_propag: assumes "(\nm\incoming n'. nm < name n') \ name n' \ name (fst n_ns) \ (incoming n' \ incoming (fst n_ns) \ {} \ new n' \ old (fst n_ns) \ new (fst n_ns)) " (is "?Q n_ns") and "\nd\snd n_ns. \nm\incoming n'. nm\incoming nd \ new n' \ old nd" (is "?P (snd n_ns)") shows "expand n_ns \ SPEC (\r. name n'\fst r \ ?P (snd r))" using assms proof (rule_tac expand_rec_rule[where \="\x. ?Q x \ ?P (snd x)"], simp, intro refine_vcg, goal_cases) case prems: (1 f x n ns) then have goal_assms: "new n = {} \ ?Q (n, ns) \ ?P ns" by simp { fix nd nm assume "nd\upd_incoming n ns" and "nm\incoming n'" and "nm\incoming nd" { assume "nd\ns" with goal_assms \nm\incoming n'\ \nm\incoming nd\ have "new n' \ old nd" by auto } moreover { assume "nd\ns" with upd_incoming__elem[OF \nd\upd_incoming n ns\] obtain nd' where "nd'\ns" and nd_eq: "nd = nd'\incoming := incoming n \ incoming nd'\" and old_next_eq: "old nd' = old n \ next nd' = next n" by auto { assume "nm\incoming nd'" with goal_assms \nm\incoming n'\ \nd'\ns\ have "new n' \ old nd" unfolding nd_eq by auto } moreover { assume "nm\incoming n" with nd_eq old_next_eq goal_assms \nm\incoming n'\ have "new n' \ old nd" by auto } ultimately have "new n' \ old nd" using \nm\incoming nd\ nd_eq by auto } ultimately have "new n' \ old nd" by fast } with prems show ?case by auto next case prems: (2 f x n ns) then have goal_assms: "new n = {} \ ?Q (n, ns) \ ?P ns" and step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\r. name n' \ fst r \ ?P (snd r))" by simp_all then show ?case proof (rule_tac step, goal_cases) case prems': 1 have expand_new_name_less: "name n < expand_new_name (name n)" by auto moreover have "name n \ incoming n'" using goal_assms by auto ultimately show ?case using prems' by auto qed next case 3 then show ?case by auto next case prems: (4 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\r. name n' \ fst r \ ?P (snd r))" by simp from prems show ?case by (rule_tac step) auto next case prems: (5 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\r. name n' \ fst r \ ?P (snd r))" by simp from prems show ?case by (rule_tac step) auto next case 6 then show ?case by auto next case prems: (7 f x n ns) then have step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\r. name n' \ fst r \ ?P (snd r))" by simp from prems show ?case by (rule_tac step) auto next case prems: (8 f x n ns \) then have goal_assms: "\ \ new n \ \ (\q. \ = prop\<^sub>r(q) \ \ = nprop\<^sub>r(q)) \ \ \ true\<^sub>r \ \ \ false\<^sub>r \ \ (\\ \. \ = \ and\<^sub>r \ \ \ = X\<^sub>r \) \ (\\ \. \ = \ or\<^sub>r \ \ \ = \ U\<^sub>r \ \ \ = \ R\<^sub>r \)" by (cases \) auto from prems have QP: "?Q (n, ns) \ ?P ns" and step: "\x. ?Q x \ ?P (snd x) \ f x \ SPEC (\r. name n' \ fst r \ ?P (snd r))" by simp_all show ?case using goal_assms QP unfolding case_prod_unfold \x = (n, ns)\ proof (rule_tac SPEC_rule_nested2, goal_cases) case 1 then show ?case by (rule_tac step) auto next case 2 then show ?case by (rule_tac step) auto qed qed lemma expand_init_propag_on_create_graph: "create_graph \ \ SPEC(\nds. \nd\nds. expand_init\incoming nd \ \ \ old nd)" unfolding create_graph_def by (intro refine_vcg, rule_tac order_trans, rule_tac expand_expand_init_propag[where n' = "\ name = expand_new_name expand_init, incoming = {expand_init}, new = {\}, old = {}, next = {} \"]) (auto simp add:expand_new_name_expand_init) lemma L4_6: assumes "q\gba.V0" shows "\\old q" using assms inres_SPEC[OF res expand_init_propag_on_create_graph] unfolding create_gba_from_nodes_def by auto lemma L4_9: assumes acc: "gba.accept \" shows "\ \\<^sub>r \" proof - from acc obtain \ where accept: "gba.is_acc_run \ \ (\i. gba.L (\ i) (\ i))" unfolding gba.accept_def by auto then have "\ 0\gba.V0" unfolding gba.is_acc_run_def gba.is_run_def by simp with L4_6 have "\\old (\ 0)" by auto with L4_8 accept show ?thesis by auto qed lemma L4_10: assumes "\ \\<^sub>r \" shows "gba.accept \" proof - define \ where "\ = auto_run \ qs" let ?G = "create_graph \" have \_prop_0: "(\ 0)\qs \ expand_init\incoming(\ 0) \ auto_run_j 0 \ (\ 0)" (is "?sbthm") using inres_SPEC[OF res L4_7[OF \\ \\<^sub>r \\]] unfolding \_def auto_run.simps by (rule_tac someI_ex, simp) blast have \_valid: "\j. \ j \ qs \ auto_run_j j \ (\ j)" (is "\j. ?\_valid j") proof fix j show "?\_valid j" proof(induct j) from \_prop_0 show "?\_valid 0" by fast next fix k assume goal_assms: "\ k \ qs \ auto_run_j k \ (\ k)" with inres_SPEC[OF res L4_5, of "suffix k \"] have sbthm: "\q'. q'\qs \ name (\ k)\incoming q' \ auto_run_j (Suc k) \ q'" (is "\q'. ?sbthm q'") by auto have "?sbthm (\ (Suc k))" using someI_ex[OF sbthm] unfolding \_def auto_run.simps by blast then show "?\_valid (Suc k)" by fast qed qed have \_prop_Suc: "\k. \ k\ qs \ \ (Suc k)\qs \ name (\ k)\incoming (\ (Suc k)) \ auto_run_j (Suc k) \ (\ (Suc k))" proof - fix k from \_valid have "\ k \ qs" and "auto_run_j k \ (\ k)" by blast+ with inres_SPEC[OF res L4_5, of "suffix k \"] have sbthm: "\q'. q'\qs \ name (\ k)\incoming q' \ auto_run_j (Suc k) \ q'" (is "\q'. ?sbthm q'") by auto show "\ k\ qs \ ?sbthm (\ (Suc k))" using \\ k\qs\ someI_ex[OF sbthm] unfolding \_def auto_run.simps by blast qed have \_vnaccpt: "\k \ \. \ U\<^sub>r \ \ old (\ k) \ \ (\i. {\, \ U\<^sub>r \} \ old (\ (k+i)) \ \ \ old (\ (k+i)))" proof clarify fix k \ \ assume U_in: "\ U\<^sub>r \ \ old (\ k)" and cntr_prm: "\i. {\, \ U\<^sub>r \} \ old (\ (k+i)) \ \ \ old (\ (k+i))" have "suffix k \ \\<^sub>r \ U\<^sub>r \" using U_in \_valid by force then obtain i where "suffix (k+i) \ \\<^sub>r \" and "\j \\<^sub>r \" by auto moreover have "\ U\<^sub>r \ \ old (\ (k+i)) \ \ \ old (\ (k+i))" using cntr_prm by auto ultimately show False using \_valid by force qed have \_exec: "gba.is_run \" using \_prop_0 \_prop_Suc \_valid unfolding gba.is_run_def ipath_def unfolding create_gba_from_nodes_def by auto moreover have \_vaccpt: "\k \ \. \ U\<^sub>r \ \ old (\ k) \ (\j. (\i, \ U\<^sub>r \} \ old (\ (k+i))) \ \ \ old (\ (k+j)))" proof(clarify) fix k \ \ assume U_in: "\ U\<^sub>r \ \ old (\ k)" then have "\ (\i. {\, \ U\<^sub>r \} \ old (suffix k \ i) \ \ \ old (suffix k \ i))" using \_vnaccpt[THEN allE, of k] by auto moreover have "suffix k \ 0 \ qs" using \_valid by auto ultimately show "\j. (\i, \ U\<^sub>r \} \ old (\ (k+i))) \ \ \ old (\ (k+j))" apply - apply (rule make_pos_rule'[OF L4_2a]) apply (fold suffix_def) apply (rule ipath_suffix) using \_exec[unfolded gba.is_run_def] apply simp using U_in apply simp apply simp done qed have "gba.is_acc \" unfolding gba.is_acc_def proof fix S assume "S\gba.F" then obtain \ \ where S_eq: "S = {q \ qs. \ U\<^sub>r \ \ old q \ \ \ old q}" and "\ U\<^sub>r \ \ subfrmlsr \" by (auto simp add: create_gba_from_nodes_def) have range_subset: "range \ \ qs" proof fix q assume "q\range \" with full_SetCompr_eq[of \] obtain k where "q = \ k" by auto then show "q \ qs" using \_valid by auto qed with limit_nonempty[of \] limit_in_range[of \] finite_subset[OF range_subset] inres_SPEC[OF res create_graph_finite] obtain q where q_in_limit: "q \ limit \" and q_is_node: "q\qs" by auto show "\\<^sub>\i. \ i \ S" proof (cases "\ U\<^sub>r \ \ old q") case False with S_eq q_in_limit q_is_node show ?thesis by (auto simp: limit_iff_frequent intro: INFM_mono) next case True obtain k where q_eq: "q = \ k" using q_in_limit unfolding limit_iff_frequent by (metis (lifting, full_types) INFM_nat_le) have "\\<^sub>\ k. \ \ old (\ k)" unfolding INFM_nat proof (rule ccontr) assume "\ (\m. \n>m. \ \ old (\ n))" then obtain m where "\n>m. \ \ old (\ n)" by auto moreover from q_eq q_in_limit limit_iff_frequent[of q \] INFM_nat[of "\n. \ n = q"] obtain n where "mn_eq: "\ n = \ k" by auto moreover obtain j where "\ \ old (\ (n+j))" using \_vaccpt \\ U\<^sub>r \ \ old q\ unfolding q_eq by (fold \n_eq) force ultimately show False by auto qed then have "\\<^sub>\ k. \ k \ qs \ \ \ old (\ k)" using \_valid by (auto intro: INF_mono) then show "\\<^sub>\ k. \ k \ S" unfolding S_eq by (rule INFM_mono) simp qed qed moreover have "gba.L (\ i) (\ i)" for i proof - from \_valid have [simp]: "\ i \ qs" by auto have "\\\old (\ i). suffix i \ \\<^sub>r \" using \_valid by auto then show ?thesis unfolding create_gba_from_nodes_def by auto qed ultimately show ?thesis unfolding gba.accept_def gba.is_acc_run_def by blast qed end end lemma create_graph__name_ident: "create_graph \ \ SPEC (\nds. \q\nds. \!q'\nds. name q = name q')" unfolding create_graph_def apply (refine_vcg expand_name_propag__name_ident) by (auto simp add:expand_new_name_expand_init) corollary create_graph__name_inj: "create_graph \ \ SPEC (\nds. inj_on name nds)" by (rule order_trans[OF create_graph__name_ident]) (auto intro: inj_onI) definition "create_gba \ \ do { nds \ create_graph\<^sub>T \; RETURN (create_gba_from_nodes \ nds) }" lemma create_graph_precond: "create_graph \ \ SPEC (create_gba_from_nodes_precond \)" apply (clarsimp simp: pw_le_iff create_graph_nofail) apply unfold_locales apply simp done lemma create_gba__invar: "create_gba \ \ SPEC gba" unfolding create_gba_def create_graph_eq_create_graph\<^sub>T[symmetric] apply (refine_rcg refine_vcg order_trans[OF create_graph_precond]) by (rule create_gba_from_nodes_precond.create_gba_from_nodes__invar) lemma create_gba_acc: shows "create_gba \ \ SPEC(\\. \\. gba.accept \ \ \ \ \\<^sub>r \)" unfolding create_gba_def create_graph_eq_create_graph\<^sub>T[symmetric] apply (refine_rcg refine_vcg order_trans[OF create_graph_precond]) using create_gba_from_nodes_precond.L4_9 using create_gba_from_nodes_precond.L4_10 by blast lemma create_gba__name_inj: shows "create_gba \ \ SPEC(\\. (inj_on name (g_V \)))" unfolding create_gba_def create_graph_eq_create_graph\<^sub>T[symmetric] apply (refine_rcg refine_vcg order_trans[OF create_graph__name_inj]) apply (auto simp: create_gba_from_nodes_def) done lemma create_gba__fin: shows "create_gba \ \ SPEC(\\. (finite (g_V \)))" unfolding create_gba_def create_graph_eq_create_graph\<^sub>T[symmetric] apply (refine_rcg refine_vcg order_trans[OF create_graph_finite]) apply (auto simp: create_gba_from_nodes_def) done lemma create_graph_old_finite: "create_graph \ \ SPEC (\nds. \nd\nds. finite (old nd))" proof - show ?thesis unfolding create_graph_def create_graph_eq_create_graph\<^sub>T[symmetric] unfolding expand_def apply (intro refine_vcg) apply (rule_tac order_trans) apply (rule_tac REC_le_RECT) apply (fold expand\<^sub>T_def) apply (rule_tac order_trans[OF expand_term_prop]) apply auto[1] apply (rule_tac SPEC_rule) apply auto by (metis infinite_super subfrmlsr_finite) qed lemma create_gba__old_fin: shows "create_gba \ \ SPEC(\\. \nd\g_V \. finite (old nd))" unfolding create_gba_def create_graph_eq_create_graph\<^sub>T[symmetric] apply (refine_rcg refine_vcg order_trans[OF create_graph_old_finite]) apply (simp add: create_gba_from_nodes_def) done lemma create_gba__incoming_exists: shows "create_gba \ \ SPEC(\\. \nd\g_V \. incoming nd \ insert expand_init (name ` (g_V \)))" unfolding create_gba_def create_graph_eq_create_graph\<^sub>T[symmetric] apply (refine_rcg refine_vcg order_trans[OF create_graph__incoming_name_exist]) apply (auto simp add: create_gba_from_nodes_def) done lemma create_gba__no_init: shows "create_gba \ \ SPEC(\\. expand_init \ name ` (g_V \))" unfolding create_gba_def create_graph_eq_create_graph\<^sub>T[symmetric] apply (refine_rcg refine_vcg order_trans[OF create_graph__incoming_name_exist]) apply (auto simp add: create_gba_from_nodes_def) done definition "nds_invars nds \ inj_on name nds \ finite nds \ expand_init \ name`nds \ (\nd\nds. finite (old nd) \ incoming nd \ insert expand_init (name ` nds))" lemma create_gba_nds_invars: "create_gba \ \ SPEC (\\. nds_invars (g_V \))" using create_gba__name_inj[of \] create_gba__fin[of \] create_gba__old_fin[of \] create_gba__incoming_exists[of \] create_gba__no_init[of \] unfolding nds_invars_def by (simp add: pw_le_iff) theorem T4_1: "create_gba \ \ SPEC( \\. gba \ \ finite (g_V \) \ (\\. gba.accept \ \ \ \ \\<^sub>r \) \ (nds_invars (g_V \)))" using create_gba__invar create_gba__fin create_gba_acc create_gba_nds_invars apply (simp add: pw_le_iff) apply blast done definition "create_name_gba \ \ do { G \ create_gba \; ASSERT (nds_invars (g_V G)); RETURN (gba_rename name G) }" theorem create_name_gba_correct: "create_name_gba \ \ SPEC(\\. gba \ \ finite (g_V \) \ (\\. gba.accept \ \ \ \ \\<^sub>r \))" unfolding create_name_gba_def apply (refine_rcg refine_vcg order_trans[OF T4_1]) apply (simp_all add: nds_invars_def gba_rename_correct) done definition create_name_igba :: "'a::linorder ltlr \ _" where "create_name_igba \ \ do { A \ create_name_gba \; A' \ gba_to_idx A; stat_set_data_nres (card (g_V A)) (card (g_V0 A')) (igbg_num_acc A'); RETURN A' }" lemma create_name_igba_correct: "create_name_igba \ \ SPEC (\G. igba G \ finite (g_V G) \ (\\. igba.accept G \ \ \ \\<^sub>r \))" unfolding create_name_igba_def apply (refine_rcg order_trans[OF create_name_gba_correct] order_trans[OF gba.gba_to_idx_ext_correct] refine_vcg) apply clarsimp_all proof - fix G :: "(nat, 'a set) gba_rec" fix A :: "nat set" assume 1: "gba G" assume 2: "finite (g_V G)" "A \ gbg_F G" interpret gba G using 1 . show "finite A" using finite_V_Fe 2 . qed (* For presentation in paper*) context notes [refine_vcg] = order_trans[OF create_name_gba_correct] begin lemma "create_name_igba \ \ SPEC (\G. igba G \ (\\. igba.accept G \ \ \ \\<^sub>r \))" unfolding create_name_igba_def proof (refine_rcg refine_vcg, clarsimp_all) fix G :: "(nat, 'a set) gba_rec" assume "gba G" then interpret gba G . note [refine_vcg] = order_trans[OF gba_to_idx_ext_correct] assume "\\. gba.accept G \ = \ \\<^sub>r \" "finite (g_V G)" then show "gba_to_idx G \ SPEC (\G'. igba G' \ (\\. igba.accept G' \ = \ \\<^sub>r \))" by (refine_rcg refine_vcg) (auto intro: finite_V_Fe) qed end end diff --git a/thys/Nested_Multisets_Ordinals/Nested_Multiset.thy b/thys/Nested_Multisets_Ordinals/Nested_Multiset.thy --- a/thys/Nested_Multisets_Ordinals/Nested_Multiset.thy +++ b/thys/Nested_Multisets_Ordinals/Nested_Multiset.thy @@ -1,408 +1,411 @@ (* Title: Nested Multisets Author: Dmitriy Traytel , 2016 Author: Jasmin Blanchette , 2016 Maintainer: Dmitriy Traytel *) section \Nested Multisets\ theory Nested_Multiset imports "HOL-Library.Multiset_Order" begin declare multiset.map_comp [simp] declare multiset.map_cong [cong] subsection \Type Definition\ datatype 'a nmultiset = Elem 'a | MSet "'a nmultiset multiset" inductive no_elem :: "'a nmultiset \ bool" where "(\X. X \# M \ no_elem X) \ no_elem (MSet M)" inductive_set sub_nmset :: "('a nmultiset \ 'a nmultiset) set" where "X \# M \ (X, MSet M) \ sub_nmset" lemma wf_sub_nmset[simp]: "wf sub_nmset" proof (rule wfUNIVI) fix P :: "'a nmultiset \ bool" and M :: "'a nmultiset" assume IH: "\M. (\N. (N, M) \ sub_nmset \ P N) \ P M" show "P M" by (induct M; rule IH[rule_format]) (auto simp: sub_nmset.simps) qed primrec depth_nmset :: "'a nmultiset \ nat" ("|_|") where "|Elem a| = 0" | "|MSet M| = (let X = set_mset (image_mset depth_nmset M) in if X = {} then 0 else Suc (Max X))" lemma depth_nmset_MSet: "x \# M \ |x| < |MSet M|" by (auto simp: less_Suc_eq_le) declare depth_nmset.simps(2)[simp del] subsection \Dershowitz and Manna's Nested Multiset Order\ text \The Dershowitz--Manna extension:\ definition less_multiset_ext\<^sub>D\<^sub>M :: "('a \ 'a \ bool) \ 'a multiset \ 'a multiset \ bool" where "less_multiset_ext\<^sub>D\<^sub>M R M N \ (\X Y. X \ {#} \ X \# N \ M = (N - X) + Y \ (\k. k \# Y \ (\a. a \# X \ R k a)))" lemma less_multiset_ext\<^sub>D\<^sub>M_imp_mult: assumes N_A: "set_mset N \ A" and M_A: "set_mset M \ A" and less: "less_multiset_ext\<^sub>D\<^sub>M R M N" shows "(M, N) \ mult {(x, y). x \ A \ y \ A \ R x y}" proof - from less obtain X Y where "X \ {#}" and "X \# N" and "M = N - X + Y" and "\k. k \# Y \ (\a. a \# X \ R k a)" unfolding less_multiset_ext\<^sub>D\<^sub>M_def by blast with N_A M_A have "(N - X + Y, N - X + X) \ mult {(x, y). x \ A \ y \ A \ R x y}" by (intro one_step_implies_mult, blast, metis (mono_tags, lifting) case_prodI mem_Collect_eq mset_subset_eqD mset_subset_eq_add_right subsetCE) with \M = N - X + Y\ \X \# N\ show "(M, N) \ mult {(x, y). x \ A \ y \ A \ R x y}" by (simp add: subset_mset.diff_add) qed lemma mult_imp_less_multiset_ext\<^sub>D\<^sub>M: assumes N_A: "set_mset N \ A" and M_A: "set_mset M \ A" and trans: "\x \ A. \y \ A. \z \ A. R x y \ R y z \ R x z" and in_mult: "(M, N) \ mult {(x, y). x \ A \ y \ A \ R x y}" shows "less_multiset_ext\<^sub>D\<^sub>M R M N" using in_mult N_A M_A unfolding mult_def less_multiset_ext\<^sub>D\<^sub>M_def proof induct case (base N) then obtain y M0 X where "N = add_mset y M0" and "M = M0 + X" and "\a. a \# X \ R a y" unfolding mult1_def by auto thus ?case by (auto intro: exI[of _ "{#y#}"]) next case (step N N') note N_N'_in_mult1 = this(2) and ih = this(3) and N'_A = this(4) and M_A = this(5) have N_A: "set_mset N \ A" using N_N'_in_mult1 N'_A unfolding mult1_def by auto obtain Y X where y_nemp: "Y \ {#}" and y_sub_N: "Y \# N" and M_eq: "M = N - Y + X" and ex_y: "\x. x \# X \ (\y. y \# Y \ R x y)" using ih[OF N_A M_A] by blast obtain z M0 Ya where N'_eq: "N' = M0 + {#z#}" and N_eq: "N = M0 + Ya" and z_gt: "\y. y \# Ya \ y \ A \ z \ A \ R y z" using N_N'_in_mult1[unfolded mult1_def] by auto let ?Za = "Y - Ya + {#z#}" let ?Xa = "X + Ya + (Y - Ya) - Y" have xa_sub_x_ya: "set_mset ?Xa \ set_mset (X + Ya)" by (metis diff_subset_eq_self in_diffD subsetI subset_mset.diff_diff_right) have x_A: "set_mset X \ A" using M_A M_eq by auto have ya_A: "set_mset Ya \ A" by (simp add: subsetI z_gt) have ex_y': "\y. y \# Y - Ya + {#z#} \ R x y" if x_in: "x \# X + Ya" for x proof (cases "x \# X") case True then obtain y where y_in: "y \# Y" and y_gt_x: "R x y" using ex_y by blast show ?thesis proof (cases "y \# Ya") case False hence "y \# Y - Ya + {#z#}" using y_in count_greater_zero_iff in_diff_count by fastforce thus ?thesis using y_gt_x by blast next case True hence "y \ A" and "z \ A" and "R y z" using z_gt by blast+ hence "R x z" using trans y_gt_x x_A ya_A x_in by (meson subsetCE union_iff) thus ?thesis by auto qed next case False hence "x \# Ya" using x_in by auto hence "x \ A" and "z \ A" and "R x z" using z_gt by blast+ thus ?thesis by auto qed show ?case proof (rule exI[of _ ?Za], rule exI[of _ ?Xa], intro conjI) show "Y - Ya + {#z#} \# N'" using mset_subset_eq_mono_add subset_eq_diff_conv y_sub_N N_eq N'_eq by (simp add: subset_eq_diff_conv) next show "M = N' - (Y - Ya + {#z#}) + (X + Ya + (Y - Ya) - Y)" unfolding M_eq N_eq N'_eq by (auto simp: multiset_eq_iff) next show "\x. x \# X + Ya + (Y - Ya) - Y \ (\y. y \# Y - Ya + {#z#} \ R x y)" using ex_y' xa_sub_x_ya by blast qed auto qed lemma less_multiset_ext\<^sub>D\<^sub>M_iff_mult: assumes N_A: "set_mset N \ A" and M_A: "set_mset M \ A" and trans: "\x \ A. \y \ A. \z \ A. R x y \ R y z \ R x z" shows "less_multiset_ext\<^sub>D\<^sub>M R M N \ (M, N) \ mult {(x, y). x \ A \ y \ A \ R x y}" using mult_imp_less_multiset_ext\<^sub>D\<^sub>M[OF assms] less_multiset_ext\<^sub>D\<^sub>M_imp_mult[OF N_A M_A] by blast +lemma sub_nmset_lex: "((a,b),(c,d)) \ sub_nmset <*lex*> sub_nmset \ (a,c) \ sub_nmset \ a=c \ (b,d) \ sub_nmset" + by auto + instantiation nmultiset :: (preorder) preorder begin lemma less_multiset_ext\<^sub>D\<^sub>M_cong[fundef_cong]: "(\X Y k a. X \ {#} \ X \# N \ M = (N - X) + Y \ k \# Y \ R k a = S k a) \ less_multiset_ext\<^sub>D\<^sub>M R M N = less_multiset_ext\<^sub>D\<^sub>M S M N" unfolding less_multiset_ext\<^sub>D\<^sub>M_def by metis function less_nmultiset :: "'a nmultiset \ 'a nmultiset \ bool" where "less_nmultiset (Elem a) (Elem b) \ a < b" | "less_nmultiset (Elem a) (MSet M) \ True" | "less_nmultiset (MSet M) (Elem a) \ False" | "less_nmultiset (MSet M) (MSet N) \ less_multiset_ext\<^sub>D\<^sub>M less_nmultiset M N" by pat_completeness auto termination - by (relation "sub_nmset <*lex*> sub_nmset", fastforce, - metis sub_nmset.simps in_lex_prod mset_subset_eqD mset_subset_eq_add_right) + apply(relation "sub_nmset <*lex*> sub_nmset", force) + by (meson sub_nmset_lex sub_nmset.intros union_iff) lemmas less_nmultiset_induct = less_nmultiset.induct[case_names Elem_Elem Elem_MSet MSet_Elem MSet_MSet] lemmas less_nmultiset_cases = less_nmultiset.cases[case_names Elem_Elem Elem_MSet MSet_Elem MSet_MSet] lemma trans_less_nmultiset: "X < Y \ Y < Z \ X < Z" for X Y Z :: "'a nmultiset" proof (induct "Max {|X|, |Y|, |Z|}" arbitrary: X Y Z rule: less_induct) case less from less(2,3) show ?case proof (cases X; cases Y; cases Z) fix M N N' :: "'a nmultiset multiset" define A where "A = set_mset M \ set_mset N \ set_mset N'" assume XYZ: "X = MSet M" "Y = MSet N" "Z = MSet N'" then have trans: "\x \ A. \y \ A. \z \ A. x < y \ y < z \ x < z" by (auto elim!: less(1)[rotated -1] dest!: depth_nmset_MSet simp add: A_def) have "set_mset M \ A" "set_mset N \ A" "set_mset N' \ A" unfolding A_def by auto with less(2,3) XYZ show "X < Z" by (auto simp: less_multiset_ext\<^sub>D\<^sub>M_iff_mult[OF _ _ trans] mult_def) qed (auto elim: less_trans) qed lemma irrefl_less_nmultiset: fixes X :: "'a nmultiset" shows "X < X \ False" proof (induct X) case (MSet M) from MSet(2) show ?case unfolding less_nmultiset.simps less_multiset_ext\<^sub>D\<^sub>M_def proof safe fix X Y :: "'a nmultiset multiset" define XY where "XY = {(x, y). x \# X \ y \# Y \ y < x}" then have fin: "finite XY" and trans: "trans XY" by (auto simp: trans_def intro: trans_less_nmultiset finite_subset[OF _ finite_cartesian_product]) assume "X \ {#}" "X \# M" "M = M - X + Y" then have "X = Y" by (auto simp: mset_subset_eq_exists_conv) with MSet(1) \X \# M\ have "irrefl XY" unfolding XY_def by (force dest: mset_subset_eqD simp: irrefl_def) with trans have "acyclic XY" by (simp add: acyclic_irrefl) moreover assume "\k. k \# Y \ (\a. a \# X \ k < a)" with \X = Y\ \X \ {#}\ have "\ acyclic XY" by (intro notI, elim finite_acyclic_wf[OF fin, elim_format]) (auto dest!: spec[of _ "set_mset Y"] simp: wf_eq_minimal XY_def) ultimately show False by blast qed qed simp lemma antisym_less_nmultiset: fixes X Y :: "'a nmultiset" shows "X < Y \ Y < X \ False" using trans_less_nmultiset irrefl_less_nmultiset by blast definition less_eq_nmultiset :: "'a nmultiset \ 'a nmultiset \ bool" where "less_eq_nmultiset X Y = (X < Y \ X = Y)" instance proof (intro_classes, goal_cases less_def refl trans) case (less_def x y) then show ?case unfolding less_eq_nmultiset_def by (metis irrefl_less_nmultiset antisym_less_nmultiset) next case (refl x) then show ?case unfolding less_eq_nmultiset_def by blast next case (trans x y z) then show ?case unfolding less_eq_nmultiset_def by (metis trans_less_nmultiset) qed lemma less_multiset_ext\<^sub>D\<^sub>M_less: "less_multiset_ext\<^sub>D\<^sub>M (<) = (<)" unfolding fun_eq_iff less_multiset_ext\<^sub>D\<^sub>M_def less_multiset\<^sub>D\<^sub>M by blast end instantiation nmultiset :: (order) order begin instance proof (intro_classes, goal_cases antisym) case (antisym x y) then show ?case unfolding less_eq_nmultiset_def by (metis trans_less_nmultiset irrefl_less_nmultiset) qed end instantiation nmultiset :: (linorder) linorder begin lemma total_less_nmultiset: fixes X Y :: "'a nmultiset" shows "\ X < Y \ Y \ X \ Y < X" proof (induct X Y rule: less_nmultiset_induct) case (MSet_MSet M N) then show ?case unfolding nmultiset.inject less_nmultiset.simps less_multiset_ext\<^sub>D\<^sub>M_less less_multiset\<^sub>H\<^sub>O by (metis add_diff_cancel_left' count_inI diff_add_zero in_diff_count less_imp_not_less mset_subset_eq_multiset_union_diff_commute subset_mset.order.refl) qed auto instance proof (intro_classes, goal_cases total) case (total x y) then show ?case unfolding less_eq_nmultiset_def by (metis total_less_nmultiset) qed end lemma less_depth_nmset_imp_less_nmultiset: "|X| < |Y| \ X < Y" proof (induct X Y rule: less_nmultiset_induct) case (MSet_MSet M N) then show ?case proof (cases "M = {#}") case False with MSet_MSet show ?thesis by (auto 0 4 simp: depth_nmset.simps(2) less_multiset_ext\<^sub>D\<^sub>M_def not_le Max_gr_iff intro: exI[of _ N] split: if_splits) qed (auto simp: depth_nmset.simps(2) less_multiset_ext\<^sub>D\<^sub>M_less split: if_splits) qed simp_all lemma less_nmultiset_imp_le_depth_nmset: "X < Y \ |X| \ |Y|" proof (induct X Y rule: less_nmultiset_induct) case (MSet_MSet M N) then have "M < N" by (simp add: less_multiset_ext\<^sub>D\<^sub>M_less) then show ?case proof (cases "M = {#}" "N = {#}" rule: bool.exhaust[case_product bool.exhaust]) case [simp]: False_False show ?thesis unfolding depth_nmset.simps(2) Let_def False_False Suc_le_mono set_image_mset image_is_empty set_mset_eq_empty_iff if_False proof (intro iffD2[OF Max_le_iff] ballI iffD2[OF Max_ge_iff]; (elim imageE)?; simp) fix X assume [simp]: "X \# M" with MSet_MSet(1)[of N M X, simplified] \M < N\ show "\Y\#N. |X| \ |Y|" by (meson ex_gt_imp_less_multiset less_asym' less_depth_nmset_imp_less_nmultiset not_le_imp_less) qed qed (auto simp: depth_nmset.simps(2)) qed simp_all lemma eq_mlex_I: fixes f :: "'a \ nat" and R :: "'a \ 'a \ bool" assumes "\X Y. f X < f Y \ R X Y" and "antisymp R" shows "{(X, Y). R X Y} = f <*mlex*> {(X, Y). f X = f Y \ R X Y}" proof safe fix X Y assume "R X Y" show "(X, Y) \ f <*mlex*> {(X, Y). f X = f Y \ R X Y}" proof (cases "f X" "f Y" rule: linorder_cases) case less with \R X Y\ show ?thesis by (elim mlex_less) next case equal with \R X Y\ show ?thesis by (intro mlex_leq) auto next case greater from \R X Y\ assms(1)[OF greater] \antisymp R\ greater show ?thesis unfolding antisymp_def by auto qed next fix X Y assume "(X, Y) \ f <*mlex*> {(X, Y). f X = f Y \ R X Y}" then show "R X Y" unfolding mlex_prod_def by (auto simp: assms(1)) qed instantiation nmultiset :: (wellorder) wellorder begin lemma depth_nmset_eq_0[simp]: "|X| = 0 \ (X = MSet {#} \ (\x. X = Elem x))" by (cases X; simp add: depth_nmset.simps(2)) lemma depth_nmset_eq_Suc[simp]: "|X| = Suc n \ (\N. X = MSet N \ (\Y \# N. |Y| = n) \ (\Y \# N. |Y| \ n))" by (cases X; auto simp add: depth_nmset.simps(2) intro!: Max_eqI) (metis (no_types, lifting) Max_in finite_imageI finite_set_mset imageE image_is_empty set_mset_eq_empty_iff) lemma wf_less_nmultiset_depth: "wf {(X :: 'a nmultiset, Y). |X| = i \ |Y| = i \ X < Y}" proof (induct i rule: less_induct) case (less i) define A :: "'a nmultiset set" where "A = {X. |X| < i}" from less have "wf ((depth_nmset :: 'a nmultiset \ nat) <*mlex*> (\j < i. {(X, Y). |X| = j \ |Y| = j \ X < Y}))" by (intro wf_UN wf_mlex) auto then have *: "wf (mult {(X :: 'a nmultiset, Y). X \ A \ Y \ A \ X < Y})" by (intro wf_mult, elim wf_subset) (force simp: A_def mlex_prod_def not_less_iff_gr_or_eq dest!: less_depth_nmset_imp_less_nmultiset) show ?case proof (cases i) case 0 then show ?thesis by (auto simp: inj_on_def intro!: wf_subset[OF wf_Un[OF wf_map_prod_image[OF wf, of Elem] wf_UN[of "Elem ` UNIV" "\x. {(x, MSet {#})}"]]]) next case (Suc n) then show ?thesis by (intro wf_subset[OF wf_map_prod_image[OF *, of MSet]]) (auto 0 4 simp: map_prod_def image_iff inj_on_def A_def dest!: less_multiset_ext\<^sub>D\<^sub>M_imp_mult[of _ A, rotated -1] split: prod.splits) qed qed lemma wf_less_nmultiset: "wf {(X :: 'a nmultiset, Y :: 'a nmultiset). X < Y}" (is "wf ?R") proof - have "?R = depth_nmset <*mlex*> {(X, Y). |X| = |Y| \ X < Y}" by (rule eq_mlex_I) (auto simp: antisymp_def less_depth_nmset_imp_less_nmultiset) also have "{(X, Y). |X| = |Y| \ X < Y} = (\i. {(X, Y). |X| = i \ |Y| = i \ X < Y})" by auto finally show ?thesis by (fastforce intro: wf_mlex wf_Union wf_less_nmultiset_depth) qed instance using wf_less_nmultiset unfolding wf_def mem_Collect_eq prod.case by intro_classes metis end end diff --git a/thys/UTP/toolkit/List_Extra.thy b/thys/UTP/toolkit/List_Extra.thy --- a/thys/UTP/toolkit/List_Extra.thy +++ b/thys/UTP/toolkit/List_Extra.thy @@ -1,890 +1,869 @@ (******************************************************************************) (* Project: Isabelle/UTP Toolkit *) (* File: List_Extra.thy *) (* Authors: Simon Foster and Frank Zeyda *) (* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *) (******************************************************************************) section \ Lists: extra functions and properties \ theory List_Extra imports "HOL-Library.Sublist" "HOL-Library.Monad_Syntax" "HOL-Library.Prefix_Order" "Optics.Lens_Instances" begin subsection \ Useful Abbreviations \ abbreviation "list_sum xs \ foldr (+) xs 0" subsection \ Folds \ context abel_semigroup begin lemma foldr_snoc: "foldr (\<^bold>*) (xs @ [x]) k = (foldr (\<^bold>*) xs k) \<^bold>* x" by (induct xs, simp_all add: commute left_commute) end subsection \ List Lookup \ text \ The following variant of the standard \nth\ function returns \\\ if the index is out of range. \ primrec nth_el :: "'a list \ nat \ 'a option" ("_\_\\<^sub>l" [90, 0] 91) where "[]\i\\<^sub>l = None" | "(x # xs)\i\\<^sub>l = (case i of 0 \ Some x | Suc j \ xs \j\\<^sub>l)" lemma nth_el_appendl[simp]: "i < length xs \ (xs @ ys)\i\\<^sub>l = xs\i\\<^sub>l" apply (induct xs arbitrary: i) apply simp apply (case_tac i) apply simp_all done lemma nth_el_appendr[simp]: "length xs \ i \ (xs @ ys)\i\\<^sub>l = ys\i - length xs\\<^sub>l" apply (induct xs arbitrary: i) apply simp apply (case_tac i) apply simp_all done subsection \ Extra List Theorems \ subsubsection \ Map \ lemma map_nth_Cons_atLeastLessThan: "map (nth (x # xs)) [Suc m.. Suc" by auto hence "map (nth xs) [m.. Suc) [m.. Sorted Lists \ lemma sorted_last [simp]: "\ x \ set xs; sorted xs \ \ x \ last xs" by (induct xs, auto) lemma sorted_prefix: assumes "xs \ ys" "sorted ys" shows "sorted xs" proof - obtain zs where "ys = xs @ zs" using Prefix_Order.prefixE assms(1) by auto thus ?thesis using assms(2) sorted_append by blast qed lemma sorted_map: "\ sorted xs; mono f \ \ sorted (map f xs)" by (simp add: monoD sorted_iff_nth_mono) lemma sorted_distinct [intro]: "\ sorted (xs); distinct(xs) \ \ (\ i Is the given list a permutation of the given set? \ definition is_sorted_list_of_set :: "('a::ord) set \ 'a list \ bool" where "is_sorted_list_of_set A xs = ((\ i set(xs) = A)" lemma sorted_is_sorted_list_of_set: assumes "is_sorted_list_of_set A xs" shows "sorted(xs)" and "distinct(xs)" using assms proof (induct xs arbitrary: A) show "sorted []" by auto next show "distinct []" by auto next fix A :: "'a set" case (Cons x xs) note hyps = this assume isl: "is_sorted_list_of_set A (x # xs)" hence srt: "(\in. \ n < length (x # xs) - 1 \ (x # xs) ! n < (x # xs) ! (n + 1)) \ set (x # xs) = A" by (meson \is_sorted_list_of_set A (x # xs)\ is_sorted_list_of_set_def) then show ?thesis by (metis \distinct xs\ add.commute add_diff_cancel_left' distinct.simps(2) leD length_Cons length_greater_0_conv length_pos_if_in_set less_le nth_Cons_0 nth_Cons_Suc plus_1_eq_Suc set_ConsD sorted.elims(2) srtd) qed qed lemma is_sorted_list_of_set_alt_def: "is_sorted_list_of_set A xs \ sorted (xs) \ distinct (xs) \ set(xs) = A" apply (auto intro: sorted_is_sorted_list_of_set) apply (auto simp add: is_sorted_list_of_set_def) apply (metis Nat.add_0_right One_nat_def add_Suc_right sorted_distinct) done definition sorted_list_of_set_alt :: "('a::ord) set \ 'a list" where "sorted_list_of_set_alt A = (if (A = {}) then [] else (THE xs. is_sorted_list_of_set A xs))" lemma is_sorted_list_of_set: "finite A \ is_sorted_list_of_set A (sorted_list_of_set A)" by (simp add: is_sorted_list_of_set_alt_def) lemma sorted_list_of_set_other_def: "finite A \ sorted_list_of_set(A) = (THE xs. sorted(xs) \ distinct(xs) \ set xs = A)" apply (rule sym) apply (rule the_equality) apply (auto) apply (simp add: sorted_distinct_set_unique) done lemma sorted_list_of_set_alt [simp]: "finite A \ sorted_list_of_set_alt(A) = sorted_list_of_set(A)" apply (rule sym) apply (auto simp add: sorted_list_of_set_alt_def is_sorted_list_of_set_alt_def sorted_list_of_set_other_def) done text \ Sorting lists according to a relation \ definition is_sorted_list_of_set_by :: "'a rel \ 'a set \ 'a list \ bool" where "is_sorted_list_of_set_by R A xs = ((\ i R) \ set(xs) = A)" definition sorted_list_of_set_by :: "'a rel \ 'a set \ 'a list" where "sorted_list_of_set_by R A = (THE xs. is_sorted_list_of_set_by R A xs)" definition fin_set_lexord :: "'a rel \ 'a set rel" where "fin_set_lexord R = {(A, B). finite A \ finite B \ (\ xs ys. is_sorted_list_of_set_by R A xs \ is_sorted_list_of_set_by R B ys \ (xs, ys) \ lexord R)}" lemma is_sorted_list_of_set_by_mono: "\ R \ S; is_sorted_list_of_set_by R A xs \ \ is_sorted_list_of_set_by S A xs" by (auto simp add: is_sorted_list_of_set_by_def) lemma lexord_mono': "\ (\ x y. f x y \ g x y); (xs, ys) \ lexord {(x, y). f x y} \ \ (xs, ys) \ lexord {(x, y). g x y}" by (metis case_prodD case_prodI lexord_take_index_conv mem_Collect_eq) lemma fin_set_lexord_mono [mono]: "(\ x y. f x y \ g x y) \ (xs, ys) \ fin_set_lexord {(x, y). f x y} \ (xs, ys) \ fin_set_lexord {(x, y). g x y}" proof assume fin: "(xs, ys) \ fin_set_lexord {(x, y). f x y}" and hyp: "(\ x y. f x y \ g x y)" from fin have "finite xs" "finite ys" using fin_set_lexord_def by fastforce+ with fin hyp show "(xs, ys) \ fin_set_lexord {(x, y). g x y}" apply (auto simp add: fin_set_lexord_def) apply (rename_tac xs' ys') apply (rule_tac x="xs'" in exI) apply (auto) apply (metis case_prodD case_prodI is_sorted_list_of_set_by_def mem_Collect_eq) apply (metis case_prodD case_prodI is_sorted_list_of_set_by_def lexord_mono' mem_Collect_eq) done qed definition distincts :: "'a set \ 'a list set" where "distincts A = {xs \ lists A. distinct(xs)}" lemma tl_element: "\ x \ set xs; x \ hd(xs) \ \ x \ set(tl(xs))" by (metis in_set_insert insert_Nil list.collapse list.distinct(2) set_ConsD) subsubsection \ List Update \ lemma listsum_update: fixes xs :: "'a::ring list" assumes "i < length xs" shows "list_sum (xs[i := v]) = list_sum xs - xs ! i + v" using assms proof (induct xs arbitrary: i) case Nil then show ?case by (simp) next case (Cons a xs) then show ?case proof (cases i) case 0 thus ?thesis by (simp add: add.commute) next case (Suc i') with Cons show ?thesis by (auto) qed qed subsubsection \ Drop While and Take While \ lemma dropWhile_sorted_le_above: "\ sorted xs; x \ set (dropWhile (\ x. x \ n) xs) \ \ x > n" apply (induct xs) apply (auto) apply (rename_tac a xs) apply (case_tac "a \ n") apply (auto) done lemma set_dropWhile_le: "sorted xs \ set (dropWhile (\ x. x \ n) xs) = {x\set xs. x > n}" apply (induct xs) apply (simp) apply (rename_tac x xs) apply (subgoal_tac "sorted xs") apply (simp) apply (safe) apply (auto) done lemma set_takeWhile_less_sorted: "\ sorted I; x \ set I; x < n \ \ x \ set (takeWhile (\x. x < n) I)" proof (induct I arbitrary: x) case Nil thus ?case by (simp) next case (Cons a I) thus ?case by auto qed lemma nth_le_takeWhile_ord: "\ sorted xs; i \ length (takeWhile (\ x. x \ n) xs); i < length xs \ \ n \ xs ! i" apply (induct xs arbitrary: i, auto) apply (rename_tac x xs i) apply (case_tac "x \ n") apply (auto) apply (metis One_nat_def Suc_eq_plus1 le_less_linear le_less_trans less_imp_le list.size(4) nth_mem set_ConsD) done lemma length_takeWhile_less: "\ a \ set xs; \ P a \ \ length (takeWhile P xs) < length xs" by (metis in_set_conv_nth length_takeWhile_le nat_neq_iff not_less set_takeWhileD takeWhile_nth) lemma nth_length_takeWhile_less: "\ sorted xs; distinct xs; (\ a \ set xs. a \ n) \ \ xs ! length (takeWhile (\x. x < n) xs) \ n" by (induct xs, auto) subsubsection \ Last and But Last \ lemma length_gt_zero_butlast_concat: assumes "length ys > 0" shows "butlast (xs @ ys) = xs @ (butlast ys)" using assms by (metis butlast_append length_greater_0_conv) lemma length_eq_zero_butlast_concat: assumes "length ys = 0" shows "butlast (xs @ ys) = butlast xs" using assms by (metis append_Nil2 length_0_conv) lemma butlast_single_element: shows "butlast [e] = []" by (metis butlast.simps(2)) lemma last_single_element: shows "last [e] = e" by (metis last.simps) lemma length_zero_last_concat: assumes "length t = 0" shows "last (s @ t) = last s" by (metis append_Nil2 assms length_0_conv) lemma length_gt_zero_last_concat: assumes "length t > 0" shows "last (s @ t) = last t" by (metis assms last_append length_greater_0_conv) subsubsection \ Prefixes and Strict Prefixes \ lemma prefix_length_eq: "\ length xs = length ys; prefix xs ys \ \ xs = ys" by (metis not_equal_is_parallel parallel_def) lemma prefix_Cons_elim [elim]: assumes "prefix (x # xs) ys" obtains ys' where "ys = x # ys'" "prefix xs ys'" using assms by (metis append_Cons prefix_def) lemma prefix_map_inj: "\ inj_on f (set xs \ set ys); prefix (map f xs) (map f ys) \ \ prefix xs ys" apply (induct xs arbitrary:ys) apply (simp_all) apply (erule prefix_Cons_elim) apply (auto) apply (metis image_insert insertI1 insert_Diff_if singletonE) done lemma prefix_map_inj_eq [simp]: "inj_on f (set xs \ set ys) \ prefix (map f xs) (map f ys) \ prefix xs ys" using map_mono_prefix prefix_map_inj by blast lemma strict_prefix_Cons_elim [elim]: assumes "strict_prefix (x # xs) ys" obtains ys' where "ys = x # ys'" "strict_prefix xs ys'" using assms by (metis Sublist.strict_prefixE' Sublist.strict_prefixI' append_Cons) lemma strict_prefix_map_inj: "\ inj_on f (set xs \ set ys); strict_prefix (map f xs) (map f ys) \ \ strict_prefix xs ys" apply (induct xs arbitrary:ys) apply (auto) using prefix_bot.bot.not_eq_extremum apply fastforce apply (erule strict_prefix_Cons_elim) apply (auto) apply (metis (hide_lams, full_types) image_insert insertI1 insert_Diff_if singletonE) done lemma strict_prefix_map_inj_eq [simp]: "inj_on f (set xs \ set ys) \ strict_prefix (map f xs) (map f ys) \ strict_prefix xs ys" by (simp add: inj_on_map_eq_map strict_prefix_def) lemma prefix_drop: "\ drop (length xs) ys = zs; prefix xs ys \ \ ys = xs @ zs" by (metis append_eq_conv_conj prefix_def) lemma list_append_prefixD [dest]: "x @ y \ z \ x \ z" using append_prefixD less_eq_list_def by blast lemma prefix_not_empty: assumes "strict_prefix xs ys" and "xs \ []" shows "ys \ []" using Sublist.strict_prefix_simps(1) assms(1) by blast lemma prefix_not_empty_length_gt_zero: assumes "strict_prefix xs ys" and "xs \ []" shows "length ys > 0" using assms prefix_not_empty by auto lemma butlast_prefix_suffix_not_empty: assumes "strict_prefix (butlast xs) ys" shows "ys \ []" using assms prefix_not_empty_length_gt_zero by fastforce lemma prefix_and_concat_prefix_is_concat_prefix: assumes "prefix s t" "prefix (e @ t) u" shows "prefix (e @ s) u" using Sublist.same_prefix_prefix assms(1) assms(2) prefix_order.dual_order.trans by blast lemma prefix_eq_exists: "prefix s t \ (\xs . s @ xs = t)" using prefix_def by auto lemma strict_prefix_eq_exists: "strict_prefix s t \ (\xs . s @ xs = t \ (length xs) > 0)" using prefix_def strict_prefix_def by auto lemma butlast_strict_prefix_eq_butlast: assumes "length s = length t" and "strict_prefix (butlast s) t" shows "strict_prefix (butlast s) t \ (butlast s) = (butlast t)" by (metis append_butlast_last_id append_eq_append_conv assms(1) assms(2) length_0_conv length_butlast strict_prefix_eq_exists) lemma butlast_eq_if_eq_length_and_prefix: assumes "length s > 0" "length z > 0" "length s = length z" "strict_prefix (butlast s) t" "strict_prefix (butlast z) t" shows "(butlast s) = (butlast z)" using assms by (auto simp add:strict_prefix_eq_exists) -lemma prefix_imp_length_lteq: - assumes "prefix s t" - shows "length s \ length t" - using assms by (simp add: Sublist.prefix_length_le) - -lemma prefix_imp_length_not_gt: - assumes "prefix s t" - shows "\ length t < length s" - using assms by (simp add: Sublist.prefix_length_le leD) - -lemma prefix_and_eq_length_imp_eq_list: - assumes "prefix s t" and "length t = length s" - shows "s=t" - using assms by (simp add: prefix_length_eq) - lemma butlast_prefix_imp_length_not_gt: assumes "length s > 0" "strict_prefix (butlast s) t" shows "\ (length t < length s)" using assms prefix_length_less by fastforce lemma length_not_gt_iff_eq_length: assumes "length s > 0" and "strict_prefix (butlast s) t" shows "(\ (length s < length t)) = (length s = length t)" proof - have "(\ (length s < length t)) = ((length t < length s) \ (length s = length t))" by (metis not_less_iff_gr_or_eq) also have "... = (length s = length t)" using assms by (simp add:butlast_prefix_imp_length_not_gt) finally show ?thesis . qed text \ Greatest common prefix \ fun gcp :: "'a list \ 'a list \ 'a list" where "gcp [] ys = []" | "gcp (x # xs) (y # ys) = (if (x = y) then x # gcp xs ys else [])" | "gcp _ _ = []" lemma gcp_right [simp]: "gcp xs [] = []" by (induct xs, auto) lemma gcp_append [simp]: "gcp (xs @ ys) (xs @ zs) = xs @ gcp ys zs" by (induct xs, auto) lemma gcp_lb1: "prefix (gcp xs ys) xs" apply (induct xs arbitrary: ys, auto) apply (case_tac ys, auto) done lemma gcp_lb2: "prefix (gcp xs ys) ys" apply (induct ys arbitrary: xs, auto) apply (case_tac xs, auto) done interpretation prefix_semilattice: semilattice_inf gcp prefix strict_prefix proof fix xs ys :: "'a list" show "prefix (gcp xs ys) xs" by (induct xs arbitrary: ys, auto, case_tac ys, auto) show "prefix (gcp xs ys) ys" by (induct ys arbitrary: xs, auto, case_tac xs, auto) next fix xs ys zs :: "'a list" assume "prefix xs ys" "prefix xs zs" thus "prefix xs (gcp ys zs)" by (simp add: prefix_def, auto) qed subsubsection \ Lexicographic Order \ lemma lexord_append: assumes "(xs\<^sub>1 @ ys\<^sub>1, xs\<^sub>2 @ ys\<^sub>2) \ lexord R" "length(xs\<^sub>1) = length(xs\<^sub>2)" shows "(xs\<^sub>1, xs\<^sub>2) \ lexord R \ (xs\<^sub>1 = xs\<^sub>2 \ (ys\<^sub>1, ys\<^sub>2) \ lexord R)" using assms proof (induct xs\<^sub>2 arbitrary: xs\<^sub>1) case (Cons x\<^sub>2 xs\<^sub>2') note hyps = this from hyps(3) obtain x\<^sub>1 xs\<^sub>1' where xs\<^sub>1: "xs\<^sub>1 = x\<^sub>1 # xs\<^sub>1'" "length(xs\<^sub>1') = length(xs\<^sub>2')" by (auto, metis Suc_length_conv) with hyps(2) have xcases: "(x\<^sub>1, x\<^sub>2) \ R \ (xs\<^sub>1' @ ys\<^sub>1, xs\<^sub>2' @ ys\<^sub>2) \ lexord R" - by (auto) + by (auto split: if_split_asm) show ?case proof (cases "(x\<^sub>1, x\<^sub>2) \ R") case True with xs\<^sub>1 show ?thesis - by (auto) + using Cons.hyps hyps(2) by auto next case False with xcases have "(xs\<^sub>1' @ ys\<^sub>1, xs\<^sub>2' @ ys\<^sub>2) \ lexord R" by (auto) with hyps(1) xs\<^sub>1 have dichot: "(xs\<^sub>1', xs\<^sub>2') \ lexord R \ (xs\<^sub>1' = xs\<^sub>2' \ (ys\<^sub>1, ys\<^sub>2) \ lexord R)" by (auto) have "x\<^sub>1 = x\<^sub>2" - using False hyps(2) xs\<^sub>1(1) by auto + using False hyps(2) xs\<^sub>1(1) by (auto split: if_split_asm) with dichot xs\<^sub>1 show ?thesis by (simp) qed next case Nil thus ?case by auto qed -lemma strict_prefix_lexord_rel: - "strict_prefix xs ys \ (xs, ys) \ lexord R" - by (metis Sublist.strict_prefixE' lexord_append_rightI) - -lemma strict_prefix_lexord_left: - assumes "trans R" "(xs, ys) \ lexord R" "strict_prefix xs' xs" +lemma prefix_lexord_left: + assumes "(xs, ys) \ lexord R" "prefix xs' xs" shows "(xs', ys) \ lexord R" - by (metis assms lexord_trans strict_prefix_lexord_rel) + using assms + apply (auto simp: lexord_def prefix_def) + apply (metis Nil_is_append_conv list.exhaust) + apply (simp add: append_eq_append_conv2) + apply (drule_tac x="u" in spec) + apply (drule_tac x="a" in spec) + apply (drule_tac x="b" in spec) + apply (auto simp: ) + apply (metis hd_Cons_tl hd_append list.sel(1) self_append_conv2) + apply (metis Nil_is_append_conv hd_Cons_tl) + done lemma prefix_lexord_right: - assumes "trans R" "(xs, ys) \ lexord R" "strict_prefix ys ys'" + assumes "(xs, ys) \ lexord R" "prefix ys ys'" shows "(xs, ys') \ lexord R" - by (metis assms lexord_trans strict_prefix_lexord_rel) + using assms by (fastforce simp: lexord_def prefix_def) + lemma lexord_eq_length: assumes "(xs, ys) \ lexord R" "length xs = length ys" - shows "\ i. (xs!i, ys!i) \ R \ i < length xs \ (\ ji. (xs!i, ys!i) \ R \ xs!i\ys!i \ i < length xs \ (\ j R") - case True with ys show ?thesis + proof (cases "(x,y) \ R \ x\y") + case True with ys Cons show ?thesis by (rule_tac x="0" in exI, simp) next case False with ys hyps(2) have xy: "x = y" "(xs, ys') \ lexord R" - by auto - with hyps(1,3) ys obtain i where "(xs!i, ys'!i) \ R" "i < length xs" "(\ j R" "xs!i\ys'!i" "i < length xs" "(\ j i" "length ys > i" "(xs!i, ys!i) \ R" "\ j i" "length ys > i" "(xs!i, ys!i) \ R" "xs!i \ ys!i" "\j lexord R" using assms proof (induct i arbitrary: xs ys) case 0 thus ?case by (auto, metis lexord_cons_cons list.exhaust nth_Cons_0) next case (Suc i) note hyps = this then obtain x' y' xs' ys' where "xs = x' # xs'" "ys = y' # ys'" by (metis Suc_length_conv Suc_lessE) - moreover with hyps(5) have "\jj Distributed Concatenation \ definition uncurry :: "('a \ 'b \ 'c) \ ('a \ 'b \ 'c)" where [simp]: "uncurry f = (\(x, y). f x y)" definition dist_concat :: "'a list set \ 'a list set \ 'a list set" (infixr "\<^sup>\" 100) where "dist_concat ls1 ls2 = (uncurry (@) ` (ls1 \ ls2))" lemma dist_concat_left_empty [simp]: "{} \<^sup>\ ys = {}" by (simp add: dist_concat_def) lemma dist_concat_right_empty [simp]: "xs \<^sup>\ {} = {}" by (simp add: dist_concat_def) lemma dist_concat_insert [simp]: "insert l ls1 \<^sup>\ ls2 = ((@) l ` ( ls2)) \ (ls1 \<^sup>\ ls2)" by (auto simp add: dist_concat_def) subsection \ List Domain and Range \ abbreviation seq_dom :: "'a list \ nat set" ("dom\<^sub>l") where "seq_dom xs \ {0.. 'a set" ("ran\<^sub>l") where "seq_ran xs \ set xs" subsection \ Extracting List Elements \ definition seq_extract :: "nat set \ 'a list \ 'a list" (infix "\\<^sub>l" 80) where "seq_extract A xs = nths xs A" lemma seq_extract_Nil [simp]: "A \\<^sub>l [] = []" by (simp add: seq_extract_def) lemma seq_extract_Cons: "A \\<^sub>l (x # xs) = (if 0 \ A then [x] else []) @ {j. Suc j \ A} \\<^sub>l xs" by (simp add: seq_extract_def nths_Cons) lemma seq_extract_empty [simp]: "{} \\<^sub>l xs = []" by (simp add: seq_extract_def) lemma seq_extract_ident [simp]: "{0..\<^sub>l xs = xs" unfolding list_eq_iff_nth_eq by (auto simp add: seq_extract_def length_nths atLeast0LessThan) lemma seq_extract_split: assumes "i \ length xs" shows "{0..\<^sub>l xs @ {i..\<^sub>l xs = xs" using assms proof (induct xs arbitrary: i) case Nil thus ?case by (simp add: seq_extract_def) next case (Cons x xs) note hyp = this have "{j. Suc j < i} = {0.. Suc j \ j < length xs} = {i - 1..\<^sub>l (xs @ ys) = (A \\<^sub>l xs) @ ({j. j + length xs \ A} \\<^sub>l ys)" by (simp add: seq_extract_def nths_append) lemma seq_extract_range: "A \\<^sub>l xs = (A \ dom\<^sub>l(xs)) \\<^sub>l xs" apply (auto simp add: seq_extract_def nths_def) apply (metis (no_types, lifting) atLeastLessThan_iff filter_cong in_set_zip nth_mem set_upt) done lemma seq_extract_out_of_range: "A \ dom\<^sub>l(xs) = {} \ A \\<^sub>l xs = []" by (metis seq_extract_def seq_extract_range nths_empty) lemma seq_extract_length [simp]: "length (A \\<^sub>l xs) = card (A \ dom\<^sub>l(xs))" proof - have "{i. i < length(xs) \ i \ A} = (A \ {0..\<^sub>l (x # xs) = (if (m = 0) then x # ({0..\<^sub>l xs) else {m-1..\<^sub>l xs)" proof - have "{j. Suc j < n} = {0.. Suc j \ Suc j < n} = {m - Suc 0..\<^sub>l xs = [xs ! i]" using assms apply (induct xs arbitrary: i) apply (auto simp add: seq_extract_Cons) apply (rename_tac xs i) apply (subgoal_tac "{j. Suc j = i} = {i - 1}") apply (auto) done lemma seq_extract_as_map: assumes "m < n" "n \ length xs" shows "{m..\<^sub>l xs = map (nth xs) [m.. (\ i\length(xs). ys = {0..\<^sub>l xs \ zs = {i..\<^sub>l xs)" proof assume xs: "xs = ys @ zs" moreover have "ys = {0..\<^sub>l (ys @ zs)" by (simp add: seq_extract_append) moreover have "zs = {length ys..\<^sub>l (ys @ zs)" proof - have "{length ys.. {0.. i\length(xs). ys = {0..\<^sub>l xs \ zs = {i..\<^sub>l xs)" by (rule_tac x="length ys" in exI, auto) next assume "\i\length xs. ys = {0..\<^sub>l xs \ zs = {i..\<^sub>l xs" thus "xs = ys @ zs" by (auto simp add: seq_extract_split) qed subsection \ Filtering a list according to a set \ definition seq_filter :: "'a list \ 'a set \ 'a list" (infix "\\<^sub>l" 80) where "seq_filter xs A = filter (\ x. x \ A) xs" lemma seq_filter_Cons_in [simp]: "x \ cs \ (x # xs) \\<^sub>l cs = x # (xs \\<^sub>l cs)" by (simp add: seq_filter_def) lemma seq_filter_Cons_out [simp]: "x \ cs \ (x # xs) \\<^sub>l cs = (xs \\<^sub>l cs)" by (simp add: seq_filter_def) lemma seq_filter_Nil [simp]: "[] \\<^sub>l A = []" by (simp add: seq_filter_def) lemma seq_filter_empty [simp]: "xs \\<^sub>l {} = []" by (simp add: seq_filter_def) lemma seq_filter_append: "(xs @ ys) \\<^sub>l A = (xs \\<^sub>l A) @ (ys \\<^sub>l A)" by (simp add: seq_filter_def) lemma seq_filter_UNIV [simp]: "xs \\<^sub>l UNIV = xs" by (simp add: seq_filter_def) lemma seq_filter_twice [simp]: "(xs \\<^sub>l A) \\<^sub>l B = xs \\<^sub>l (A \ B)" by (simp add: seq_filter_def) subsection \ Minus on lists \ instantiation list :: (type) minus begin text \ We define list minus so that if the second list is not a prefix of the first, then an arbitrary list longer than the combined length is produced. Thus we can always determined from the output whether the minus is defined or not. \ definition "xs - ys = (if (prefix ys xs) then drop (length ys) xs else [])" instance .. end lemma minus_cancel [simp]: "xs - xs = []" by (simp add: minus_list_def) lemma append_minus [simp]: "(xs @ ys) - xs = ys" by (simp add: minus_list_def) lemma minus_right_nil [simp]: "xs - [] = xs" by (simp add: minus_list_def) lemma list_concat_minus_list_concat: "(s @ t) - (s @ z) = t - z" by (simp add: minus_list_def) lemma length_minus_list: "y \ x \ length(x - y) = length(x) - length(y)" by (simp add: less_eq_list_def minus_list_def) lemma map_list_minus: "xs \ ys \ map f (ys - xs) = map f ys - map f xs" by (simp add: drop_map less_eq_list_def map_mono_prefix minus_list_def) lemma list_minus_first_tl [simp]: "[x] \ xs \ (xs - [x]) = tl xs" by (metis Prefix_Order.prefixE append.left_neutral append_minus list.sel(3) not_Cons_self2 tl_append2) text \ Extra lemmas about @{term prefix} and @{term strict_prefix} \ lemma prefix_concat_minus: assumes "prefix xs ys" shows "xs @ (ys - xs) = ys" using assms by (metis minus_list_def prefix_drop) lemma prefix_minus_concat: assumes "prefix s t" shows "(t - s) @ z = (t @ z) - s" using assms by (simp add: Sublist.prefix_length_le minus_list_def) lemma strict_prefix_minus_not_empty: assumes "strict_prefix xs ys" shows "ys - xs \ []" using assms by (metis append_Nil2 prefix_concat_minus strict_prefix_def) lemma strict_prefix_diff_minus: assumes "prefix xs ys" and "xs \ ys" shows "(ys - xs) \ []" using assms by (simp add: strict_prefix_minus_not_empty) lemma length_tl_list_minus_butlast_gt_zero: assumes "length s < length t" and "strict_prefix (butlast s) t" and "length s > 0" shows "length (tl (t - (butlast s))) > 0" using assms by (metis Nitpick.size_list_simp(2) butlast_snoc hd_Cons_tl length_butlast length_greater_0_conv length_tl less_trans nat_neq_iff strict_prefix_minus_not_empty prefix_order.dual_order.strict_implies_order prefix_concat_minus) lemma list_minus_butlast_eq_butlast_list: assumes "length t = length s" and "strict_prefix (butlast s) t" shows "t - (butlast s) = [last t]" using assms by (metis append_butlast_last_id append_eq_append_conv butlast.simps(1) length_butlast less_numeral_extra(3) list.size(3) prefix_order.dual_order.strict_implies_order prefix_concat_minus prefix_length_less) lemma butlast_strict_prefix_length_lt_imp_last_tl_minus_butlast_eq_last: assumes "length s > 0" "strict_prefix (butlast s) t" "length s < length t" shows "last (tl (t - (butlast s))) = (last t)" using assms by (metis last_append last_tl length_tl_list_minus_butlast_gt_zero less_numeral_extra(3) list.size(3) append_minus strict_prefix_eq_exists) lemma tl_list_minus_butlast_not_empty: assumes "strict_prefix (butlast s) t" and "length s > 0" and "length t > length s" shows "tl (t - (butlast s)) \ []" using assms length_tl_list_minus_butlast_gt_zero by fastforce lemma tl_list_minus_butlast_empty: assumes "strict_prefix (butlast s) t" and "length s > 0" and "length t = length s" shows "tl (t - (butlast s)) = []" using assms by (simp add: list_minus_butlast_eq_butlast_list) -lemma concat_minus_list_concat_butlast_eq_list_minus_butlast: - assumes "prefix (butlast u) s" - shows "(t @ s) - (t @ (butlast u)) = s - (butlast u)" - using assms by (metis append_assoc prefix_concat_minus append_minus) - lemma tl_list_minus_butlast_eq_empty: assumes "strict_prefix (butlast s) t" and "length s = length t" shows "tl (t - (butlast s)) = []" using assms by (metis list.sel(3) list_minus_butlast_eq_butlast_list) -(* this can be shown using length_tl, but care is needed when list is empty? *) -lemma prefix_length_tl_minus: - assumes "strict_prefix s t" - shows "length (tl (t-s)) = (length (t-s)) - 1" - by (auto) - lemma length_list_minus: assumes "strict_prefix s t" shows "length(t - s) = length(t) - length(s)" using assms by (simp add: minus_list_def prefix_order.dual_order.strict_implies_order) subsection \ Laws on @{term take}, @{term drop}, and @{term nths} \ lemma take_prefix: "m \ n \ take m xs \ take n xs" by (metis Prefix_Order.prefixI append_take_drop_id min_absorb2 take_append take_take) lemma nths_atLeastAtMost_0_take: "nths xs {0..m} = take (Suc m) xs" by (metis atLeast0AtMost lessThan_Suc_atMost nths_upt_eq_take) lemma nths_atLeastLessThan_0_take: "nths xs {0.. n \ nths xs {0..m} \ nths xs {0..n}" by (simp add: nths_atLeastAtMost_0_take take_prefix) lemma sorted_nths_atLeastAtMost_0: "\ m \ n; sorted (nths xs {0..n}) \ \ sorted (nths xs {0..m})" using nths_atLeastAtMost_prefix sorted_prefix by blast lemma sorted_nths_atLeastLessThan_0: "\ m \ n; sorted (nths xs {0.. \ sorted (nths xs {0.. list_augment xs k x = list_update xs k x" by (metis list_augment_def list_augment_idem list_update_overwrite) lemma nths_list_update_out: "k \ A \ nths (list_update xs k x) A = nths xs A" apply (induct xs arbitrary: k x A) apply (auto) apply (rename_tac a xs k x A) apply (case_tac k) apply (auto simp add: nths_Cons) done lemma nths_list_augment_out: "\ k < length xs; k \ A \ \ nths (list_augment xs k x) A = nths xs A" by (simp add: list_augment_as_update nths_list_update_out) end \ No newline at end of file diff --git a/thys/UTP/toolkit/Sequence.thy b/thys/UTP/toolkit/Sequence.thy --- a/thys/UTP/toolkit/Sequence.thy +++ b/thys/UTP/toolkit/Sequence.thy @@ -1,294 +1,279 @@ (******************************************************************************) (* Project: Isabelle/UTP Toolkit *) (* File: Sequence.thy *) (* Authors: Simon Foster and Frank Zeyda *) (* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *) (******************************************************************************) section \ Infinite Sequences \ theory Sequence imports HOL.Real List_Extra "HOL-Library.Sublist" "HOL-Library.Nat_Bijection" begin typedef 'a seq = "UNIV :: (nat \ 'a) set" by (auto) setup_lifting type_definition_seq definition ssubstr :: "nat \ nat \ 'a seq \ 'a list" where "ssubstr i j xs = map (Rep_seq xs) [i ..< j]" lift_definition nth_seq :: "'a seq \ nat \ 'a" (infixl "!\<^sub>s" 100) is "\ f i. f i" . abbreviation sinit :: "nat \ 'a seq \ 'a list" where "sinit i xs \ ssubstr 0 i xs" lemma sinit_len [simp]: "length (sinit i xs) = i" by (simp add: ssubstr_def) lemma sinit_0 [simp]: "sinit 0 xs = []" by (simp add: ssubstr_def) lemma prefix_upt_0 [intro]: "i \ j \ prefix [0.. j \ prefix (sinit i xs) (sinit j xs)" by (simp add: map_mono_prefix prefix_upt_0 ssubstr_def) lemma sinit_strict_prefix: "i < j \ strict_prefix (sinit i xs) (sinit j xs)" by (metis sinit_len sinit_prefix le_less nat_neq_iff prefix_order.dual_order.strict_iff_order) lemma nth_sinit: "i < n \ sinit n xs ! i = xs !\<^sub>s i" apply (auto simp add: ssubstr_def) apply (transfer, auto) done lemma sinit_append_split: assumes "i < j" shows "sinit j xs = sinit i xs @ ssubstr i j xs" proof - have "[0.. lexord R" "(sinit j ys, sinit j xs) \ lexord R" shows False proof - have sinit_xs: "sinit j xs = sinit i xs @ ssubstr i j xs" by (metis assms(2) sinit_append_split) have sinit_ys: "sinit j ys = sinit i ys @ ssubstr i j ys" by (metis assms(2) sinit_append_split) from sinit_xs sinit_ys assms(4) have "(sinit i ys, sinit i xs) \ lexord R \ (sinit i ys = sinit i xs \ (ssubstr i j ys, ssubstr i j xs) \ lexord R)" by (auto dest: lexord_append) with assms lexord_asymmetric show False by (force) qed lemma sinit_linear_asym_lemma2: assumes "asym R" "(sinit i xs, sinit i ys) \ lexord R" "(sinit j ys, sinit j xs) \ lexord R" shows False proof (cases i j rule: linorder_cases) case less with assms show ?thesis by (auto dest: sinit_linear_asym_lemma1) next case equal with assms show ?thesis by (simp add: lexord_asymmetric) next case greater with assms show ?thesis by (auto dest: sinit_linear_asym_lemma1) qed lemma range_ext: assumes "\i :: nat. \x\{0.. x" by (metis lessI) with assms show "f(x) = g(x)" by (auto) qed lemma sinit_ext: "(\ i. sinit i xs = sinit i ys) \ xs = ys" by (simp add: ssubstr_def, transfer, auto intro: range_ext) definition seq_lexord :: "'a rel \ ('a seq) rel" where "seq_lexord R = {(xs, ys). (\ i. (sinit i xs, sinit i ys) \ lexord R)}" lemma seq_lexord_irreflexive: "\x. (x, x) \ R \ (xs, xs) \ seq_lexord R" by (auto dest: lexord_irreflexive simp add: irrefl_def seq_lexord_def) lemma seq_lexord_irrefl: "irrefl R \ irrefl (seq_lexord R)" by (simp add: irrefl_def seq_lexord_irreflexive) lemma seq_lexord_transitive: - assumes "trans R" + assumes "trans R" "antisym R" shows "trans (seq_lexord R)" -unfolding seq_lexord_def + unfolding seq_lexord_def proof (rule transI, clarify) fix xs ys zs :: "'a seq" and m n :: nat assume las: "(sinit m xs, sinit m ys) \ lexord R" "(sinit n ys, sinit n zs) \ lexord R" hence inz: "m > 0" using gr0I by force - from las(1) obtain i where sinitm: "(sinit m xs!i, sinit m ys!i) \ R" "i < m" "\ j R" "sinit m xs!i \ sinit m ys!i" + "i < m" "\ j R" "j < n" "\ k R" "sinit n ys!j \ sinit n zs!j" + "j < n" "\ ki. (sinit i xs, sinit i zs) \ lexord R" proof (cases "i \ j") case True note lt = this with sinitm sinitn have "(sinit n xs!i, sinit n zs!i) \ R" by (metis assms le_eq_less_or_eq le_less_trans nth_sinit transD) + moreover have "sinit n xs!i \ sinit n zs!i" + by (metis antisymD assms(2) dual_order.strict_trans2 le_eq_less_or_eq lt nth_sinit sinitm(1) sinitm(2) sinitm(3) sinitn(1) sinitn(3) sinitn(4)) moreover from lt sinitm sinitn have "\ j lexord R" using sinitm(2) sinitn(2) lt apply (rule_tac lexord_intro_elems) - apply (auto) - apply (metis less_le_trans less_trans nth_sinit) - done + apply (auto) + by (metis less_trans nth_sinit sinitm(3)) thus ?thesis by auto next case False then have ge: "i > j" by auto with assms sinitm sinitn have "(sinit n xs!j, sinit n zs!j) \ R" by (metis less_trans nth_sinit) + moreover have "sinit n xs!j \ sinit n zs!j" + by (metis ge less_trans nth_sinit sinitm(3) sinitm(4) sinitn(2) sinitn(3)) moreover from ge sinitm sinitn have "\ k lexord R" using sinitm(2) sinitn(2) ge apply (rule_tac lexord_intro_elems) - apply (auto) - apply (metis less_trans nth_sinit) - done + apply (auto) + by (metis less_trans nth_sinit sinitm(3)) thus ?thesis by auto qed qed lemma seq_lexord_trans: - "\ (xs, ys) \ seq_lexord R; (ys, zs) \ seq_lexord R; trans R \ \ (xs, zs) \ seq_lexord R" + "\ (xs, ys) \ seq_lexord R; (ys, zs) \ seq_lexord R; trans R; antisym R \ \ (xs, zs) \ seq_lexord R" by (meson seq_lexord_transitive transE) lemma seq_lexord_antisym: "\ asym R; (a, b) \ seq_lexord R \ \ (b, a) \ seq_lexord R" by (auto dest: sinit_linear_asym_lemma2 simp add: seq_lexord_def) lemma seq_lexord_asym: assumes "asym R" shows "asym (seq_lexord R)" by (meson assms asym.simps seq_lexord_antisym seq_lexord_irrefl) lemma seq_lexord_total: assumes "total R" shows "total (seq_lexord R)" using assms by (auto simp add: total_on_def seq_lexord_def, meson lexord_linear sinit_ext) -lemma seq_lexord_strict_linear_order: - assumes "strict_linear_order R" - shows "strict_linear_order (seq_lexord R)" - using assms - by (auto simp add: strict_linear_order_on_def partial_order_on_def preorder_on_def - intro: seq_lexord_transitive seq_lexord_irrefl seq_lexord_total) - lemma seq_lexord_linear: assumes "(\ a b. (a,b)\ R \ a = b \ (b,a) \ R)" shows "(x,y) \ seq_lexord R \ x = y \ (y,x) \ seq_lexord R" proof - have "total R" using assms total_on_def by blast hence "total (seq_lexord R)" using seq_lexord_total by blast thus ?thesis by (auto simp add: total_on_def) qed instantiation seq :: (ord) ord begin definition less_seq :: "'a seq \ 'a seq \ bool" where "less_seq xs ys \ (xs, ys) \ seq_lexord {(xs, ys). xs < ys}" definition less_eq_seq :: "'a seq \ 'a seq \ bool" where "less_eq_seq xs ys = (xs = ys \ xs < ys)" instance .. end instance seq :: (order) order proof - fix xs :: "'a seq" - show "xs \ xs" by (simp add: less_eq_seq_def) -next - fix xs ys zs :: "'a seq" - assume "xs \ ys" and "ys \ zs" - then show "xs \ zs" - by (force dest: seq_lexord_trans simp add: less_eq_seq_def less_seq_def trans_def) -next - fix xs ys :: "'a seq" - assume "xs \ ys" and "ys \ xs" - then show "xs = ys" + have \
: "antisym {(xs, ys::'a). xs < ys}" "trans {(xs, ys::'a). xs < ys}" + using antisym_def trans_def by fastforce+ + show "xs \ xs" for xs :: "'a seq" + by (simp add: less_eq_seq_def) + show "xs \ zs" if "xs \ ys" and "ys \ zs" for xs ys zs :: "'a seq" + using that + by (auto intro: \
seq_lexord_trans simp: less_eq_seq_def less_seq_def) + show "xs = ys" if "xs \ ys" and "ys \ xs" for xs ys :: "'a seq" + using that apply (auto simp add: less_eq_seq_def less_seq_def) - apply (rule seq_lexord_irreflexive [THEN notE]) - defer - apply (rule seq_lexord_trans) - apply (auto intro: transI) - done -next - fix xs ys :: "'a seq" - show "xs < ys \ xs \ ys \ \ ys \ xs" - apply (auto simp add: less_seq_def less_eq_seq_def) - defer - apply (rule seq_lexord_irreflexive [THEN notE]) - apply auto - apply (rule seq_lexord_irreflexive [THEN notE]) - defer - apply (rule seq_lexord_trans) - apply (auto intro: transI) - apply (simp add: seq_lexord_irreflexive) - done + by (metis \
case_prodD less_irrefl mem_Collect_eq seq_lexord_irreflexive seq_lexord_trans) + show "xs < ys \ xs \ ys \ \ ys \ xs" for xs ys :: "'a seq" + apply (auto simp add: less_seq_def less_eq_seq_def seq_lexord_irreflexive) + by (metis \
case_prodD less_irrefl mem_Collect_eq seq_lexord_irreflexive seq_lexord_trans) qed instance seq :: (linorder) linorder proof fix xs ys :: "'a seq" have "(xs, ys) \ seq_lexord {(u, v). u < v} \ xs = ys \ (ys, xs) \ seq_lexord {(u, v). u < v}" by (rule seq_lexord_linear) auto then show "xs \ ys \ ys \ xs" by (auto simp add: less_eq_seq_def less_seq_def) qed lemma seq_lexord_mono [mono]: "(\ x y. f x y \ g x y) \ (xs, ys) \ seq_lexord {(x, y). f x y} \ (xs, ys) \ seq_lexord {(x, y). g x y}" apply (auto simp add: seq_lexord_def) apply (metis case_prodD case_prodI lexord_take_index_conv mem_Collect_eq) done fun insort_rel :: "'a rel \ 'a \ 'a list \ 'a list" where "insort_rel R x [] = [x]" | "insort_rel R x (y # ys) = (if (x = y \ (x,y) \ R) then x # y # ys else y # insort_rel R x ys)" inductive sorted_rel :: "'a rel \ 'a list \ bool" where Nil_rel [iff]: "sorted_rel R []" | Cons_rel: "\ y \ set xs. (x = y \ (x, y) \ R) \ sorted_rel R xs \ sorted_rel R (x # xs)" definition list_of_set :: "'a rel \ 'a set \ 'a list" where "list_of_set R = folding.F (insort_rel R) []" lift_definition seq_inj :: "'a seq seq \ 'a seq" is "\ f i. f (fst (prod_decode i)) (snd (prod_decode i))" . lift_definition seq_proj :: "'a seq \ 'a seq seq" is "\ f i j. f (prod_encode (i, j))" . lemma seq_inj_inverse: "seq_proj (seq_inj x) = x" by (transfer, simp) lemma seq_proj_inverse: "seq_inj (seq_proj x) = x" by (transfer, simp) lemma seq_inj: "inj seq_inj" by (metis injI seq_inj_inverse) lemma seq_inj_surj: "bij seq_inj" apply (rule bijI) apply (auto simp add: seq_inj) apply (metis rangeI seq_proj_inverse) done end \ No newline at end of file