theory LTS
imports
"Abstract-Rewriting.Abstract_Rewriting"
Show.Show_Instances
Deriving.Compare_Generator
Ord.Formula
Ord.Non_Inf_Order
Auxx.Map_Of
begin
hide_const (open) FuncSet.Pi
datatype 'v trans_var = Pre 'v | Post 'v | Intermediate 'v
instantiation trans_var :: (showl) showl
begin
fun showsl_trans_var where
"showsl_trans_var (Pre v) = showsl v"
| "showsl_trans_var (Post v) = showsl v o showsl_lit (STR 0x27)"
| "showsl_trans_var (Intermediate v) = showsl v o showsl_lit (STR ''#'')"
definition "showsl_list (xs :: 'a trans_var list) = default_showsl_list showsl xs"
instance ..
end
derive compare_order trans_var
fun untrans_var where
"untrans_var (Pre x) = x"
| "untrans_var (Post x) = x"
| "untrans_var (Intermediate x) = x"
type_synonym ('f,'v,'t) transition_formula = "('f,'v trans_var,'t) exp formula"
datatype ('f,'v,'t,'l) transition_rule =
Transition 'l 'l "('f,'v trans_var,'t) exp formula"
fun source where
"source (Transition l _ _) = l"
fun target where
"target (Transition _ r _) = r"
fun transition_formula where
"transition_formula (Transition _ _ φ) = φ"
datatype ('v,'t,'d,'l) state = State (valuation: "('v,'t,'d) valuation") (location: 'l)
fun relabel_state where "relabel_state f (State α l) = State α (f l)"
lemma valuation_relabel_state[simp]: "valuation (relabel_state f s) = valuation s"
and location_relabel_state[simp]: "location (relabel_state f s) = f (location s)"
by (atomize(full), cases s, auto)
record ('f,'v,'t,'l) lts =
initial :: "'l set"
transition_rules :: "('f,'v,'t,'l) transition_rule set"
assertion :: "'l ⇒ ('f,'v,'t) exp formula"
definition nodes_lts :: "('f,'v,'t,'l) lts ⇒ 'l set" where
"nodes_lts P = source ` transition_rules P ∪ target ` transition_rules P"
definition sub_lts :: "('f,'v,'t,'l) lts ⇒ ('f,'v,'t,'l) lts ⇒ bool" where
"sub_lts P Q ≡ initial P ⊆ initial Q ∧ transition_rules P ⊆ transition_rules Q ∧ assertion P = assertion Q"
lemma sub_ltsI[intro!]:
assumes "initial P ⊆ initial Q"
and "transition_rules P ⊆ transition_rules Q"
and "assertion P = assertion Q"
shows "sub_lts P Q" by (insert assms, auto simp: sub_lts_def)
lemma sub_ltsD:
assumes "sub_lts P Q"
shows "initial P ⊆ initial Q"
and "transition_rules P ⊆ transition_rules Q"
and "assertion P = assertion Q"
using assms unfolding sub_lts_def by auto
lemma sub_ltsE[elim!]:
assumes "sub_lts P Q"
and "initial P ⊆ initial Q ⟹ transition_rules P ⊆ transition_rules Q ⟹
assertion P = assertion Q ⟹ thesis"
shows thesis using assms unfolding sub_lts_def by auto
lemma sub_lts_trans[trans]: "sub_lts P Q ⟹ sub_lts Q R ⟹ sub_lts P R" by auto
definition call_graph_of_lts :: "('f,'v,'t,'l) lts ⇒ 'l rel" where
"call_graph_of_lts P = { (source τ, target τ) | τ. τ ∈ transition_rules P}"
definition delete_transitions :: "('f,'v,'t,'l) lts ⇒ ('f,'v,'t,'l) transition_rule set ⇒ ('f,'v,'t,'l) lts" where
"delete_transitions lts ts = ⦇lts.initial = lts.initial lts, transition_rules = transition_rules lts - ts, assertion = assertion lts⦈"
lemma delete_transitions_simps[simp]:
"lts.initial (delete_transitions P TD) = lts.initial P"
"transition_rules (delete_transitions lts ts) = transition_rules lts - ts"
"assertion (delete_transitions lts ts) = assertion lts"
by (simp_all add: delete_transitions_def)
lemma delete_transistions_eq[simp]:
"delete_transitions P (transition_rules P ∩ TD) = delete_transitions P TD"
unfolding sub_lts_def delete_transitions_def by auto
lemma delete_transitions_sublts: "sub_lts (delete_transitions lts ts) lts"
unfolding sub_lts_def delete_transitions_def by auto
locale lts = prelogic where type_fixer = type_fixer
for type_fixer :: "('f×'t×'d) itself"
begin
fun transition_rule where
"transition_rule (Transition l r φ) = formula φ"
lemma transition_ruleI:
assumes "⋀l r φ. τ = Transition l r φ ⟹ formula φ"
shows "transition_rule τ"
using assms by (cases τ, auto)
lemma transition_ruleE[elim]:
assumes "transition_rule τ" "⋀l r φ. τ = Transition l r φ ⟹ formula φ ⟹ thesis"
shows thesis using assms by (cases τ, auto)
definition state :: "('v,'t,'d,'l) state ⇒ bool" where [simp]: "state s ≡ assignment (valuation s)"
definition lts :: "('f,'v,'t,'l) lts ⇒ bool" where
"lts P ≡ (∀ τ ∈ transition_rules P. transition_rule τ) ∧ (∀ l. formula (assertion P l))"
lemma ltsI[intro]:
assumes "⋀τ. τ ∈ transition_rules P ⟹ transition_rule τ" and "⋀ l. formula (assertion P l)"
shows "lts P" using assms by (auto simp: lts_def)
lemma ltsE[elim]:
assumes "lts P"
and "(⋀τ. τ ∈ transition_rules P ⟹ transition_rule τ) ⟹ (⋀ l. formula (assertion P l)) ⟹ thesis"
shows thesis using assms by (auto simp: lts_def)
fun pre_post_inter where
"pre_post_inter α β γ (Pre x,t) = α (x,t)"
| "pre_post_inter α β γ (Post x,t) = β (x,t)"
| "pre_post_inter α β γ (Intermediate x,t) = γ (x,t)"
lemma pre_post_inter_same: "pre_post_inter α α α x = α (apfst untrans_var x)"
proof(cases x)
case (Pair a b)
then show ?thesis by (cases a, auto)
qed
lemma pre_post_inter_same_exp:
"⟦e⟧(pre_post_inter α α α) = ⟦rename_vars untrans_var e⟧α"
proof (induct e)
case (Var x)
show ?case
proof(cases x)
case (Pair a b)
then show ?thesis by (cases a, auto)
qed
next
case (Fun x1a x2)
then have [simp]: "(map (λs. ⟦s⟧ (pre_post_inter α α α)) x2) =
(map (λx. ⟦rename_vars untrans_var x⟧ α) x2)" by (induct x2, auto)
show ?case by (auto simp add: o_def)
qed
lemma pre_post_inter_same_satisfies:
"pre_post_inter α α α ⊨ φ ⟷ α ⊨ rename_vars untrans_var φ"
by(induct φ, auto simp: pre_post_inter_same_exp)
context
fixes α β γ :: "('v,'t,'d) valuation"
begin
abbreviation "δ ≡ pre_post_inter α β γ"
lemma pre_post_inter_update[simp]:
"δ((Pre x,ty):=a) = pre_post_inter (α((x,ty):=a)) β γ" (is "?l1 = ?r1")
"δ((Post x,ty):=a) = pre_post_inter α (β((x,ty):=a)) γ" (is "?l2 = ?r2")
"δ((Intermediate x,ty):=a) = pre_post_inter α β (γ((x,ty):=a))" (is "?l3 = ?r3")
proof-
have "?l1 xx = ?r1 xx ∧ ?l2 xx = ?r2 xx ∧ ?l3 xx = ?r3 xx" for xx by(cases xx, cases "fst xx", auto)
then show "?l1 = ?r1" "?l2 = ?r2" "?l3 = ?r3" by auto
qed
lemma assignment_pre_post_inter[simp]:
"assignment δ ⟷ assignment α ∧ assignment β ∧ assignment γ" (is "?l ⟷ ?r")
proof(intro iffI)
assume ?r
then have "δ (x, t) ∈ Values_of_type t" for x t by(cases x, auto)
then show ?l by auto
next
assume ?l
note assignmentD[OF this, of "(_,_)"]
from this[of "Pre _"] this[of "Post _"] this[of "Intermediate _"] show ?r by auto
qed
lemma eval_pre_post_inter_rename_vars[simp]:
shows "⟦rename_vars Pre e⟧δ = ⟦e⟧α" (is ?a)
and "⟦rename_vars Post e⟧δ = ⟦e⟧β" (is ?b)
and "⟦rename_vars Intermediate e⟧δ = ⟦e⟧γ" (is ?c)
proof -
have "?a ∧ ?b ∧ ?c"
proof(induct e)
case (Var xx)
show ?case by (cases xx, auto simp: rename_vars_exp_def)
case IH: (Fun f es)
from IH have 1: "map (λe.⟦e⟧δ) (map (rename_vars Pre) es) = map (λe.⟦e⟧α) es" by(induct es; auto)
from IH have 2: "map (λe.⟦e⟧δ) (map (rename_vars Post) es) = map (λe.⟦e⟧β) es" by(induct es; auto)
from IH have 3: "map (λe.⟦e⟧δ) (map (rename_vars Intermediate) es) = map (λe.⟦e⟧γ) es" by(induct es; auto)
show ?case unfolding rename_vars_exp_simps eval.simps 1 2 3 by auto
qed
then show ?a ?b ?c by auto
qed
lemma pre_post_inter_satisfies_rename_vars[simp]:
"δ ⊨ rename_vars Pre φ ⟷ α ⊨ φ"
"δ ⊨ rename_vars Post φ ⟷ β ⊨ φ"
"δ ⊨ rename_vars Intermediate φ ⟷ γ ⊨ φ" by (induct φ, auto)
end
definition transition_step :: "_ ⇒ _ ⇒ _" where
"transition_step lc τ ≡
case τ of Transition l r φ ⇒ { (s,t). ∃ γ. lc s ∧ lc t ∧ assignment γ ∧ location s = l ∧ location t = r ∧
pre_post_inter (valuation s) (valuation t) γ ⊨ φ}"
lemma mem_transition_stepI:
assumes "lc s" "lc t"
"⋀l r φ. τ = Transition l r φ ⟹
assignment γ ∧ location s = l ∧ location t = r ∧ pre_post_inter (valuation s) (valuation t) γ ⊨ φ"
shows "(s,t) ∈ transition_step lc τ"
using assms by (atomize, cases τ, auto simp: transition_step_def)
lemma mem_transition_step_TransitionI[intro!]:
assumes "lc s" "lc t" "location s = l" "location t = r" "assignment γ" "pre_post_inter (valuation s) (valuation t) γ ⊨ φ"
shows "(s,t) ∈ transition_step lc (Transition l r φ)"
using assms by (auto simp: transition_step_def)
lemma mem_transition_stepE[elim, consumes 1, case_names Skip Transition]:
assumes "(s,t) ∈ transition_step lc τ"
"⋀φ γ. τ = Transition (location s) (location t) φ ⟹ lc s ⟹ lc t ⟹
assignment γ ⟹ pre_post_inter (valuation s) (valuation t) γ ⊨ φ ⟹ thesis"
shows thesis
using assms by (cases τ; auto simp: transition_step_def)
lemma mem_transition_step_TransitionE[elim!]:
assumes "(s,t) ∈ transition_step lc (Transition l r φ)"
"⋀γ. lc s ⟹ lc t ⟹ location s = l ⟹ location t = r ⟹
assignment γ ⟹ pre_post_inter (valuation s) (valuation t) γ ⊨ φ ⟹ thesis"
shows thesis using assms by auto
lemma transition_step_dom: "transition_step lc τ ⊆ Collect lc × Collect lc" by (auto elim: mem_transition_stepE)
abbreviation transitions_step where "transitions_step P τs ≡ ⋃ (transition_step P ` τs)"
abbreviation transitions_steps where "transitions_steps P τs ≡ (transitions_step P τs)⇧*"
abbreviation "state_lts (P::('f,'v,'t,'l) lts) s ≡ state s ∧ (valuation s ⊨ assertion P (location s))"
abbreviation transitions_lts where "transitions_lts P ≡ transitions_step (state_lts P)"
abbreviation transition_step_lts where "transition_step_lts P ≡ transition_step (state_lts P)"
abbreviation transitions_steps_lts where "transitions_steps_lts P ≡ transitions_steps (state_lts P)"
abbreviation transitions_step_lts where "transitions_step_lts P ≡ transitions_step (state_lts P)"
definition transition :: "('f,'v,'t,'l) lts ⇒ ('v,'t,'d,'l) state rel" where
"transition P ≡ transitions_lts P (transition_rules P)"
lemma mem_transitionI[intro!]:
"τ ∈ transition_rules P ⟹ (s,t) ∈ transition_step_lts P τ ⟹ (s,t) ∈ transition P"
unfolding transition_def by auto
lemma mem_transitionE[elim]:
assumes "(s,t) ∈ transition P"
and "⋀φ γ. Transition (location s) (location t) φ ∈ transition_rules P ⟹
state_lts P s ⟹ state_lts P t ⟹ assignment γ ⟹ pre_post_inter (valuation s) (valuation t) γ ⊨ φ ⟹ thesis"
shows "thesis"
using assms unfolding transition_def by auto
lemma mem_transition_location:
"(s,t) ∈ transition P ⟹ location s ∈ nodes_lts P"
by (auto intro!: rev_image_eqI simp: nodes_lts_def elim!: mem_transitionE)
lemma mem_transition_dom:
assumes "(s,t) ∈ transition P"
shows "state_lts P s" and "state_lts P t"
using assms by auto
lemma transition_dom: "transition P ⊆ Collect (state_lts P) × Collect (state_lts P)" by auto
definition skip_formula :: "('f,'v trans_var,'t) exp formula ⇒ bool" where
"skip_formula φ ≡ ∀ α. assignment α ⟶ (pre_post_inter α α α ⊨ φ)"
lemma skip_formula_transition_step:
assumes "skip_formula φ" and "assignment α"
and lc: "lc (State α a)" "lc (State α b)"
shows "(State α a, State α b) ∈ transition_step lc (Transition a b φ)"
using assms(1)[unfolded skip_formula_def] assms(2) lc by auto
lemma skip_formula_transitions:
assumes "Transition a b φ ∈ transition_rules P"
and "skip_formula φ"
and "assignment α"
and "α ⊨ assertion P a" "α ⊨ assertion P b"
shows "(State α a, State α b) ∈ transition P"
using skip_formula_transition_step[OF assms(2-3), of "state_lts P" a b] assms(1,3-5) by auto
definition skip_transition :: "_ ⇒ bool" where
"skip_transition τ = (case τ of Transition _ _ φ ⇒ skip_formula φ)"
lemma skip_transition_step: assumes "skip_transition τ"
and "assignment α"
and "lc (State α (source τ))" "lc (State α (target τ))"
shows "(State α (source τ), State α (target τ)) ∈ transition_step lc τ"
proof (cases τ)
case (Transition a b φ)
with assms have "skip_formula φ" unfolding skip_transition_def by auto
from skip_formula_transition_step[OF this assms(2), of lc, OF assms(3-4)]
show ?thesis unfolding Transition by auto
qed
lemma skip_transition: assumes "τ ∈ transition_rules P"
and "skip_transition τ"
and "assignment α"
and "α ⊨ assertion P (source τ)" "α ⊨ assertion P (target τ)"
shows "(State α (source τ), State α (target τ)) ∈ transition P"
using assms by (auto intro!: skip_transition_step)
definition initial_states :: "('f,'v,'t,'l) lts ⇒ ('v,'t,'d,'l) state set" where
"initial_states P = { s. location s ∈ initial P ∧ state_lts P s}"
lemma initial_states: "initial_states P ⊆ Collect (state_lts P)" unfolding initial_states_def by auto
lemma initial_states_delete_transitions[simp]:
"initial_states (delete_transitions P TD) = initial_states P"
by (simp add: initial_states_def)
abbreviation lts_termination :: "('f,'v,'t,'l) lts ⇒ bool" where
"lts_termination P ≡ SN_on (transition P) (initial_states P)"
abbreviation reachable_states :: "('f,'v,'t,'l) lts ⇒ ('v,'t,'d,'l) state set" where
"reachable_states P ≡ (transition P)⇧* `` initial_states P"
definition lts_safe :: "('f,'v,'t,'l) lts ⇒ 'l set ⇒ bool" where
"lts_safe P err ≡ ∀ α l. l ∈ err ⟶ State α l ∉ reachable_states P"
lemma reachable_state: assumes "s ∈ reachable_states P" shows "state_lts P s"
proof -
from assms obtain t where steps: "(t, s) ∈ (transition P)^*"
and t: "state_lts P t" unfolding initial_states_def by auto
from steps show ?thesis by (induct rule: rtrancl_induct, insert t, auto)
qed
lemma sub_lts_initial_states: "sub_lts P Q ⟹ initial_states P ⊆ initial_states Q"
by (auto simp: initial_states_def)
lemma reachable_states_mono:
assumes "sub_lts P Q"
shows "reachable_states P ⊆ reachable_states Q"
proof
have tr: "transition P ⊆ transition Q" using assms by (auto elim!: mem_transitionE)
fix x
assume "x ∈ reachable_states P"
then obtain start where "(start,x) ∈ (transition P)⇧*" "start ∈ initial_states P" by auto
then have "(start,x) ∈ (transition Q)⇧*" "start ∈ initial_states Q"
using rtrancl_mono[OF tr] assms by (auto simp: initial_states_def)
then show "x ∈ reachable_states Q" by auto
qed
subsection‹Invariants›
definition invariant :: "('f,'v,'t,'l) lts ⇒ 'l ⇒ ('f,'v,'t) exp formula ⇒ bool" where
"invariant P l φ ≡ formula φ ∧ (∀α. State α l ∈ reachable_states P ⟶ α ⊨ φ)"
lemma invariantI[intro]:
assumes "formula φ" and "⋀α. State α l ∈ reachable_states P ⟹ α ⊨ φ" shows "invariant P l φ"
using assms by (auto simp: invariant_def)
lemma invariantE[elim]:
assumes "invariant P l φ"
and "formula φ ⟹ (⋀α. State α l ∈ reachable_states P ⟹ α ⊨ φ) ⟹ thesis"
shows thesis using assms by (auto simp: invariant_def)
lemma invariantD[dest]:
assumes "invariant P l φ" "State α l ∈ reachable_states P"
shows "formula φ ∧ α ⊨ φ" using assms by auto
definition invariants :: "('f,'v,'t,'l) lts ⇒ ('l ⇒ ('f,'v,'t) exp formula) ⇒ bool"
where "invariants P Φ ≡ ∀l. invariant P l (Φ l)"
lemma invariantsI[intro!]:
assumes "⋀l :: 'l. invariant P l (Φ l)"
shows "invariants P Φ" by (insert assms, auto simp: invariants_def)
lemma invariantsE[elim!]:
assumes "invariants P Φ" and "(⋀l :: 'l. invariant P l (Φ l)) ⟹ thesis"
shows "thesis" by (insert assms, auto simp: invariants_def)
lemma invariantsD:
assumes "invariants P Φ" shows "invariant P l (Φ l)" by (insert assms, auto)
lemma invariants_mono:
assumes sub: "sub_lts P' P" and inv: "invariants P Φ" shows "invariants P' Φ"
proof(intro invariantsI invariantI)
fix l α assume "State α l ∈ reachable_states P'"
with reachable_states_mono[OF sub] have "State α l ∈ reachable_states P" by auto
from inv this show "α ⊨ Φ l" by auto
next
from inv show "formula (Φ l)" for l by auto
qed
end
subsection ‹An Implementation of Labeled Transition Systems›
type_synonym ('f,'v,'t,'l,'tr) transitions_impl = "('tr × ('f,'v,'t,'l) transition_rule) list"
type_synonym ('f,'v,'t,'l) assertion_impl = "('l × ('f,'v,'t) exp formula) list"
datatype ('f,'v,'t,'l,'tr) lts_impl = Lts_Impl
(initial: "'l list")
(transitions_impl: "('f,'v,'t,'l,'tr) transitions_impl")
(assertion_impl: "('f,'v,'t,'l) assertion_impl")
definition "transition_of Pi ≡ the ∘ map_of (lts_impl.transitions_impl Pi)"
definition "assertion_of Pi = map_of_default form_True (lts_impl.assertion_impl Pi)"
lemma transition_of_code[code]: "transition_of Pi = map_of_total
(λ a. showsl_lit (STR ''access to non-existing transition '') o showsl a o
showsl_lit (STR ''⏎available transitions:⏎'') o showsl_list (map fst (lts_impl.transitions_impl Pi))) (lts_impl.transitions_impl Pi)"
unfolding transition_of_def by simp
definition lts_of :: "('f,'v,'t,'l,'tr) lts_impl ⇒ ('f,'v,'t,'l) lts" where
"lts_of Pi = ⦇
lts.initial = set (lts_impl.initial Pi),
transition_rules = snd ` set (lts_impl.transitions_impl Pi),
assertion = assertion_of Pi ⦈"
lemma lts_of_simps[simp]:
"lts.initial (lts_of Pi) = set (lts_impl.initial Pi)"
"transition_rules (lts_of Pi) = snd ` set (lts_impl.transitions_impl Pi)"
"assertion (lts_of Pi) = assertion_of Pi"
by (auto simp: lts_of_def)
fun succ_transitions :: "('f,'v,'t,'l,'tr) lts_impl ⇒ 'l ⇒ ('f,'v,'t,'l) transition_rule list" where
"succ_transitions (Lts_Impl i ts lc) l = [ τ. (tr,τ) ← ts, source τ = l ]"
lemma succ_transitions[simp]:
"set (succ_transitions Pi l) =
{ τ. τ ∈ transition_rules (lts_of Pi) ∧ source τ = l}" by (cases Pi, auto)
definition "nodes_lts_impl Pi = remdups (map (source ∘ snd) (lts_impl.transitions_impl Pi) @ map (target o snd) (lts_impl.transitions_impl Pi))"
lemma nodes_lts_of[code_unfold]: "nodes_lts (lts_of Pi) = set (nodes_lts_impl Pi)"
by (unfold nodes_lts_impl_def nodes_lts_def, force)
declare nodes_lts_of[symmetric,simp]
context lts begin
fun lts_impl where "lts_impl (Lts_Impl Φ Ti lc) = (
(∀ (tr,τ) ∈ set Ti. transition_rule τ) ∧
(∀ (l,φ) ∈ set lc. formula φ))"
lemma lts_impl: "lts_impl P ⟹ lts (lts_of P)"
by (cases P, auto simp: lts_def assertion_of_def intro: map_of_defaultI)
lemma lts_implI:
assumes
"⋀tr τ. (tr,τ) ∈ set (lts_impl.transitions_impl Pi) ⟹ transition_rule τ"
"⋀l φ. (l,φ) ∈ set (lts_impl.assertion_impl Pi) ⟹ formula φ"
shows "lts_impl Pi"
using assms by (cases Pi, auto)
lemma lts_implE:
assumes "lts_impl Pi"
and "
(⋀tr τ. (tr,τ) ∈ set (lts_impl.transitions_impl Pi) ⟹ transition_rule τ) ⟹
(⋀l φ. (l,φ) ∈ set (lts_impl.assertion_impl Pi) ⟹ formula φ) ⟹ thesis"
shows thesis
by (rule assms(2); cases Pi, insert assms(1), auto simp: assertion_of_def intro: map_of_defaultI)
lemma lts_impl_formula_assertion_of:
assumes "lts_impl Pi"
shows "⋀l. formula (assertion_of Pi l)"
by (unfold assertion_of_def, rule map_of_defaultI, insert assms, auto elim:lts_implE)
lemma lts_impl_transitions_impl:
assumes "lts_impl Pi"
and "(tr,τ) ∈ set (lts_impl.transitions_impl Pi)"
shows "transition_rule τ"
using assms by (elim lts_implE)
definition "check_lts_impl Pi = (case Pi of Lts_Impl I Ti lc ⇒ do {
check_allm (λ (tr, t). check (transition_rule t) (showsl_lit (STR ''ill-formed transition in LTS''))) Ti;
check_allm (λ (l, f). check (formula f) (showsl_lit (STR ''ill-formed location condition in LTS''))) lc})"
lemma check_lts_impl[simp]: "isOK (check_lts_impl Pi) = lts_impl Pi"
by (cases Pi, auto simp: lts_def check_lts_impl_def)
subsection ‹Deleting transitions›
fun sub_lts_impl where "sub_lts_impl (Lts_Impl Φ ts lc) (Lts_Impl I' ts' lc')
= (Φ = I' ∧ mset ts ⊆# mset ts' ∧ lc = lc')"
lemma set_filter_mem: "set (filter (λx. x ∈ X) xs) = X ∩ set xs" by auto
lemma sub_lts_impl_sub_lts: "sub_lts_impl P Q ⟹ sub_lts (lts_of P) (lts_of Q)"
proof (cases P, cases Q, goal_cases)
case (1 I ts lc I' ts' lc')
then have "mset ts ⊆# mset ts'" by auto
from set_mset_mono[OF this] have sub: "set ts ⊆ set ts'" by auto
{ fix a b
assume "(a,b) ∈ set ts"
with sub have "(a,b) ∈ set ts'" by auto
then have "b ∈ snd ` set ts'" by auto
}
with 1 show ?thesis by (auto simp: assertion_of_def)
qed
lemma distinct_count_le_1:
"distinct xs ⟷ (∀x. count (mset xs) x ≤ 1)"
by (metis count_greater_eq_one_iff distinct_count_atmost_1 eq_iff in_multiset_in_set nat_le_linear not_in_iff)
lemma distinct_mset_subseteq:
assumes "distinct ys" and "mset xs ⊆# mset ys" shows "distinct xs"
apply (insert assms, unfold distinct_count_le_1 subseteq_mset_def) using le_trans by blast
lemma sub_lts_impl: "sub_lts_impl P Q ⟹ lts_impl Q ⟹ lts_impl P"
proof (cases P, cases Q, goal_cases)
case (1 Φ ts lc Φ' ts' lc')
from 1 have msub: "mset ts ⊆# mset ts'" by auto
from set_mset_mono[OF msub] have set: "set ts ⊆ set ts'" by auto
{
fix tr τ assume "(tr, τ) ∈ set ts"
with 1 set set_filter_mem[of "set ts" ts'] have "transition_rule τ" by (auto elim!: ballE[of _ _ "(tr,τ)"])
}
then show ?case using 1 by auto
qed
fun update_transitions_impl where
"update_transitions_impl (Lts_Impl i ts lc) ts' = (Lts_Impl i ts' lc)"
lemma update_transitions_impl_simps[simp]:
"transitions_impl (update_transitions_impl P v) = v"
"initial (update_transitions_impl P v) = lts_impl.initial P"
"assertion_impl (update_transitions_impl P v) = lts_impl.assertion_impl P" by (atomize(full),cases P,auto)
definition diff_by_label :: "('a × 'b) list ⇒ 'a set ⇒ ('a × 'b) list" where
"diff_by_label pairs L = filter (λ v. fst v ∉ L) pairs"
lemma diff_by_label_subset [intro]:
"set (diff_by_label a b) ⊆ set a"
unfolding diff_by_label_def by (induct a, auto)
lemma map_fst_diff_by_label:
"map fst (diff_by_label pairs L) = filter (λv. v ∉ L) (map fst pairs)"
by(induct pairs, auto simp: diff_by_label_def)
lemma diff_by_label_preseves_distinct:
"distinct (map fst a) ⟹ distinct (map fst (diff_by_label a b))"
by (unfold map_fst_diff_by_label, rule distinct_filter)
definition del_transitions_impl ::
"('f,'v,'t,'lx,'tr) lts_impl ⇒ 'tr list ⇒ ('f,'v,'t,'lx,'tr) lts_impl" where
"del_transitions_impl P TD
= (update_transitions_impl P (diff_by_label (transitions_impl P) (set TD)))"
lemma transitions_of_del_transitions_impl[simp]:
"transitions_impl (del_transitions_impl P D) = diff_by_label (transitions_impl P) (set D)"
unfolding del_transitions_impl_def by simp
lemma del_transitions_impl_set:
assumes "set transs ⊆ set transs2"
shows "set (diff_by_label transs (fst ` set TD)) ⊆ set transs2"
using diff_by_label_subset[of "transs" "(fst ` set TD)"] assms by simp
lemma del_transitions_impl:
shows "sub_lts_impl (del_transitions_impl Pi TD) Pi"
and "sub_lts (delete_transitions (lts_of Pi) {τ | τ tr. (tr,τ) ∈ set (transitions_impl Pi) ∧ tr ∈ set TD})
(lts_of (del_transitions_impl Pi TD))"
by (atomize(full), cases Pi, intro conjI sub_ltsI,
auto simp: assertion_of_def delete_transitions_def del_transitions_impl_def diff_by_label_def mset_filter)
definition "check_invariant_checker f ≡
∀ P. lts (lts_of P) ⟶ (case f P
of Inl _ ⇒ True
| Inr Φ ⇒ ∀l. invariant (lts_of P) l (Φ l) ∧ formula (Φ l))"
subsection ‹Refining transition formulas›
fun refine_transition_formula where
"refine_transition_formula (Transition l r φ) ψ = Transition l r (φ ∧⇩f ψ)"
definition "refine_transition_formulas P f ≡
Lts_Impl (lts_impl.initial P)
(map (λ(tr,τ). (tr, refine_transition_formula τ (f tr)))
(transitions_impl P))
(assertion_impl P)"
lemma transition_refine_transition_formula: assumes "transition_rule τ"
and "formula φ"
shows "transition_rule (refine_transition_formula τ φ)"
using assms by (cases τ, auto)
lemma lts_impl_refine_transition_formulas: assumes "lts_impl P"
and "⋀ tr τ. (tr, τ) ∈ set (transitions_impl P) ⟹ formula (f tr)"
shows "lts_impl (refine_transition_formulas P f)"
using assms unfolding refine_transition_formulas_def
by (cases P, auto intro!: transition_refine_transition_formula)
lemma initial_refine_transition_formulas[simp]:
"lts_impl.initial (refine_transition_formulas P f) = lts_impl.initial P"
by (auto simp: refine_transition_formulas_def)
lemma lc_refine_transition_formulas[simp]:
"assertion_impl (refine_transition_formulas P f) = assertion_impl P"
by (auto simp: refine_transition_formulas_def)
lemma Transition_mem_refine_transition_formulas:
assumes "(tr, Transition l r φ') ∈ set (transitions_impl (refine_transition_formulas Pi f))"
shows "∃φ. (tr, Transition l r φ) ∈ set (transitions_impl Pi) ∧ φ' = (φ ∧⇩f f tr)"
proof-
from assms[unfolded refine_transition_formulas_def,simplified]
obtain τ
where "(tr,τ) ∈ set (transitions_impl Pi)"
and "Transition l r φ' = refine_transition_formula τ (f tr)"
by auto
moreover then obtain φ
where "τ = Transition l r φ" and "φ' = (φ ∧⇩f f tr)" by (cases τ, auto)
ultimately show ?thesis by auto
qed
subsection ‹Switching between transition encodings›
fun transition_weakening where
"transition_weakening assr_l assr_r (Transition s_l t_l f_l) (Transition s_r t_r f_r) =
(s_l = s_r ∧ t_l = t_r ∧
(f_l ∧⇩f rename_vars Pre (assr_l s_l) ∧⇩f rename_vars Post (assr_l t_l) ⟹⇩f
f_r ∧⇩f rename_vars Pre (assr_r s_r) ∧⇩f rename_vars Post (assr_r t_r)))"
definition transitions_weakened where
"transitions_weakened assr_l assr_r l r
≡ ∀ t_l ∈ l. (∃ t_r ∈ r. transition_weakening assr_l assr_r t_l t_r)"
definition weakened_lts where
"weakened_lts P Q ≡ lts.initial P ⊆ lts.initial Q ∧
Ball (lts.initial P) (λ l. assertion P l ⟹⇩f assertion Q l) ∧
transitions_weakened (assertion P) (assertion Q) (transition_rules P) (transition_rules Q)"
lemma weakened_lts_initial_states: "weakened_lts P Q ⟹ initial_states P ⊆ initial_states Q"
proof fix x :: "('a, 't, 'd, 'b) state"
assume "weakened_lts P Q"
then have "∀l∈lts.initial P. ℒ (assertion P l) ⊆ ℒ (assertion Q l)" and
l:"location x ∈ lts.initial P ⟹ location x ∈ lts.initial Q"
by (auto simp: weakened_lts_def)
then have "location x ∈ lts.initial P ⟹
assignment (valuation x) ⟹ valuation x ⊨ assertion P (location x)
⟹ valuation x ⊨ assertion Q (location x)"
using satisfies_Language by blast
with l show "x ∈ initial_states P ⟹ x ∈ initial_states Q"
by (auto simp: initial_states_def weakened_lts_def)
qed
lemma transition_weakened_mono:
assumes "transitions_weakened (assertion P) (assertion Q) (transition_rules P) (transition_rules Q)"
shows "transition P ⊆ transition Q"
proof fix x y
assume "(x, y) ∈ transition P"
then obtain τ where τ:"τ ∈ transition_rules P" "(x,y) ∈ transition_step_lts P τ" by fastforce
from assms τ obtain t_r where t_r: "t_r ∈ transition_rules Q"
"transition_weakening (assertion P) (assertion Q) τ t_r"
unfolding transitions_weakened_def by force
then have trans_w:
"transition_formula τ ∧⇩f rename_vars Pre (assertion P (location x)) ∧⇩f rename_vars Post (assertion P (location y)) ⟹⇩f
transition_formula t_r ∧⇩f rename_vars Pre (assertion Q (location x)) ∧⇩f rename_vars Post (assertion Q (location y))"
"source τ = source t_r"
"target τ = target t_r"
using τ by (atomize(full),cases τ,cases t_r,auto)
from τ obtain γ where
γ:"δ (valuation x) (valuation y) γ ⊨ transition_formula τ"
"(valuation x) ⊨ assertion P (location x)"
"(valuation y) ⊨ assertion P (location y)"
"assignment γ" "assignment (valuation x)" "assignment (valuation y)" by auto
then have "δ (valuation x) (valuation y) γ ⊨ transition_formula τ
∧⇩f rename_vars Pre (assertion P (location x))
∧⇩f rename_vars Post (assertion P (location y))"
"assignment (δ (valuation x) (valuation y) γ)"
by auto
from impliesD[OF trans_w(1) this(2,1)] trans_w(2,3) τ(2) γ(4-)
have "(x,y) ∈ transition_step_lts Q t_r" by (cases t_r,auto)
with t_r(1) show "(x, y) ∈ transition Q" by auto
qed
lemma weakened_transition_mono: "weakened_lts P Q ⟹ transition P ⊆ transition Q"
by (intro transition_weakened_mono, auto simp:weakened_lts_def)
lemma weakened_reachable_states_mono:
assumes "weakened_lts P Q"
shows "reachable_states P ⊆ reachable_states Q"
proof
note ini= assms[THEN weakened_lts_initial_states]
note tr = weakened_transition_mono[OF assms]
fix x
assume "x ∈ reachable_states P"
then obtain start where "(start,x) ∈ (transition P)⇧*" "start ∈ initial_states P" by auto
then have "(start,x) ∈ (transition Q)⇧*" "start ∈ initial_states Q"
using rtrancl_mono[OF tr] ini by (auto simp: initial_states_def)
then show "x ∈ reachable_states Q" by auto
qed
lemma wekend_lts_SN_on:
assumes "weakened_lts P Q"
shows "lts_termination Q ⟹ lts_termination P"
proof -
note ini= SN_on_subset2[OF weakened_lts_initial_states[OF assms]]
note tr = SN_on_mono[OF _ weakened_transition_mono[OF assms]]
show "SN_on (transition Q) (initial_states Q) ⟹ SN_on (transition P) (initial_states P)"
by (rule tr,rule ini)
qed
subsection ‹Renaming variables on transitions›
fun transition_renamed where
"transition_renamed r ass_l ass_r (Transition s_l t_l f_l) (Transition s_r t_r f_r) =
(let r' = (λv. case v of Pre v' ⇒ Pre (r s_l v') | Post v' ⇒ Post (r t_l v') |
Intermediate v' ⇒ Intermediate (r s_l v') ) in
(s_l = s_r ∧ t_l = t_r
∧ f_r ⟹⇩f rename_vars r' f_l
∧ ass_r s_l ⟹⇩f rename_vars (r s_l) (ass_l s_l)
∧ ass_r t_l ⟹⇩f rename_vars (r t_l) (ass_l t_l)))"
definition renamed_lts where
"renamed_lts r L L⇩R ≡ lts.initial L⇩R ⊆ lts.initial L
∧ (∀ trL⇩R ∈ transition_rules L⇩R.
(∃ trL ∈ transition_rules L. transition_renamed r (assertion L) (assertion L⇩R) trL trL⇩R))"
lemma rename_delta_formula_implies:
assumes "δ v1 v2 v3 ⊨ map_formula (rename_vars (λv. case v of Pre v' ⇒ Pre (r1 v') | Post v' ⇒ Post (r2 v') |
Intermediate v' ⇒ Intermediate (r3 v'))) φ"
shows "δ (λ(x, t). v1 (r1 x, t)) (λ(x, t). v2 (r2 x, t)) (λ(x, t). v3 (r3 x, t)) ⊨ φ"
(is "?δ ⊨ φ" )
proof -
have "?δ (x, t) = δ v1 v2 v3 ((λv. case v of Pre v' ⇒ Pre (r1 v') | Post v' ⇒ Post (r2 v') |
Intermediate v' ⇒ Intermediate (r3 v')) x, t)" for x t
by (cases x) (auto)
then show ?thesis
using assms apply(subst (asm) satisfies_rename_vars[of ?δ])
by auto
qed
lemma lts_renaming_termination:
assumes "lts_termination L" "renamed_lts r L L⇩R"
shows "lts_termination L⇩R"
proof -
have 1: False if assms': "f 0 ∈ initial_states L⇩R" "∀i. (f i, f (Suc i)) ∈ transition L⇩R" for f
proof -
have af: "assignment (valuation (f i))" for i
using lts.state_def that(2) by blast
define f' where "f' = (λn. case (f n) of State v l ⇒ State (λ(x, t). v (r l x, t)) l)"
have af': "assignment (valuation (f' i))" for i
using lts.state_def that(2)
by (metis (mono_tags, lifting) af f'_def old.prod.case pre_sorted_algebra.assignmentE
pre_sorted_algebra.assignmentI snd_conv state.case_eq_if state.sel(1))
have b: "valuation (f 0) ⊨ (assertion L⇩R (location (f 0)))"
using that unfolding initial_states_def by (auto)
have a: "f' 0 ∈ initial_states L"
proof -
obtain v l where f0: "f 0 = State v l"
by (cases "f 0") auto
obtain τ⇩R φ⇩R where τ⇩R: "τ⇩R = Transition (location (f 0)) (location (f 1)) φ⇩R" "τ⇩R ∈ transition_rules L⇩R"
using assms' by fastforce
obtain τ where τ: "transition_renamed r (assertion L) (assertion L⇩R) τ τ⇩R"
using τ⇩R assms unfolding renamed_lts_def by blast
have a: "implies (assertion L⇩R l) (rename_vars (r l) (assertion L l))"
using τ⇩R f0 τ by (cases τ, cases τ⇩R) (simp)
have "v ⊨ rename_vars (r l) (assertion L l)"
by (rule impliesD) (use a f0 b af[of 0] in auto)
then have "(λ(x, t). v ((r l) x, t)) ⊨ assertion L l"
by (metis (mono_tags, lifting) old.prod.case satisfies_rename_vars)
then have "valuation (f' 0) ⊨ assertion L (location (f' 0))"
using b f0 assms unfolding renamed_lts_def
by (auto simp add: f'_def split: state.splits)
then show ?thesis
unfolding initial_states_def using af' assms that unfolding renamed_lts_def
f'_def initial_states_def
by (auto split: state.splits)
qed
have b: "(f' i, f' (Suc i)) ∈ transition L" for i
proof -
have "(f i, f (Suc i)) ∈ transition L⇩R"
using that by simp
then obtain γ φ where φ: "Transition (location (f i)) (location (f (Suc i))) φ ∈ transition_rules L⇩R"
"assignment γ" "δ (valuation (f i)) (valuation (f (Suc i))) γ ⊨ φ"
by auto
define t⇩R where "t⇩R = Transition (location (f i)) (location (f (Suc i))) φ"
obtain t where t: "t ∈ transition_rules L" "transition_renamed r (assertion L) (assertion L⇩R) t t⇩R"
apply(atomize_elim)
using assms φ unfolding renamed_lts_def t⇩R_def by auto
define φ⇩L where "φ⇩L = transition_formula t"
obtain x1 x2 x1a x2a where x1: "f i = State x1 x2" "f (Suc i) = State x1a x2a"
by (metis state.exhaust state.sel)
have a: "δ (valuation (f' i)) (valuation (f' (Suc i))) (λ(x,t). γ (r (location (f' i)) x, t)) ⊨ φ⇩L"
proof -
have "δ x1 x1a γ ⊨ φ"
using φ x1 by simp
then have "δ x1 x1a γ ⊨ map_formula (rename_vars (λv. case v of Pre v' ⇒ Pre (r x2 v') |
Post v' ⇒ Post (r x2a v') | Intermediate v' ⇒ Intermediate (r x2 v'))) φ⇩L"
apply(cases t)
using t x1 t⇩R_def af[of i] af[of "Suc i"] transition_renamed.simps φ assignment_pre_post_inter φ⇩L_def state.sel
by (auto intro!: impliesD[of φ] simp del : implies_Language)
then show ?thesis
unfolding f'_def using x1 rename_delta_formula_implies by fastforce
qed
have b: "Transition (location (f' i)) (location (f' (Suc i))) φ⇩L ∈ transition_rules L"
using t φ⇩L_def unfolding t⇩R_def f'_def transition_renamed.simps by (cases t) (auto split: state.splits)
have c: "(λ(x, t). x1 (r x2 x, t)) ⊨ assertion L x2"
proof -
have "x1 ⊨ assertion L⇩R x2"
using x1 ‹(f i, f (Suc i)) ∈ transition L⇩R› by auto
then have "x1 ⊨ rename_vars (r x2) (assertion L x2)"
using x1 t t⇩R_def by (cases t, auto)
(metis ‹(f i, f (Suc i)) ∈ transition L⇩R› impliesD implies_Language mem_transitionE state.sel(1) state_def)
then show ?thesis
using satisfies_rename_vars by (smt case_prod_conv)
qed
have d: "(λ(x, t). x1a (r x2a x, t)) ⊨ assertion L x2a"
proof -
have "x1a ⊨ assertion L⇩R x2a"
using x1 ‹(f i, f (Suc i)) ∈ transition L⇩R› by auto
then have "x1a ⊨ rename_vars (r x2a) (assertion L x2a)"
using x1 t t⇩R_def by (cases t, auto)
(metis ‹(f i, f (Suc i)) ∈ transition L⇩R› impliesD implies_Language mem_transitionE state.sel(1) state_def)
then show ?thesis
using satisfies_rename_vars by (smt case_prod_conv)
qed
from a show ?thesis
apply(intro mem_transitionI[of "Transition (location (f' i)) (location (f' (Suc i))) φ⇩L"])
using f'_def x1 a b c d af[of i] af[of "Suc i"] af'[of i] af'[of "Suc i"] φ(2)
by (auto split: state.splits intro: assignment_rename_vars simp add: assignment_rename_vars)
qed
then show ?thesis
using a b assms SN_onE by blast
qed
then show ?thesis
using SN_onI by blast
qed
end
declare lts.transition_rule.simps[code]
declare lts.check_lts_impl_def[code]
declare lts.del_transitions_impl_def[code]
declare lts.refine_transition_formulas_def[code]
declare lts.update_transitions_impl.simps[code]
declare lts.diff_by_label_def[code]
declare lts.refine_transition_formula.simps[code]
end