theory "CoCallGraph-FTree"
imports CoCallGraph "FTree-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 ftree \ 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_ftree_restr_nxt_below:
"ccApprox (ftree_restr S (nxt t x)) \ ccApprox (ftree_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_ftree_restr[simp]: "ccApprox (ftree_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 (FTree.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 (ftree_restr (-S) (substitute f T t)) \ G"
proof(rule ccApprox_belowI)
fix xs
def seen \ "{} :: var set"
assume "xs \ paths (ftree_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 ftree_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 (ftree_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 (ftree_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 "cc_restr (-seen_T) (ccFromList xs'') \ G" unfolding seen_T_def by simp
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 (auto simp add: insert_Diff_if ccProd_insert2[where S' = "set xs - seen_T" for xs])
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 \