Theory SestoftConf

theory SestoftConf
imports "Terms" "Substitution"
begin

datatype stack_elem = Alts exp exp | Arg var | Upd var | Dummy var

instantiation stack_elem :: pt
begin
definition  "π ∙ x = (case x of (Alts e1 e2) ⇒ Alts (π ∙ e1) (π ∙ e2) | (Arg v) ⇒ Arg (π ∙ v) | (Upd v) ⇒ Upd (π ∙ v) | (Dummy v) ⇒ Dummy (π ∙ v))"
instance
  by standard (auto simp add: permute_stack_elem_def split:stack_elem.split)
end

lemma Alts_eqvt[eqvt]: "π ∙ (Alts e1 e2) = Alts (π ∙ e1) (π ∙ e2)"
  and Arg_eqvt[eqvt]: "π ∙ (Arg v) = Arg (π ∙ v)"
  and Upd_eqvt[eqvt]: "π ∙ (Upd v) = Upd (π ∙ v)"
  and Dummy_eqvt[eqvt]: "π ∙ (Dummy v) = Dummy (π ∙ v)"
  by (auto simp add: permute_stack_elem_def split:stack_elem.split)

lemma supp_Alts[simp]: "supp (Alts e1 e2) = supp e1 ∪ supp e2" unfolding supp_def by (auto simp add: Collect_imp_eq Collect_neg_eq)
lemma supp_Arg[simp]: "supp (Arg v) = supp v"  unfolding supp_def by auto
lemma supp_Upd[simp]: "supp (Upd v) = supp v"  unfolding supp_def by auto
lemma supp_Dummy[simp]: "supp (Dummy v) = supp v"  unfolding supp_def by auto
lemma fresh_Alts[simp]: "a ♯ Alts e1 e2 = (a ♯ e1 ∧ a ♯ e2)" unfolding fresh_def by auto
lemma fresh_star_Alts[simp]: "a ♯* Alts e1 e2 = (a ♯* e1 ∧ a ♯* e2)" unfolding fresh_star_def by auto
lemma fresh_Arg[simp]: "a ♯ Arg v = a ♯ v" unfolding fresh_def by auto
lemma fresh_Upd[simp]: "a ♯ Upd v = a ♯ v" unfolding fresh_def by auto
lemma fresh_Dummy[simp]: "a ♯ Dummy v = a ♯ v" unfolding fresh_def by auto
lemma fv_Alts[simp]: "fv (Alts e1 e2) = fv e1 ∪ fv e2"  unfolding fv_def by auto
lemma fv_Arg[simp]: "fv (Arg v) = fv v"  unfolding fv_def by auto
lemma fv_Upd[simp]: "fv (Upd v) = fv v"  unfolding fv_def by auto
lemma fv_Dummy[simp]: "fv (Dummy v) = fv v"  unfolding fv_def by auto

instance stack_elem :: fs
  by standard (case_tac x, auto simp add: finite_supp)

type_synonym stack = "stack_elem list"

fun ap :: "stack ⇒ var set" where
  "ap [] = {}"
| "ap (Alts e1 e2 # S) = ap S"
| "ap (Arg x # S) = insert x (ap S)"
| "ap (Upd x # S) = ap S"
| "ap (Dummy x # S) = ap S"
fun upds :: "stack ⇒ var set" where
  "upds [] = {}"
| "upds (Alts e1 e2 # S) = upds S"
| "upds (Upd x # S) = insert x (upds S)"
| "upds (Arg x # S) = upds S"
| "upds (Dummy x # S) = upds S"
fun dummies :: "stack ⇒ var set" where
  "dummies [] = {}"
| "dummies (Alts e1 e2 # S) = dummies S"
| "dummies (Upd x # S) = dummies S"
| "dummies (Arg x # S) = dummies S"
| "dummies (Dummy x # S) = insert x (dummies S)"
fun flattn :: "stack ⇒ var list" where
  "flattn [] = []"
| "flattn (Alts e1 e2 # S) = fv_list e1 @ fv_list e2 @ flattn S"
| "flattn (Upd x # S) = x # flattn S"
| "flattn (Arg x # S) = x # flattn S"
| "flattn (Dummy x # S) = x # flattn S"
fun upds_list :: "stack ⇒ var list" where
  "upds_list [] = []"
| "upds_list (Alts e1 e2 # S) = upds_list S"
| "upds_list (Upd x # S) = x # upds_list S"
| "upds_list (Arg x # S) = upds_list S"
| "upds_list (Dummy x # S) = upds_list S"

lemma set_upds_list[simp]:
  "set (upds_list S) = upds S"
  by (induction S rule: upds_list.induct) auto

lemma ups_fv_subset: "upds S ⊆ fv S"
  by (induction S rule: upds.induct) auto
lemma fresh_distinct_ups: "atom ` V ♯* S ⟹ V ∩ upds S = {}"
   by (auto dest!: fresh_distinct_fv set_mp[OF ups_fv_subset])
lemma ap_fv_subset: "ap S ⊆ fv S"
  by (induction S rule: upds.induct) auto
lemma dummies_fv_subset: "dummies S ⊆ fv S"
  by (induction S rule: dummies.induct) auto

lemma fresh_flattn[simp]: "atom (a::var) ♯ flattn S ⟷ atom a ♯ S"
  by (induction S rule:flattn.induct) (auto simp add: fresh_Nil fresh_Cons fresh_append fresh_fv[OF finite_fv])
lemma fresh_star_flattn[simp]: "atom ` (as:: var set) ♯* flattn S ⟷ atom ` as ♯* S"
  by (auto simp add: fresh_star_def)
lemma fresh_upds_list[simp]: "atom a ♯ S ⟹ atom (a::var) ♯ upds_list S"
  by (induction S rule:upds_list.induct) (auto simp add: fresh_Nil fresh_Cons fresh_append fresh_fv[OF finite_fv])
lemma fresh_star_upds_list[simp]: "atom ` (as:: var set) ♯* S ⟹ atom ` (as:: var set) ♯* upds_list S"
  by (auto simp add: fresh_star_def)

lemma upds_append[simp]: "upds (S@S') = upds S ∪ upds S'"
  by (induction S rule: upds.induct) auto
lemma upds_map_Dummy[simp]: "upds (map Dummy l) = {}"
  by (induction l) auto

lemma upds_list_append[simp]: "upds_list (S@S') = upds_list S @ upds_list S'"
  by (induction S rule: upds.induct) auto
lemma upds_list_map_Dummy[simp]: "upds_list (map Dummy l) = []"
  by (induction l) auto

lemma dummies_append[simp]: "dummies (S@S') = dummies S ∪ dummies S'"
  by (induction S rule: dummies.induct) auto
lemma dummies_map_Dummy[simp]: "dummies (map Dummy l) = set l"
  by (induction l) auto

lemma map_Dummy_inj[simp]: "map Dummy l = map Dummy l' ⟷ l = l'"
  apply (induction l arbitrary: l')
  apply (case_tac [!] l')
  apply auto
  done

type_synonym conf = "(heap × exp × stack)"

inductive boring_step where
  "isVal e ⟹ boring_step (Γ, e, Upd x # S)"


fun restr_stack :: "var set ⇒ stack ⇒ stack"
  where "restr_stack V [] = []"
      | "restr_stack V (Alts e1 e2 # S) = Alts e1 e2 # restr_stack V S"
      | "restr_stack V (Arg x # S) = Arg x # restr_stack V S"
      | "restr_stack V (Upd x # S) = (if x ∈ V then Upd x # restr_stack V S else restr_stack V S)"
      | "restr_stack V (Dummy x # S) = Dummy x # restr_stack V S"

lemma restr_stack_cong:
  "(⋀ x. x ∈ upds S ⟹ x ∈ V ⟷ x ∈ V') ⟹ restr_stack V S = restr_stack V' S"
  by (induction V S rule: restr_stack.induct) auto

lemma upds_restr_stack[simp]: "upds (restr_stack V S) = upds S ∩ V"
  by (induction V S rule: restr_stack.induct) auto

lemma fresh_star_restict_stack[intro]:
  "a ♯* S ⟹ a ♯* restr_stack V S"
  by (induction V S rule: restr_stack.induct) (auto simp add: fresh_star_Cons)

lemma restr_stack_restr_stack[simp]:
  "restr_stack V (restr_stack V' S) = restr_stack (V ∩ V') S"
  by (induction V S rule: restr_stack.induct) auto

lemma Upd_eq_restr_stackD:
  assumes "Upd x # S = restr_stack V S'"
  shows "x ∈ V"
  using arg_cong[where f = upds, OF assms]
  by auto
lemma Upd_eq_restr_stackD2:
  assumes "restr_stack V S' = Upd x # S"
  shows "x ∈ V"
  using arg_cong[where f = upds, OF assms]
  by auto


lemma restr_stack_noop[simp]:
  "restr_stack V S = S ⟷ upds S ⊆ V"
  by (induction V S rule: restr_stack.induct)
     (auto dest: Upd_eq_restr_stackD2)
  

subsubsection {* Invariants of the semantics *}

inductive invariant :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ bool"
  where "(⋀ x y. rel x y ⟹ I x ⟹ I y) ⟹ invariant rel I"

lemmas invariant.intros[case_names step]

lemma invariantE:
  "invariant rel I ⟹ rel x y ⟹ I x ⟹ I y" by (auto elim: invariant.cases)

lemma invariant_starE:
  "rtranclp rel x y ⟹ invariant rel I ⟹  I x ⟹ I y"
  by (induction rule: rtranclp.induct) (auto elim: invariantE)

lemma invariant_True:
  "invariant rel (λ _. True)"
by (auto intro: invariant.intros)

lemma invariant_conj:
  "invariant rel I1 ⟹ invariant rel I2 ⟹ invariant rel (λ x. I1 x ∧ I2 x)"
by (auto simp add: invariant.simps)


lemma rtranclp_invariant_induct[consumes 3, case_names base step]:
  assumes "r⇧*⇧* a b"
  assumes "invariant r I"
  assumes "I a"
  assumes "P a"
  assumes "(⋀y z. r⇧*⇧* a y ⟹ r y z ⟹ I y ⟹ I z ⟹ P y ⟹ P z)"
  shows "P b"
proof-
  from assms(1,3)
  have "P b" and "I b"
  proof(induction)
    case base
    from `P a` show "P a".
    from `I a` show "I a".
  next
    case (step y z)
    with `I a` have "P y" and "I y" by auto

    from assms(2) `r y z` `I y`
    show "I z" by (rule invariantE)

    from `r⇧*⇧* a y` `r y z` `I y` `I z` `P y`
    show "P z" by (rule assms(5))
  qed
  thus "P b" by-
qed


fun closed :: "conf ⇒ bool"
  where "closed (Γ, e, S) ⟷ fv (Γ, e, S) ⊆ domA Γ ∪ upds S"

fun heap_upds_ok where "heap_upds_ok (Γ,S) ⟷ domA Γ ∩ upds S = {} ∧ distinct (upds_list S)"

abbreviation heap_upds_ok_conf :: "conf ⇒ bool"
  where "heap_upds_ok_conf c ≡ heap_upds_ok (fst c, snd (snd c))"

lemma heap_upds_okE: "heap_upds_ok (Γ, S) ⟹ x ∈ domA Γ ⟹ x ∉ upds S"
  by auto

lemma heap_upds_ok_Nil[simp]: "heap_upds_ok (Γ, [])" by auto
lemma heap_upds_ok_app1: "heap_upds_ok (Γ, S) ⟹ heap_upds_ok (Γ,Arg x # S)" by auto
lemma heap_upds_ok_app2: "heap_upds_ok (Γ, Arg x # S) ⟹ heap_upds_ok (Γ, S)" by auto
lemma heap_upds_ok_alts1: "heap_upds_ok (Γ, S) ⟹ heap_upds_ok (Γ,Alts e1 e2 # S)" by auto
lemma heap_upds_ok_alts2: "heap_upds_ok (Γ, Alts e1 e2 # S) ⟹ heap_upds_ok (Γ, S)" by auto

lemma heap_upds_ok_append:
  assumes "domA Δ ∩ upds S = {}"
  assumes "heap_upds_ok (Γ,S)"
  shows "heap_upds_ok (Δ@Γ, S)"
  using assms
  unfolding heap_upds_ok.simps
  by auto

lemma heap_upds_ok_let:
  assumes "atom ` domA Δ ♯* S"
  assumes "heap_upds_ok (Γ, S)"
  shows "heap_upds_ok (Δ @ Γ, S)"
using assms(2) fresh_distinct_fv[OF assms(1)]
by (auto intro: heap_upds_ok_append dest: set_mp[OF ups_fv_subset])

lemma heap_upds_ok_to_stack:
  "x ∈ domA Γ ⟹ heap_upds_ok (Γ, S) ⟹ heap_upds_ok (delete x Γ, Upd x #S)"
  by (auto)

lemma heap_upds_ok_to_stack':
  "map_of Γ x = Some e ⟹ heap_upds_ok (Γ, S) ⟹ heap_upds_ok (delete x Γ, Upd x #S)"
  by (metis Domain.DomainI domA_def fst_eq_Domain heap_upds_ok_to_stack map_of_SomeD)

lemma heap_upds_ok_delete:
  "heap_upds_ok (Γ, S) ⟹ heap_upds_ok (delete x Γ, S)"
  by auto

lemma heap_upds_ok_restrictA:
  "heap_upds_ok (Γ, S) ⟹ heap_upds_ok (restrictA V Γ, S)"
  by auto

lemma heap_upds_ok_restr_stack:
  "heap_upds_ok (Γ, S) ⟹ heap_upds_ok (Γ, restr_stack V S)"
  apply auto
  by (induction V S rule: restr_stack.induct) auto

lemma heap_upds_ok_to_heap:
  "heap_upds_ok (Γ, Upd x # S) ⟹ heap_upds_ok ((x,e) # Γ, S)"
  by auto

lemma heap_upds_ok_reorder:
  "x ∈ domA Γ ⟹ heap_upds_ok (Γ, S) ⟹ heap_upds_ok ((x,e) # delete x Γ, S)"
  by (intro heap_upds_ok_to_heap heap_upds_ok_to_stack)

lemma heap_upds_ok_upd:
"heap_upds_ok (Γ, Upd x # S) ⟹ x ∉ domA Γ ∧ x ∉ upds S"
  by auto


lemmas heap_upds_ok_intros[intro] =
  heap_upds_ok_to_heap heap_upds_ok_to_stack heap_upds_ok_to_stack' heap_upds_ok_reorder
  heap_upds_ok_app1 heap_upds_ok_app2 heap_upds_ok_alts1 heap_upds_ok_alts2 heap_upds_ok_delete
  heap_upds_ok_restrictA heap_upds_ok_restr_stack
  heap_upds_ok_let
lemmas heap_upds_ok.simps[simp del]


end