theory Invariant_Checker
imports
Certification_Monads.Check_Monad
"HOL-Library.RBT_Mapping"
LTS
Show_LTS
begin
text ‹In this theory we provide an invariant checker which establishes the
@{const lts.invariant} property.›
lemma is_ok_try_catch: "isOK (try e catch f) = (isOK(e) ∨ isOK( f (projl e)))"
by (cases e, auto simp: isOK_def)
subsection ‹ART›
datatype ('f,'v,'t,'l,'n) art_edge = is_cover_node: Cover 'n | Children "(('f,'v,'t,'l) transition_rule × 'n) list"
record ('f,'v,'t,'l,'n) art =
initial_nodes :: "'n list"
nodes :: "'n list"
edge :: "'n ⇒ ('f,'v,'t,'l,'n) art_edge"
node_location :: "'n ⇒ 'l"
node_invariant :: "'n ⇒ ('f,'v,'t) exp formula"
fun (in prelogic) transition_entailment ::
"('l ⇒ ('f,'v,'t) exp formula) ⇒ ('f,'v,'t) exp formula ⇒ ('f,'v,'t,'l) transition_rule ⇒ ('f,'v,'t) exp formula ⇒ bool"
where
"transition_entailment lc φ (Transition l r χ) ψ =
(rename_vars Pre (lc l) ∧⇩f rename_vars Post (lc r) ∧⇩f rename_vars Pre φ ∧⇩f χ ⟹⇩f rename_vars Post ψ)"
definition get_disj_invariant :: "('f,'v,'t,'l,'n) art ⇒ 'l ⇒ ('f,'v,'t) exp formula"
where "get_disj_invariant A l ≡ Disjunction (map (node_invariant A) (filter (λa. node_location A a = l ∧ ¬ is_cover_node (edge A a)) (nodes A)))"
record ('h,'l,'n,'tr) hinter =
nodes :: "'n list"
succ_trans_list :: "'l ⇒ 'tr list"
cover_hints :: "'n ⇒ 'h"
transition_hints :: "'n ⇒ 'h list option"
hide_const (open) nodes
locale pre_art_checker =
pre_lts_checker
where type_fixer = type_fixer
and logic_checker = tc
and showsl_atom = sa
and negate_atom = ne +
tc2: pre_logic_checker
where type_fixer = "TYPE('f × 'v trans_var × 't × 'd × 'h)"
and logic_checker = tc2
and showsl_atom = sa2
and negate_atom = ne2
for type_fixer :: "('f::showl × 'v::showl × 't::showl × 'd × 'h::{default,showl}) itself"
and tc tc2 sa sa2 ne ne2
begin
definition "art A ≡ ∀a ∈ set (nodes A). formula (node_invariant A a)"
lemma artD[dest]: "art A ⟹ a ∈ set (nodes A) ⟹ formula (node_invariant A a)" by (auto simp:art_def)
lemma artE[elim]:
assumes "art A" "(⋀a. a ∈ set (nodes A) ⟹ formula (node_invariant A a)) ⟹ thesis" shows thesis
using assms by (auto simp: art_def)
definition "check_art A ≡ check (art A) (showsl_lit (STR ''ill-formed invariant''))"
lemma check_art[intro]: "isOK (check_art A) ⟹ art A" unfolding check_art_def by auto
definition "initial_cond A ≡
set (initial_nodes A) ⊆ set (nodes A) ∧
(∀ a ∈ set (initial_nodes A). node_invariant A a = form_True)"
definition "simulation_cond A P ≡
lts.initial P ⊆ node_location A ` set (initial_nodes A) ∧
(∀ a children τ.
a ∈ set (nodes A)
⟶ edge A a = Children children
⟶ satisfiable (node_invariant A a)
⟶ τ ∈ transition_rules P
⟶ source τ = node_location A a
⟶ (∃ b ∈ set (nodes A). (τ, b) ∈ set children ∧ node_location A b = target τ))"
definition "cover_edges_cond A ≡ ∀ a b.
a ∈ set (nodes A)
⟶ edge A a = Cover b
⟶ b ∈ set (nodes A) ∧
node_location A a = node_location A b ∧
¬ is_cover_node (edge A b) ∧
node_invariant A a ⟹⇩f node_invariant A b"
definition "children_edges_cond A P ≡ ∀ a children τ b.
a ∈ set (nodes A)
⟶ edge A a = Children children
⟶ τ ∈ transition_rules P
⟶ b ∈ set (nodes A)
⟶ (τ,b) ∈ set children
⟶ transition_entailment (assertion P) (node_invariant A a) τ (node_invariant A b)"
definition "well_formed A P ≡
children_edges_cond A P ∧ cover_edges_cond A ∧ initial_cond A ∧ simulation_cond A P ∧ art A"
fun corresponds_to where
"corresponds_to A (State α l) a = (node_location A a = l ∧ (α ⊨ node_invariant A a))"
lemma formula_node_invariant [intro]: "well_formed A P ⟹ a ∈ set (nodes A) ⟹ formula (node_invariant A a)"
unfolding well_formed_def art_def by auto
lemma well_formed_imp_disj_invariant:
assumes "well_formed A P"
and lts: "lts P"
shows "invariant P l (get_disj_invariant A l)" (is "invariant _ _ ?φ")
proof (intro invariantI)
note [intro] = formula_node_invariant[OF assms(1)]
show "formula ?φ" unfolding formula_ex get_disj_invariant_def by auto
fix α
assume reach: "State α l ∈ reachable_states P"
from reachable_state[OF reach] have state: "state_lts P (State α l)" .
then have α: "assignment α" by auto
from reach obtain init
where init: "init ∈ initial_states P"
and steps: "(init, State α l) ∈ (transition P)^*" by auto
from assms[unfolded well_formed_def]
have ic: "initial_cond A"
and sc: "simulation_cond A P" and cec: "children_edges_cond A P"
and cc: "cover_edges_cond A" and art: "art A" by auto
obtain l0 α0 where *: "init = State α0 l0" by (cases init, auto)
with init[unfolded initial_states_def]
have **: "l0 ∈ lts.initial P" "state_lts P init" by auto
from this(1) sc[unfolded simulation_cond_def] obtain n0 where "n0 ∈ set (initial_nodes A)"
"l0 = node_location A n0" by auto
with ic **(2) * have ic: "n0 ∈ set (nodes A)" "corresponds_to A init n0"
by (auto simp: initial_cond_def)
{
fix s1 s2 a1
assume s1t1: "(s1,s2) ∈ transition P" and s1a1: "corresponds_to A s1 a1" and a1: "a1 ∈ set (nodes A)"
from s1t1 have "∃ a2 ∈ set (nodes A). corresponds_to A s2 a2"
proof(elim mem_transitionE, goal_cases)
case (1 φ γ)
from 1(1,4) lts have φ: "formula φ" unfolding lts_def by auto
let ?α = "(pre_post_inter (valuation s1) (valuation s2) γ)"
from 1 have ass: "assignment ?α"
and lc: "valuation s1 ⊨ assertion P (location s1)" "valuation s2 ⊨ assertion P (location s2)" by auto
have "∃ a1 tas. corresponds_to A s1 a1 ∧ edge A a1 = Children tas ∧ a1 ∈ set (nodes A)"
proof (cases "edge A a1")
case (Children tas)
with s1a1 a1 show ?thesis by blast
next
case (Cover b)
from cc[unfolded cover_edges_cond_def, rule_format, OF a1 Cover] obtain tas where
b: "b ∈ set (nodes A)" and loc: "node_location A a1 = node_location A b"
and edge: "edge A b = Children tas"
and impl: "node_invariant A a1 ⟹⇩f node_invariant A b" by (cases "edge A b", auto)
show ?thesis
proof (rule exI[of _ b], rule exI[of _ tas], intro conjI)
from s1a1 loc
have "node_location A b = location s1" and "valuation s1 ⊨ node_invariant A a1" by (induct s1, auto)
with impl 1 show "corresponds_to A s1 b" by (cases s1, auto simp: satisfies_Language)
qed (insert b edge, auto)
qed
then obtain a1 tas where s1a1: "corresponds_to A s1 a1"
and edge: "edge A a1 = Children tas"
and a1: "a1 ∈ set (nodes A)" by blast
from s1a1 have l1: "location s1 = node_location A a1"
and α1: "valuation s1 ⊨ node_invariant A a1" by (induct s1, auto)
let ?τ = "Transition (location s1) (location s2) φ"
have "assignment (valuation s1)" using 1(2) state_def by blast
with α1 have "satisfiable (node_invariant A a1)" unfolding satisfiable_def by auto
from sc[unfolded simulation_cond_def, THEN conjunct2, rule_format, OF a1 edge this 1(1)] trans l1 1
obtain b where b: "b ∈ set (nodes A)" and mem: "(?τ, b) ∈ set tas" and l2: "node_location A b = location s2" by auto
have "valuation s2 ⊨ node_invariant A b"
proof(subst satisfies_rename_vars[symmetric])
from cec[unfolded children_edges_cond_def, rule_format, OF a1 edge 1(1) b mem]
have "transition_entailment (assertion P) (node_invariant A a1) ?τ (node_invariant A b)".
from this 1
have *: "rename_vars Pre (assertion P (location s1))
∧⇩f rename_vars Post (assertion P (location s2))
∧⇩f rename_vars Pre (node_invariant A a1) ∧⇩f φ ⟹⇩f
rename_vars Post (node_invariant A b)"
by auto
from α1 1 φ lc show "?α ⊨ ..." by (intro impliesD[OF * ass], auto)
qed auto
with l2 have "corresponds_to A s2 b" by (cases s2, simp)
with b show ?thesis by blast
qed
} note one_step_simulation = this
{
fix s1 s2 a1
assume t: "(s1,s2) ∈ (transition P)^*" and mem: "a1 ∈ set (nodes A)" and s1a1: "corresponds_to A s1 a1"
from t have "∃ a2 ∈ set (nodes A). corresponds_to A s2 a2"
proof (induct rule: rtrancl_induct)
case (step s2 s3)
from step(3) obtain a2 where a2: "a2 ∈ set (nodes A)" and s2a2: "corresponds_to A s2 a2" by blast
from one_step_simulation[OF step(2) s2a2 a2] show ?case .
qed (insert s1a1 mem, auto)
}
from this[OF steps ic]
obtain a where a: "a ∈ set (nodes A)" "corresponds_to A (State α l) a" by blast
then have "∃ a. a ∈ set (nodes A) ∧ corresponds_to A (State α l) a ∧ ¬ is_cover_node (edge A a)"
proof (cases "edge A a")
case (Children cs)
with a show ?thesis by auto
next
case (Cover b)
from cc[unfolded cover_edges_cond_def, rule_format, OF a(1) Cover] have
b: "b ∈ set (nodes A)" and loc: "node_location A a = node_location A b"
and nc: "¬ is_cover_node (edge A b)"
and impl: "node_invariant A a ⟹⇩f node_invariant A b" by (cases "edge A b", auto)
from a(2) impl loc α have "corresponds_to A (State α l) b" by (auto simp: satisfies_Language)
with b nc show ?thesis by auto
qed
then show "α ⊨ ?φ" by (auto simp: get_disj_invariant_def)
qed
sublocale showsl_transition sa sa2 .
definition check_simulation_cond where
"check_simulation_cond A P H ≡ do {
check (lts.initial P ⊆ set (map (node_location A) (initial_nodes A)))
(showsl_lit (STR ''not all initial nodes of LTS are represented by initial nodes in ART''));
check_allm (λ a.
case edge A a
of Cover _ ⇒ succeed
| Children children ⇒
let l = node_location A a in
try (check_allm
(λ τ.
check (∃ (τ',b) ∈ set children. τ' = τ ∧ node_location A b = target τ ∧ b ∈ set (art.nodes A))
(showsl_lit (STR ''could not find matching transition in ART for node '') ∘
showsl a ∘ showsl_lit (STR '' and transition '') ∘ showsl (source τ) ∘ showsl_lit (STR '' --> '') ∘ showsl (target τ)))
(succ_trans_list H l))
catch (λ e1.
check_valid_formula (¬⇩f (node_invariant A a))
<+? (λ e2. e1 o showsl_lit (STR ''⏎and could not prove unsatisfiability of the node invariant'')))
) (hinter.nodes H)
} <+? (λ s. showsl_lit (STR ''could not ensure simulation condition of ART⏎'') o s)"
definition check_cover_edges_cond where
"check_cover_edges_cond A P H ≡ let lc = assertion P in do {
check_allm (λ a.
case edge A a of Children _ ⇒ succeed
| Cover b ⇒ do {
check (b ∈ set (art.nodes A)) (showsl_lit (STR ''target node is not listed as art-node''));
check (node_location A a = node_location A b) (showsl_lit (STR ''node-locations differ''));
check (¬ is_cover_node (edge A b)) (showsl_lit (STR ''target node must not have cover edge''));
check_formula (cover_hints H a) (Disjunction [
― ‹ position 0 › node_invariant A b,
― ‹ position 1 › ¬⇩f node_invariant A a
])
} <+? (λ s. showsl_lit (STR ''problem in checking cover edge of node '') o showsl a o showsl_nl o s)
) (hinter.nodes H)
} <+? (λ s. showsl_lit (STR ''could not ensure cover edge condition of ART⏎'') o s)"
definition check_initial_cond where
"check_initial_cond A ≡
check_allm (λ init.
do { check (init ∈ set (art.nodes A))
(showsl_lit (STR ''initial node of A ('') o showsl init o showsl_lit (STR '') is not mentioned as node of ART'')
);
check (node_invariant A init = True⇩f)
(showsl_lit (STR ''the node invariant for the initial ART node ('') o showsl init o
showsl_lit (STR '') must be TRUE, but it is '') o showsl_formula (node_invariant A init))})
(initial_nodes A)
"
definition check_children_edges_cond where
"check_children_edges_cond A P H ≡ let lc = assertion P in do {
check_allm (λ a.
case edge A a of Cover _ ⇒ succeed
| Children children ⇒ (
case transition_hints H a of None ⇒
error (showsl_lit (STR ''not yet''))
| Some hints ⇒ do {
check (length hints = length children)
(showsl_lit (STR ''the number of hints differs from the number of children''));
check_allm (λ ((τ,b),h).
case τ of Transition l r φ ⇒
tc2.check_formula h (Disjunction [
― ‹ position 0 › rename_vars Post (node_invariant A b),
― ‹ position 1 › ¬⇩f rename_vars Pre (node_invariant A a),
― ‹ position 2 › ¬⇩f rename_vars Pre (lc l),
― ‹ position 3 › ¬⇩f φ
― ‹ position 4, deactivated ¬ rename_vars Post (lc r) ›
])
<+? (λ s. showsl_lit (STR ''problem in checking edge '') o showsl a o showsl_lit (STR '' --> '') o showsl b o
showsl_lit (STR '' for transition⏎'') o
showsl_transition τ o showsl_nl o s)
) (zip children hints)
} <+? (λ s. showsl_lit (STR ''problem in checking transitions of node '') o showsl a o showsl_nl o s)
)
) (hinter.nodes H)
} <+? (λ s. showsl_lit (STR ''could not ensure transition edge condition of ART⏎'') o s)"
definition check_art_invariants where
"check_art_invariants A P H≡ do {
check_art A;
check_initial_cond A;
check_simulation_cond A P H;
check_cover_edges_cond A P H;
check_children_edges_cond A P H
} <+? (λ s. showsl_lit (STR ''could not ensure validity of art-graph:⏎'') o s)"
end
locale art_checker =
pre_art_checker where type_fixer = type_fixer +
lts_checker
where type_fixer = type_fixer
and logic_checker = tc
and showsl_atom = sa
and negate_atom = ne +
tc2: logic_checker
where type_fixer = "TYPE('f×'v trans_var×'t×'d×'h)"
and logic_checker = tc2
and showsl_atom = sa2
and negate_atom = ne2
for type_fixer :: "('f::showl × 'v::showl × 't::showl × 'd × 'h::{default,showl}) itself"
locale art_checker_body =
art_checker where type_fixer = "TYPE('f×'v×'t×'d×'h)"
for type_fixer :: "('f::showl × 'v::showl × 't::showl × 'd × 'l::showl × 'n::showl × 'h::{default,showl}) itself"
and A :: "('f,'v,'t,'l,'n) art"
and P :: "('f,'v,'t,'l) lts"
and H :: "('h hint,'l,'n,_) hinter" +
assumes ans: "set (hinter.nodes H) = set (art.nodes A)"
and P: "lts P"
and succ_trans_list: "⋀ l. set (succ_trans_list H l) = { τ ∈ transition_rules P. source τ = l }"
begin
lemma check_initial_cond[iff]: "isOK(check_initial_cond A) = initial_cond A"
unfolding initial_cond_def check_initial_cond_def by auto
lemma check_cover_edges_cond[dest]:
assumes ok: "isOK(check_cover_edges_cond A P H)" and A: "art A"
shows "cover_edges_cond A"
unfolding cover_edges_cond_def
proof (intro allI impI conjI)
note * = ok[unfolded check_cover_edges_cond_def,simplified, unfolded ans]
note [split] = art_edge.splits option.splits
fix a b assume a: "a ∈ set (nodes A)" and ab: "edge A a = Cover b"
from * a ab
show "node_location A a = node_location A b"
and b: "b ∈ set (nodes A)"
and "¬ is_cover_node (edge A b)" by auto
from *[rule_format,OF a, unfolded ab,simplified]
obtain hints where "isOK (check_formula hints (Disjunction [node_invariant A b, ¬⇩f node_invariant A a ]))" by auto
from check_formula[OF this] artD[OF A] a b
show "node_invariant A a ⟹⇩f node_invariant A b" by (auto simp: valid_Language)
qed
lemma check_simulation_cond[dest]: assumes "isOK(check_simulation_cond A P H)" and A: "art A"
shows "simulation_cond A P"
proof -
note ok = assms(1)[unfolded check_simulation_cond_def, simplified, unfolded Let_def ans]
show ?thesis
unfolding simulation_cond_def
proof (intro conjI allI impI)
fix a tas τ
assume a: "a ∈ set (art.nodes A)"
assume *: "edge A a = Children tas" "τ ∈ transition_rules P" "source τ = node_location A a" "satisfiable (node_invariant A a)"
note [simp] = is_ok_try_catch
{
from *(4) obtain α where sat: "assignment α" "α ⊨ node_invariant A a" unfolding satisfiable_def by auto
from A[unfolded art_def] a have form: "formula (¬⇩f node_invariant A a)" by auto
assume "isOK (check_valid_formula (¬⇩f node_invariant A a))"
from check_valid_formula[OF this form] sat(1) sat(2) Language_not[of "node_invariant A a"]
have False unfolding Language_def by auto
}
with conjunct2[OF ok, rule_format, OF a, unfolded *(1), simplified] *
show "(∃b ∈ set (art.nodes A). (τ, b) ∈ set tas ∧ node_location A b = target τ)" by (auto simp: succ_trans_list)
qed (insert ok, auto)
qed
lemma check_children_edges_cond[dest]:
assumes ok: "isOK(check_children_edges_cond A P H)" and A: "art A"
shows "children_edges_cond A P"
unfolding children_edges_cond_def
proof (intro allI impI)
fix a children τ b
assume a: "a ∈ set (art.nodes A)"
and edge: "edge A a = Children children"
and τ: "τ ∈ transition_rules P"
and b: "b ∈ set (art.nodes A)"
and mem: "(τ, b) ∈ set children"
note ok = ok[unfolded check_children_edges_cond_def, simplified, unfolded ans, rule_format, OF a,
unfolded edge, simplified]
from ok obtain hints where tr: "transition_hints H a = Some hints" and len: "length hints = length children"
by (auto split: option.splits)
from mem len obtain h where mem: "((τ,b),h) ∈ set (zip children hints)" unfolding set_zip
by (auto simp: set_conv_nth)
note ok = ok[unfolded tr, simplified, THEN conjunct2, rule_format, OF mem]
show "transition_entailment (assertion P) (node_invariant A a) τ (node_invariant A b)"
proof(cases τ)
case *: (Transition l r φ)
with A a b P τ have "formula (node_invariant A b) ∧
formula (node_invariant A a) ∧ formula (assertion P l) ∧ formula φ" by auto
from tc2.check_formula[OF ok[unfolded *, simplified],simplified, OF this]
show ?thesis
by (auto simp: * valid_Language)
qed
qed
lemma check_art_invariants[dest]:
assumes ok: "isOK(check_art_invariants A P H)" shows "well_formed A P"
proof-
from ok have A: "art A" by (auto simp: check_art_invariants_def)
with ok show ?thesis by (auto simp: well_formed_def check_art_invariants_def)
qed
end
datatype ('n,'tr,'h) art_edge_impl =
Cover_Edge 'n 'h
| Children_Edge "('tr × 'n × 'h) list"
datatype ('f,'v,'t,'l,'n,'tr,'h) art_node_impl = Art_Node
(name: 'n) (invariant: "('f,'v,'t) exp formula") (location: 'l) (edge: "('n,'tr,'h) art_edge_impl")
fun is_cover_node :: "('f,'v,'t,'l,'n,'tr,'h) art_node_impl ⇒ bool" where
"is_cover_node (Art_Node _ _ _ (Cover_Edge _ _)) = True"
| "is_cover_node (Art_Node _ _ _ (Children_Edge _)) = False"
record ('f,'v,'t,'l,'n,'tr,'h) art_impl =
initial_nodes :: "'n list"
nodes :: "('f,'v,'t,'l,'n,'tr,'h) art_node_impl list"
fun showsl_art_node :: "('f,'v,'t,'l :: showl,'n :: showl,'tr :: showl,'h) art_node_impl ⇒ showsl" where
"showsl_art_node (Art_Node n _ l (Cover_Edge m _)) = showsl n o showsl_lit (STR ''(@ '') o showsl l o showsl_lit (STR ''): covered by '') o showsl m"
| "showsl_art_node (Art_Node n _ l (Children_Edge ls)) = showsl n o showsl_lit (STR ''(@ '') o showsl l o showsl_lit (STR ''): goes to '')
o default_showsl_list (λ (tr,n,_). showsl_lit (STR ''-'') o showsl tr o showsl_lit (STR ''->'') o showsl n) ls"
definition showsl_art :: "('f,'v,'t,'l :: showl,'n :: showl,'tr :: showl,'h) art_impl ⇒ showsl" where
"showsl_art A = showsl_lit (STR ''ART:⏎Initial node: '') o showsl_list (initial_nodes A) o showsl_lit (STR ''⏎Arcs⏎'')
o showsl_sep showsl_art_node showsl_nl (nodes A) o showsl_nl"
hide_const (open) nodes
definition art_nodes :: "('f,'v,'t,'l,'n,'tr,'h) art_impl ⇒ 'n list" where
"art_nodes Ai = map name (art_impl.nodes Ai)"
context
fixes Pi :: "('f,'v,'t,'l,'tr) lts_impl"
begin
fun art_edge_of :: "('n,'tr,'h) art_edge_impl ⇒ ('f,'v,'t,'l,'n) art_edge" where
"art_edge_of (Cover_Edge an _) = Cover an"
| "art_edge_of (Children_Edge ans) = Children (map (λ (t,a,h). (transition_of Pi t, a)) ans)"
definition art_of :: "('f,'v,'t,'l,'n,'tr,'h) art_impl ⇒ ('f,'v,'t,'l,'n) art" where
"art_of Ai ≡
let ans = art_impl.nodes Ai in ⦇
art.initial_nodes = art_impl.initial_nodes Ai,
art.nodes = art_nodes Ai,
art.edge = (the o map_of (map (λ a. (name a, art_edge_of (edge a))) ans)),
node_location = (the o map_of (map (λ a. (name a, location a)) ans)),
node_invariant = (the o map_of (map (λ a. (name a, invariant a)) ans))
⦈"
lemma art_of_code[code]: "art_of Ai = (
let ans = art_impl.nodes Ai in ⦇
art.initial_nodes = art_impl.initial_nodes Ai,
art.nodes = art_nodes Ai,
art.edge = (map_of_total (λ a. showsl_lit (STR ''error in looking up art edge '') o showsl a) (map (λ a. (name a, art_edge_of (edge a))) ans)),
node_location = (map_of_total (λ a. showsl_lit (STR ''error in looking up node location '') o showsl a) (map (λ a. (name a, location a)) ans)),
node_invariant = (map_of_total (λ a. showsl_lit (STR ''error in looking up node invariant '') o showsl a) (map (λ a. (name a, invariant a)) ans))
⦈)"
unfolding art_of_def Let_def by simp
lemma node_invariant_art_of[simp] :
"node_invariant (art_of Ai) = the o map_of (map (λ a. (art_node_impl.name a, art_node_impl.invariant a)) (art_impl.nodes Ai))"
by (simp add: art_of_def Let_def)
lemma nodes_art_of[simp]: "art.nodes (art_of Ai) = art_nodes Ai" by (simp add: art_of_def Let_def)
lemma node_location_art_of[simp]:
"node_location (art_of Ai) = the o map_of (map (λ a. (name a, location a)) (art_impl.nodes Ai))"
by (simp add: art_of_def Let_def)
definition cover_hints :: "('f,'v,'t,'l,'n,'tr,'h::default) art_impl ⇒ 'n ⇒ 'h" where
"cover_hints Ai =
map_of_default default (map (λ a. (name a, case edge a of Cover_Edge _ h ⇒ h))
(filter is_cover_node (art_impl.nodes Ai)))"
definition transition_hints :: "('f,'v,'t,'l,'n,'tr,'h) art_impl ⇒ 'n ⇒ 'h list option" where
"transition_hints Ai =
map_of (map (λ a. (name a, case edge a of Children_Edge cs ⇒ map (λ (_,_,h). h) cs))
(filter (λ a. ¬ is_cover_node a) (art_impl.nodes Ai)))"
end
context pre_art_checker begin
definition "make_hinter Pi Ai ≡ ⦇
hinter.nodes = art_nodes Ai,
succ_trans_list = succ_transitions Pi,
cover_hints = cover_hints Ai,
transition_hints = transition_hints Ai
⦈"
definition check_art_invariants_impl where
"check_art_invariants_impl Ai Pi ≡ check_art_invariants (art_of Pi Ai) (lts_of Pi) (make_hinter Pi Ai)"
definition unique_names where
"unique_names Ai ≡ distinct (map name (art_impl.nodes Ai))"
definition check_unique_names where
"check_unique_names Ai ≡
check (distinct (map name (art_impl.nodes Ai)))
(showsl_lit (STR ''Nodes in art graph must have unique names''))"
lemma check_unique_names[simp]: "isOK(check_unique_names Ai) = unique_names Ai"
unfolding check_unique_names_def unique_names_def by auto
abbreviation post :: "('f,'v,'t) exp formula ⇒ ('f,'v trans_var,'t) exp formula" where
"post f ≡ rename_vars Post f"
fun translate_f
where
"translate_f is_cover f 0 = f 0" |
"translate_f is_cover f (Suc n)
= (if is_cover (f 1) then translate_f is_cover (shift f 2) n else translate_f is_cover (shift f 1) n)"
lemma translate_f_skips:
assumes "⋀ n. is_cover (f n) ⟹ ¬ is_cover (f (Suc n))"
and "¬ is_cover (f 0)"
shows "¬ is_cover (translate_f is_cover f n)"
using assms by (induct n arbitrary: f;cases "is_cover (f 1)";auto)
definition get_node where
"get_node Ai = the o map_of (map (λ a. (name a, a)) (art_impl.nodes Ai))"
abbreviation node_exists where
"node_exists Ai x ≡ x ∈ art_node_impl.name ` set (art_impl.nodes Ai)"
definition is_cover_state where
"is_cover_state Ai = is_cover_node ∘ get_node Ai o state.location"
lemma unique_names_eq:
assumes "unique_names Ai"
"name node = name a"
"node ∈ set (art_impl.nodes Ai)"
"a ∈ set (art_impl.nodes Ai)"
shows "node = a"
using distinct_map_eq[OF assms(1)[unfolded unique_names_def] assms(2-4)].
abbreviation satisfies_invariant where
"satisfies_invariant Ai s ≡
assignment (state.valuation s) ∧
node_exists Ai (state.location s) ∧
state.valuation s ⊨ art_node_impl.invariant (get_node Ai (state.location s))"
lemma map_of_helper:
assumes "map_of (map (λa. (f1 a, a)) lst) l = Some v"
shows "map_of (map (λa. (f1 a, f a)) lst) l = Some (f v)"
using assms by(induct lst;auto)
lemma get_node :
assumes "node_exists Ai l"
shows "get_node Ai l ∈ set (art_impl.nodes Ai)" (is ?t1)
"name (get_node Ai l) = l" (is ?t2)
"map_of (map (λa. (name a, a)) (art_impl.nodes Ai)) l = Some (get_node Ai l)" (is ?t3)
proof -
from assms weak_map_of_SomeI obtain a where a:"name a = l" "a ∈ set (art_impl.nodes Ai)" by auto
then have ins:"(name a,a) ∈ set (map (λ a. (name a, a)) (art_impl.nodes Ai))" by auto
obtain x where x:"map_of (map (λa. (name a, a)) (art_impl.nodes Ai)) (name a) = Some x"
using weak_map_of_SomeI[OF ins] by auto
then have x_is:"x = get_node Ai l" unfolding get_node_def o_def a by simp
from map_of_SomeD[OF x,unfolded a x_is] show ?t1 ?t2 by auto
from x[unfolded x_is a] show ?t3 by auto
qed
lemma unique_get_node:
assumes "unique_names Ai" "a ∈ set (art_impl.nodes Ai)"
shows "get_node Ai (name a) = a"
using assms(2) unique_names_eq[OF assms(1) get_node(2,1)[of "name a"] assms(2)] by blast
lemma is_cover_state:
assumes "node_exists Ai (state.location x)" "is_cover_state Ai x"
shows "∃v. map_of (map (λa. (name a, art_edge_of Pi (art_node_impl.edge a)))
(art_impl.nodes Ai)) (state.location x) = Some (Cover v)
∧ (∃ h. art_node_impl.edge (get_node Ai (state.location x)) = Cover_Edge v h)
"
proof -
let ?gn = "get_node Ai (state.location x)"
note x[simp]= get_node(3)[OF assms(1)]
from assms(2)[unfolded is_cover_state_def,simplified] show ?thesis
by (cases ?gn;cases "edge ?gn";auto simp:map_of_helper)
qed
lemma no_cover_state:
assumes "node_exists Ai (state.location x)" "¬ is_cover_state Ai x"
shows "∃v. map_of (map (λa. (name a, art_edge_of Pi (art_node_impl.edge a)))
(art_impl.nodes Ai)) (state.location x) = Some (Children v)"
proof -
have [simp]:"map_of (map (λa. (name a, a)) (art_impl.nodes Ai)) (state.location x) =
Some (get_node Ai (state.location x))"
using get_node(3)[OF assms(1)].
from assms(2)[unfolded is_cover_state_def,simplified] show ?thesis
by (cases "(get_node Ai (state.location x))";cases "edge (get_node Ai (state.location x))"
;auto simp:map_of_helper)
qed
definition lts_transitions_of_art
:: "('f, 'v, 't, 'l, 'tr) lts_impl ⇒ ('f, 'v, 't, 'l, 'n, 'tr, 'hintList) art_node_impl ⇒ ('f,'v,'t,'n,'tr option) transitions_impl"
where
"lts_transitions_of_art Pi a = (case edge a of
(Cover_Edge v _) ⇒ [(None, Transition (name a) v True⇩f)] | ― ‹ TODO: the formula True should be a skip ›
(Children_Edge cs) ⇒ map (λ (nm,an,_). case transition_of Pi nm of
Transition _ _ _ ⇒ (Some nm,Transition (name a) an (transition_formula (transition_of Pi nm)))) cs)"
fun renumber_rename :: "int ⇒ ('b option × 'c) list ⇒ (('b + int) × 'c) list"
where
"renumber_rename i (Cons (a,v) rs)
= Cons (case a of None ⇒ Inr i | Some l ⇒ Inl l,v) (renumber_rename (i+1) rs)" |
"renumber_rename i Nil = Nil"
lemma snd_rename [simp]:
shows "map snd (renumber_rename n xs) = map snd xs"
by(induct xs arbitrary:n,auto)
lemma snd_set_rename [simp]:
shows "snd ` set (renumber_rename n xs) = snd ` set xs"
using set_map[of snd xs, folded snd_rename[of n], unfolded set_map].
fun relabel_transition where
"relabel_transition f (Transition l r φ) = Transition (f l) (f r) φ"
end
context art_checker begin
lemma check_art_invariants_impl:
assumes impl: "lts_impl Pi"
and ok: "isOK (check_art_invariants_impl Ai Pi)"
shows "invariant (lts_of Pi) l (get_disj_invariant (art_of Pi Ai) l)"
proof-
note impl = lts_impl[OF impl]
interpret body: art_checker_body
where type_fixer = "TYPE(_)"
and P = "lts_of Pi"
and A = "art_of Pi Ai"
and H = "make_hinter Pi Ai"
using impl by (unfold_locales, auto simp: make_hinter_def)
from ok
have wf: "well_formed (art_of Pi Ai) (lts_of Pi)" by (intro body.check_art_invariants, unfold check_art_invariants_impl_def)
from well_formed_imp_disj_invariant[OF this impl]
show ?thesis.
qed
end
lemmas [code] =
pre_art_checker.check_art_invariants_impl_def
pre_art_checker.check_art_invariants_def
pre_art_checker.check_children_edges_cond_def
pre_art_checker.check_cover_edges_cond_def
pre_art_checker.check_simulation_cond_def
pre_art_checker.check_initial_cond_def
pre_art_checker.make_hinter_def
pre_art_checker.check_art_def
pre_art_checker.art_def
pre_art_checker.check_unique_names_def
end