theory "CoCallGraph-TTree"
imports CoCallGraph "TTree-HOLCF"
begin
lemma interleave_ccFromList:
"xs ∈ interleave ys zs ⟹ ccFromList xs = ccFromList ys ⊔ ccFromList zs ⊔ ccProd (set ys) (set zs)"
by (induction rule: interleave_induct)
(auto simp add: interleave_set ccProd_comm ccProd_insert2[where S' = "set xs" for xs] ccProd_insert1[where S' = "set xs" for xs] )
lift_definition ccApprox :: "var ttree ⇒ CoCalls"
is "λ xss . lub (ccFromList ` xss)".
lemma ccApprox_paths: "ccApprox t = lub (ccFromList ` (paths t))" by transfer simp
lemma ccApprox_strict[simp]: "ccApprox ⊥ = ⊥"
by (simp add: ccApprox_paths empty_is_bottom[symmetric])
lemma in_ccApprox: "(x--y∈(ccApprox t)) ⟷ (∃ xs ∈ paths t. (x--y∈(ccFromList xs)))"
unfolding ccApprox_paths
by transfer auto
lemma ccApprox_mono: "paths t ⊆ paths t' ⟹ ccApprox t ⊑ ccApprox t'"
by (rule below_CoCallsI) (auto simp add: in_ccApprox)
lemma ccApprox_mono': "t ⊑ t' ⟹ ccApprox t ⊑ ccApprox t'"
by (metis below_set_def ccApprox_mono paths_mono_iff)
lemma ccApprox_belowI: "(⋀ xs. xs ∈ paths t ⟹ ccFromList xs ⊑ G) ⟹ ccApprox t ⊑ G"
unfolding ccApprox_paths
by transfer auto
lemma ccApprox_below_iff: "ccApprox t ⊑ G ⟷ (∀ xs ∈ paths t. ccFromList xs ⊑ G)"
unfolding ccApprox_paths by transfer auto
lemma cc_restr_ccApprox_below_iff: "cc_restr S (ccApprox t) ⊑ G ⟷ (∀ xs ∈ paths t. cc_restr S (ccFromList xs) ⊑ G)"
unfolding ccApprox_paths cc_restr_lub
by transfer auto
lemma ccFromList_below_ccApprox:
"xs ∈ paths t ⟹ ccFromList xs ⊑ ccApprox t"
by (rule below_CoCallsI)(auto simp add: in_ccApprox)
lemma ccApprox_nxt_below:
"ccApprox (nxt t x) ⊑ ccApprox t"
by (rule below_CoCallsI)(auto simp add: in_ccApprox paths_nxt_eq elim!: bexI[rotated])
lemma ccApprox_ttree_restr_nxt_below:
"ccApprox (ttree_restr S (nxt t x)) ⊑ ccApprox (ttree_restr S t)"
by (rule below_CoCallsI)
(auto simp add: in_ccApprox filter_paths_conv_free_restr[symmetric] paths_nxt_eq elim!: bexI[rotated])
lemma ccApprox_ttree_restr[simp]: "ccApprox (ttree_restr S t) = cc_restr S (ccApprox t)"
by (rule CoCalls_eqI) (auto simp add: in_ccApprox filter_paths_conv_free_restr[symmetric] )
lemma ccApprox_both: "ccApprox (t ⊗⊗ t') = ccApprox t ⊔ ccApprox t' ⊔ ccProd (carrier t) (carrier t')"
proof (rule below_antisym)
show "ccApprox (t ⊗⊗ t') ⊑ ccApprox t ⊔ ccApprox t' ⊔ ccProd (carrier t) (carrier t')"
by (rule below_CoCallsI)
(auto 4 4 simp add: in_ccApprox paths_both Union_paths_carrier[symmetric] interleave_ccFromList)
next
have "ccApprox t ⊑ ccApprox (t ⊗⊗ t')"
by (rule ccApprox_mono[OF both_contains_arg1])
moreover
have "ccApprox t' ⊑ ccApprox (t ⊗⊗ t')"
by (rule ccApprox_mono[OF both_contains_arg2])
moreover
have "ccProd (carrier t) (carrier t') ⊑ ccApprox (t ⊗⊗ t')"
proof(rule ccProd_belowI)
fix x y
assume "x ∈ carrier t" and "y ∈ carrier t'"
then obtain xs ys where "x ∈ set xs" and "y ∈ set ys"
and "xs ∈ paths t" and "ys ∈ paths t'" by (auto simp add: Union_paths_carrier[symmetric])
hence "xs @ ys ∈ paths (t ⊗⊗ t')" by (metis paths_both append_interleave)
moreover
from `x ∈ set xs` `y ∈ set ys`
have "x--y∈(ccFromList (xs@ys))" by simp
ultimately
show "x--y∈(ccApprox (t ⊗⊗ t'))" by (auto simp add: in_ccApprox simp del: ccFromList_append)
qed
ultimately
show "ccApprox t ⊔ ccApprox t' ⊔ ccProd (carrier t) (carrier t') ⊑ ccApprox (t ⊗⊗ t')"
by (simp add: join_below_iff)
qed
lemma ccApprox_many_calls[simp]:
"ccApprox (many_calls x) = ccProd {x} {x}"
by transfer' (rule CoCalls_eqI, auto)
lemma ccApprox_single[simp]:
"ccApprox (TTree.single y) = ⊥"
by transfer' auto
lemma ccApprox_either[simp]: "ccApprox (t ⊕⊕ t') = ccApprox t ⊔ ccApprox t'"
by transfer' (rule CoCalls_eqI, auto)
lemma wild_recursion:
assumes "ccApprox t ⊑ G"
assumes "⋀ x. x ∉ S ⟹ f x = empty"
assumes "⋀ x. x ∈ S ⟹ ccApprox (f x) ⊑ G"
assumes "⋀ x. x ∈ S ⟹ ccProd (ccNeighbors x G) (carrier (f x)) ⊑ G"
shows "ccApprox (ttree_restr (-S) (substitute f T t)) ⊑ G"
proof(rule ccApprox_belowI)
fix xs
def seen ≡ "{} :: var set"
assume "xs ∈ paths (ttree_restr (- S) (substitute f T t))"
then obtain xs' xs'' where "xs = [x←xs' . x ∉ S]" and "substitute'' f T xs'' xs'" and "xs'' ∈ paths t"
by (auto simp add: filter_paths_conv_free_restr2[symmetric] substitute_substitute'')
note this(2)
moreover
from `ccApprox t ⊑ G` and `xs'' ∈ paths t`
have "ccFromList xs'' ⊑ G"
by (auto simp add: ccApprox_below_iff)
moreover
note assms(2)
moreover
from assms(3,4)
have "⋀ x ys. x ∈ S ⟹ ys ∈ paths (f x) ⟹ ccFromList ys ⊑ G"
and "⋀ x ys. x ∈ S ⟹ ys ∈ paths (f x) ⟹ ccProd (ccNeighbors x G) (set ys) ⊑ G"
by (auto simp add: ccApprox_below_iff Union_paths_carrier[symmetric] cc_lub_below_iff)
moreover
have "ccProd seen (set xs'') ⊑ G" unfolding seen_def by simp
ultimately
have "ccFromList [x←xs' . x ∉ S] ⊑ G ∧ ccProd (seen) (set xs') ⊑ G"
proof(induction f T xs'' xs' arbitrary: seen rule: substitute''.induct[case_names Nil Cons])
case Nil thus ?case by simp
next
case (Cons zs f x xs' xs T ys)
have seen_x: "ccProd seen {x} ⊑ G"
using `ccProd seen (set (x # xs)) ⊑ G`
by (auto simp add: ccProd_insert2[where S' = "set xs" for xs] join_below_iff)
show ?case
proof(cases "x ∈ S")
case True
from `ccFromList (x # xs) ⊑ G`
have "ccProd {x} (set xs) ⊑ G" by (auto simp add: join_below_iff)
hence subset1: "set xs ⊆ ccNeighbors x G" by transfer auto
from `ccProd seen (set (x # xs)) ⊑ G`
have subset2: "seen ⊆ ccNeighbors x G"
by (auto simp add: subset_ccNeighbors ccProd_insert2[where S' = "set xs" for xs] join_below_iff ccProd_comm)
from subset1 and subset2
have "seen ∪ set xs ⊆ ccNeighbors x G" by auto
hence "ccProd (seen ∪ set xs) (set zs) ⊑ ccProd (ccNeighbors x G) (set zs)"
by (rule ccProd_mono1)
also
from `x ∈ S` `zs ∈ paths (f x)`
have "… ⊑ G"
by (rule Cons.prems(4))
finally
have "ccProd (seen ∪ set xs) (set zs) ⊑ G" by this simp
with `x ∈ S` Cons.prems Cons.hyps
have "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd (seen) (set ys) ⊑ G"
apply -
apply (rule Cons.IH)
apply (auto simp add: f_nxt_def join_below_iff interleave_ccFromList interleave_set ccProd_insert2[where S' = "set xs" for xs]
split: if_splits)
done
with `x ∈ S` seen_x
show "ccFromList [x←x # ys . x ∉ S] ⊑ G ∧ ccProd seen (set (x#ys)) ⊑ G"
by (auto simp add: ccProd_insert2[where S' = "set xs" for xs] join_below_iff)
next
case False
from False Cons.prems Cons.hyps
have "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd ((insert x seen)) (set ys) ⊑ G"
apply -
apply (rule Cons.IH[where seen = "insert x seen"])
apply (auto simp add: ccApprox_both join_below_iff ttree_restr_both interleave_ccFromList insert_Diff_if
simp add: ccProd_insert2[where S' = "set xs" for xs]
simp add: ccProd_insert1[where S' = "seen"])
done
moreover
from False this
have "ccProd {x} (set ys) ⊑ G"
by (auto simp add: insert_Diff_if ccProd_insert1[where S' = "seen"] join_below_iff)
hence "ccProd {x} {x ∈ set ys. x ∉ S} ⊑ G"
by (rule below_trans[rotated, OF _ ccProd_mono2]) auto
moreover
note False seen_x
ultimately
show "ccFromList [x←x # ys . x ∉ S] ⊑ G ∧ ccProd (seen) (set (x # ys)) ⊑ G"
by (auto simp add: join_below_iff simp add: insert_Diff_if ccProd_insert2[where S' = "set xs" for xs] ccProd_insert1[where S' = "seen"])
qed
qed
with `xs = _`
show "ccFromList xs ⊑ G" by simp
qed
lemma wild_recursion_thunked:
assumes "ccApprox t ⊑ G"
assumes "⋀ x. x ∉ S ⟹ f x = empty"
assumes "⋀ x. x ∈ S ⟹ ccApprox (f x) ⊑ G"
assumes "⋀ x. x ∈ S ⟹ ccProd (ccNeighbors x G - {x} ∩ T) (carrier (f x)) ⊑ G"
shows "ccApprox (ttree_restr (-S) (substitute f T t)) ⊑ G"
proof(rule ccApprox_belowI)
fix xs
def seen ≡ "{} :: var set"
def seen_T ≡ "{} :: var set"
assume "xs ∈ paths (ttree_restr (- S) (substitute f T t))"
then obtain xs' xs'' where "xs = [x←xs' . x ∉ S]" and "substitute'' f T xs'' xs'" and "xs'' ∈ paths t"
by (auto simp add: filter_paths_conv_free_restr2[symmetric] substitute_substitute'')
note this(2)
moreover
from `ccApprox t ⊑ G` and `xs'' ∈ paths t`
have "ccFromList xs'' ⊑ G"
by (auto simp add: ccApprox_below_iff)
hence "ccFromList xs'' G|` (- seen_T) ⊑ G"
by (rule rev_below_trans[OF _ cc_restr_below_arg])
moreover
note assms(2)
moreover
from assms(3,4)
have "⋀ x ys. x ∈ S ⟹ ys ∈ paths (f x) ⟹ ccFromList ys ⊑ G"
and "⋀ x ys. x ∈ S ⟹ ys ∈ paths (f x) ⟹ ccProd (ccNeighbors x G - {x} ∩ T) (set ys) ⊑ G"
by (auto simp add: ccApprox_below_iff seen_T_def Union_paths_carrier[symmetric] cc_lub_below_iff)
moreover
have "ccProd seen (set xs'' - seen_T) ⊑ G" unfolding seen_def seen_T_def by simp
moreover
have "seen ∩ S = {}" unfolding seen_def by simp
moreover
have "seen_T ⊆ S" unfolding seen_T_def by simp
moreover
have "⋀ x. x ∈ seen_T ⟹ f x = empty" unfolding seen_T_def by simp
ultimately
have "ccFromList [x←xs' . x ∉ S] ⊑ G ∧ ccProd (seen) (set xs' - seen_T) ⊑ G"
proof(induction f T xs'' xs' arbitrary: seen seen_T rule: substitute''.induct[case_names Nil Cons])
case Nil thus ?case by simp
next
case (Cons zs f x xs' xs T ys)
let ?seen_T = "if x ∈ T then insert x seen_T else seen_T"
have subset: "- insert x seen_T ⊆ - seen_T" by auto
have subset2: "set xs ∩ - insert x seen_T ⊆ insert x (set xs) ∩ - seen_T" by auto
have subset3: "set zs ∩ - insert x seen_T ⊆ set zs" by auto
have subset4: "set xs ∩ - seen_T ⊆ insert x (set xs) ∩ - seen_T" by auto
have subset5: "set zs ∩ - seen_T ⊆ set zs" by auto
have subset6: "set ys - seen_T ⊆ (set ys - ?seen_T) ∪ {x}" by auto
show ?case
proof(cases "x ∈ seen_T")
assume "x ∈ seen_T"
have [simp]: "f x = empty" using `x ∈ seen_T` Cons.prems by auto
have [simp]: "f_nxt f T x = f" by (auto simp add: f_nxt_def split:if_splits)
have [simp]: "zs = []" using `zs ∈ paths (f x)` by simp
have [simp]: "xs' = xs" using `xs' ∈ xs ⊗ zs` by simp
have [simp]: "x ∈ S" using `x ∈ seen_T` Cons.prems by auto
from Cons.hyps Cons.prems
have "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd seen (set ys - seen_T) ⊑ G"
apply -
apply (rule Cons.IH[where seen_T = seen_T])
apply (auto simp add: join_below_iff Diff_eq)
apply (erule below_trans[OF ccProd_mono[OF order_refl subset4]])
done
thus ?thesis using `x ∈ seen_T` by simp
next
assume "x ∉ seen_T"
have seen_x: "ccProd seen {x} ⊑ G"
using `ccProd seen (set (x # xs) - seen_T) ⊑ G` `x ∉ seen_T`
by (auto simp add: insert_Diff_if ccProd_insert2[where S' = "set xs - seen_T" for xs] join_below_iff)
show ?case
proof(cases "x ∈ S")
case True
from `cc_restr (- seen_T) (ccFromList (x # xs)) ⊑ G`
have "ccProd {x} (set xs - seen_T) ⊑ G" using `x ∉ seen_T` by (auto simp add: join_below_iff Diff_eq)
hence "set xs - seen_T ⊆ ccNeighbors x G" by transfer auto
moreover
from seen_x
have "seen ⊆ ccNeighbors x G" by (simp add: subset_ccNeighbors ccProd_comm)
moreover
have "x ∉ seen" using True `seen ∩ S = {}` by auto
ultimately
have "seen ∪ (set xs ∩ - ?seen_T) ⊆ ccNeighbors x G - {x}∩T" by auto
hence "ccProd (seen ∪ (set xs ∩ - ?seen_T)) (set zs) ⊑ ccProd (ccNeighbors x G - {x}∩T) (set zs)"
by (rule ccProd_mono1)
also
from `x ∈ S` `zs ∈ paths (f x)`
have "… ⊑ G"
by (rule Cons.prems(4))
finally
have "ccProd (seen ∪ (set xs ∩ - ?seen_T)) (set zs) ⊑ G" by this simp
with `x ∈ S` Cons.prems Cons.hyps(1,2)
have "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd (seen) (set ys - ?seen_T) ⊑ G"
apply -
apply (rule Cons.IH[where seen_T = "?seen_T"])
apply (auto simp add: Un_Diff Int_Un_distrib2 Diff_eq f_nxt_def join_below_iff interleave_ccFromList interleave_set ccProd_insert2[where S' = "set xs" for xs]
split: if_splits)
apply (erule below_trans[OF cc_restr_mono1[OF subset]])
apply (rule below_trans[OF cc_restr_below_arg], simp)
apply (erule below_trans[OF ccProd_mono[OF order_refl Int_lower1]])
apply (rule below_trans[OF cc_restr_below_arg], simp)
apply (erule below_trans[OF ccProd_mono[OF order_refl Int_lower1]])
apply (erule below_trans[OF ccProd_mono[OF order_refl subset2]])
apply (erule below_trans[OF ccProd_mono[OF order_refl subset3]])
apply (erule below_trans[OF ccProd_mono[OF order_refl subset4]])
apply (erule below_trans[OF ccProd_mono[OF order_refl subset5]])
done
with `x ∈ S` seen_x `x ∉ seen_T`
show "ccFromList [x←x # ys . x ∉ S] ⊑ G ∧ ccProd seen (set (x#ys) - seen_T) ⊑ G"
apply (auto simp add: insert_Diff_if ccProd_insert2[where S' = "set ys - seen_T" for xs] join_below_iff)
apply (rule below_trans[OF ccProd_mono[OF order_refl subset6]])
apply (subst ccProd_union2)
apply (auto simp add: join_below_iff)
done
next
case False
from False Cons.prems Cons.hyps
have "ccFromList [x←ys . x ∉ S] ⊑ G ∧ ccProd ((insert x seen)) (set ys - seen_T) ⊑ G"
apply -
apply (rule Cons.IH[where seen = "insert x seen" and seen_T = seen_T])
apply (auto simp add: `x ∉ seen_T` Diff_eq ccApprox_both join_below_iff ttree_restr_both interleave_ccFromList insert_Diff_if
simp add: ccProd_insert2[where S' = "set xs ∩ - seen_T" for xs]
simp add: ccProd_insert1[where S' = "seen"])
done
moreover
{
from False this
have "ccProd {x} (set ys - seen_T) ⊑ G"
by (auto simp add: insert_Diff_if ccProd_insert1[where S' = "seen"] join_below_iff)
hence "ccProd {x} {x ∈ set ys - seen_T. x ∉ S} ⊑ G"
by (rule below_trans[rotated, OF _ ccProd_mono2]) auto
also have "{x ∈ set ys - seen_T. x ∉ S} = {x ∈ set ys. x ∉ S}"
using `seen_T ⊆ S` by auto
finally
have "ccProd {x} {x ∈ set ys. x ∉ S} ⊑ G".
}
moreover
note False seen_x
ultimately
show "ccFromList [x←x # ys . x ∉ S] ⊑ G ∧ ccProd (seen) (set (x # ys) - seen_T) ⊑ G"
by (auto simp add: join_below_iff simp add: insert_Diff_if ccProd_insert2[where S' = "set ys - seen_T" for xs] ccProd_insert1[where S' = "seen"])
qed
qed
qed
with `xs = _`
show "ccFromList xs ⊑ G" by simp
qed
inductive_set valid_lists :: "var set ⇒ CoCalls ⇒ var list set"
for S G
where "[] ∈ valid_lists S G"
| "set xs ⊆ ccNeighbors x G ⟹ xs ∈ valid_lists S G ⟹ x ∈ S ⟹ x#xs ∈ valid_lists S G"
inductive_simps valid_lists_simps[simp]: "[] ∈ valid_lists S G" "(x#xs) ∈ valid_lists S G"
inductive_cases vald_lists_ConsE: "(x#xs) ∈ valid_lists S G"
lemma valid_lists_downset_aux:
"xs ∈ valid_lists S CoCalls ⟹ butlast xs ∈ valid_lists S CoCalls"
by (induction xs) (auto dest: in_set_butlastD)
lemma valid_lists_subset: "xs ∈ valid_lists S G ⟹ set xs ⊆ S"
by (induction rule: valid_lists.induct) auto
lemma valid_lists_mono1:
assumes "S ⊆ S'"
shows "valid_lists S G ⊆ valid_lists S' G"
proof
fix xs
assume "xs ∈ valid_lists S G"
thus "xs ∈ valid_lists S' G"
by (induction rule: valid_lists.induct) (auto dest: set_mp[OF assms])
qed
lemma valid_lists_chain1:
assumes "chain Y"
assumes "xs ∈ valid_lists (UNION UNIV Y) G"
shows "∃ i. xs ∈ valid_lists (Y i) G"
proof-
note `chain Y`
moreover
from assms(2)
have "set xs ⊆ UNION UNIV Y" by (rule valid_lists_subset)
moreover
have "finite (set xs)" by simp
ultimately
have "∃i. set xs ⊆ Y i" by (rule finite_subset_chain)
then obtain i where "set xs ⊆ Y i"..
from assms(2) this
have "xs ∈ valid_lists (Y i) G" by (induction rule:valid_lists.induct) auto
thus ?thesis..
qed
lemma valid_lists_chain2:
assumes "chain Y"
assumes "xs ∈ valid_lists S (⨆i. Y i)"
shows "∃ i. xs ∈ valid_lists S (Y i)"
using assms(2)
proof(induction rule:valid_lists.induct[case_names Nil Cons])
case Nil thus ?case by simp
next
case (Cons xs x)
from `chain Y`
have "chain (λ i. ccNeighbors x (Y i))"
apply (rule ch2ch_monofun[OF monofunI, rotated])
unfolding below_set_def
by (rule ccNeighbors_mono)
moreover
from `set xs ⊆ ccNeighbors x (⨆ i. Y i)`
have "set xs ⊆ (⋃ i. ccNeighbors x (Y i))"
by (simp add: lub_set)
moreover
have "finite (set xs)" by simp
ultimately
have "∃i. set xs ⊆ ccNeighbors x (Y i)" by (rule finite_subset_chain)
then obtain i where i: "set xs ⊆ ccNeighbors x (Y i)"..
from Cons.IH
obtain j where j: "xs ∈ valid_lists S (Y j)"..
from i
have "set xs ⊆ ccNeighbors x (Y (max i j))"
by (rule order_trans[OF _ ccNeighbors_mono[OF chain_mono[OF `chain Y` max.cobounded1]]])
moreover
from j
have "xs ∈ valid_lists S (Y (max i j))"
by (induction rule: valid_lists.induct)
(auto del: subsetI elim: order_trans[OF _ ccNeighbors_mono[OF chain_mono[OF `chain Y` max.cobounded2]]])
moreover
note `x ∈ S`
ultimately
have "x # xs ∈ valid_lists S (Y (max i j))" by rule
thus ?case..
qed
lemma valid_lists_cc_restr: "valid_lists S G = valid_lists S (cc_restr S G)"
proof(rule set_eqI)
fix xs
show "(xs ∈ valid_lists S G) = (xs ∈ valid_lists S (cc_restr S G))"
by (induction xs) (auto dest: set_mp[OF valid_lists_subset])
qed
lemma interleave_valid_list:
"xs ∈ ys ⊗ zs ⟹ ys ∈ valid_lists S G ⟹ zs ∈ valid_lists S' G' ⟹ xs ∈ valid_lists (S ∪ S') (G ⊔ (G' ⊔ ccProd S S'))"
proof (induction rule:interleave_induct)
case Nil
show ?case by simp
next
case (left ys zs xs x)
from `x # ys ∈ valid_lists S G`
have "x ∈ S" and "set ys ⊆ ccNeighbors x G" and "ys ∈ valid_lists S G"
by auto
from `xs ∈ ys ⊗ zs`
have "set xs = set ys ∪ set zs" by (rule interleave_set)
with `set ys ⊆ ccNeighbors x G` valid_lists_subset[OF `zs ∈ valid_lists S' G'`]
have "set xs ⊆ ccNeighbors x (G ⊔ (G' ⊔ ccProd S S'))"
by (auto simp add: ccNeighbors_ccProd `x ∈ S`)
moreover
from `ys ∈ valid_lists S G` `zs ∈ valid_lists S' G'`
have "xs ∈ valid_lists (S ∪ S') (G ⊔ (G' ⊔ ccProd S S'))"
by (rule left.IH)
moreover
from `x ∈ S`
have "x ∈ S ∪ S'" by simp
ultimately
show ?case..
next
case (right ys zs xs x)
from `x # zs ∈ valid_lists S' G'`
have "x ∈ S'" and "set zs ⊆ ccNeighbors x G'" and "zs ∈ valid_lists S' G'"
by auto
from `xs ∈ ys ⊗ zs`
have "set xs = set ys ∪ set zs" by (rule interleave_set)
with `set zs ⊆ ccNeighbors x G'` valid_lists_subset[OF `ys ∈ valid_lists S G`]
have "set xs ⊆ ccNeighbors x (G ⊔ (G' ⊔ ccProd S S'))"
by (auto simp add: ccNeighbors_ccProd `x ∈ S'`)
moreover
from `ys ∈ valid_lists S G` `zs ∈ valid_lists S' G'`
have "xs ∈ valid_lists (S ∪ S') (G ⊔ (G' ⊔ ccProd S S'))"
by (rule right.IH)
moreover
from `x ∈ S'`
have "x ∈ S ∪ S'" by simp
ultimately
show ?case..
qed
lemma interleave_valid_list':
"xs ∈ valid_lists (S ∪ S') G ⟹ ∃ ys zs. xs ∈ ys ⊗ zs ∧ ys ∈ valid_lists S G ∧ zs ∈ valid_lists S' G"
proof(induction rule: valid_lists.induct[case_names Nil Cons])
case Nil show ?case by simp
next
case (Cons xs x)
then obtain ys zs where "xs ∈ ys ⊗ zs" "ys ∈ valid_lists S G" "zs ∈ valid_lists S' G" by auto
from `xs ∈ ys ⊗ zs` have "set xs = set ys ∪ set zs" by (rule interleave_set)
with `set xs ⊆ ccNeighbors x G`
have "set ys ⊆ ccNeighbors x G" and "set zs ⊆ ccNeighbors x G" by auto
from `x ∈ S ∪ S'`
show ?case
proof
assume "x ∈ S"
with `set ys ⊆ ccNeighbors x G` `ys ∈ valid_lists S G`
have "x # ys ∈ valid_lists S G"
by rule
moreover
from `xs ∈ ys ⊗ zs`
have "x#xs ∈ x#ys ⊗ zs"..
ultimately
show ?thesis using `zs ∈ valid_lists S' G` by blast
next
assume "x ∈ S'"
with `set zs ⊆ ccNeighbors x G` `zs ∈ valid_lists S' G`
have "x # zs ∈ valid_lists S' G"
by rule
moreover
from `xs ∈ ys ⊗ zs`
have "x#xs ∈ ys ⊗ x#zs"..
ultimately
show ?thesis using `ys ∈ valid_lists S G` by blast
qed
qed
lemma many_calls_valid_list:
"xs ∈ valid_lists {x} (ccProd {x} {x}) ⟹ xs ∈ range (λn. replicate n x)"
by (induction rule: valid_lists.induct) (auto, metis UNIV_I image_iff replicate_Suc)
lemma filter_valid_lists:
"xs ∈ valid_lists S G ⟹ filter P xs ∈ valid_lists {a ∈ S. P a} G"
by (induction rule:valid_lists.induct) auto
lift_definition ccTTree :: "var set ⇒ CoCalls ⇒ var ttree" is "λ S G. valid_lists S G"
by (auto intro: valid_lists_downset_aux)
lemma paths_ccTTree[simp]: "paths (ccTTree S G) = valid_lists S G" by transfer auto
lemma carrier_ccTTree[simp]: "carrier (ccTTree S G) = S"
apply transfer
apply (auto dest: valid_lists_subset)
apply (rule_tac x = "[x]" in bexI)
apply auto
done
lemma valid_lists_ccFromList:
"xs ∈ valid_lists S G ⟹ ccFromList xs ⊑ cc_restr S G"
by (induction rule:valid_lists.induct)
(auto simp add: join_below_iff subset_ccNeighbors ccProd_below_cc_restr elim: set_mp[OF valid_lists_subset])
lemma ccApprox_ccTTree[simp]: "ccApprox (ccTTree S G) = cc_restr S G"
proof (transfer' fixing: S G, rule below_antisym)
show "lub (ccFromList ` valid_lists S G) ⊑ cc_restr S G"
apply (rule is_lub_thelub_ex)
apply (metis coCallsLub_is_lub)
apply (rule is_ubI)
apply clarify
apply (erule valid_lists_ccFromList)
done
next
show "cc_restr S G ⊑ lub (ccFromList ` valid_lists S G)"
proof (rule below_CoCallsI)
fix x y
have "x--y∈(ccFromList [y,x])" by simp
moreover
assume "x--y∈(cc_restr S G)"
hence "[y,x] ∈ valid_lists S G" by (auto simp add: elem_ccNeighbors)
ultimately
show "x--y∈(lub (ccFromList ` valid_lists S G))"
by (rule in_CoCallsLubI[OF _ imageI])
qed
qed
lemma below_ccTTreeI:
assumes "carrier t ⊆ S" and "ccApprox t ⊑ G"
shows "t ⊑ ccTTree S G"
unfolding paths_mono_iff[symmetric] below_set_def
proof
fix xs
assume "xs ∈ paths t"
with assms
have "xs ∈ valid_lists S G"
proof(induction xs arbitrary : t)
case Nil thus ?case by simp
next
case (Cons x xs)
from `x # xs ∈ paths t`
have "possible t x" and "xs ∈ paths (nxt t x)" by (auto simp add: Cons_path)
have "ccProd {x} (set xs) ⊑ ccFromList (x # xs)" by simp
also
from `x # xs ∈ paths t`
have "… ⊑ ccApprox t"
by (rule ccFromList_below_ccApprox)
also
note `ccApprox t ⊑ G`
finally
have "ccProd {x} (set xs) ⊑ G" by this simp_all
hence "set xs ⊆ ccNeighbors x G" unfolding subset_ccNeighbors.
moreover
have "xs ∈ valid_lists S G"
proof(rule Cons.IH)
show "xs ∈ paths (nxt t x)" by fact
next
from `carrier t ⊆ S`
show "carrier (nxt t x) ⊆ S"
by (rule order_trans[OF carrier_nxt_subset])
next
from `ccApprox t ⊑ G`
show "ccApprox (nxt t x) ⊑ G"
by (rule below_trans[OF ccApprox_nxt_below])
qed
moreover
from `carrier t ⊆ S` and `possible t x`
have "x ∈ S" by (rule carrier_possible_subset)
ultimately
show ?case..
qed
thus "xs ∈ paths (ccTTree S G)" by (metis paths_ccTTree)
qed
lemma ccTTree_mono1:
"S ⊆ S' ⟹ ccTTree S G ⊑ ccTTree S' G"
by (rule below_ccTTreeI) (auto simp add: cc_restr_below_arg)
lemma cont_ccTTree1:
"cont (λ S. ccTTree S G)"
apply (rule contI2)
apply (rule monofunI)
apply (erule ccTTree_mono1[folded below_set_def])
apply (rule ttree_belowI)
apply (simp add: paths_Either lub_set lub_is_either)
apply (drule (1) valid_lists_chain1[rotated])
apply simp
done
lemma ccTTree_mono2:
"G ⊑ G' ⟹ ccTTree S G ⊑ ccTTree S G'"
apply (rule ttree_belowI)
apply simp
apply (induct_tac rule:valid_lists.induct) apply assumption
apply simp
apply simp
apply (erule (1) order_trans[OF _ ccNeighbors_mono])
done
lemma ccTTree_mono:
"S ⊆ S' ⟹ G ⊑ G' ⟹ ccTTree S G ⊑ ccTTree S' G'"
by (metis below_trans[OF ccTTree_mono1 ccTTree_mono2])
lemma cont_ccTTree2:
"cont (ccTTree S)"
apply (rule contI2)
apply (rule monofunI)
apply (erule ccTTree_mono2)
apply (rule ttree_belowI)
apply (simp add: paths_Either lub_set lub_is_either)
apply (drule (1) valid_lists_chain2)
apply simp
done
lemmas cont_ccTTree = cont_compose2[where c = ccTTree, OF cont_ccTTree1 cont_ccTTree2, simp, cont2cont]
lemma ccTTree_below_singleI:
assumes "S ∩ S' = {}"
shows "ccTTree S G ⊑ singles S'"
proof-
{
fix xs x
assume "xs ∈ valid_lists S G" and "x ∈ S'"
from this assms
have "length [x'←xs . x' = x] ≤ Suc 0"
by(induction rule: valid_lists.induct[case_names Nil Cons]) auto
}
thus ?thesis by transfer auto
qed
lemma ccTTree_cc_restr: "ccTTree S G = ccTTree S (cc_restr S G)"
by transfer' (rule valid_lists_cc_restr)
lemma ccTTree_cong_below: "cc_restr S G ⊑ cc_restr S G' ⟹ ccTTree S G ⊑ ccTTree S G'"
by (metis ccTTree_mono2 ccTTree_cc_restr)
lemma ccTTree_cong: "cc_restr S G = cc_restr S G' ⟹ ccTTree S G = ccTTree S G'"
by (metis ccTTree_cc_restr)
lemma either_ccTTree:
"ccTTree S G ⊕⊕ ccTTree S' G' ⊑ ccTTree (S ∪ S') (G ⊔ G')"
by (auto intro!: either_belowI ccTTree_mono)
lemma interleave_ccTTree:
"ccTTree S G ⊗⊗ ccTTree S' G' ⊑ ccTTree (S ∪ S') (G ⊔ G' ⊔ ccProd S S')"
by transfer' (auto, erule (2) interleave_valid_list)
lemma interleave_ccTTree':
"ccTTree (S ∪ S') G ⊑ ccTTree S G ⊗⊗ ccTTree S' G"
by transfer' (auto dest!: interleave_valid_list')
lemma many_calls_ccTTree:
shows "many_calls x = ccTTree {x} (ccProd {x} {x})"
apply(transfer')
apply (auto intro: many_calls_valid_list)
apply (induct_tac n)
apply (auto simp add: ccNeighbors_ccProd)
done
lemma filter_valid_lists':
"xs ∈ valid_lists {x' ∈ S. P x'} G ⟹ xs ∈ filter P ` valid_lists S G"
proof (induction xs )
case Nil thus ?case by auto (metis filter.simps(1) image_iff valid_lists_simps(1))
next
case (Cons x xs)
from Cons.prems
have "set xs ⊆ ccNeighbors x G" and "xs ∈ valid_lists {x' ∈ S. P x'} G" and "x ∈ S" and "P x" by auto
from this(2) have "set xs ⊆ {x' ∈ S. P x'}" by (rule valid_lists_subset)
hence "∀x ∈ set xs. P x" by auto
hence [simp]: "filter P xs = xs" by (rule filter_True)
from Cons.IH[OF `xs ∈ _`]
have "xs ∈ filter P ` valid_lists S G".
from `xs ∈ valid_lists {x' ∈ S. P x'} G`
have "xs ∈ valid_lists S G" by (rule set_mp[OF valid_lists_mono1, rotated]) auto
from `set xs ⊆ ccNeighbors x G` this `x ∈ S`
have "x # xs ∈ valid_lists S G" by rule
hence "filter P (x # xs) ∈ filter P ` valid_lists S G" by (rule imageI)
thus ?case using `P x` `filter P xs =xs` by simp
qed
lemma without_ccTTree[simp]:
"without x (ccTTree S G) = ccTTree (S - {x}) G"
by (transfer' fixing: x) (auto dest: filter_valid_lists' filter_valid_lists[where P = "(λ x'. x'≠ x)"] simp add: set_diff_eq)
lemma ttree_restr_ccTTree[simp]:
"ttree_restr S' (ccTTree S G) = ccTTree (S ∩ S') G"
by (transfer' fixing: S') (auto dest: filter_valid_lists' filter_valid_lists[where P = "(λ x'. x' ∈ S')"] simp add:Int_def)
lemma repeatable_ccTTree_ccSquare: "S ⊆ S' ⟹ repeatable (ccTTree S (ccSquare S'))"
unfolding repeatable_def
by transfer (auto simp add:ccNeighbors_ccSquare dest: set_mp[OF valid_lists_subset])
text {* An alternative definition *}
inductive valid_lists' :: "var set ⇒ CoCalls ⇒ var set ⇒ var list ⇒ bool"
for S G
where "valid_lists' S G prefix []"
| "prefix ⊆ ccNeighbors x G ⟹ valid_lists' S G (insert x prefix) xs ⟹ x ∈ S ⟹ valid_lists' S G prefix (x#xs)"
inductive_simps valid_lists'_simps[simp]: "valid_lists' S G prefix []" "valid_lists' S G prefix (x#xs)"
inductive_cases vald_lists'_ConsE: "valid_lists' S G prefix (x#xs)"
lemma valid_lists_valid_lists':
"xs ∈ valid_lists S G ⟹ ccProd prefix (set xs) ⊑ G ⟹ valid_lists' S G prefix xs"
proof(induction arbitrary: prefix rule: valid_lists.induct[case_names Nil Cons])
case Nil thus ?case by simp
next
case (Cons xs x)
from Cons.prems Cons.hyps Cons.IH[where prefix = "insert x prefix"]
show ?case
by (auto simp add: insert_is_Un[where A = "set xs"] insert_is_Un[where A = prefix]
join_below_iff subset_ccNeighbors elem_ccNeighbors ccProd_comm simp del: Un_insert_left )
qed
lemma valid_lists'_valid_lists_aux:
"valid_lists' S G prefix xs ⟹ x ∈ prefix ⟹ ccProd (set xs) {x} ⊑ G"
proof(induction rule: valid_lists'.induct[case_names Nil Cons])
case Nil thus ?case by simp
next
case (Cons prefix x xs)
thus ?case
apply (auto simp add: ccProd_insert2[where S' = prefix] ccProd_insert1[where S' = "set xs"] join_below_iff subset_ccNeighbors)
by (metis Cons.hyps(1) dual_order.trans empty_subsetI insert_subset subset_ccNeighbors)
qed
lemma valid_lists'_valid_lists:
"valid_lists' S G prefix xs ⟹ xs ∈ valid_lists S G"
proof(induction rule: valid_lists'.induct[case_names Nil Cons])
case Nil thus ?case by simp
next
case (Cons prefix x xs)
thus ?case
by (auto simp add: insert_is_Un[where A = "set xs"] insert_is_Un[where A = prefix]
join_below_iff subset_ccNeighbors elem_ccNeighbors ccProd_comm simp del: Un_insert_left
intro: valid_lists'_valid_lists_aux)
qed
text {* Yet another definition *}
lemma valid_lists_characterization:
"xs ∈ valid_lists S G ⟷ set xs ⊆ S ∧ (∀n. ccProd (set (take n xs)) (set (drop n xs)) ⊑ G)"
proof(safe)
fix x
assume "xs ∈ valid_lists S G"
from valid_lists_subset[OF this]
show "x ∈ set xs ⟹ x ∈ S" by auto
next
fix n
assume "xs ∈ valid_lists S G"
thus "ccProd (set (take n xs)) (set (drop n xs)) ⊑ G"
proof(induction arbitrary: n rule: valid_lists.induct[case_names Nil Cons])
case Nil thus ?case by simp
next
case (Cons xs x)
show ?case
proof(cases n)
case 0 thus ?thesis by simp
next
case (Suc n)
with Cons.hyps Cons.IH[where n = n]
show ?thesis
apply (auto simp add: ccProd_insert1[where S' = "set xs" for xs] join_below_iff subset_ccNeighbors)
by (metis dual_order.trans set_drop_subset subset_ccNeighbors)
qed
qed
next
assume "set xs ⊆ S"
and "∀ n. ccProd (set (take n xs)) (set (drop n xs)) ⊑ G"
thus "xs ∈ valid_lists S G"
proof (induction xs)
case Nil thus ?case by simp
next
case (Cons x xs)
from `∀n. ccProd (set (take n (x # xs))) (set (drop n (x # xs))) ⊑ G`
have "∀n. ccProd (set (take n xs)) (set (drop n xs)) ⊑ G"
by -(rule, erule_tac x = "Suc n" in allE, auto simp add: ccProd_insert1[where S' = "set xs" for xs] join_below_iff)
from Cons.prems Cons.IH[OF _ this]
have "xs ∈ valid_lists S G" by auto
with Cons.prems(1) spec[OF `∀n. ccProd (set (take n (x # xs))) (set (drop n (x # xs))) ⊑ G`, where x = 1]
show ?case by (simp add: subset_ccNeighbors)
qed
qed
end