Theory Construct_SSA_code
subsection ‹Code Equations for SSA Construction›
theory Construct_SSA_code imports
SSA_CFG_code
Construct_SSA
Mapping_Exts
"HOL-Library.Product_Lexorder"
begin
definition[code]: "lookup_multimap m k ≡ (case_option {} id (Mapping.lookup m k))"
locale CFG_Construct_linorder = CFG_Construct_wf αe αn invar inEdges' Entry "defs" "uses"
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry::"'g ⇒ 'node" and
"defs" :: "'g ⇒ 'node ⇒ ('var::linorder) set" and
"uses" :: "'g ⇒ 'node ⇒ 'var set"
begin
type_synonym ('n, 'v) sparse_phis = "('n × 'v, ('n, 'v) ssaVal list) mapping"
function readVariableRecursive :: "'g ⇒ 'var ⇒ 'node ⇒ ('node, 'var) sparse_phis ⇒ (('node, 'var) ssaVal × ('node, 'var) sparse_phis)"
and readArgs :: "'g ⇒ 'var ⇒ 'node ⇒ ('node, 'var) sparse_phis ⇒ 'node list ⇒ ('node, 'var) sparse_phis × ('node, 'var) ssaVal list"
where[code]: "readVariableRecursive g v n phis = (if v ∈ defs g n then ((v,n,SimpleDef), phis)
else case predecessors g n of
[] ⇒ ((v,n,PhiDef), Mapping.update (n,v) [] phis)
| [m] ⇒ readVariableRecursive g v m phis
| ms ⇒ (case Mapping.lookup phis (n,v) of
Some _ ⇒ ((v,n,PhiDef),phis)
| None ⇒
let phis = Mapping.update (n,v) [] phis in
let (phis,args) = readArgs g v n phis ms in
((v,n,PhiDef), Mapping.update (n,v) args phis)
))"
| "readArgs g v n phis [] = (phis,[])"
| "readArgs g v n phis (m#ms) = (
let (phis,args) = readArgs g v n phis ms in
let (v,phis) = readVariableRecursive g v m phis in
(phis,v#args))"
by pat_completeness auto
lemma length_filter_less2:
assumes "x ∈ set xs" "¬P x" "Q x" "⋀x. P x ⟹ Q x"
shows "length (filter P xs) < length (filter Q xs)"
proof-
have "⋀x. (Q x ∧ P x) = P x"
using assms(4) by auto
hence "filter P xs = filter P (filter Q xs)"
by auto
also have "length (...) < length (filter Q xs)"
using assms(1-3) by - (rule length_filter_less, auto)
finally show ?thesis .
qed
lemma length_filter_le2:
assumes "⋀x. P x ⟹ Q x"
shows "length (filter P xs) ≤ length (filter Q xs)"
proof-
have "⋀x. (Q x ∧ P x) = P x"
using assms by auto
hence "filter P xs = filter P (filter Q xs)"
by auto
also have "length (...) ≤ length (filter Q xs)"
by - (rule length_filter_le)
finally show ?thesis .
qed
abbreviation "phis_measure g v phis ≡ length [n ← αn g. Mapping.lookup phis (n,v) = None]"
lemma phis_measure_update_le: "phis_measure g v (Mapping.update k a p) ≤ phis_measure g v p"
apply (rule length_filter_le2)
apply (case_tac "k = (x, v)")
apply (auto simp: lookup_update lookup_update_neq)
done
lemma phis_measure_update_le': "phis_measure g v p ≤ phis_measure g v (Mapping.update k [] phis) ⟹
phis_measure g v (Mapping.update k a p) ≤ phis_measure g v phis"
apply (rule le_trans, rule phis_measure_update_le)
apply (rule le_trans, assumption, rule phis_measure_update_le)
done
lemma readArgs_phis_le:
"readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)) ⟹ (val,p) = readVariableRecursive g v n phis ⟹ phis_measure g v p ≤ phis_measure g v phis"
"readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, ms)) ⟹ (p,u) = readArgs g v n phis ms ⟹ phis_measure g v p ≤ phis_measure g v phis"
proof (induction arbitrary: val p and p u rule: readVariableRecursive_readArgs.pinduct)
case (1 g v n phis)
show ?case
using "1.IH"(1,2) "1.prems"
apply (auto simp: readVariableRecursive.psimps Let_def phis_measure_update_le split: if_split_asm list.splits option.splits prod.splits)
apply (subgoal_tac "phis_measure g v x1 ≤ phis_measure g v (Mapping.update (n,v) [] phis)")
defer
apply (rule "1.IH"(3))
apply (auto simp: phis_measure_update_le')
done
next
case (3 g v n m ms phis)
from "3.IH"(1) "3.prems" show ?case
apply (auto simp: readArgs.psimps split: prod.splits)
apply (rule le_trans)
apply (rule "3.IH"(3))
apply auto
apply (rule "3.IH"(2))
apply auto
done
qed (auto simp: readArgs.psimps split: prod.splits)
termination
apply (relation "measures [
λargs. let (g,v,phis) = case args of Inl((g,v,n,phis)) ⇒ (g,v,phis) | Inr((g,v,n,phis,ms)) ⇒ (g,v,phis) in
phis_measure g v phis,
λargs. case args of Inl(_) ⇒ 0 | Inr((g,v,n,phis,ms)) ⇒ length ms,
λargs. let (g,n) = case args of Inl((g,v,n,phis)) ⇒ (g,n) | Inr((g,v,n,ms,phis)) ⇒ (g,n) in
shortestPath g n
]")
apply (auto intro: shortestPath_single_predecessor)[2]
apply clarsimp
apply (rule_tac x=n in length_filter_less2)
apply (rule successor_in_αn; auto)
apply (auto simp: lookup_update)[2]
apply (case_tac "x=n"; auto simp: lookup_update_neq)
apply (auto dest: readArgs_phis_le)
done
declare readVariableRecursive.simps[simp del] readArgs.simps[simp del]
lemma fst_readVariableRecursive:
assumes "n ∈ set (αn g)"
shows "fst (readVariableRecursive g v n phis) = lookupDef g n v"
using assms
apply (induction rule: lookupDef_induct[where v=v])
apply (simp add: readVariableRecursive.simps)
apply (simp add: readVariableRecursive.simps; auto simp: split_def Let_def split: list.split option.split)
apply (auto simp add: readVariableRecursive.simps)
done
definition "phis'_aux g v ns (phis:: ('node,'var) sparse_phis) ≡ Mapping.Mapping (λ(m,v⇩2).
(if v⇩2=v ∧ m ∈ ⋃(phiDefNodes_aux g v [n ← αn g. (n,v) ∉ Mapping.keys phis] ` ns) ∧ v ∈ vars g then Some (map (λm. lookupDef g m v) (predecessors g m)) else (Mapping.lookup phis (m,v⇩2))))"
lemma phis'_aux_keys_super: "Mapping.keys (phis'_aux g v ns phis) ⊇ Mapping.keys phis"
by (auto simp: keys_dom_lookup phis'_aux_def)
lemma phiDefNodes_aux_in_unvisited:
shows "phiDefNodes_aux g v un n ⊆ set un"
proof (induction un arbitrary: n rule:removeAll_induct)
case (1 un)
show ?case
apply (simp only: phiDefNodes_aux.simps)
apply (auto elim!: fold_union_elem)
apply (rename_tac m n')
apply (drule_tac x2=n and n2=n' in 1)
apply auto[1]
apply (rename_tac m n')
apply (drule_tac x2=n and n2=n' in 1)
apply auto
done
qed
lemma phiDefNodes_aux_unvisited_monotonic:
assumes "set un ⊆ set un'"
shows "phiDefNodes_aux g v un n ⊆ phiDefNodes_aux g v un' n"
using assms proof (induction un arbitrary: un' n rule:removeAll_induct)
case (1 un)
{
fix m A
assume "n ∈ set un"
hence a: "⋀m. phiDefNodes_aux g v (removeAll n un) m ⊆ phiDefNodes_aux g v (removeAll n un') m"
apply (rule 1)
using 1(2)
by auto
assume "m ∈ fold (∪) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) A"
hence "m ∈ fold (∪) (map (phiDefNodes_aux g v (removeAll n un')) (predecessors g n)) A"
apply (rule fold_union_elem)
apply (rule fold_union_elemI')
apply (auto simp: image_def dest: a[THEN subsetD])
done
}
with 1(2) show ?case
apply (subst(1 2) phiDefNodes_aux.simps)
by auto
qed
lemma phiDefNodes_aux_single_pred:
assumes "predecessors g n = [m]"
shows "phiDefNodes_aux g v (removeAll n un) m = phiDefNodes_aux g v un m"
proof-
{
fix n' ns
assume asm: "g ⊢ n'-ns→m" "distinct ns" "length (predecessors g n') ≠ 1" "n ∈ set ns"
then obtain ns⇩1 ns⇩2 where split: "g ⊢ n'-ns⇩1→n" "g ⊢ n-ns⇩2→m" "ns = butlast ns⇩1 @ ns⇩2"
by - (rule path2_split_ex)
with ‹distinct ns› have "m ∉ set (butlast ns⇩1)"
by (auto dest: path2_last_in_ns)
from split(1,2) have False
apply-
apply (frule path2_unsnoc)
apply (erule path2_nontrivial)
using assms asm(3) ‹m ∉ set (butlast ns⇩1)›
apply (auto dest: path2_not_Nil)
done
}
with assms show ?thesis
apply-
apply rule
apply (rule phiDefNodes_aux_unvisited_monotonic; auto)
apply (rule subsetI)
apply (rename_tac n')
apply (erule phiDefNodes_auxE)
apply (rule predecessor_is_node[where n'=n]; auto)
apply (rule phiDefNodes_auxI; auto)
done
qed
lemma phis'_aux_finite:
assumes "finite (Mapping.keys phis)"
shows "finite (Mapping.keys (phis'_aux g v ns phis))"
proof-
have a: "⋀n. phiDefNodes_aux g v [n←αn g . (n, v) ∉ dom (Mapping.lookup phis)] n ⊆ (set (αn g))"
by (rule subset_trans, rule phiDefNodes_aux_in_unvisited, auto)
have "Mapping.keys (phis'_aux g v ns phis) ⊆ set (αn g) × vars g ∪ Mapping.keys phis"
by (auto simp: phis'_aux_def keys_dom_lookup split: if_split_asm dest: subsetD[OF a])
thus ?thesis by (rule finite_subset, auto intro: assms)
qed
lemma phiDefNodes_aux_redirect:
assumes asm: "g ⊢ n-ns→m" "∀n ∈ set ns. v ∉ defs g n" "length (predecessors g n) ≠ 1" "unvisitedPath un ns"
assumes n': "n' ∈ set ns" "n' ∈ phiDefNodes_aux g v un m'" "m' ∈ set (αn g)"
shows "n ∈ phiDefNodes_aux g v un m'"
proof-
from asm(1) n'(1) obtain ns⇩1 where ns⇩1: "g ⊢ n-ns⇩1→n'" "set ns⇩1 ⊆ set ns"
by (rule path2_split_ex, simp)
from n'(2-3) obtain ns' where ns': "g ⊢ n'-ns'→m'" "∀n ∈ set ns'. v ∉ defs g n" "length (predecessors g n') ≠ 1"
"unvisitedPath un ns'"
by (rule phiDefNodes_auxE)
from ns⇩1(1) ns'(1) obtain ms where ms: "g ⊢ n-ms→m'" "distinct ms" "set ms ⊆ set ns⇩1 ∪ set (tl ns')"
by - (drule path2_app, auto elim: simple_path2)
show ?thesis
using ms(1)
apply (rule phiDefNodes_auxI)
using ms asm(4) ns⇩1(2) ns'(4)
apply clarsimp
apply (rename_tac x)
apply (case_tac "x ∈ set ns⇩1")
apply (drule_tac A="set ns" and c=x in subsetD; auto)
apply (drule_tac A="set ns'" and c=x in subsetD; auto)
using asm(2-3) ns⇩1(2) ns'(2) ms(3)
apply (auto dest!: bspec)
done
qed
lemma snd_readVariableRecursive:
assumes "v ∈ vars g" "n ∈ set (αn g)" "finite (Mapping.keys phis)"
"⋀n. (n,v) ∈ Mapping.keys phis ⟹ length (predecessors g n) ≠ 1" "Mapping.lookup phis (Entry g,v) ∈ {None, Some []}"
shows
"phis'_aux g v {n} phis = snd (readVariableRecursive g v n phis)"
"set ms ⊆ set (αn g) ⟹ (phis'_aux g v (set ms) phis, map (λm. lookupDef g m v) ms) = readArgs g v n phis ms"
using assms proof (induction g v n phis and g v n phis ms rule: readVariableRecursive_readArgs.induct)
case (1 g v n phis)
note "1.prems"(1-3)[simp]
note phis_wf = "1.prems"(4)[rule_format]
from "1.prems"(5) have a: "(Entry g,v) ∈ Mapping.keys phis ⟹ Mapping.lookup phis (Entry g, v) = Some []"
by (auto simp: keys_dom_lookup)
have IH1: "⋀m. v ∉ defs g n ⟹ predecessors g n = [m] ⟹ phis'_aux g v {m} phis = snd (readVariableRecursive g v m phis)"
apply (rule "1.IH"[rule_format])
apply auto[4]
apply (rule_tac n'=n in predecessor_is_node; auto)
using "1.prems"(5)
apply (auto dest: phis_wf)
done
{
fix m⇩1 m⇩2 :: 'node
fix ms' :: "'node list"
let ?ms = "m⇩1#m⇩2#ms'"
let ?phis' = "Mapping.update (n,v) [] phis"
assume asm: "v ∉ defs g n" "predecessors g n = ?ms" "Mapping.lookup phis (n, v) = None"
moreover have "set ?ms ⊆ set (αn g)"
by (rule subsetI, rule predecessor_is_node[of _ g n]; auto simp: asm(2))
ultimately have "readArgs g v n ?phis' ?ms = (phis'_aux g v (set ?ms) ?phis', map (λm. lookupDef g m v) ?ms)"
using "1.prems"(5)
by - (rule "1.IH"(2)[symmetric, rule_format]; auto dest: phis_wf simp: lookup_update_cases)
}
note IH2 = this
note foldr_Cons[simp del] fold_Cons[simp del] list.map(2)[simp del] set_simps(2)[simp del]
have c: "⋀f x. ⋃(f ` {x}) = f x" by auto
show ?case
unfolding phis'_aux_def c
apply (subst readVariableRecursive.simps)
apply (subst phiDefNodes_aux.simps[abs_def])
apply (cases "predecessors g n")
apply (auto simp: a Mapping_eq_lookup lookup_update_cases Entry_iff_unreachable[OF invar] split: list.split intro!: ext)[1]
apply (rename_tac m⇩1 ms)
apply (case_tac ms)
apply (subst Mapping_eq_lookup)
apply (intro ext)
apply (auto simp: fold_Cons list.map(2))[1]
apply (auto dest: phis_wf)[1]
apply (subst IH1[symmetric], assumption, assumption)
apply (auto simp: phis'_aux_def)[1]
apply (drule rev_subsetD, rule phiDefNodes_aux_unvisited_monotonic[where un'="[n←αn g . (n, v) ∉ Mapping.keys phis]"]; auto)
apply (subst IH1[symmetric], assumption, assumption)
apply (auto simp: phis'_aux_def)[1]
apply (subst IH1[symmetric], assumption, assumption)
apply (auto simp: phis'_aux_def phiDefNodes_aux_single_pred)[1]
apply (auto simp: Mapping_eq_lookup lookup_update_cases intro!: ext)
apply (auto simp: keys_dom_lookup)[1]
apply (auto split: option.split prod.split)[1]
apply (subst(asm) IH2, assumption, assumption, assumption)
apply (erule fold_union_elem)
apply (auto simp: lookup_update_cases phis'_aux_def[abs_def])[1]
apply (drule rev_subsetD, rule phiDefNodes_aux_unvisited_monotonic[where un'="[n'←αn g . n' ≠ n ∧ (n', v) ∉ Mapping.keys phis]"]; auto)
apply (drule rev_subsetD, rule phiDefNodes_aux_unvisited_monotonic[where un'="[n'←αn g . n' ≠ n ∧ (n', v) ∉ Mapping.keys phis]"]; auto)
apply (rename_tac m)
apply (erule_tac x=m in ballE)
apply (drule rev_subsetD, rule phiDefNodes_aux_unvisited_monotonic[where un'="[n'←αn g . n' ≠ n ∧ (n', v) ∉ Mapping.keys phis]"]; auto)
apply auto[1]
apply (subst(asm) IH2, assumption, assumption)
apply (auto simp: keys_dom_lookup)[2]
apply (auto split: option.split prod.split)[1]
apply (subst(asm) IH2, assumption, assumption, assumption)
apply (auto simp: lookup_update_neq phis'_aux_def)[1]
apply (auto split: option.splits prod.splits)[1]
apply (subst(asm) IH2, assumption, assumption, assumption)
apply (auto simp: lookup_update_cases phis'_aux_def removeAll_filter_not_eq image_def split: if_split_asm)[1]
apply (cut_tac fold_union_elemI)
apply auto[3]
apply (cut_tac fold_union_elemI)
apply auto[1]
apply assumption
apply (subgoal_tac "[x←αn g . x ≠ n ∧ (x, v) ∉ Mapping.keys phis] = [x←αn g . (x, v) ∉ Mapping.keys phis ∧ n ≠ x]")
apply auto[1]
apply (rule arg_cong2[where f=filter])
apply auto[2]
apply (cut_tac fold_union_elemI)
apply auto[1]
apply assumption
apply (subgoal_tac "[x←αn g . x ≠ n ∧ (x, v) ∉ Mapping.keys phis] = [x←αn g . (x, v) ∉ Mapping.keys phis ∧ n ≠ x]")
apply auto[1]
apply (rule arg_cong2[where f=filter])
apply auto[2]
apply (cut_tac fold_union_elemI)
apply auto[1]
apply assumption
apply (subgoal_tac "[x←αn g . x ≠ n ∧ (x, v) ∉ Mapping.keys phis] = [x←αn g . (x, v) ∉ Mapping.keys phis ∧ n ≠ x]")
apply auto[1]
apply (rule arg_cong2[where f=filter])
apply auto[2]
done
next
case (3 g v n phis m ms)
note "3.prems"(2-4)[simp]
from "3.prems"(1) have[simp]: "m ∈ set (αn g)" by auto
from 3 have IH1: "readArgs g v n phis ms = (phis'_aux g v (set ms) phis, map (λm. lookupDef g m v) ms)"
by auto
have IH2: "phis'_aux g v {m} (phis'_aux g v (set ms) phis) = snd (readVariableRecursive g v m (phis'_aux g v (set ms) phis))"
apply (rule "3.IH"(2))
apply (auto simp: IH1 intro: phis'_aux_finite)[5]
apply (simp add: phis'_aux_def keys_dom_lookup dom_def split: if_split_asm)
apply safe
apply (erule phiDefNodes_auxE)
using "3.prems"(1,5)
apply (auto simp: keys_dom_lookup)[3]
using "3.prems"(6)
apply (auto simp: phis'_aux_def split: if_split_asm)
done
have a: "phiDefNodes_aux g v [n←αn g . (n, v) ∉ Mapping.keys (phis'_aux g v (set ms) phis)] m ⊆ phiDefNodes_aux g v [n←αn g . (n, v) ∉ Mapping.keys phis] m"
apply (rule phiDefNodes_aux_unvisited_monotonic)
by (auto dest: phis'_aux_keys_super[THEN subsetD])
{
fix n
assume m: "n ∈ phiDefNodes_aux g v [n←αn g . (n, v) ∉ Mapping.keys phis] m" and
ms: "∀x∈set ms. n ∉ phiDefNodes_aux g v [n←αn g . (n, v) ∉ Mapping.keys phis] x"
have "n ∈ phiDefNodes_aux g v [n←αn g . (n, v) ∉ Mapping.keys (phis'_aux g v (set ms) phis)] m"
using m
apply-
apply (erule phiDefNodes_auxE, simp)
apply (rule phiDefNodes_auxI)
apply (auto simp: phis'_aux_def keys_dom_lookup split: if_split_asm)[3]
apply (drule phiDefNodes_aux_redirect)
using "3.prems"(1)
apply auto[6]
apply (rule ms[THEN ballE]; auto simp: keys_dom_lookup)
apply auto
done
}
note b = this
show ?case
unfolding readArgs.simps phis'_aux_def
unfolding IH1
apply (simp add: split_def Let_def IH2[symmetric])
apply (subst phis'_aux_def)
apply (subst(2) phis'_aux_def)
apply (auto simp: Mapping_eq_lookup fst_readVariableRecursive split: prod.splits intro!: ext dest!: a[THEN subsetD] b)
done
qed (auto simp: readArgs.simps phis'_aux_def)
definition "aux_1 g n = (λv (uses,phis).
let (use,phis') = readVariableRecursive g v n phis in
(Mapping.update n (insert use (lookup_multimap uses n)) uses, phis')
)"
definition "aux_2 g n = foldr (aux_1 g n) (sorted_list_of_set (uses g n))"
abbreviation "init_state ≡ (Mapping.empty, Mapping.empty)"
abbreviation "from_sparse ≡ λ(n,v). (n,(v,n,PhiDef))"
definition "uses'_phis' g = (
let (u,p) = foldr (aux_2 g) (αn g) init_state in
(u, map_keys from_sparse p)
)"
lemma from_sparse_inj: "inj from_sparse"
by (rule injI, auto)
declare uses'_phis'_def[unfolded aux_2_def[abs_def] aux_1_def, code]
lift_definition phis'_code :: "'g ⇒ ('node, ('node, 'var) ssaVal) phis_code" is phis' .
lemma foldr_prod: "foldr (λx y. (f1 x (fst y), f2 x (snd y))) xs y = (foldr f1 xs (fst y), foldr f2 xs (snd y))"
by (induction xs, auto)
lemma foldr_aux_1:
assumes "set us ⊆ uses g n" "Mapping.lookup u n = None" "foldr (aux_1 g n) us (u,p) = (u',p')" (is "foldr ?f _ _ = _")
assumes "finite (Mapping.keys p)" "⋀n v. (n,v) ∈ Mapping.keys p ⟹ length (predecessors g n) ≠ 1" "⋀v. Mapping.lookup p (Entry g,v) ∈ {None, Some []}"
shows "lookupDef g n ` set us = lookup_multimap u' n" "⋀m. m ≠ n ⟹ Mapping.lookup u' m = Mapping.lookup u m"
"⋀m v. (if m ∈ phiDefNodes_aux g v [n ← αn g. (n,v) ∉ Mapping.keys p] n ∧ v ∈ set us then
Some (map (λm. lookupDef g m v) (predecessors g m)) else
(Mapping.lookup p (m,v))) = Mapping.lookup p' (m,v)"
using assms proof (induction us arbitrary: u' p')
case (Cons v us)
let ?u = "fst (foldr ?f us (u,p))"
let ?p = "snd (foldr ?f us (u,p))"
{
case 1
have "n ∈ set (αn g)" using 1(1) uses_in_αn by auto
hence "lookupDef g n v = fst (readVariableRecursive g v n ?p)"
by (rule fst_readVariableRecursive[symmetric])
moreover have "lookupDef g n ` set us = lookup_multimap ?u n"
using 1 by - (rule Cons(1)[of ?u ?p], auto)
ultimately show ?case
using 1(3) by (auto simp: aux_1_def split_def Let_def lookup_multimap_def lookup_update split: option.splits)
next
case 2
have "Mapping.lookup ?u m = Mapping.lookup u m"
using 2 by - (rule Cons(2)[of _ ?u ?p], auto)
thus ?case
using 2 by (auto simp: aux_1_def split_def Let_def lookup_multimap_def lookup_update_neq split: option.splits)
next
case (3 m v' u' p')
from 3(1) have[simp]: "⋀v. v ∈ set us ⟹ v ∈ vars g"
by auto
from 3 have IH: "⋀m v'. (if m ∈ phiDefNodes_aux g v' [n ← αn g. (n,v') ∉ Mapping.keys p] n ∧ v' ∈ set us then
Some (map (λm. lookupDef g m v') (predecessors g m)) else
(Mapping.lookup p (m,v'))) = Mapping.lookup ?p (m,v')"
by - (rule Cons(3)[of ?u ?p], auto)
have rVV: "phis'_aux g v {n} ?p = snd (readVariableRecursive g v n ?p)"
apply (rule snd_readVariableRecursive(1))
using 3
apply (auto simp: uses_in_αn)[2]
apply (rule finite_subset[where B="set (αn g) × vars g ∪ Mapping.keys p"])
apply (auto simp: keys_dom_lookup IH[symmetric] split: if_split_asm dest!: phiDefNodes_aux_in_unvisited[THEN subsetD])[1]
apply (simp add: 3(4))[1]
using 3(5-6)
apply (auto simp: keys_dom_lookup dom_def IH[symmetric] split: if_split_asm dest!: phiDefNode_aux_is_join_node)
done
have a: "m ∈ phiDefNodes_aux g v [n←αn g . (n, v) ∉ Mapping.keys ?p] n ⟹ m ∈ phiDefNodes_aux g v [n←αn g . (n, v) ∉ Mapping.keys p] n"
apply (erule rev_subsetD)
apply (rule phiDefNodes_aux_unvisited_monotonic)
by (auto simp: IH[symmetric] keys_dom_lookup split: if_split_asm)
have b: "v ∉ set us ⟹ [n←αn g . (n, v) ∉ Mapping.keys ?p] = [n←αn g . (n, v) ∉ Mapping.keys p]"
by (rule arg_cong2[where f=filter], auto simp: keys_dom_lookup IH[symmetric])
from 3 show ?case
unfolding aux_1_def
unfolding foldr.foldr_Cons
unfolding aux_1_def[symmetric]
by (auto simp: Let_def split_def IH[symmetric] rVV[symmetric] phis'_aux_def b dest: a uses_in_vars split: if_split_asm)
}
qed (auto simp: lookup_multimap_def)
lemma foldr_aux_2:
assumes "set ns ⊆ set (αn g)" "distinct ns" "foldr (aux_2 g) ns init_state = (u',p')"
shows "⋀n. n ∈ set ns ⟹ uses' g n = lookup_multimap u' n" "⋀n. n ∉ set ns ⟹ Mapping.lookup u' n = None"
"⋀m v. (if ∃n ∈ set ns. m ∈ phiDefNodes_aux g v (αn g) n ∧ v ∈ uses g n then
Some (map (λm. lookupDef g m v) (predecessors g m)) else
None) = Mapping.lookup p' (m,v)"
using assms proof (induction ns arbitrary: u' p')
case (Cons n ns)
let ?u = "fst (foldr (aux_2 g) ns init_state)"
let ?p = "snd (foldr (aux_2 g) ns init_state)"
fix m u' p'
assume asm: "set (n#ns) ⊆ set (αn g)" "distinct (n#ns)" "foldr (aux_2 g) (n#ns) init_state = (u', p')"
hence IH:
"⋀n. n ∈ set ns ⟹ uses' g n = lookup_multimap ?u n"
"⋀n. n ∉ set ns ⟹ Mapping.lookup ?u n = None"
"⋀m v. (if ∃n ∈ set ns. m ∈ phiDefNodes_aux g v (αn g) n ∧ v ∈ uses g n then
Some (map (λm. lookupDef g m v) (predecessors g m)) else
None) = Mapping.lookup ?p (m,v)"
apply -
apply (rule Cons.IH(1)[where p'2="?p"]; auto; fail)
apply (rule Cons.IH(2)[where p'2="?p"]; auto; fail)
by (rule Cons.IH(3)[where u'2="?u"], auto)
with this[of n] asm(2) have a': "Mapping.lookup ?u n = None" by simp
moreover have "finite (Mapping.keys ?p)"
by (rule finite_subset[where B="set (αn g) × vars g"]) (auto simp: keys_dom_lookup IH[symmetric] split: if_split_asm dest!: phiDefNodes_aux_in_unvisited[THEN subsetD])
moreover have "⋀n v. (n,v) ∈ Mapping.keys ?p ⟹ length (predecessors g n) ≠ 1"
by (auto simp: keys_dom_lookup dom_def IH[symmetric] split: if_split_asm dest!: phiDefNode_aux_is_join_node)
moreover have "⋀v. Mapping.lookup ?p (Entry g,v) ∈ {None, Some []}"
by (auto simp: IH[symmetric])
ultimately have aux_2: "lookupDef g n ` uses g n = lookup_multimap u' n" "⋀m. m ≠ n ⟹ Mapping.lookup u' m = Mapping.lookup ?u m"
"⋀m v. (if m ∈ phiDefNodes_aux g v [n ← αn g. (n,v) ∉ Mapping.keys ?p] n ∧ v ∈ uses g n then
Some (map (λm. lookupDef g m v) (predecessors g m)) else
(Mapping.lookup ?p (m,v))) = Mapping.lookup p' (m,v)"
apply-
apply (rule foldr_aux_1(1)[of "sorted_list_of_set (uses g n)" g n ?u ?p u' p', simplified]; simp add: aux_2_def[symmetric] asm(3)[simplified]; fail)
apply (rule foldr_aux_1(2)[of "sorted_list_of_set (uses g n)" g n ?u ?p u' p', simplified]; simp add: aux_2_def[symmetric] asm(3)[simplified]; fail)
apply (rule foldr_aux_1(3)[of "sorted_list_of_set (uses g n)" g n ?u ?p u' p', simplified]; simp add: aux_2_def[symmetric] asm(3)[simplified]; fail)
done
{
assume 1: "m ∈ set (n#ns)"
show "uses' g m = lookup_multimap u' m"
apply (cases "m = n")
apply (simp add: uses'_def aux_2)
using 1 asm(2)
apply (auto simp: IH(1) lookup_multimap_def aux_2(2))
done
next
assume 2: "m ∉ set (n#ns)"
thus "Mapping.lookup u' m = None"
by (simp add: aux_2(2) IH(2))
next
fix v
show "(if ∃n ∈ set (n#ns). m ∈ phiDefNodes_aux g v (αn g) n ∧ v ∈ uses g n then
Some (map (λm. lookupDef g m v) (predecessors g m)) else
None) = Mapping.lookup p' (m,v)"
apply (auto simp: aux_2(3)[symmetric] IH(3)[symmetric] keys_dom_lookup dom_def)
apply (erule phiDefNodes_auxE)
apply (erule uses_in_αn)
apply (rule phiDefNodes_auxI)
apply auto[4]
apply (drule phiDefNodes_aux_redirect; auto simp: uses_in_αn; fail)
apply (drule rev_subsetD)
apply (rule phiDefNodes_aux_unvisited_monotonic)
apply auto
done
}
qed (auto simp: lookup_empty)
lemma fst_uses'_phis': "uses' g = lookup_multimap (fst (uses'_phis' g))"
apply (rule ext)
apply (simp add: uses'_phis'_def Let_def split_def)
apply (case_tac "x ∈ set (αn g)")
apply (rule foldr_aux_2(1)[OF _ _ surjective_pairing]; auto simp: lookup_empty intro: αn_distinct; fail)
unfolding lookup_multimap_def
apply (subst foldr_aux_2(2)[OF _ _ surjective_pairing]; auto simp: lookup_empty uses_in_αn uses'_def intro: αn_distinct)
done
lemma fst_uses'_phis'_in_αn: "Mapping.keys (fst (uses'_phis' g)) ⊆ set (αn g)"
apply (rule subsetI)
apply (rule ccontr)
apply (simp add: uses'_phis'_def Let_def split_def keys_dom_lookup dom_def)
apply (subst(asm) foldr_aux_2(2)[OF _ _ surjective_pairing]; auto intro: αn_distinct)
done
lemma snd_uses'_phis': "phis'_code g = snd (uses'_phis' g)"
proof-
have a: "⋀n v. (THE k. (λp. (fst p, snd p, fst p, PhiDef)) -` {(n, v, n, PhiDef)} = {k}) = (n,v)"
by (rule the1_equality) (auto simp: vimage_def)
show ?thesis
apply (subst Mapping_eq_lookup)
apply transfer
apply (simp add: phis'_def uses'_phis'_def Let_def split_def)
apply (auto simp: lookup_map_keys a intro!: ext)
subgoal by (auto simp: vimage_def)[1]
subgoal
apply (subst foldr_aux_2(3)[OF _ _ surjective_pairing, symmetric])
by (auto simp: phiDefNodes_def vimage_def elim!: fold_union_elem intro!: αn_distinct split: if_split_asm)
subgoal
apply (subst(asm) foldr_aux_2(3)[OF _ _ surjective_pairing, symmetric])
by (auto simp: phiDefNodes_def vimage_def elim!: fold_union_elem intro!: αn_distinct split: if_split_asm)
subgoal
apply (subst(asm) foldr_aux_2(3)[OF _ _ surjective_pairing, symmetric])
by (auto simp: phiDefNodes_def vimage_def elim!: fold_union_elem intro!: αn_distinct fold_union_elemI split: if_split_asm)
done
qed
end
end