Commit ccafa39b authored by wenzelm's avatar wenzelm
Browse files

eliminated old 'def' command;

parent 8ac8a7f5adce
......@@ -4588,7 +4588,7 @@ proof rule
thus "\<exists>y\<in>ccpo_class.iterates g. f x \<le> y" ..
next
case (Sup M)
def N \<equiv> "{SOME y. y\<in>ccpo_class.iterates g \<and> x\<le>y | x. x\<in>M}"
define N where "N = {SOME y. y\<in>ccpo_class.iterates g \<and> x\<le>y | x. x\<in>M}"
have N1: "\<forall>y\<in>N. y\<in>ccpo_class.iterates g \<and> (\<exists>x\<in>M. x\<le>y)"
unfolding N_def
......
......@@ -908,7 +908,7 @@ begin
proof -
assume R0: "r 0 \<in> V0" and RS: "\<forall>i. (r i, r (Suc i)) \<in> E"
def r'\<equiv>"rec_nat
define r' where "r' = rec_nat
(r 0,0)
(\<lambda>i (q,n). (r (Suc i), if n \<in> acc q then (n+1) mod num_acc else n))"
......@@ -926,7 +926,8 @@ begin
have R0': "r' 0 \<in> degen.V0 T m" using R0
unfolding degeneralize_ext_def by auto
have MAP: "r = fst o r'" proof (rule ext)
have MAP: "r = fst o r'"
proof (rule ext)
fix i
show "r i = (fst o r') i"
by (cases i) (auto simp: split: prod.split)
......@@ -979,7 +980,7 @@ begin
assumes RI: "r i = (q,n)"
shows "\<exists>j\<ge>i. \<exists>q'. r j = (q',n) \<and> n \<in> acc q'"
proof -
def j \<equiv> "LEAST j. j\<ge>i \<and> n \<in> acc (fst (r j))"
define j where "j = (LEAST j. j\<ge>i \<and> n \<in> acc (fst (r j)))"
from RI have "n<num_acc" using degen_run_bound[OF NN0 R, of i] by auto
from EXJ have
......@@ -1130,7 +1131,7 @@ begin
from degen_run_bound[OF NN0 R] A have "n<num_acc" "n'<num_acc"
by (metis snd_conv)+
def k \<equiv> "LEAST k. i<k \<and> snd (r k) \<noteq> n"
define k where "k = (LEAST k. i<k \<and> snd (r k) \<noteq> n)"
have "i<k" "snd (r k) \<noteq> n"
by (metis (lifting, mono_tags) LeastI_ex A k_def leD less_linear snd_conv)+
......
......@@ -84,7 +84,8 @@ begin
from init_sim obtain rb0 where rel0: "(ra 0, rb0) \<in> R" and binit: "rb0 \<in> b.V0"
by (auto intro: ainit)
def rb \<equiv> "rec_nat rb0 (\<lambda>i rbi. SOME rbsi. (rbi, rbsi) \<in> b.E \<and> (ra (Suc i), rbsi) \<in> R)"
define rb
where "rb = rec_nat rb0 (\<lambda>i rbi. SOME rbsi. (rbi, rbsi) \<in> b.E \<and> (ra (Suc i), rbsi) \<in> R)"
have [simp]:
"rb 0 = rb0"
......
......@@ -515,16 +515,16 @@ proof -
"
let "REC\<^sub>T ?body ?init" = "?dfs_red"
def pre \<equiv> "\<lambda>S (V,u0). gen_dfs_pre E U S V u0 \<and> E``V \<inter> onstack = {}"
def post \<equiv> "\<lambda>S (V0,u0) (V,cyc). gen_dfs_post E U S V0 u0 V (cyc\<noteq>None)
define pre where "pre = (\<lambda>S (V,u0). gen_dfs_pre E U S V u0 \<and> E``V \<inter> onstack = {})"
define post where "post = (\<lambda>S (V0,u0) (V,cyc). gen_dfs_post E U S V0 u0 V (cyc\<noteq>None)
\<and> (case cyc of None \<Rightarrow> E``V \<inter> onstack = {}
| Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v)
| Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v))
"
def fe_inv \<equiv> "\<lambda>S V0 u0 it (V,cyc).
define fe_inv where "fe_inv = (\<lambda>S V0 u0 it (V,cyc).
gen_dfs_fe_inv E U S V0 u0 it V (cyc\<noteq>None)
\<and> (case cyc of None \<Rightarrow> E``V \<inter> onstack = {}
| Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v)
| Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v))
"
......@@ -671,14 +671,14 @@ proof -
let ?U = "?E\<^sup>*``?V0"
def add_inv \<equiv> "\<lambda>blues reds onstack.
define add_inv where "add_inv = (\<lambda>blues reds onstack.
\<not>(\<exists>v\<in>(blues-onstack)\<inter>?A. (v,v)\<in>?E\<^sup>+) (* No cycles over finished,
accepting states *)
\<and> reds \<subseteq> blues (* Red nodes are also blue *)
\<and> reds \<inter> onstack = {} (* No red nodes on stack *)
\<and> red_dfs_inv ?E ?U reds onstack"
\<and> red_dfs_inv ?E ?U reds onstack)"
def cyc_post \<equiv> "\<lambda>blues reds onstack u0 cyc. (case cyc of
define cyc_post where "cyc_post = (\<lambda>blues reds onstack u0 cyc. (case cyc of
NO_CYC \<Rightarrow> add_inv blues reds onstack
| REACH u p \<Rightarrow>
path ?E u0 p u
......@@ -689,22 +689,22 @@ proof -
\<and> path ?E v pl v
\<and> path ?E u0 pr v
\<and> set pl \<inter> ?A \<noteq> {}
)"
))"
def pre \<equiv> "\<lambda>(blues,reds,onstack,u::'v).
gen_dfs_pre ?E ?U onstack blues u \<and> add_inv blues reds onstack"
define pre where "pre = (\<lambda>(blues,reds,onstack,u::'v).
gen_dfs_pre ?E ?U onstack blues u \<and> add_inv blues reds onstack)"
def post \<equiv> "\<lambda>(blues0,reds0::'v set,onstack0,u0) (blues,reds,onstack,cyc).
define post where "post = (\<lambda>(blues0,reds0::'v set,onstack0,u0) (blues,reds,onstack,cyc).
onstack = onstack0
\<and> gen_dfs_post ?E ?U onstack0 blues0 u0 blues (cyc\<noteq>NO_CYC)
\<and> cyc_post blues reds onstack u0 cyc"
\<and> cyc_post blues reds onstack u0 cyc)"
def fe_inv \<equiv> "\<lambda>blues0 u0 onstack0 it (blues,reds,onstack,cyc).
define fe_inv where "fe_inv = (\<lambda>blues0 u0 onstack0 it (blues,reds,onstack,cyc).
onstack=onstack0
\<and> gen_dfs_fe_inv ?E ?U onstack0 blues0 u0 it blues (cyc\<noteq>NO_CYC)
\<and> cyc_post blues reds onstack u0 cyc"
\<and> cyc_post blues reds onstack u0 cyc)"
def outer_inv \<equiv> "\<lambda>it (blues,reds,cyc).
define outer_inv where "outer_inv = (\<lambda>it (blues,reds,cyc).
case cyc of
NO_CYC \<Rightarrow>
add_inv blues reds {}
......@@ -714,7 +714,7 @@ proof -
\<and> path ?E v pl v
\<and> path ?E v0 pr v
\<and> set pl \<inter> ?A \<noteq> {}
| _ \<Rightarrow> False"
| _ \<Rightarrow> False)"
have OUTER_INITIAL: "outer_inv V0 ({}, {}, NO_CYC)"
unfolding outer_inv_def add_inv_def
......
......@@ -416,16 +416,16 @@ proof -
"
let "REC\<^sub>T ?body ?init" = "?dfs_red"
def pre \<equiv> "\<lambda>S (V,u0). gen_dfs_pre E U S V u0 \<and> E``V \<inter> onstack = {}"
def post \<equiv> "\<lambda>S (V0,u0) (V,cyc). gen_dfs_post E U S V0 u0 V (cyc\<noteq>None)
define pre where "pre = (\<lambda>S (V,u0). gen_dfs_pre E U S V u0 \<and> E``V \<inter> onstack = {})"
define post where "post = (\<lambda>S (V0,u0) (V,cyc). gen_dfs_post E U S V0 u0 V (cyc\<noteq>None)
\<and> (case cyc of None \<Rightarrow> E``V \<inter> onstack = {}
| Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v)
| Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v))
"
def fe_inv \<equiv> "\<lambda>S V0 u0 it (V,cyc).
define fe_inv where "fe_inv = (\<lambda>S V0 u0 it (V,cyc).
gen_dfs_fe_inv E U S V0 u0 it V (cyc\<noteq>None)
\<and> (case cyc of None \<Rightarrow> E``V \<inter> onstack = {}
| Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v)
| Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v))
"
......@@ -592,32 +592,32 @@ proof -
let ?U = "E\<^sup>*``{v0}"
def add_inv \<equiv> "\<lambda>blues reds onstack.
define add_inv where "add_inv = (\<lambda>blues reds onstack.
\<not>(\<exists>v\<in>(blues-onstack)\<inter>A. (v,v)\<in>E\<^sup>+) (* No cycles over finished,
accepting states *)
\<and> reds \<subseteq> blues (* Red nodes are also blue *)
\<and> reds \<inter> onstack = {} (* No red nodes on stack *)
\<and> red_dfs_inv E ?U reds onstack"
\<and> red_dfs_inv E ?U reds onstack)"
def cyc_post \<equiv> "\<lambda>blues reds onstack u0 cyc. (case cyc of
define cyc_post where "cyc_post = (\<lambda>blues reds onstack u0 cyc. (case cyc of
NO_CYC \<Rightarrow> add_inv blues reds onstack
| REACH v p u p' \<Rightarrow> v\<in>A \<and> u\<in>onstack-{u0} \<and> p\<noteq>[]
\<and> path E v p u \<and> path E u0 p' v
| CIRC v pc pr \<Rightarrow> v\<in>A \<and> pc\<noteq>[] \<and> path E v pc v \<and> path E u0 pr v
)"
))"
def pre \<equiv> "\<lambda>(blues,reds,onstack,u).
gen_dfs_pre E ?U onstack blues u \<and> add_inv blues reds onstack"
define pre where "pre = (\<lambda>(blues,reds,onstack,u).
gen_dfs_pre E ?U onstack blues u \<and> add_inv blues reds onstack)"
def post \<equiv> "\<lambda>(blues0,reds0::'v set,onstack0,u0) (blues,reds,onstack,cyc).
define post where "post = (\<lambda>(blues0,reds0::'v set,onstack0,u0) (blues,reds,onstack,cyc).
onstack = onstack0
\<and> gen_dfs_post E ?U onstack0 blues0 u0 blues (cyc\<noteq>NO_CYC)
\<and> cyc_post blues reds onstack u0 cyc"
\<and> cyc_post blues reds onstack u0 cyc)"
def fe_inv \<equiv> "\<lambda>blues0 u0 onstack0 it (blues,reds,onstack,cyc).
define fe_inv where "fe_inv = (\<lambda>blues0 u0 onstack0 it (blues,reds,onstack,cyc).
onstack=onstack0
\<and> gen_dfs_fe_inv E ?U onstack0 blues0 u0 it blues (cyc\<noteq>NO_CYC)
\<and> cyc_post blues reds onstack u0 cyc"
\<and> cyc_post blues reds onstack u0 cyc)"
have GENPRE: "gen_dfs_pre E ?U {} {} v0"
apply (auto intro: gen_dfs_pre_initial)
......
......@@ -725,14 +725,13 @@ lemma ahm_rehash_aux_correct:
shows "ahm_invar_aux bhc n (ahm_rehash_aux bhc a sz)" (is "?thesis1")
and "ahm_\<alpha>_aux bhc (ahm_rehash_aux bhc a sz) = ahm_\<alpha>_aux bhc a" (is "?thesis2")
proof -
thm ahm_rehash_aux'_def
let ?a = "ahm_rehash_aux bhc a sz"
def I \<equiv> "\<lambda>it a'.
define I where "I it a' \<longleftrightarrow>
ahm_invar_aux bhc (n - card it) a'
\<and> array_length a' = sz
\<and> (\<forall>k. if k \<in> it then
ahm_\<alpha>_aux bhc a' k = None
else ahm_\<alpha>_aux bhc a' k = ahm_\<alpha>_aux bhc a k)"
else ahm_\<alpha>_aux bhc a' k = ahm_\<alpha>_aux bhc a k)" for it a'
note iterator_rule = map_iterator_no_cond_rule_P[
OF ahm_iteratei_aux_impl[OF inv bhc],
......
......@@ -182,7 +182,7 @@ begin
fix s i
assume "invar s" "i < length (\<alpha> s)"
def l \<equiv> "\<alpha> s"
define l where "l = \<alpha> s"
from `i < length (\<alpha> s)`
show "it_get s i = \<alpha> s ! i"
unfolding it_get_def iteratei_correct l_def[symmetric]
......
......@@ -572,7 +572,7 @@ begin
unfolding transforms_to_unique_keys_def inj_on_def Ball_def map_to_set_def
by auto (metis option.inject)
def vP \<equiv> "\<lambda>k v. \<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, v)"
define vP where "vP k v \<longleftrightarrow> (\<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, v))" for k v
have vP_intro: "\<And>k v. (\<exists>k' v'. m1.\<alpha> m k' = Some v'
\<and> f (k', v') = Some (k, v)) \<longleftrightarrow> vP k v"
unfolding vP_def by simp
......@@ -667,4 +667,3 @@ sublocale g_value_image_filter_loc
end
......@@ -164,7 +164,7 @@ begin
show "iam_rev_iterateoi m = foldli kvs"
unfolding iam_rev_iterateoi_foldli_conv kvs_def by simp
next
def al \<equiv> "array_length m"
define al where "al = array_length m"
show dist_kvs: "distinct (map fst kvs)" and "sorted (rev (map fst kvs))"
unfolding kvs_def al_def[symmetric]
apply (induct al)
......@@ -242,7 +242,7 @@ begin
show "iam_iterateoi m = foldli kvs"
unfolding iam_iterateoi_foldli_conv kvs_def by simp
next
def al \<equiv> "array_length m::nat"
define al where "al = array_length m"
show dist_kvs: "distinct (map fst kvs)" and "sorted (map fst kvs)"
unfolding kvs_def al_def[symmetric]
apply (induct al)
......
......@@ -77,8 +77,8 @@ proof (rule proper_it'I)
apply (rule pi_union)
apply (auto split: option.split intro: icf_proper_iteratorI) []
proof (rule pi_image)
def bs \<equiv> "\<lambda>(k,t). SOME l'::('k list \<times> 'v) list.
?ITA (k#l) t = foldli l' \<and> ?ITB (k#l) t = foldli l'"
define bs where "bs = (\<lambda>(k,t). SOME l'::('k list \<times> 'v) list.
?ITA (k#l) t = foldli l' \<and> ?ITB (k#l) t = foldli l')"
have EQ1: "\<forall>(k,t)\<in>set kvs. ?ITA (k#l) t = foldli (bs (k,t))" and
EQ2: "\<forall>(k,t)\<in>set kvs. ?ITB (k#l) t = foldli (bs (k,t))"
......
......@@ -70,23 +70,23 @@ proof (induct t arbitrary: ks0)
by (simp_all add: Ball_def distinct_map)
-- "root iterator"
def it_vo \<equiv> "(case vo of None \<Rightarrow> set_iterator_emp
| Some v \<Rightarrow> set_iterator_sng (ks0, v)) ::
('key list \<times> 'val, '\<sigma>) set_iterator"
def vo_S \<equiv> "case vo of None \<Rightarrow> {} | Some v \<Rightarrow> {(ks0, v)}"
define it_vo :: "('key list \<times> 'val, '\<sigma>) set_iterator"
where "it_vo =
(case vo of None \<Rightarrow> set_iterator_emp
| Some v \<Rightarrow> set_iterator_sng (ks0, v))"
define vo_S where "vo_S = (case vo of None \<Rightarrow> {} | Some v \<Rightarrow> {(ks0, v)})"
have it_vo_OK: "set_iterator it_vo vo_S"
unfolding it_vo_def vo_S_def
by (simp split: option.split
add: set_iterator_emp_correct set_iterator_sng_correct)
-- "children iterator"
def it_prod \<equiv> "(set_iterator_product (foldli kvs)
(\<lambda>(k, y). iteratei_postfixed (k # ks0) y))::
(('key \<times> ('key, 'val) trie) \<times> 'key list \<times> 'val, '\<sigma>) set_iterator"
define it_prod :: "(('key \<times> ('key, 'val) trie) \<times> 'key list \<times> 'val, '\<sigma>) set_iterator"
where "it_prod = set_iterator_product (foldli kvs) (\<lambda>(k, y). iteratei_postfixed (k # ks0) y)"
def it_prod_S \<equiv> "SIGMA kt:set kvs.
define it_prod_S where "it_prod_S = (SIGMA kt:set kvs.
(\<lambda>ksv. (rev (fst ksv) @ ((fst kt) # ks0), snd ksv)) `
map_to_set (lookup_trie (snd kt))"
map_to_set (lookup_trie (snd kt)))"
have it_prod_OK: "set_iterator it_prod it_prod_S"
proof -
......
......@@ -304,7 +304,7 @@ assumes sort_fun_OK: "\<And>l. sorted_by_rel R (sort_fun l) \<and> mset (sort_fu
and it_OK: "set_iterator it S0"
shows "set_iterator_genord (iterator_to_ordered_iterator sort_fun it) S0 R"
proof -
def l \<equiv> "iterate_to_list it"
define l where "l = iterate_to_list it"
have l_props: "set l = S0" "distinct l"
using iterate_to_list_correct [OF it_OK, folded l_def] by simp_all
......
......@@ -315,7 +315,7 @@ proof -
from Cons(4) have dist_as: "distinct as" and a_nin_as: "a \<notin> set as" by simp_all
note ind_hyp = Cons(1)[OF sorted_as sorted_bs_as dist_as]
def bs_a \<equiv> "bs a"
define bs_a where "bs_a = bs a"
from sorted_bs_a
have sorted_prod_a : "sorted_by_rel (set_iterator_product_order R_a R_b) (map (Pair a) (bs a))"
unfolding bs_a_def[symmetric]
......@@ -736,7 +736,7 @@ lemma map_iterator_genord_dom_filter_correct :
m k2 = Some v2; P (k2, v2); R (k1, v1) (k2, v2)\<rbrakk> \<Longrightarrow> R' k1 k2"
shows "set_iterator_genord (map_iterator_dom_filter P it) {k . \<exists>v. m k = Some v \<and> P (k, v)} R'"
proof -
def g \<equiv> "\<lambda>xy::('a \<times> 'b). if P xy then Some (fst xy) else None"
define g where "g xy = (if P xy then Some (fst xy) else None)" for xy :: "'a \<times> 'b"
note set_iterator_genord_image_filter_correct [OF it_OK, of g R']
......
......@@ -266,7 +266,7 @@ lemma array_map_conv_array_foldl:
"array_map f a = array_foldl (\<lambda>h a v. array_set a h (f h v)) a a"
proof(cases a)
case (Array xs)
def a == xs
define a where "a = xs"
hence "length xs \<le> length a" by simp
hence "foldl (\<lambda>a (k, v). array_set a k (f k v))
(Array a) (zip [0..<length xs] xs)
......
......@@ -666,8 +666,8 @@ proof -
from sem_eq have sem_eq_a: "\<And>a. robdd_\<alpha> (robdd_var i1 l1 v1 r1) a = robdd_\<alpha> (robdd_var i2 l2 v2 r2) a"
by (simp add: fun_eq_iff)
def a1 \<equiv> "\<lambda>a v'. if v1 = v' then True else a v'"
def a2 \<equiv> "\<lambda>a v'. if v1 = v' then False else a v'"
define a1 where "a1 a v' = (if v1 = v' then True else a v')" for a v'
define a2 where "a2 a v' = (if v1 = v' then False else a v')" for a v'
have a12_eval: "\<And>a. a1 a v1" "\<And>a. ~(a2 a v1)" "\<And>a v. v \<noteq> v1 \<Longrightarrow> a1 a v = a v \<and> a2 a v = a v"
unfolding a1_def a2_def by simp_all
......@@ -1379,8 +1379,8 @@ locale robdd_locale =
shows "robdd_invar_ext bs' v b \<and> rev_map_invar bs' rev_map' \<and>
robdd_\<alpha> b = robdd_\<alpha> (robdd_var 0 l v r)"
proof -
def l_id \<equiv> "robdd_get_id l"
def r_id \<equiv> "robdd_get_id r"
define l_id where "l_id = robdd_get_id l"
define r_id where "r_id = robdd_get_id r"
note bs_OK = rev_map_invar_implies_invar_bs[OF invar_rev_map]
......@@ -1448,7 +1448,7 @@ locale robdd_locale =
by (simp add: map_eq bs'_eq invar_b b_\<alpha> lr'_eq invar_rev_map)
next
case None note map_eq = this
def b' \<equiv> "robdd_var (snd rev_map) l v r"
define b' where "b' = robdd_var (snd rev_map) l v r"
have \<alpha>_b': "robdd_\<alpha> b' = robdd_\<alpha> (robdd_var 0 l v r)"
unfolding b'_def by (simp add: fun_eq_iff)
......@@ -1988,8 +1988,10 @@ locale robdd_locale =
obtain r apply_map'' rev_map'' where
apply_r_eq: "robdd_apply apply_map' rev_map' bop b1_r b2_r = (r, apply_map'', rev_map'')"
by (metis prod.exhaust)
obtain b' rev_map''' where const_eq: "robdd_construct rev_map'' l v'' r = (b', rev_map''')" by (metis prod.exhaust)
def apply_map''' \<equiv> "c_update (robdd_get_id b1, robdd_get_id b2) b' apply_map''"
obtain b' rev_map''' where const_eq: "robdd_construct rev_map'' l v'' r = (b', rev_map''')"
by (metis prod.exhaust)
define apply_map'''
where "apply_map''' = c_update (robdd_get_id b1, robdd_get_id b2) b' apply_map''"
note next_props = robdd_apply_next_correct [OF b1_invar b2_invar next_eq] not_leaf_b12
note v''_eq = next_props(13)
......@@ -2025,7 +2027,7 @@ locale robdd_locale =
have l_invar1: "robdd_invar_ext bs'' (Suc v'') l"
unfolding robdd_invar_ext_def by simp (metis subrobdds_set_mono subsetD)
def bs''' \<equiv> "insert b' bs''"
define bs''' where "bs''' = insert b' bs''"
from robdd_construct_correct[OF invar_rev_map'' _ _ l_invar1 r_invar1]
have b'_invar: "robdd_invar_ext bs''' v'' b'"
and invar_rev_map''': "rev_map_invar bs''' rev_map'''"
......@@ -2709,7 +2711,7 @@ next
robdd_invar_vars_greater.simps(2) robdd_invar_vars_impl)
then obtain a where a_sem_neq: "robdd_\<alpha> ll a \<noteq> robdd_\<alpha> rr a" by (auto simp add: fun_eq_iff)
def aa \<equiv> "\<lambda>v. a (v + n)"
define aa where "aa v = a (v + n)" for v
from invar(1) have ll_sem: "\<And>b. robdd_\<alpha> ll (\<lambda>v'. (aa(v - n := b)) (v' - n)) = robdd_\<alpha> ll a"
apply (rule_tac robdd_\<alpha>_invar_greater [of "Suc v"])
apply (simp_all add: aa_def)
......
......@@ -148,7 +148,7 @@ lemma perm_weak_contr_mono:
proof -
from contr weak have contr': "! x xs. P(x#x#xs) = P (x#xs)" by blast
def y' == "filter (% z. z : set x) y"
define y' where "y' = filter (% z. z : set x) y"
from xy have "set x = set y'" apply(simp add: y'_def) apply blast done
hence rxry': "remdups x <~~> remdups y'" by(simp add: perm_remdups_iff_eq_set)
......
......@@ -113,8 +113,8 @@ proof(clarsimp simp add: PO_rhoare_defs CT_trans_step_def all_conj_distrib)
by(auto)
from r have same_coord: "coord (Suc r) = coord r"
by(auto simp add: three_step_phase_Suc intro: coord_phase)
def cand \<equiv> "commt (sc' (coord (Suc r)))"
def C \<equiv> "{cand}"
define cand where "cand = commt (sc' (coord (Suc r)))"
define C where "C = {cand}"
have guard: "\<forall>cand\<in>C. \<exists>Q. majorities.opt_mru_guard (mru_vote \<circ> sc) Q cand"
proof(simp add: C_def)
let ?Q = "HOs r (coord r)"
......@@ -134,7 +134,7 @@ proof(clarsimp simp add: PO_rhoare_defs CT_trans_step_def all_conj_distrib)
by blast
qed
def sa' \<equiv> "sa\<lparr>
define sa' where "sa' = sa\<lparr>
next_round := Suc r,
candidates := C
\<rparr>"
......@@ -163,9 +163,9 @@ proof(clarsimp simp add: PO_rhoare_defs CT_trans_step_def all_conj_distrib)
and nxt: "\<forall>p. next1 r p (sc p) (\<mu> p) (crds r p) (sc' p)"
note \<mu>nxt = \<mu> nxt
def v \<equiv> "commt (sc (coord r))"
def S \<equiv> "{p. coord r \<in> HOs r p}"
def sa' \<equiv> "sa\<lparr> next_round := Suc r,
define v where "v = commt (sc (coord r))"
define S where "S = {p. coord r \<in> HOs r p}"
define sa' where "sa' = sa\<lparr> next_round := Suc r,
opt_mru_state.mru_vote := opt_mru_state.mru_vote sa ++ const_map (three_phase r, v) S
\<rparr>"
have "(sa, sa') \<in> majorities.opt_mru_step1 r S v" using r R
......@@ -202,7 +202,8 @@ proof(clarsimp simp add: PO_rhoare_defs CT_trans_step_def all_conj_distrib)
and nxt: "\<forall>p. next2 r p (sc p) (\<mu> p) (crds r p) (sc' p)"
note \<mu>nxt = \<mu> nxt
def dec_f \<equiv> "\<lambda>p. if decide (sc' p) \<noteq> decide (sc p) then decide (sc' p) else None"
define dec_f
where "dec_f p = (if decide (sc' p) \<noteq> decide (sc p) then decide (sc' p) else None)" for p
have dec_f: "(decide \<circ> sc) ++ dec_f = decide \<circ> sc'"
proof
......@@ -211,7 +212,7 @@ proof(clarsimp simp add: PO_rhoare_defs CT_trans_step_def all_conj_distrib)
by(auto simp add: map_add_def dec_f_def next2_def split: option.split intro!: ext)
qed
def sa' \<equiv> "sa\<lparr>
define sa' where "sa' = sa\<lparr>
next_round := Suc r,
decisions := decisions sa ++ dec_f
\<rparr>"
......@@ -221,9 +222,9 @@ proof(clarsimp simp add: PO_rhoare_defs CT_trans_step_def all_conj_distrib)
mru_vote_evolution2[OF nxt])
moreover have "(sa, sa') \<in> majorities.opt_mru_step2 r dec_f" using r R
proof-
def sc_r_votes \<equiv> "\<lambda>p. if (\<exists>v. mru_vote (sc p) = Some (three_phase r, v))
define sc_r_votes where "sc_r_votes p = (if (\<exists>v. mru_vote (sc p) = Some (three_phase r, v))
then map_option snd (mru_vote (sc p))
else None"
else None)" for p
have sc_r_votes: "sc_r_votes = majorities.r_votes sa r" using R r
by(auto simp add: ct_ref_rel_def sc_r_votes_def majorities.r_votes_def intro!: ext)
have "majorities.step2_d_guard dec_f sc_r_votes"
......@@ -291,13 +292,13 @@ proof -
by(auto simp add: CT_CHOMachine_def CT_commGlobal_def CT_commPerRd_def three_step_def)
-- {* The tedious bit: obtain three consecutive rounds linked by send/next functions *}
def r0 \<equiv> "nr_steps * ph"
def cfg0 \<equiv> "rho r0"
def r1 \<equiv> "Suc r0"
def cfg1 \<equiv> "rho r1"
def r2 \<equiv> "Suc r1"
def cfg2 \<equiv> "rho r2"
def cfg3 \<equiv> "rho (Suc r2)"
define r0 where "r0 = nr_steps * ph"
define cfg0 where "cfg0 = rho r0"
define r1 where "r1 = Suc r0"
define cfg1 where "cfg1 = rho r1"
define r2 where "r2 = Suc r1"
define cfg2 where "cfg2 = rho r2"
define cfg3 where "cfg3 = rho (Suc r2)"
from
run[simplified CHORun_def, THEN CSHORun_step, THEN spec, where x="r0"]
......
......@@ -101,7 +101,7 @@ proof(clarsimp simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distrib
note \<mu>nxt = \<mu> nxt
have r_phase_step: "nr_steps * three_phase r = r" using r three_phase_step[of r]
by(auto)
def C \<equiv> "ran (prop_vote o sc')"
define C where "C = ran (prop_vote o sc')"
have guard: "\<forall>cand\<in>C. \<exists>Q. majorities.opt_mru_guard (mru_vote \<circ> sc) Q cand"
proof(simp add: C_def ran_def, safe)
fix p cand
......@@ -126,7 +126,7 @@ proof(clarsimp simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distrib
by blast
qed
def sa' \<equiv> "sa\<lparr>
define sa' where "sa' = sa\<lparr>
next_round := Suc r,
candidates := C
\<rparr>"
......@@ -156,7 +156,7 @@ proof(clarsimp simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distri
and nxt: "\<forall>p. next1 r p (sc p) (\<mu> p) (crds r) (sc' p)"
note \<mu>nxt = \<mu> nxt
def S \<equiv> "{p. mru_vote (sc' p) \<noteq> mru_vote (sc p)}"
define S where "S = {p. mru_vote (sc' p) \<noteq> mru_vote (sc p)}"
have S: "S \<subseteq> {p. \<exists>Q v. Q \<subseteq> HOs r p
\<and> (\<forall>q \<in> Q. prop_vote (sc q) = Some v)
......@@ -205,7 +205,7 @@ proof(clarsimp simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distri
by (metis all_not_in_conv comp_eq_dest_lhs majorities.empty_not_quorum ranI)
qed(auto)
def sa' \<equiv> "sa\<lparr> next_round := Suc r,
define sa' where "sa' = sa\<lparr> next_round := Suc r,
opt_mru_state.mru_vote := opt_mru_state.mru_vote sa ++ const_map (three_phase r, v) S
\<rparr>"
......@@ -243,7 +243,8 @@ proof(clarsimp simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distri
and nxt: "\<forall>p. next2 r p (sc p) (\<mu> p) (crds r) (sc' p)"
note \<mu>nxt = \<mu> nxt
def dec_f \<equiv> "\<lambda>p. if decide (sc' p) \<noteq> decide (sc p) then decide (sc' p) else None"
define dec_f
where "dec_f p = (if decide (sc' p) \<noteq> decide (sc p) then decide (sc' p) else None)" for p
have dec_f: "(decide \<circ> sc) ++ dec_f = decide \<circ> sc'"
proof
......@@ -252,7 +253,7 @@ proof(clarsimp simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distri
by(auto simp add: map_add_def dec_f_def next2_def Let_def split: option.split intro!: ext)
qed
def sa' \<equiv> "sa\<lparr>
define sa' where "sa' = sa\<lparr>
next_round := Suc r,
decisions := decisions sa ++ dec_f
\<rparr>"
......@@ -262,9 +263,9 @@ proof(clarsimp simp add: PO_rhoare_defs New_Algo_trans_step_def all_conj_distri
mru_vote_evolution2[OF nxt])
moreover have "(sa, sa') \<in> majorities.opt_mru_step2 r dec_f" using r R
proof-
def sc_r_votes \<equiv> "\<lambda>p. if (\<exists>v. mru_vote (sc p) = Some (three_phase r, v))
define sc_r_votes where "sc_r_votes p = (if (\<exists>v. mru_vote (sc p) = Some (three_phase r, v))
then map_option snd (mru_vote (sc p))
else None"
else None)" for p
have sc_r_votes: "sc_r_votes = majorities.r_votes sa r" using R r
by(auto simp add: new_algo_ref_rel_def sc_r_votes_def majorities.r_votes_def intro!: ext)
have "majorities.step2_d_guard dec_f sc_r_votes"
......@@ -329,13 +330,13 @@ proof -
by(auto simp add: New_Algo_HOMachine_def NA_commGlobal_def)
-- {* The tedious bit: obtain four consecutive rounds linked by send/next functions *}
def r0 \<equiv> "nr_steps * ph"
def cfg0 \<equiv> "rho r0"
def r1 \<equiv> "Suc r0"
def cfg1 \<equiv> "rho r1"
def r2 \<equiv> "Suc r1"
def cfg2 \<equiv> "rho r2"
def cfg3 \<equiv> "rho (Suc r2)"
define r0 where "r0 = nr_steps * ph"
define cfg0 where "cfg0 = rho r0"
define r1 where "r1 = Suc r0"
define cfg1 where "cfg1 = rho r1"
define r2 where "r2 = Suc r1"
define cfg2 where "cfg2 = rho r2"
define cfg3 where "cfg3 = rho (Suc r2)"
from
run[simplified HORun_def SHORun_def, THEN CSHORun_step, THEN spec, where x="r0"]
......
......@@ -107,7 +107,7 @@ proof(clarsimp simp add: PO_rhoare_defs Paxos_trans_step_def all_conj_distrib)
note \<mu>nxt = \<mu> nxt
from r have same_coord: "coord (Suc r) = coord r"
by(auto simp add: three_step_phase_Suc intro: coord_phase)
def C \<equiv> "coord_vote_to_set (Suc r) sc'"
define C where "C = coord_vote_to_set (Suc r) sc'"
have guard: "\<forall>cand\<in>C. \<exists>Q. majorities.opt_mru_guard (mru_vote \<circ> sc) Q cand"
proof
fix cand
......@@ -132,7 +132,7 @@ proof(clarsimp simp add: PO_rhoare_defs Paxos_trans_step_def all_conj_distrib)
by blast
qed
def sa' \<equiv> "sa\<lparr>
define sa' where "sa' = sa\<lparr>
next_round := Suc r,
candidates := C
\<rparr>"
......@@ -161,9 +161,9 @@ proof(clarsimp simp add: PO_rhoare_defs Paxos_trans_step_def all_conj_distrib)
and nxt: "\<forall>p. next1 r p (sc p) (\<mu> p) (crds r) (sc' p)"
note \<mu>nxt = \<mu> nxt
def v \<equiv> "the (commt (sc (coord r)))"
def S \<equiv> "{p. coord r \<in> HOs r p \<and> commt (sc (coord r)) \<noteq> None}"
def sa' \<equiv> "sa\<lparr> next_round := Suc r,
define v where "v = the (commt (sc (coord r)))"
define S where "S = {p. coord r \<in> HOs r p \<and> commt (sc (coord r)) \<noteq> None}"
define sa' where "sa' = sa\<lparr> next_round := Suc r,
opt_mru_state.mru_vote := opt_mru_state.mru_vote sa ++ const_map (three_phase r, v) S
\<rparr>"
have "(sa, sa') \<in> majorities.opt_mru_step1 r S v" using r R
......@@ -200,7 +200,8 @@ proof(clarsimp simp add: PO_rhoare_defs Paxos_trans_step_def all_conj_distrib)
and nxt: "\<forall>p. next2 r p (sc p) (\<mu> p) (crds r) (sc' p)"
note \<mu>nxt = \<mu> nxt
def dec_f \<equiv> "\<lambda>p. if decide (sc' p) \<noteq> decide (sc p) then decide (sc' p) else None"
define dec_f
where "dec_f p = (if decide (sc' p) \<noteq> decide (sc p) then decide (sc' p) else None)" for p
have dec_f: "(decide \<circ> sc) ++ dec_f = decide \<circ> sc'"
proof
......@@ -209,7 +210,7 @@ proof(clarsimp simp add: PO_rhoare_defs Paxos_trans_step_def all_conj_distrib)
by(auto simp add: map_add_def dec_f_def next2_def split: option.split intro!: ext)
qed
def sa' \<equiv> "sa\<lparr>