theory Indirections
imports Terms "Nominal-Utils" "AList-Utils-Nominal" "FMap-Heap" "FMap-Nominal"
begin
type_synonym indirections = "(var \ var) list "
class resolvable =
fixes resolve :: "'a \ indirections \ 'a" (infixl "\" 60)
assumes resolve_append[simp]: "x \ (is'@is) = x \ is' \ is"
assumes resolve_Nil[simp]: "x \ [] = x"
class resolvable_eqvt = resolvable + pt +
assumes resolve_eqvt: "p \ (x \ is) = (p \ x) \ (p \ is)"
assumes resolve_fresh_noop[simp]: "atom a \ x \ x \ ((a, b) # is) = x \ is"
declare resolve_eqvt[eqvt]
instantiation list :: (resolvable) resolvable
begin
definition resolve_list :: "'a list \ indirections \ 'a list"
where "m \ is = map (\x. x \ is) m"
lemma resolve_list_Nil[simp]: "[] \ is = []"
unfolding resolve_list_def by simp
lemma resolve_list_Cons[simp]: "(x # xs) \ is = (x \ is) # (xs \ is)"
unfolding resolve_list_def by simp
instance
apply default
apply (induct_tac "x", auto)
apply (simp add: resolve_list_def)
done
end
instance list :: (resolvable_eqvt) resolvable_eqvt
apply default
apply (simp add: resolve_list_def)
apply (simp add: resolve_list_def fresh_list_elem)
done
instantiation var :: resolvable_eqvt
begin
fun resolve_var :: "var \ indirections \ var" where
"v \ [] = (v::var)"
| "v \ ((x,y)#is) = v[x ::v= y] \ is"
lemma resolve_var_append: "(v::var) \ (is'@is) = v \ is' \ is"
by (induct "is'" arbitrary: v) auto
instance
apply default
apply (rule resolve_var_append)
apply (simp)
apply (induct_tac x "is" rule:resolve_var.induct, simp+)
done
end
lemma resove_var_noop[simp]: "x \ heapVars is \ x \ is = x"
by (induct x "is" rule: resolve_var.induct) auto
instantiation exp :: resolvable_eqvt
begin
fun resolve_exp :: "exp \ indirections \ exp" where
"e \ [] = (e::exp)"
| "e \ ((x,y)#is) = (e[x ::= y]) \ is"
lemma resolve_exp_append: "(e::exp) \ (is'@is) = e \ is' \ is"
by (induct "is'" arbitrary: e) auto
lemma resolve_exp_eqvt[eqvt]: "p \ ((e::exp) \ is) = (p \ e) \ (p \ is)"
by (induction e "is" rule:resolve_exp.induct) simp+
instance
apply default
apply (rule resolve_exp_append)
apply simp
apply (rule resolve_exp_eqvt)
apply (simp add: subst_fresh_noop)
done
end
instantiation assn :: resolvable_eqvt
begin
fun resolve_assn :: "assn \ indirections \ assn" where
"as \ [] = (as::assn)"
| "as \ ((x,y)#is) = (as[x ::a= y]) \ is"
lemma resolve_assn_append: "(as::assn) \ (is'@is) = as\ is' \ is"
by (induct "is'" arbitrary: as) auto
lemma resolve_assn_eqvt[eqvt]: "p \ ((as::assn) \ is) = (p \ as) \ (p \ is)"
by (induction as "is" rule:resolve_assn.induct) simp+
instance
apply default
apply (rule resolve_assn_append)
apply simp
apply (rule resolve_assn_eqvt)
apply (simp add: subst_assn_fresh_noop)
done
end
lemma resolve_var_fresh: "atom ` heapVars is \* v \ (v::var) \ is = v"
by (induct "is" rule:resolve_var.induct)(auto simp add: fresh_star_def fresh_def )
lemma resolve_var_fresh'[simp]: "atom v \ is \ (v::var) \ is = v"
by (induct "is" rule:resolve_var.induct)(auto simp add: fresh_Cons fresh_Pair)
lemma resolve_var_list_fresh: "atom ` heapVars is \* L \ (L::var list) \ is = L"
by (induct L) (auto simp add: fresh_star_list resolve_var_fresh)
lemma resolveExp_Lam: "atom x \ is \ (Lam [x]. e) \ is = Lam [x]. (e \ is)"
apply (induction "is" arbitrary: e)
apply simp
apply (auto simp add: fresh_Cons)
done
lemma resolveExp_App: "App e x \ is = App (e \ is) (x \ is)"
by (induction "is" arbitrary: e x) auto
lemma resolveExp_Var: "Var x \ is = Var (x \ is)"
by (induction "is" arbitrary: x) auto
lemma resolveExp_Let: "set (bn as) \* is \ (Let as e) \ is = Let (as \ is) (e \ is)"
by (induction "is" arbitrary: as e) (auto simp add: fresh_star_list)
lemma resolve_assn_ANil[simp]: "ANil \ is = ANil"
by (induction "is") auto
lemma resolve_assn_ACons[simp]: "x \ heapVars is \ (ACons x e as) \ is = (ACons (x \ is) (e \ is) (as \ is))"
by (induction "is" arbitrary: x e as) auto
definition resolveHeap' :: "Heap \ indirections \ Heap" (infixl "\\<^sub>H" 60) where
"\ \\<^sub>H is = fmap_map (\e. e \ is) (\ f|` (- heapVars is))"
lemma resolveHeap'_empty[simp]: "f\ \\<^sub>H is = f\"
unfolding resolveHeap'_def by auto
lemma resolveHeap'_Nil[simp]: "\ \\<^sub>H [] = \"
unfolding resolveHeap'_def by auto
lemma resolveHeap'fdom[simp]:
"fdom (\ \\<^sub>H is) = fdom \ - heapVars is"
unfolding resolveHeap'_def by auto
lemma resolveHeap'_fmap_upd[simp]: "x \ heapVars is \ (\(x f\ e)) \\<^sub>H is = \ \\<^sub>H is"
unfolding resolveHeap'_def by auto
lemma resolveHeap'_fmap_upd_other[simp]: "x \ heapVars is \ (\(x f\ e)) \\<^sub>H is = (\ \\<^sub>H is)(x f\ e \ is)"
unfolding resolveHeap'_def by simp
lemma resolveHeap'_fun_merge[simp]: "fdom \ \ heapVars is = {} \ (\ f++ \) \\<^sub>H is = (\ \\<^sub>H is) f++ (\ \\<^sub>H is)"
by (induction \ rule:fmap_induct) (auto simp add: fun_merge_upd)
lemma resolveHeap'_fmap_copy[simp]: "x \ heapVars is \ (fmap_copy \ y x) \\<^sub>H is = \ \\<^sub>H is"
unfolding resolveHeap'_def by simp
lemma resolveHeap'_fmap_copy_other[simp]: "x \ heapVars is \ y \ heapVars is \ (fmap_copy \ y x) \\<^sub>H is = fmap_copy (\ \\<^sub>H is) y x"
unfolding resolveHeap'_def by auto
lemma resolveHeap'_fresh_Cons[simp]: "atom y \ \ \ \ \\<^sub>H (y,x)#is = \ \\<^sub>H is"
unfolding resolveHeap'_def
by (rule fmap_map_cong[OF resolve_fresh_noop])
(auto dest: set_mp[OF fran_fmap_restr_subset] intro: fmap_restr_cong simp add: fresh_def supp_fmap supp_set_elem_finite)
lemma resolveHeap'_eqvt[eqvt]: "p \ resolveHeap' \ is = resolveHeap' (p \ \) (p \ is)"
unfolding resolveHeap'_def
by (simp add: fmap_restr_eqvt Compl_eqvt)
fun resolveHeapOne :: "heap \ var \ var \ heap" where
"resolveHeapOne [] _ _ = []"
| "resolveHeapOne ((x,e)#\) a b = (if a = x then (resolveHeapOne \ a b) else (x, e[a ::= b]) # (resolveHeapOne \ a b))"
lemma resolveHeapOneFresh: "atom y \ x \ atom y \ resolveHeapOne \ y x"
by (induction \ y x rule:resolveHeapOne.induct)
(auto simp add: fresh_Nil fresh_Cons fresh_Pair)
lemma resolveHeapOne_eqvt[eqvt]: "p \ resolveHeapOne \ a b = resolveHeapOne (p \ \) (p \ a) (p \ b)"
by (induction \ a b rule:resolveHeapOne.induct) simp_all
lemma resolveHeapOneNoop[simp]: "atom y \ \ \ resolveHeapOne \ y x = \"
by (induction \ y x rule:resolveHeapOne.induct)
(auto simp add: fresh_Nil fresh_Cons fresh_Pair subst_fresh_noop)
fun resolveHeap :: "heap \ indirections \ heap" (infixl "\\<^sub>h" 60) where
"\ \\<^sub>h [] = \"
| "\ \\<^sub>h ((a,b)#is) = resolveHeapOne \ a b \\<^sub>h is"
lemma resolveHeapNil[simp]: "[] \\<^sub>h is = []"
by (induct "[]::heap" "is" rule:resolveHeap.induct) simp_all
lemma resolveHeapConsRemoved[simp]: "x \ heapVars is \ (x,e)#\ \\<^sub>h is = \ \\<^sub>h is"
apply (induct "(x,e)#\" "is" arbitrary: x e \ rule:resolveHeap.induct)
apply simp_all
apply (erule disjE)
apply auto
done
lemma resolveHeapCons[simp]: "x \ heapVars is \ (x,e)#\ \\<^sub>h is = (x, e \ is) # (\ \\<^sub>h is)"
apply (induct "(x,e)#\" "is" arbitrary: x e \ rule:resolveHeap.induct)
apply simp_all
done
lemma resolveHeapConsRemoved'[simp]: "x \ heapVars is \ (y,z)#(x,e)#\ \\<^sub>h is = ((y,z)#\) \\<^sub>h is"
apply (cases "y \ heapVars is")
apply simp_all
done
lemma resolveHeapOneDelete[simp]: "resolveHeapOne (delete x \) a b = delete x (resolveHeapOne \ a b)"
by (induct \ a b rule:resolveHeapOne.induct) auto
lemma resolveHeapDelete[simp]: "delete x \ \\<^sub>h is = delete x (\ \\<^sub>h is)"
by (induct \ "is" arbitrary: x rule:resolveHeap.induct) simp_all
lemma resolveHeapOneHeapVars[simp]:
"heapVars (resolveHeapOne \ a b) = heapVars \ - {a}"
by (induct \ a b rule:resolveHeapOne.induct) auto
lemma resolveHeapHeapVars[simp]:
"heapVars (\ \\<^sub>h is) = heapVars \ - heapVars is"
by (induct \ "is" rule:resolveHeap.induct) auto
lemma resolveHeapOneDeleted[simp]:
"delete a (resolveHeapOne \ a b \\<^sub>h is) = resolveHeapOne \ a b \\<^sub>h is"
by (rule delete_no_there, simp)
lemma resolveHeapDeleted[simp]: "x \ heapVars is \ delete x (\ \\<^sub>h is) = \ \\<^sub>h is"
by (rule delete_no_there, simp)
lemma resolveHeap_eqvt[eqvt]: "p \ resolveHeap \ is = resolveHeap (p \ \) (p \ is)"
by(induction \ "is" rule:resolveHeap.induct) simp_all
lemma resolveHeap_append[simp]: "\ \\<^sub>h (is'@is) = \