theory Closed_Checker_Proofs
imports Closed_Checker
begin
unbundle IA_formula_notation
lemma Mapping_values: "(x ∈ Mapping_values m) ⟷ (∃n. Mapping.lookup m n = Some x)"
proof -
have "∃n. Mapping.lookup m n = Some x" if a: "x ∈ Mapping_values m"
proof -
obtain n where "n ∈ Mapping.keys m" "x = the (Mapping.lookup m n)"
using a unfolding Mapping_values_def by auto
then have "Mapping.lookup m n = Some x"
by (simp add: domIff keys_dom_lookup)
then show ?thesis
by blast
qed
moreover have "x ∈ Mapping_values m" if a: "Mapping.lookup m n = Some x" for n
proof -
have "n ∈ Mapping.keys m"
using a by (simp add: keys_is_none_rep)
then show ?thesis
unfolding Mapping_values_def using a by (force simp add: image_def)
qed
ultimately show ?thesis
by blast
qed
lemma Mapping_values_ran: "Mapping_values m = ran (Mapping.lookup m)"
using Mapping_values by (fastforce simp add: ran_def)
context formula
begin
lemma form_imp_implies: "valid (φ ⟶⇩f ρ) ⟷ implies φ ρ"
using satisfies_Language valid_def by (auto)
end
lemma lookup_None_keys': "x ∉ Mapping.keys m ⟷ Mapping.lookup m x = None"
by (simp add: domIff keys_dom_lookup)
lemma update_asFun:
assumes "isOK (update_asFun as⇩1 as⇩2 n v⇩n φ)"
shows "update_as (asm_to_as as⇩1) (asm_to_as as⇩2) n v⇩n φ"
proof -
have "IA.implies (Formula.form_and (kb as⇩1) φ) (kb as⇩2)"
apply(subst IA.form_imp_implies[symmetric])
using assms by (auto intro!: IA.check_valid_formula)
moreover have "Mapping.lookup (abstract_state_mapping.stack as⇩2) x =
(Mapping.lookup (abstract_state_mapping.stack as⇩1)(n ↦ v⇩n)) x" for x
apply(cases "x ∈ Mapping.keys (abstract_state_mapping.stack as⇩1)")
using assms by (auto simp add: asm_to_as_simps simp add: lookup_None_keys')
ultimately show ?thesis
using assms Mapping_values
by (fastforce intro!: update_as.intros)
qed
lemma checkFormula:
assumes "isOK (checkFormula (φ ⟶⇩f ρ))"
shows "φ ⟹⇩I⇩A ρ"
using assms
unfolding checkFormula_def IA.form_imp_implies[symmetric]
using IA.check_valid_formula by (force)
lemma checkFormula_formula:
assumes "isOK (checkFormula (φ ⟶⇩f ρ))"
shows "IA.formula (φ ⟶⇩f ρ)"
using assms
unfolding checkFormula_def by (force)
context graph_exec
begin
lemma evalFun_evalInf:
assumes "isOK (evalFun n⇩1 n⇩2 v⇩n)"
shows "evalInf n⇩1 n⇩2"
proof -
obtain n binop o⇩1 o⇩2 where
"find_statement prog (abstract_state_mapping.pos (as_map_of_node n⇩1)) =
Inr (Instruction (Named n (Binop binop o⇩1 o⇩2)))"
using assms by (auto simp add: evalFun_def split: stuck.splits sum.splits option.splits action.splits named.splits instruction.splits)
then show ?thesis
using assms
apply(auto simp add: evalFun_def isOK_def check_def
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits
elim!: option_to_sum.elims)
apply(intro evalInf.intros[of "asm_to_as (as_map_of_node n⇩1)" "asm_to_as (as_map_of_node n⇩2)" n⇩1 n⇩2])
by (auto simp add: renaming_of_edge'_def intro!: update_asFun evalAsInf.intros)
qed
lemma evalExternalFun_evalExternalInf:
assumes "isOK (evalExternalFun n⇩1 n⇩2 v⇩n)"
shows "evalExternalInf n⇩1 n⇩2"
proof -
obtain n t fn as where
"find_statement prog (abstract_state_mapping.pos (as_map_of_node n⇩1)) =
Inr (Instruction (Named n (Call t fn as)))"
using assms by (auto simp add: evalExternalFun_def split: stuck.splits sum.splits option.splits action.splits named.splits instruction.splits)
then show ?thesis
using assms
apply(auto simp add: evalExternalFun_def isOK_def check_def
split: sum.splits option.splits action.splits named.splits instruction.splits sum_bind_splits if_splits
llvm_fun.splits
elim!: option_to_sum.elims)
apply(intro evalExternalInf.intros[of n⇩1 n⇩2])
by (auto simp add: renaming_of_edge'_def intro!: update_asFun evalExternalAsInf.intros)
qed
lemma genFun_genInf:
assumes "isOK (genFun n⇩1 n⇩2)"
shows "genInf n⇩1 n⇩2"
proof -
have 1: "IA.implies φ ρ" if "IA.check_valid_formula (φ ⟶⇩f ρ) = Inr ()"
"IA.formula (φ ⟶⇩f ρ)"
for φ ρ :: "'lv IA.formula"
apply(subst IA.form_imp_implies[symmetric])
using that IA.check_valid_formula by blast
have "genAsInf (asm_to_as (as_map_of_node n⇩1)) (asm_to_as (as_map_of_node n⇩2)) (renaming_of_edge' (n⇩1, n⇩2))"
using assms
apply(auto simp add: isOK_def check_def genFun_def renaming_of_edge'_def
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits option.splits
elim!: option_to_sum.elims)
apply(rule genAsInf.intros)
prefer 3
apply(rule 1)
apply (auto intro!: 1 simp add: lookup_None_keys intro!: update_asFun)
by (metis domD domI keys_dom_lookup)
then show ?thesis
using assms
apply(auto simp add: isOK_def check_def genFun_def
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits option.splits
elim!: option_to_sum.elims)
using genInf.intros[of "asm_to_as (as_map_of_node n⇩1)" "asm_to_as (as_map_of_node n⇩2)"]
by (auto intro!: 1 simp add: lookup_None_keys intro!: update_asFun)
qed
lemma refineFun_refineInf:
assumes "isOK (refineFun n n⇩t n⇩f φ )"
shows "refineInf n n⇩t n⇩f"
proof -
have 1: "φ ⟹⇩I⇩A ρ" if "IA.check_valid_formula (φ ⟶⇩f ρ) = Inr ()" "IA.formula (φ ⟶⇩f ρ)"
for φ ρ :: "'lv IA.formula"
apply(subst IA.form_imp_implies[symmetric])
using that IA.check_valid_formula by blast
have a: "IA.check_valid_formula (abstract_state.kb (asm_to_as (as_map_of_node n)) ∧⇩f φ ⟶⇩f abstract_state.kb (asm_to_as (as_map_of_node n⇩t))) = Inr ()"
"IA.check_valid_formula (abstract_state.kb (asm_to_as (as_map_of_node n)) ∧⇩f ¬⇩f φ ⟶⇩f abstract_state.kb (asm_to_as (as_map_of_node n⇩f))) = Inr ()"
using assms by (auto simp add: isOK_def check_def refineFun_def split: sum_bind_splits)
have b: "IA.formula (abstract_state.kb (asm_to_as (as_map_of_node n)) ∧⇩f ¬⇩f φ ⟶⇩f abstract_state.kb (asm_to_as (as_map_of_node n⇩f)))"
"IA.formula (abstract_state.kb (asm_to_as (as_map_of_node n)) ∧⇩f φ ⟶⇩f abstract_state.kb (asm_to_as (as_map_of_node n⇩t)))"
using assms by (auto simp add: isOK_def check_def refineFun_def split: sum_bind_splits if_splits)
have c: "abstract_state.kb (asm_to_as (as_map_of_node n)) ∧⇩f φ ⟹⇩I⇩A abstract_state.kb (asm_to_as (as_map_of_node n⇩t))"
using a b by (intro 1) auto
have d: "abstract_state.kb (asm_to_as (as_map_of_node n)) ∧⇩f ¬⇩f φ ⟹⇩I⇩A abstract_state.kb (asm_to_as (as_map_of_node n⇩f))"
using a b by (intro 1) auto
have "refineAsInf (asm_to_as (as_map_of_node n)) (asm_to_as (as_map_of_node n⇩t)) (asm_to_as (as_map_of_node n⇩f))"
using assms c d
by (intro refineAsInf.intros[where φ=φ])
(auto intro!: 1 simp add: isOK_def check_def refineFun_def split: if_splits)
then show ?thesis
using assms
by (auto intro: refineInf.intros simp add: renaming_of_edge'_def isOK_def check_def refineFun_def split: sum_bind_splits if_splits)
qed
lemma phi_abstract'Fun_phi_abstract':
assumes "isOK (phi_abstract'Fun as⇩1 as⇩2 x ps v⇩x t⇩x old_b_id)"
shows "phi_abstract' (asm_to_as as⇩1) (asm_to_as as⇩2) x ps v⇩x t⇩x old_b_id"
proof -
have "ran (abstract_state.stack (asm_to_as as⇩1)) =
Mapping_values (stack as⇩1)"
using Mapping_values by (fastforce simp add: ran_def)
then show ?thesis
using assms
by (auto simp add: isOK_def check_def phi_abstract'Fun_def lookup_None_keys vars_formula_list
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits option.splits
elim!: option_to_sum.elims intro!: update_asFun phi_abstract'.intros)
qed
lemma phi_abstractFun_phi_abstract:
assumes "isOK (phi_abstractFun as⇩1 as⇩2 xs ys old_b_id)"
shows "phi_abstract (asm_to_as as⇩1) (asm_to_as as⇩2) xs ys old_b_id"
proof -
have "ran (abstract_state.stack (asm_to_as as⇩1)) =
Mapping_values (stack as⇩1)"
using Mapping_values by (fastforce simp add: ran_def)
then show ?thesis
using assms
apply(induction as⇩1 as⇩2 xs ys old_b_id rule: phi_abstractFun.induct)
apply(auto simp add: isOK_def check_def
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits option.splits
elim!: option_to_sum.elims)
apply(intro phi_abstract.intros)
by (auto simp add: lookup_None_keys intro!: update_asFun phi_abstract.intros phi_abstract'Fun_phi_abstract')
qed
lemma map_sum_is_Inr:
assumes "map_sum f g m = Inr x"
shows "∃y. m = Inr y"
using assms by (cases m) auto
lemma branchFun_branchInf:
assumes "isOK (branchFun n⇩1 n⇩2 φs)"
shows "branchInf n⇩1 n⇩2"
proof -
have [simp]: "foldr union (map (vars_term ∘ snd) φs) {} = ⋃ (vars_term ` snd ` set φs)" for φs
by (induction φs) (auto)
note find_statement.simps[simp del] find_phis.simps[simp del] formula.simps[simp del] IA.implies_Language[simp del]
have 1: "φ ⟹⇩I⇩A ρ" if "IA.check_valid_formula (φ ⟶⇩f ρ) = Inr ()" "IA.formula (φ ⟶⇩f ρ)"
for φ ρ :: "name IA.formula"
apply(subst IA.form_imp_implies[symmetric])
using that IA.check_valid_formula by blast
obtain f_id old_b_id p where f_id: "abstract_state.pos (asm_to_as (as_map_of_node n⇩1)) = (f_id, old_b_id, p)"
using prod.exhaust by metis
have "∃t new_b_id . find_statement prog (pos (as_map_of_node n⇩1)) = Inr (Terminator t) ∧ named_instruction t = LLVM_Syntax.Br new_b_id"
using assms
by (auto simp add: branchFun_def
split: sum.splits stuck.splits action.splits named.splits instruction.splits terminator.splits sum_bind_splits option.splits)
then obtain t new_b_id where t: "find_statement prog (pos (as_map_of_node n⇩1)) = Inr (Terminator t)"
"named_instruction t = LLVM_Syntax.Br new_b_id"
by blast
have "∃phis_stats. find_phis prog f_id new_b_id = Inr phis_stats"
using assms t f_id
by (auto simp add: isOK_def branchFun_def
split: sum.splits action.splits named.splits instruction.splits terminator.splits sum_bind_splits option.splits
elim!: option_to_sum.elims intro!: map_sum_is_Inr)
then obtain phis_stats where phis_stats: "find_phis prog f_id new_b_id = Inr phis_stats"
by metis
have "branchAsInf prog (asm_to_as (as_map_of_node n⇩1)) (asm_to_as (as_map_of_node n⇩2))"
apply(intro branchAsInf.intros[where as⇩1 = "asm_to_as (as_map_of_node n⇩1)"
and as⇩2 = "asm_to_as (as_map_of_node n⇩2)" and φs=φs and t=t and new_b_id=new_b_id
and f_id=f_id and old_b_id=old_b_id and p=p and phis_stats=phis_stats])
subgoal
using t by auto
subgoal
using t by auto
subgoal
using f_id by auto
subgoal
using assms f_id t phis_stats
by (auto simp add: check_def branchFun_def
split: action.splits named.splits instruction.splits sum_bind_splits if_splits)
subgoal
using phis_stats by auto
subgoal
using assms phis_stats f_id t
by (intro phi_abstractFun_phi_abstract) (auto simp add: check_def branchFun_def
split: action.splits named.splits instruction.splits sum_bind_splits if_splits)
subgoal
using assms
by (auto simp add: check_def branchFun_def intro!: checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def branchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def branchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def branchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def branchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def branchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def branchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
done
then show ?thesis
using assms
by(intro branchInf.intros[where as⇩1 = "asm_to_as (as_map_of_node n⇩1)" and as⇩2 = "asm_to_as (as_map_of_node n⇩2)"])
(auto simp add: renaming_of_edge'_def isOK_def check_def branchFun_def split: sum_bind_splits if_splits option.splits prod.splits)
qed
lemma condBranchFun_condBranchInf:
assumes "isOK (condBranchFun n⇩1 n⇩2 φs b)"
shows "condBranchInf n⇩1 n⇩2"
proof -
have [simp]: "foldr union (map (vars_term ∘ snd) φs) {} = ⋃ (vars_term ` snd ` set φs)" for φs
by (induction φs) (auto)
note find_statement.simps[simp del] find_phis.simps[simp del] formula.simps[simp del] IA.implies_Language[simp del]
have 1: "φ ⟹⇩I⇩A ρ" if "IA.check_valid_formula (φ ⟶⇩f ρ) = Inr ()" "IA.formula (φ ⟶⇩f ρ)"
for φ ρ :: "name IA.formula"
apply(subst IA.form_imp_implies[symmetric])
using that IA.check_valid_formula by blast
obtain f_id old_b_id p where f_id: "abstract_state.pos (asm_to_as (as_map_of_node n⇩1)) = (f_id, old_b_id, p)"
using prod.exhaust by metis
have "∃t c b⇩t b⇩f. find_statement prog (pos (as_map_of_node n⇩1)) = Inr (Terminator t) ∧ named_instruction t = LLVM_Syntax.CondBr c b⇩t b⇩f"
using assms
by (auto simp add: condBranchFun_def
split: sum.splits stuck.splits action.splits named.splits instruction.splits terminator.splits sum_bind_splits option.splits)
then obtain t c b⇩t b⇩f where t: "find_statement prog (pos (as_map_of_node n⇩1)) = Inr (Terminator t)"
"named_instruction t = LLVM_Syntax.CondBr c b⇩t b⇩f"
by blast
have "∃phis_stats. find_phis prog f_id (if b then b⇩t else b⇩f) = Inr phis_stats"
using assms t f_id
by (auto simp add: isOK_def condBranchFun_def
split: sum.splits action.splits named.splits instruction.splits terminator.splits sum_bind_splits option.splits
elim!: option_to_sum.elims intro!: map_sum_is_Inr)
then obtain phis_stats where phis_stats: "find_phis prog f_id (if b then b⇩t else b⇩f) = Inr phis_stats"
by metis
have "∃c'. operand_value (asm_to_as (as_map_of_node n⇩1)) c = Some c'"
using assms t f_id
by (auto simp add: isOK_def condBranchFun_def
split: action.splits named.splits instruction.splits terminator.splits sum_bind_splits option.splits
elim!: option_to_sum.elims)
then obtain c' where c': "operand_value (asm_to_as (as_map_of_node n⇩1)) c = Some c'"
by metis
have "condBranchAsInf prog (asm_to_as (as_map_of_node n⇩1)) (asm_to_as (as_map_of_node n⇩2))"
apply(intro condBranchAsInf.intros[where as⇩1 = "asm_to_as (as_map_of_node n⇩1)"
and as⇩2 = "asm_to_as (as_map_of_node n⇩2)" and φs=φs and t=t and new_b_id="if b then b⇩t else b⇩f"
and b_id_true=b⇩t and b_id_false=b⇩f and c=c and c'=c' and b=b
and f_id=f_id and old_b_id=old_b_id and p=p and phis_stats=phis_stats])
subgoal
using t by auto
subgoal
using t by auto
subgoal
using assms f_id t c' by auto
subgoal
using assms f_id t by auto
subgoal
using assms phis_stats f_id t c'
by (auto simp add: check_def condBranchFun_def split: named.splits intro!: checkFormula)
subgoal
using assms phis_stats f_id t c'
by (auto simp add: check_def condBranchFun_def split: named.splits intro!: checkFormula)
subgoal
using assms phis_stats f_id t c'
by (auto simp add: check_def condBranchFun_def split: named.splits)
subgoal
using assms phis_stats f_id t c'
by (auto simp add: check_def condBranchFun_def split: named.splits)
subgoal
using assms phis_stats f_id t c' by auto
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def condBranchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def condBranchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def condBranchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def condBranchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def condBranchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def condBranchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def condBranchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
subgoal
using assms phis_stats f_id t
by (auto simp add: check_def condBranchFun_def lookup_None_keys keys_dom_lookup split: named.splits
intro!: update_asFun phi_abstract.intros phi_abstractFun_phi_abstract checkFormula)
done
then show ?thesis
using assms
by(intro condBranchInf.intros[where as⇩1 = "asm_to_as (as_map_of_node n⇩1)" and as⇩2 = "asm_to_as (as_map_of_node n⇩2)"])
(auto simp add: renaming_of_edge'_def isOK_def check_def condBranchFun_def split: sum_bind_splits if_splits option.splits prod.splits)
qed
lemma icmpFun_icmpInf:
assumes "isOK (icmpFun n⇩1 n⇩2 v⇩n b)"
shows "icmpInf n⇩1 n⇩2"
proof -
obtain n p o⇩1 o⇩2 where
"find_statement prog (abstract_state_mapping.pos (as_map_of_node n⇩1)) =
Inr (Instruction (Named n (LLVM_Syntax.Icmp p o⇩1 o⇩2)))"
using assms by (auto simp add: icmpFun_def split: sum.splits stuck.splits option.splits action.splits named.splits instruction.splits)
then have "icmpAsInf prog (asm_to_as (as_map_of_node n⇩1)) (asm_to_as (as_map_of_node n⇩2)) "
using assms
apply(auto simp add: icmpFun_def isOK_def check_def
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits
elim!: option_to_sum.elims)
by (intro icmpAsInf.intros[where b=b and o⇩1=o⇩1 and o⇩2=o⇩2],
auto intro!: checkFormula update_asFun simp del: IA.implies_Language)+
then show ?thesis
using assms
apply(intro icmpInf.intros[where as⇩1 = "asm_to_as (as_map_of_node n⇩1)" and as⇩2 = "asm_to_as (as_map_of_node n⇩2)"])
subgoal
by ( auto intro!: icmpInf.intros simp add: icmpFun_def isOK_def check_def
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits
elim!: option_to_sum.elims)
subgoal
by ( auto intro!: icmpInf.intros simp add: icmpFun_def isOK_def check_def
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits
elim!: option_to_sum.elims)
subgoal
by ( auto intro!: icmpInf.intros simp add: icmpFun_def isOK_def check_def
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits
elim!: option_to_sum.elims)
subgoal
by (auto intro!: icmpInf.intros simp add: icmpFun_def renaming_of_edge'_def)
subgoal
by (auto simp add: icmpFun_def split: sum_bind_splits)
subgoal
by (auto simp add: icmpFun_def split: sum_bind_splits)
subgoal
by (auto simp add: icmpFun_def split: sum_bind_splits)
done
qed
lemma returnFun_returnInf:
assumes "isOK (returnFun n⇩1)"
shows "returnInf n⇩1"
proof -
obtain op t where "find_statement prog (pos (as_map_of_node n⇩1)) = Inr (Terminator t)"
"named_instruction t = Ret (Some op)"
using assms
by (auto simp add: isOK_def check_def returnFun_def simp del: find_statement.simps find_phis.simps formula.simps
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits option.splits
prod.splits terminator.splits stuck.splits
elim!: option_to_sum.elims)
then show ?thesis
using assms
apply(auto simp add: returnFun_def isOK_def check_def
split: sum.splits action.splits named.splits instruction.splits sum_bind_splits if_splits
elim!: option_to_sum.elims)
apply(intro returnInf.intros[of "asm_to_as (as_map_of_node n⇩1)"])
apply (auto intro!: checkFormula update_asFun simp del: IA.implies_Language)
apply(intro returnInf.intros[of "asm_to_as (as_map_of_node n⇩1)"])
apply (auto intro!: checkFormula update_asFun simp del: IA.implies_Language)
done
qed
end
context graph_exec'
begin
lemma isOK_map_sum:
assumes "isOK (map_sum e f m)"
shows "isOK m"
using assms by (cases m) auto
lemma closedGraphFun':
assumes "isOK closedGraphFun" "n ∈ nodes"
shows "isOK (option_to_sum (Mapping.lookup edge n) ((showsl STR ''No edge found for node: '' ∘∘ showsl) n) ⤜ checkEdge' n)"
proof -
have a: "nodes = set (map fst (nodes_as seg))"
using assms unfolding closedGraphFun_def by (auto)
show ?thesis
by (rule sequence_isOK[of closedGraphFun'])
(use assms in ‹auto dest!: isOK_map_sum simp add: collectErrorMessages_sequence a closedGraphFun_def closedGraphFun'_def›)
qed
lemmas seg_fun_inf = evalFun_evalInf genFun_genInf refineFun_refineInf
branchFun_branchInf condBranchFun_condBranchInf
icmpFun_icmpInf returnFun_returnInf evalExternalFun_evalExternalInf
lemma valid_edge_fun_intros:
"isOK (evalFun n n' v⇩n) ⟹ valid_edge n"
"isOK (genFun n n') ⟹ valid_edge n"
"isOK (refineFun n n⇩t n⇩f φ) ⟹ valid_edge n"
"isOK (branchFun n n' φs) ⟹ valid_edge n"
"isOK (condBranchFun n n' φs b) ⟹ valid_edge n"
"isOK (icmpFun n n' v⇩n b) ⟹ valid_edge n"
"isOK (returnFun n) ⟹ valid_edge n"
"isOK (evalExternalFun n n' v⇩n) ⟹ valid_edge n"
by (auto intro: valid_edge.intros seg_fun_inf)
lemma closedGraphFun:
assumes "isOK (closedGraphFun)"
shows "seg_represents"
proof -
let ?f = "(λn. option_to_sum (Mapping.lookup edge n) ((showsl STR ''No edge found for node: '' ∘∘ showsl) n) ⤜ checkEdge' n)"
have "valid_edge n" if "Mapping.lookup local.edge n = Some e" "isOK (checkEdge' n e)" for n e
using that by (cases e) (auto dest!: isOK_map_sum
simp add: choice_collect_error_messages_def checkEdge'_def
intro: valid_edge_fun_intros isOK_map_sum)
then have "valid_edge n" if "isOK (?f n)" for n
using that
by(cases "Mapping.lookup edge n")
(auto split: sum.splits simp add: checkEdge'_def elim!: checkEdge.elims)
then show ?thesis
using assms closedGraphFun' unfolding seg_represents_def closedGraphFun_def
by (auto)
qed
end
unbundle no_IA_formula_notation
end