section‹Fresh variable addition›
theory Fresh_Variable_Addition
imports Cooperation_Program Show_LTS
begin
lemma range_lookup_default_of_alist: "range (Mapping.lookup_default d (Mapping.of_alist xs)) ⊆ insert d (snd ` set xs)"
proof
fix y
assume "y ∈ range (Mapping.lookup_default d (Mapping.of_alist xs))"
then obtain x where y: "y = Mapping.lookup_default d (Mapping.of_alist xs) x" by auto
show "y ∈ insert d (snd ` set xs)"
proof (cases "Mapping.lookup (Mapping.of_alist xs) x")
case None
then show ?thesis unfolding y Mapping.lookup_default_def by auto
next
case (Some z)
then have y: "y = z" unfolding Mapping.lookup_default_def y by auto
from Some have "(x,z) ∈ set xs" unfolding lookup_of_alist by (metis map_of_SomeD)
then show ?thesis unfolding y by auto
qed
qed
context lts begin
lemma transition_rule_refine_transition_formula: "transition_rule (refine_transition_formula tau f) =
(transition_rule tau ∧ formula f)" by (cases tau, auto)
lemma assignment_update[intro]:
"assignment α ⟹ a ∈ Values_of_type ty ⟹ assignment (α((x,ty):=a))"
unfolding assignment_def by auto
definition update_state ("_ |⇩s _ := _")
where "update_state s x a = State ((valuation s)(x:=a)) (location s)"
lemma location_update[simp]: "location (s |⇩s x := a) = location s"
and valuation_update[simp]: "valuation (s |⇩s x := a) = (valuation s)(x:=a)"
by (auto simp: update_state_def)
lemma state_update:
"state s ⟹ a ∈ Values_of_type ty ⟹ state (s |⇩s (x,ty):=a)"
unfolding state_def valuation_update by(rule assignment_update)
definition change_fresh :: "'v ⇒ 't ⇒ (('v,'t,'d,'l) state × ('v,'t,'d,'l) state) set"
where "change_fresh x ty ≡ { (s, s |⇩s (x,ty) := a ) | s a. state s ∧ a ∈ Values_of_type ty }"
lemma mem_change_freshI[intro]:
assumes a: "a ∈ Values_of_type ty"
and s: "state s"
and l: "location s = location t"
and v: "valuation t = (valuation s)((x,ty):=a)"
shows "(s,t) ∈ change_fresh x ty"
unfolding change_fresh_def mem_Collect_eq prod.inject
proof(intro exI conjI)
show "t = (s |⇩s (x, ty) := a)" unfolding update_state_def l v[symmetric] by auto
qed (insert a s, auto)
lemma mem_change_freshD[dest]:
assumes "(s,t) ∈ change_fresh x ty"
shows "location s = location t"
and "state s"
and "state t"
and "∃a ∈ Values_of_type ty. valuation t = (valuation s)((x,ty):=a)"
using assms[unfolded change_fresh_def] state_update by auto
lemma change_fresh_sym:
assumes "(s,t) ∈ change_fresh x ty"
shows "(t,s) ∈ change_fresh x ty"
proof
from assms obtain a
where a: "a ∈ Values_of_type ty" and ts: "valuation t = (valuation s)((x,ty):=a)" by auto
with assms
show "state t"
and "valuation s = (valuation t)((x,ty):= valuation s (x,ty))"
and "location t = location s" by auto
from assms have "state s" by auto
then show "valuation s (x, ty) ∈ Values_of_type ty" by auto
qed
lemma change_fresh_refl_on:
shows "refl_on (Collect state :: ('v, 't, 'd, 'l) state set) (change_fresh x ty)"
proof(rule refl_onI)
fix s :: "('v, 't, 'd, 'l) state" assume s: "s ∈ Collect state"
show "(s,s) ∈ change_fresh x ty"
proof
from s show "state s" by auto
then show "valuation s (x,ty) ∈ Values_of_type ty" by auto
qed auto
qed auto
lemma change_fresh_trans: "trans (change_fresh x ty)" (is "trans ?S")
proof(rule transI)
fix s t u assume st: "(s,t) ∈ ?S" and tu: "(t,u) ∈ ?S"
show "(s,u) ∈ ?S"
proof
from tu show "valuation u (x,ty) ∈ Values_of_type ty" by auto
qed(insert mem_change_freshD[OF st] mem_change_freshD[OF tu], auto)
qed
definition "fresh_variable_cond P P' x ty ≡
lts.initial P' = lts.initial P ∧ assertion P' = assertion P ∧
(∀ l. (x,ty) ∉ vars_formula (assertion P l)) ∧
(∀ l r φ. Transition l r φ ∈ transition_rules P ⟶
(∃ φ'. Transition l r φ' ∈ transition_rules P' ∧
(∀α. assignment α ⟶ α ⊨ φ ⟶ (∃a ∈ Values_of_type ty. α((Post x,ty) := a) ⊨ φ')))) ∧
(∀ τ' ∈ transition_rules P'. ∀ (s,t) ∈ transition_step_lts P τ'. ∀ a ∈ Values_of_type ty.
∃ b ∈ Values_of_type ty. (s |⇩s (x,ty):=a, t |⇩s (x,ty):=b) ∈ transition_step_lts P τ')"
lemma fresh_variable_condD:
assumes "fresh_variable_cond P P' x ty"
shows "lts.initial P' = lts.initial P"
and "⋀l r φ. Transition l r φ ∈ transition_rules P ⟹ ∃φ'. Transition l r φ' ∈ transition_rules P' ∧
(∀α. assignment α ⟶ α ⊨ φ ⟶ (∃a ∈ Values_of_type ty. α((Post x,ty) := a) ⊨ φ'))"
and "⋀τ' s t a. τ' ∈ transition_rules P' ⟹ (s,t) ∈ transition_step_lts P τ' ⟹ a ∈ Values_of_type ty ⟹
∃ b ∈ Values_of_type ty. (s |⇩s (x,ty):=a, t |⇩s (x,ty):=b) ∈ transition_step_lts P τ'"
and "assertion P' = assertion P"
and "⋀ l. (x,ty) ∉ vars_formula (assertion P l)"
using assms[unfolded fresh_variable_cond_def] by (atomize(full), force)
lemma fresh_variable_cond_imp_step:
assumes "fresh_variable_cond P P' x ty" and "τ ∈ transition_rules P"
shows "∃τ' ∈ transition_rules P'.
source τ' = source τ ∧
target τ' = target τ ∧
(∀(s,t) ∈ transition_step_lts P τ. ∃a ∈ Values_of_type ty. (s, t |⇩s (x,ty):=a) ∈ transition_step_lts P τ')"
proof(cases τ)
case τ: (Transition l r φ)
let ?ppi = "λs t. pre_post_inter (valuation s) (valuation t)"
from τ fresh_variable_condD(2)[OF assms[unfolded τ]] obtain φ'
where 1: "Transition l r φ' ∈ transition_rules P'"
and 2: "⋀α. assignment α ⟹ α ⊨ φ ⟹ (∃a ∈ Values_of_type ty. α((Post x, ty) := a) ⊨ φ')" by auto
note lc = fresh_variable_condD(5)[OF assms(1)]
show ?thesis
proof (intro bexI[OF _ 1] conjI ballI2)
fix s t assume "(s,t) ∈ transition_step_lts P τ"
with τ obtain α
where α: "assignment α"
and s: "state s"
and t: "state t"
and 3: "?ppi s t α ⊨ φ" (is "?a ⊨ _")
and 4: "state_lts P s" "state_lts P t"
and [simp]: "l = location s" "r = location t" by auto
from s t α have "assignment ?a" by auto
from 2[OF this 3] obtain a
where a: "a ∈ Values_of_type ty" and *: "?a((Post x, ty) := a) ⊨ φ'" by auto
from 4(2) fresh_variable_condD(5)[OF assms(1), of r]
have lct: "(valuation t)((x, ty) := a) ⊨ assertion P (location t)" by auto
note *
also have "(?a((Post x, ty) := a)) xx = ?ppi s (t |⇩s (x,ty):=a) α xx" for xx by(cases xx, cases "fst xx",auto)
then have "?a((Post x, ty) := a) = ?ppi s (t |⇩s (x,ty):=a) α" by auto
finally have "... ⊨ φ'" by auto
with s t α a 4 lct show "∃a∈Values_of_type ty. (s, t |⇩s (x, ty) := a) ∈ transition_step_lts P (Transition l r φ')"
by (intro bexI[OF _ a] mem_transition_stepI, auto simp: lc)
qed (insert τ, auto)
qed
context
fixes P P' :: "('f,'v,'t,'l sharp) lts" and x :: 'v and ty :: 't
assumes fv: "fresh_variable_cond P P' x ty"
begin
interpretation indexed_rewriting "transition_step_lts P" .
lemma change_fresh_O_transition_step:
assumes τ': "τ' ∈ transition_rules P'"
shows "change_fresh x ty O transition_step_lts P τ' ⊆ transition_step_lts P τ' O change_fresh x ty" (is "?L ⊆ ?R")
proof
fix s u assume L: "(s,u) ∈ ?L"
then obtain t where st: "(s,t) ∈ change_fresh x ty" and tu: "(t,u) ∈ transition_step_lts P τ'" by auto
let ?a = "valuation s (x,ty)"
from st have s: "assignment (valuation s)" and t: "assignment (valuation t)" by auto
then have a': "?a ∈ Values_of_type ty" by auto
from tu have u: "assignment (valuation u)" by auto
from st obtain a where "valuation t = (valuation s)((x,ty):=a)" by auto
moreover have "...((x,ty):= valuation s (x,ty)) = valuation s" by auto
moreover from st have "location t = location s" by auto
ultimately have "(t |⇩s (x,ty) := ?a) = s" unfolding update_state_def by (cases t, auto)
from fresh_variable_condD(3)[OF fv τ' tu a', unfolded this]
obtain b where b: "b ∈ Values_of_type ty" and sv: "(s, u |⇩s (x, ty) := b) ∈ transition_step_lts P τ'" by auto
from b u have vu: "(u |⇩s (x, ty) := b, u) ∈ change_fresh x ty" by (subst change_fresh_sym, auto)
from sv vu show "(s,u) ∈ ?R" by auto
qed
lemma change_fresh_push:
assumes τ': "τ' ∈ transition_rules P'"
shows "change_fresh x ty O transition_step_lts P τ' ⊆ transition_step_lts P τ' O (change_fresh x ty)⇧*" (is "?L ⊆ ?R O ?S⇧*")
proof-
from change_fresh_O_transition_step[OF assms]
have "?L ⊆ ?R O ?S".
also have "... ⊆ ?R O ?S⇧*" by auto
finally show ?thesis.
qed
lemma change_fresh_O_traverse:
assumes τs': "τs' ⊆ transition_rules P'"
shows "change_fresh x ty O traverse τs' ⊆ traverse τs' O (change_fresh x ty)⇧*" (is "?S O ?R ⊆ _")
proof-
have "?S O ?R ⊆ ?S⇧* O ?R" by auto
also have "... ⊆ ?R O ?S⇧*" using τs' by (intro traverse_push change_fresh_push, auto)
finally show ?thesis .
qed
lemma change_fresh_O_flat_transitions:
shows "change_fresh x ty O transitions_step_lts P (flat_transitions_of P') ⊆ transitions_step_lts P (flat_transitions_of P') O (change_fresh x ty)⇧*"
(is "?L ⊆ ?R")
proof
fix s t assume "(s,t) ∈ ?L"
then obtain τ
where *: "τ ∈ flat_transitions_of P'" "(s,t) ∈ change_fresh x ty O transition_step_lts P τ" by auto
then have "τ ∈ transition_rules P'" by auto
from * change_fresh_O_transition_step[OF this] have "(s,t) ∈ transition_step_lts P τ O change_fresh x ty" by auto
with * show "(s,t) ∈ ?R" by auto
qed
lemma transition_simulate:
assumes τ: "τ ∈ transition_rules P"
shows "∃ τ' ∈ transition_rules P'.
source τ' = source τ ∧
target τ' = target τ ∧
transition_step_lts P τ ⊆ transition_step_lts P τ' O (change_fresh x ty)⇧*"
proof-
from fresh_variable_cond_imp_step[OF fv τ]
obtain τ'
where τ': "τ' ∈ transition_rules P'"
and [simp]: "source τ' = source τ" "target τ' = target τ"
and *: "∀(s,t) ∈ transition_step_lts P τ. ∃a∈Values_of_type ty.
(s, t |⇩s (x, ty) := a) ∈ transition_step_lts P τ'" by auto
{ fix s t assume st: "(s,t) ∈ transition_step_lts P τ"
from st have vs: "assignment (valuation s)" and vt: "assignment (valuation t)" by auto
then have a': "valuation t (x,ty) ∈ Values_of_type ty" by auto
from * st obtain a
where a: "a ∈ Values_of_type ty" and st': "(s, t |⇩s (x,ty) := a) ∈ transition_step_lts P τ'" by auto
moreover with vt have "(t |⇩s (x,ty) := a, t) ∈ change_fresh x ty"
by (intro mem_change_freshI[OF a'] state_update, auto)
ultimately have "(s,t) ∈ transition_step_lts P τ' O change_fresh x ty" by auto
also have "... ⊆ transition_step_lts P τ' O (change_fresh x ty)⇧*" by auto
finally have "(s,t) ∈ ...".
}
then show ?thesis by(intro bexI[OF _ τ'],auto)
qed
lemma flat_transitions_simulate:
shows "transitions_step_lts P (flat_transitions_of P) ⊆ transitions_step_lts P (flat_transitions_of P') O (change_fresh x ty)⇧*"
(is "?L ⊆ ?R")
proof
fix s t assume "(s,t) ∈ ?L"
then obtain τ where *: "τ ∈ flat_transitions_of P" "(s,t) ∈ transition_step_lts P τ" by auto
with transition_simulate obtain τ'
where 1: "τ' ∈ transition_rules P'"
and 2: "transition_step_lts P τ ⊆ transition_step_lts P τ' O (change_fresh x ty)⇧*" by auto
from * 2 have 3: "(s,t) ∈ transition_step_lts P τ' O (change_fresh x ty)⇧*" by auto
then have "source τ' = location s" by auto
moreover from * have "¬ is_sharp (location s)" by auto
ultimately have "¬ is_sharp_transition τ'" by auto
with 1 have "τ' ∈ flat_transitions_of P'" by auto
with 3 show "(s,t) ∈ ?R" by auto
qed
lemma sharp_transition_simulate:
assumes τ: "τ ∈ sharp_transitions_of P"
shows "∃ τ' ∈ sharp_transitions_of P'. transition_step_lts P τ ⊆ transition_step_lts P τ' O (change_fresh x ty)⇧*"
(is "∃ τ' ∈ _. ?goal τ'")
proof-
from τ have "τ ∈ transition_rules P" by auto
from transition_simulate[OF this] obtain τ'
where 1: "τ' ∈ transition_rules P'"
and 2: "source τ' = source τ"
and 3: "?goal τ'" by auto
from τ 1 2 have "τ' ∈ sharp_transitions_of P'" by auto
with 3 show ?thesis by auto
qed
lemma sharp_transition_simulate_fun:
"∃f. ∀τ ∈ sharp_transitions_of P.
f τ ∈ sharp_transitions_of P' ∧ transition_step_lts P τ ⊆ transition_step_lts P (f τ) O (change_fresh x ty)⇧*"
using sharp_transition_simulate by (intro bchoice, auto)
lemma sharp_traverse_simulate:
assumes τs: "τs ⊆ sharp_transitions_of P" and nonemp: "τs ≠ {}"
shows "∃τs' ⊆ sharp_transitions_of P'. τs' ≠ {} ∧ traverse τs ⊆ traverse τs' O (change_fresh x ty)⇧*"
proof-
let ?S = "change_fresh x ty"
interpret I': indexed_rewriting "(λτ'. transition_step_lts P τ' O ?S⇧* )".
from sharp_transition_simulate_fun obtain f
where dom: "∀τ ∈ sharp_transitions_of P. f τ ∈ sharp_transitions_of P'"
and mono: "∀τ ∈ sharp_transitions_of P. transition_step_lts P τ ⊆ transition_step_lts P (f τ) O ?S⇧*" by auto
with transition_simulate
interpret rule_morphism id "sharp_transitions_of P" f "transition_step_lts P" "(λτ'. transition_step_lts P τ' O ?S⇧* )"
by (unfold_locales,auto)
note recurring_morphism
interpret I: indexed_rewriting "(λτ. transition_step_lts P (f τ) O ?S⇧* )".
have *: "I.traversed τs seq i ⟹ I'.traversed (f ` τs) seq i" for seq i
by(induct rule: I.traversed.induct, unfold image_empty image_insert; intro I'.traversed.intros)
show ?thesis
proof (intro exI conjI)
from τs dom show "f ` τs ⊆ sharp_transitions_of P'" by auto
have "traverse τs ⊆ I.traverse τs" apply(rule traverse_mono) using mono assms by auto
also have "... ⊆ I'.traverse (f ` τs)" unfolding I'.traverse_def I.traverse_def using * by auto
also have "... ⊆ traverse (f ` τs) O ?S⇧*"
apply(rule traverse_push2[OF change_fresh_push]) using dom assms by auto
finally show "traverse τs ⊆ ...".
qed (insert nonemp, auto)
qed
end
context
fixes P P' :: "('f,'v,'t,'l sharp) lts" and x :: 'v and ty :: 't
assumes fv: "fresh_variable_cond P P' x ty"
begin
lemma fresh_variable_addition:
assumes "cooperation_SN P'"
shows "cooperation_SN P"
unfolding indexed_rewriting.cooperation_SN_on_as_SN_on_traverse
proof(intro allI impI)
fix τs assume τs: "τs ⊆ sharp_transitions_of P" "τs ≠ {}"
let ?S = "change_fresh x ty"
let ?F = "transitions_step_lts P (flat_transitions_of P)"
let ?F' = "transitions_step_lts P (flat_transitions_of P')"
from fresh_variable_condD(4)[OF fv]
have lc: "assertion P' = assertion P" .
have ts: "transition_step_lts P' = transition_step_lts P"
by (intro ext, auto simp: lc)
from fresh_variable_condD(1)[OF fv]
have [simp]: "initial_states P' = initial_states P" by (auto simp: initial_states_def lc)
interpret indexed_rewriting "transition_step_lts P" .
from sharp_traverse_simulate[OF fv τs] obtain τs'
where τs': "τs' ⊆ sharp_transitions_of P'"
and nonemp: "τs' ≠ {}"
and sim: "traverse τs ⊆ traverse τs' O (change_fresh x ty)⇧*" (is "?T ⊆ ?T' O _") by auto
from τs' nonemp assms[unfolded ts, unfolded cooperation_SN_on_as_SN_on_traverse]
have "SN_on ?T' (?F'⇧* `` initial_states P)" by auto
from SN_on_Image_push[OF change_fresh_O_traverse this, OF fv] τs' SN_on_mono
have SN: "SN_on ?T' ((?F'⇧* O ?S⇧* ) `` initial_states P)" by (auto simp: relcomp_Image)
from flat_transitions_simulate[OF fv] have "?F⇧* ⊆ (?F' O ?S⇧* )⇧*" by (intro rtrancl_mono,auto)
also have "... ⊆ (?S ∪ ?F')⇧*" by regexp
also have "... = (?F')⇧* O ?S⇧*" unfolding rtrancl_U_push[OF change_fresh_O_flat_transitions[OF fv]]..
finally have "?F⇧* ⊆ ?F'⇧* O ?S⇧*" by auto
from SN_on_subset2[OF Image_mono[OF this] SN, OF subset_refl]
have "SN_on ?T' (?F⇧* `` initial_states P)" by auto
from SN_on_O_push[OF change_fresh_O_traverse, OF fv _ this] τs'
have "SN_on (?T' O ?S⇧* ) (?F⇧* `` initial_states P)" by auto
from SN_on_mono[OF this sim]
show "SN_on ?T (?F⇧* `` initial_states P)" by auto
qed
end
end
datatype ('f,'v,'ty,'tr) fresh_variable_addition_info = Fresh_Variable_Addition_Info
'v
'ty
"('tr × ('f,'v trans_var, 'ty) exp formula) list"
locale pre_transition_definability_checker =
lts where type_fixer = "TYPE('f×'t×'d)" +
pre_definability_checker where type_fixer = "TYPE('f×'v trans_var×'t×'d)" +
showsl_transition sa sa2
for type_fixer :: "('f::showl × 'v::showl × 't::showl × 'd) itself"
and sa :: "('f,'v,'t) exp ⇒ showsl"
and sa2 :: "('f,'v trans_var,'t)exp ⇒ showsl"
begin
definition fresh_variable_checker ::
"('f,'v,'t,'l :: showl,'tr :: showl) lts_impl ⇒ ('tr ⇒ ('f, 'v trans_var, 't) exp formula) ⇒ 'v ⇒ 't ⇒ showsl check" where
"fresh_variable_checker P f x ty ≡ do {
check_allm (λ (l, f). check ((x,ty) ∉ vars_formula f)
(showsl x o showsl_lit (STR '' is not fresh, it occurs in location condition of '') o showsl l))
(assertion_impl P);
check_allm (λ (tr,τ). let ψ = f tr in
(check (formula ψ) (showsl_lit (STR ''new transition formula seems to be not well-formed'')) ⪢
(case τ
of Transition l r φ ⇒
do {definability_checker (Post x) ty ψ;
check ((Post x,ty) ∉ vars_formula φ) (showsl_lit (STR ''Post x in transition formula'') o T.showsl_formula φ);
check ((Pre x, ty) ∉ vars_formula φ) (showsl_lit (STR ''Pre x in transition formula'') o T.showsl_formula φ)
})
<+? (λ s. showsl_lit (STR ''problem in transition formula of transition '') o showsl tr o showsl_nl o s)))
(transitions_impl P)
}
<+? (λ s. showsl_lit (STR ''fresh_variable_checker failed⏎'') o s)"
fun fresh_variable_addition :: "('f,'v,'t,'l :: showl,'tr :: showl) lts_impl ⇒ ('f, 'v, 't, 'tr) fresh_variable_addition_info
⇒ showsl + ('f, 'v, 't, 'l, 'tr) lts_impl" where
"fresh_variable_addition P (Fresh_Variable_Addition_Info x ty forms) = (let
m = Mapping.of_alist forms;
f = Mapping.lookup_default form_True m in
check_return (do {
check_allm (λ f. check (formula f) (showsl f o showsl_lit (STR '' is not a valid formula''))) (map snd forms);
fresh_variable_checker P f x ty
} <+? (λ s. showsl_lit (STR ''problem in adding fresh variable '') o showsl x o showsl_nl o s) )
(refine_transition_formulas P f))"
end
declare pre_transition_definability_checker.fresh_variable_checker_def[code]
declare pre_transition_definability_checker.fresh_variable_addition.simps[code]
locale transition_definability_checker =
pre_transition_definability_checker + definability_checker where type_fixer = "TYPE(_)"
begin
lemma fresh_variable_checker:
assumes ok: "isOK (fresh_variable_checker P f x ty)"
shows "fresh_variable_cond (lts_of P) (lts_of (refine_transition_formulas P f)) x ty"
(is "fresh_variable_cond _ ?P x ty")
proof(unfold fresh_variable_cond_def, intro conjI ballI2 ballI allI impI)
note ok = ok[unfolded fresh_variable_checker_def, simplified]
from ok show "lts.initial ?P = lts.initial (lts_of P)" by auto
{ fix l r φ
assume τ: "Transition l r φ ∈ transition_rules (lts_of P)"
then obtain tr where tr: "(tr, Transition l r φ) ∈ set (transitions_impl P)" by auto
with ok
have 1: "isOK (definability_checker (Post x) ty (f tr))"
and 2: "(Post x, ty) ∉ vars_formula φ" by auto
show "∃φ'.
Transition l r φ' ∈ transition_rules ?P ∧
(∀α. assignment α ⟶ α ⊨ φ ⟶ (∃a ∈ Values_of_type ty. α((Post x, ty) := a) ⊨ φ'))"
proof(intro exI conjI allI impI)
from tr show "Transition l r (φ ∧⇩f f tr) ∈ transition_rules ?P" by (unfold refine_transition_formulas_def, force)
fix α
assume α: "assignment α"
and 4: "α ⊨ φ"
from definability_checker[OF 1 α] obtain a
where 5: "a ∈ Values_of_type ty"
and 6: "α((Post x, ty) := a) ⊨ f tr" by auto
from 2 4 have "α((Post x, ty) := a) ⊨ φ" by auto
with 6 have "α((Post x, ty) := a) ⊨ φ ∧⇩f f tr" by auto
with 5 show "∃a ∈ Values_of_type ty. α((Post x, ty) := a) ⊨ (φ ∧⇩f f tr)" by auto
qed
}
show "assertion (lts_of (refine_transition_formulas P f)) =
assertion (lts_of P)"
by (cases P, auto simp: refine_transition_formulas_def assertion_of_def)
from ok have lc: "⋀ l f. (l,f) ∈ set (assertion_impl P) ⟹ (x,ty) ∉ vars_formula f" by auto
show lc: "(x, ty) ∉ vars_formula (assertion (lts_of P) l)" for l
by (unfold lts_of_simps assertion_of_def, rule map_of_defaultI[OF lc], auto)
{ fix τ' s t a
assume τ': "τ' ∈ transition_rules ?P"
and st: "(s,t) ∈ transition_step_lts (lts_of P) τ'"
and a: "a ∈ Values_of_type ty"
let ?s = "s |⇩s (x,ty) := a"
show "∃b ∈ Values_of_type ty. (?s, t |⇩s (x, ty) := b) ∈ transition_step_lts (lts_of P) τ'"
proof(cases τ')
case (Transition l r φ')
from τ'[unfolded this, simplified] obtain tr
where tr: "(tr, Transition l r φ') ∈ set (transitions_impl (refine_transition_formulas P f))"
by auto
from Transition_mem_refine_transition_formulas[OF this] obtain φ
where "(tr, Transition l r φ) ∈ set (transitions_impl P)" and φ': "φ' = (φ ∧⇩f f tr)" by auto
with ok
have 1: "isOK (definability_checker (Post x) ty (f tr))"
and 2: "(Post x, ty) ∉ vars_formula φ"
and 3: "(Pre x, ty) ∉ vars_formula φ" by auto
let ?ppi = "pre_post_inter"
let ?α = "valuation s"
let ?β = "valuation t"
from τ' st φ' Transition obtain γ
where γ: "assignment γ" and "?ppi ?α ?β γ ⊨ φ ∧⇩f f tr"
and lc': "state_lts (lts_of P) s" "state_lts (lts_of P) t" by auto
then have 5: "?ppi ?α ?β γ ⊨ φ" and 6: "?ppi ?α ?β γ ⊨ f tr" by auto
have ass: "assignment ((?ppi (valuation ?s) ?β γ))" unfolding assignment_pre_post_inter
proof (intro conjI γ)
show "assignment ?β" using st by auto
from st have "assignment ?α" by auto
with a
show "assignment (valuation s |⇩s (x, ty) := a)" by auto
qed
from definability_checker[OF 1 this] obtain b
where b: "b ∈ Values_of_type ty"
and *: "(?ppi (valuation ?s) ?β γ)((Post x, ty) := b) ⊨ f tr" by blast
let ?t = "t |⇩s (x,ty) := b"
from 5 have "(?ppi ?α ?β γ)((Pre x, ty) := a) ⊨ φ"
unfolding satisfies_with_fresh_var[OF 3] by auto
then have "?ppi (valuation ?s) ?β γ ⊨ φ" by auto
then have "(?ppi (valuation ?s) ?β γ)((Post x, ty) := b) ⊨ φ"
unfolding satisfies_with_fresh_var[OF 2] by auto
then have "?ppi (valuation ?s) (valuation ?t) γ ⊨ φ" by auto
with * have "?ppi (valuation ?s) (valuation ?t) γ ⊨ φ'" by (auto simp: φ')
with γ a st b lc' lc have "(?s,?t) ∈ transition_step_lts (lts_of P) τ'" by (auto simp: Transition)
with b show ?thesis by auto
qed
}
qed
lemma fresh_variable_addition_impl:
assumes ok: "isOK (fresh_variable_checker P f x ty)"
and SN: "cooperation_SN_impl (refine_transition_formulas P f)"
shows "cooperation_SN_impl P"
proof
assume P: "lts_impl P"
have "lts_impl (refine_transition_formulas P f)"
by (rule lts_impl_refine_transition_formulas[OF P], insert ok[unfolded fresh_variable_checker_def], auto)
then show "cooperation_SN (lts_of P)"
using SN fresh_variable_addition[OF fresh_variable_checker[OF ok]]
by auto
qed
lemma check_fresh_variable_addition:
assumes fva: "fresh_variable_addition P info = return Q"
and SN: "cooperation_SN_impl Q"
shows "cooperation_SN_impl P"
proof (cases info)
case (Fresh_Variable_Addition_Info x ty forms)
from fva[unfolded this] obtain f where ok: "isOK(fresh_variable_checker P f x ty)"
and Q: "Q = refine_transition_formulas P f"
and f: "f = Mapping.lookup_default form_True (Mapping.of_alist forms)" by (auto simp: Let_def)
show ?thesis using fresh_variable_addition_impl ok Q SN by auto
qed
end
end