Quelle  SestoftGC.thy

theory SestoftGC
imports Sestoft 
begin

inductive gc_step :: "conf ==> conf ==> bool" (infix ‹==>_G› 50) where
  normal:  "c ==> c' ==> c ==>_G c'"
| dropUpd: "(Γ, e, Upd x # S) ==>_G (Γ, e, S @ [Dummy x])"
(*
| drop: "x \<in> domA \<Gamma>  \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e, S @ [Dummy x])"
*)

lemmas gc_step_intros[intro] =
  normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)]
  normal[OF step.intros(4)] normal[OF step.intros(5)]  dropUpd

abbreviation gc_steps (infix ‹==>_G^*› 50) where "gc_steps ≡ gc_step^**"
lemmas converse_rtranclp_into_rtranclp[of gc_step, OF _ r_into_rtranclp, trans]

lemma var_onceI:
  assumes "map_of Γ x = Some e"
  shows "(Γ, Var x, S) ==>_G^* (delete x Γ, e , S@[Dummy x])"
proof-
  from assms 
  have "(Γ, Var x, S) ==>_G (delete x Γ, e , Upd x # S)"..
  moreover
  have "… ==>_G (delete x Γ, e, S@[Dummy x])"..
  ultimately
  show ?thesis by (rule converse_rtranclp_into_rtranclp[OF _ r_into_rtranclp])
qed

(*
lemma lam_and_restrict:
  assumes "atom ` domA \<Delta> \<sharp>* \<Gamma>" and "atom ` domA \<Delta> \<sharp>* S"
  assumes "V \<subseteq> domA \<Delta>"
  shows "(\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G\<^sup>* (restrictA V \<Delta> @ \<Gamma>, e, S)"
proof-
  from assms(1,2) have "(\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G (\<Delta> @ \<Gamma>, e, S)"..
  also
  have "\<dots> \<Rightarrow>\<^sub>G (restrictA (V \<union> domA \<Gamma>) (\<Delta> @ \<Gamma>), e, S)"..
  also
  from fresh_distinct[OF assms(1)]
  have "restrictA (V \<union> domA \<Gamma>) \<Delta> = restrictA V \<Delta>" by (induction \<Delta>) auto
  hence "restrictA (V \<union> domA \<Gamma>) (\<Delta> @ \<Gamma>) = restrictA V \<Delta> @ \<Gamma>"
    by (simp add: restrictA_append restrictA_noop)
  finally show ?thesis.
qed
*)

lemma normal_trans:  "c ==>^* c' ==> c ==>_G^* c'"
  by (induction rule:rtranclp_induct)
     (simp, metis normal rtranclp.rtrancl_into_rtrancl)

fun to_gc_conf :: "var list ==> conf ==> conf"
  where "to_gc_conf r (Γ, e, S) = (restrictA (- set r) Γ, e, restr_stack (- set r) S @ (map Dummy (rev r)))"

lemma restr_stack_map_Dummy[simp]: "restr_stack V (map Dummy l) = map Dummy l"
  by (induction l) auto

lemma restr_stack_append[simp]: "restr_stack V (l@l') = restr_stack V l @ restr_stack V l'"
  by (induction l rule: restr_stack.induct) auto

lemma to_gc_conf_append[simp]:
  "to_gc_conf (r@r') c = to_gc_conf r (to_gc_conf r' c)"
  by (cases c) auto

lemma to_gc_conf_eqE[elim!]:
  assumes  "to_gc_conf r c = (Γ, e, S)"
  obtains Γ' S' where "c = (Γ', e, S')" and "Γ = restrictA (- set r) Γ'" and "S = restr_stack (- set r) S' @ map Dummy (rev r)"
  using assms by (cases c) auto

fun safe_hd :: "'a list ==> 'a option"
 where  "safe_hd (x#_) = Some x"
     |  "safe_hd [] = None"

lemma safe_hd_None[simp]: "safe_hd xs = None ⟷ xs = []"
  by (cases xs) auto

abbreviation r_ok :: "var list ==> conf ==> bool"
  where "r_ok r c ≡ set r ⊆ domA (fst c) ∪ upds (snd (snd c))"

lemma subset_bound_invariant:
  "invariant step (r_ok r)"
proof
  fix x y
  assume "x ==> y" and "r_ok r x" thus "r_ok r y"
  by (induction) auto
qed

lemma safe_hd_restr_stack[simp]:
  "Some a = safe_hd (restr_stack V (a # S)) ⟷ restr_stack V (a # S) = a # restr_stack V S"
  apply (cases a)
  apply (auto split: if_splits)
  apply (thin_tac "P a" for P)
  apply (induction S rule: restr_stack.induct)
  apply (auto split: if_splits)
  done

lemma sestoftUnGCStack:
  assumes "heap_upds_ok (Γ, S)"
  obtains Γ' S' where
    "(Γ, e, S) ==>^* (Γ', e, S')"
    "to_gc_conf r (Γ, e, S) = to_gc_conf r (Γ', e, S')"
    "¬ isVal e ∨ safe_hd S' = safe_hd (restr_stack (- set r) S')"
proof-
  show ?thesis
  proof(cases "isVal e")
    case False
    thus ?thesis using assms  by -(rule that, auto)
  next
    case True
    from that assms 
    show ?thesis
    apply (atomize_elim)
    proof(induction S arbitrary: Γ)
      case Nil thus ?case by (fastforce)
    next
      case (Cons s S)
      show ?case
      proof(cases "Some s = safe_hd (restr_stack (- set r) (s#S))")
        case True
        thus ?thesis
          using ‹isVal e› ‹heap_upds_ok (Γ, s # S)›
          apply auto
          apply (intro exI conjI)
          apply (rule rtranclp.intros(1))
          apply auto
          done
      next
        case False
        then obtain x where [simp]: "s = Upd x" and [simp]: "x ∈ set r"
          by(cases s) (auto split: if_splits)
      
        from ‹heap_upds_ok (Γ, s # S)› ‹s = Upd x›
        have [simp]: "x ∉ domA Γ" and "heap_upds_ok ((x,e) # Γ, S)"
          by (auto dest: heap_upds_okE) 

        have "(Γ, e, s # S) ==>^* (Γ, e, Upd x # S)" unfolding ‹s = _› ..
        also have "… ==> ((x,e) # Γ, e, S)" by (rule step.var₂[OF ‹x ∉ domA Γ› ‹isVal e›])
        also
        from Cons.IH[OF ‹heap_upds_ok ((x,e) # Γ, S)› ]
        obtain Γ' S' where  "((x,e) # Γ, e, S) ==>^* (Γ', e, S')"
            and res: "to_gc_conf r ((x,e) # Γ, e, S) = to_gc_conf r (Γ', e, S')"
                     "(¬ isVal e ∨ safe_hd S' = safe_hd (restr_stack (- set r) S'))"
          by blast
        note this(1)
        finally
        have "(Γ, e, s # S) ==>^* (Γ', e, S')".
        thus ?thesis  using res by auto
      qed
    qed
  qed
qed

lemma perm_exI_trivial:
  "P x x ==> ∃ π. P (π ∙ x) x"
by (rule exI[where x = "0::perm"]) auto

lemma upds_list_restr_stack[simp]:
  "upds_list (restr_stack V S) = filter (λ x. x∈V) (upds_list S)"
by (induction S rule: restr_stack.induct) auto

lemma heap_upd_ok_to_gc_conf:
  "heap_upds_ok (Γ, S) ==> to_gc_conf r (Γ, e, S) = (Γ'', e'', S'') ==> heap_upds_ok (Γ'', S'')"
by (auto simp add: heap_upds_ok.simps)

lemma delete_restrictA_conv:
  "delete x Γ = restrictA (-{x}) Γ"
by (induction Γ) auto

lemma sestoftUnGCstep:
  assumes "to_gc_conf r c ==>_G d"
  assumes "heap_upds_ok_conf c"
  assumes "closed c"
  and "r_ok r c"
  shows   "∃ r' c'. c ==>^* c' ∧ d = to_gc_conf r' c' ∧ r_ok r' c'"
proof-
  obtain Γ e S where "c = (Γ, e, S)" by (cases c) auto
  with assms
  have "heap_upds_ok (Γ,S)" and "closed (Γ, e, S)" and "r_ok r (Γ, e, S)" by auto
  from sestoftUnGCStack[OF this(1)]
  obtain Γ' S' where
    "(Γ, e, S) ==>^* (Γ', e, S')"
    and *: "to_gc_conf r (Γ, e, S) = to_gc_conf r (Γ', e, S')"
    and disj: "¬ isVal e ∨ safe_hd S' = safe_hd (restr_stack (- set r) S')"
    by metis

  from invariant_starE[OF ‹_ ==>^* _› heap_upds_ok_invariant]  ‹heap_upds_ok (Γ,S)›
  have "heap_upds_ok (Γ', S')" by auto

  from invariant_starE[OF ‹_ ==>^* _› closed_invariant  ‹closed (Γ, e, S)› ]
  have "closed (Γ', e, S')" by auto

  from invariant_starE[OF ‹_ ==>^* _› subset_bound_invariant ‹r_ok r (Γ, e, S)› ]
  have "r_ok r (Γ', e, S')" by auto

  from assms(1)[unfolded ‹c =_ › *]
  have "∃ r' Γ'' e'' S''. (Γ', e, S') ==>^* (Γ'', e'', S'') ∧ d = to_gc_conf r' (Γ'', e'', S'') ∧ r_ok r' (Γ'', e'', S'')"
  proof(cases rule: gc_step.cases)
    case normal
    hence "∃ Γ'' e'' S''. (Γ', e, S') ==> (Γ'', e'', S'') ∧ d = to_gc_conf r (Γ'', e'', S'')"
    proof(cases rule: step.cases)
      case app₁
      thus ?thesis
        apply auto
        apply (intro exI conjI)
        apply (rule  step.intros)
        apply auto
        done
    next
      case (app₂ Γ y ea x S)
      thus ?thesis
        using disj 
        apply (cases S')
        apply auto
        apply (intro exI conjI)
        apply (rule step.intros)
        apply auto
        done
    next
      case var₁
      thus ?thesis
        apply auto
        apply (intro  exI conjI)
        apply (rule step.intros)
        apply (auto simp add: restr_delete_twist)
        done
    next
      case var₂
      thus ?thesis
        using disj 
        apply (cases S')
        apply auto
        apply (intro exI conjI)
        apply (rule step.intros)
        apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
        done
    next
      case (let₁ Δ'' Γ'' S'' e')

      from ‹closed (Γ', e, S')› let₁
      have "closed (Γ', Let Δ'' e', S')" by simp

      from fresh_distinct[OF let₁(3)] fresh_distinct_fv[OF let₁(4)]
      have "domA Δ'' ∩ domA Γ'' = {}" and "domA Δ'' ∩ upds S'' = {}"  and "domA Δ'' ∩ dummies S'' = {}" 
        by (auto dest: subsetD[OF ups_fv_subset] subsetD[OF dummies_fv_subset])
      moreover
      from let₁(1)
      have "domA Γ' ∪ upds S' ⊆ domA Γ'' ∪ upds S'' ∪ dummies S''"
        by auto
      ultimately
      have disj: "domA Δ'' ∩ domA Γ' = {}" "domA Δ'' ∩ upds S' = {}"
        by auto
      
      from ‹domA Δ'' ∩ dummies S'' = {}› let₁(1)
      have "domA Δ'' ∩ set r = {}" by auto
      hence [simp]: "restrictA (- set r) Δ'' = Δ''"
        by (auto intro: restrictA_noop)

      from let₁(1-3)
      show ?thesis
        apply auto
        apply (intro  exI[where x = "r"] exI[where x = "Δ'' @ Γ'"] exI[where x = "S'"] conjI)
        apply (rule let₁_closed[OF ‹closed (Γ', Let Δ'' e', S')› disj])
        apply (auto simp add: restrictA_append)
        done
    next
      case if₁
      thus ?thesis
        apply auto
        apply (intro exI[where x = "0::perm"] exI conjI)
        unfolding permute_zero
        apply (rule step.intros)
        apply (auto)
        done
    next
      case if₂
      thus ?thesis
        using disj
        apply (cases S')
        apply auto
        apply (intro exI exI conjI)
        apply (rule step.if₂[where b = True, simplified] step.if₂[where b = False, simplified])
        apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
        apply (intro exI conjI)
        apply (rule step.if₂[where b = True, simplified] step.if₂[where b = False, simplified])
        apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
        done
    qed
    with invariantE[OF subset_bound_invariant _ ‹r_ok r (Γ', e, S')›]
    show ?thesis by blast
  next
  case (dropUpd Γ'' e'' x S'')
    from ‹to_gc_conf r (Γ', e, S') = (Γ'', e'', Upd x # S'')›
    have "x ∉ set r" by (auto dest!: arg_cong[where f = upds])
    
    from ‹heap_upds_ok (Γ', S')› and ‹to_gc_conf r (Γ', e, S') = (Γ'', e'', Upd x # S'')›
    have "heap_upds_ok (Γ'', Upd x # S'')" by (rule heap_upd_ok_to_gc_conf)
    hence [simp]: "x ∉ domA Γ''" "x ∉ upds S''" by (auto dest: heap_upds_ok_upd)

    have "to_gc_conf (x # r) (Γ', e, S') = to_gc_conf ([x]@ r) (Γ', e, S')" by simp
    also have "… = to_gc_conf [x] (to_gc_conf r (Γ', e, S'))" by (rule to_gc_conf_append)
    also have "… = to_gc_conf [x] (Γ'', e'', Upd x # S'')" unfolding ‹to_gc_conf r (Γ', e, S') = _›..
    also have "… = (Γ'', e'', S''@[Dummy x])" by (auto intro: restrictA_noop)
    also have "… = d" using ‹ d= _› by simp
    finally have "to_gc_conf (x # r) (Γ', e, S') = d".
    moreover
    from ‹to_gc_conf r (Γ', e, S') = (Γ'', e'', Upd x # S'')›
    have "x ∈ upds S'" by (auto dest!: arg_cong[where f = upds])
    with ‹r_ok r (Γ', e, S')›
    have "r_ok (x # r) (Γ', e, S')" by auto
    moreover
    note ‹to_gc_conf r (Γ', e, S') = (Γ'', e'', Upd x # S'')›
    ultimately
    show ?thesis by fastforce
(*
  next
    case (drop x \<Gamma>'' e'' S'')
    from `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', S'')` and `x \<in> domA \<Gamma>''`
    have "x \<notin> set r" by auto

    from `heap_upds_ok (\<Gamma>', S')` and  `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', S'')`
    have "heap_upds_ok (\<Gamma>'', S'')" by (rule heap_upd_ok_to_gc_conf)
    with `x \<in> domA \<Gamma>''`
    have [simp]: "x \<notin> upds S''" by (metis heap_upds_okE)


    have "to_gc_conf (x # r) (\<Gamma>', e, S') = to_gc_conf ([x]@ r) (\<Gamma>', e, S')" by simp
    also have "\<dots> = to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S'))" by (rule to_gc_conf_append)
    also have "\<dots> = to_gc_conf [x] (\<Gamma>'', e'', S'')" unfolding `to_gc_conf r (\<Gamma>', e, S') = _`..
    also have "\<dots> = (delete x \<Gamma>'', e'', S''@[Dummy x])" by (auto  simp add: delete_restrictA_conv)
    also have "\<dots> = d" using ` d= _` by simp
    finally have "to_gc_conf (x # r) (\<Gamma>', e, S') = d".
    moreover
    from `to_gc_conf r (\<Gamma>', e, S') = _` `x \<in> domA \<Gamma>''`
    have "x \<in> domA \<Gamma>'" by auto
    with `r_ok r (\<Gamma>', e, S')`
    have "r_ok (x # r) (\<Gamma>', e, S')" by auto
    moreover
    note `to_gc_conf r (\<Gamma>', e, S') = _`
    ultimately
    show ?thesis by fastforce
*)
  qed
  then obtain r' Γ'' e'' S''
    where "(Γ', e, S') ==>^* (Γ'', e'', S'')"
    and "d = to_gc_conf r' (Γ'', e'', S'')"
    and "r_ok r' (Γ'', e'', S'')"
    by metis 

  from  ‹(Γ, e, S) ==>^* (Γ', e, S')› and ‹(Γ', e, S') ==>^* (Γ'', e'', S'')›
  have "(Γ, e, S) ==>^* (Γ'', e'', S'')" by (rule rtranclp_trans)
  with ‹d = _› ‹r_ok r' _›
  show ?thesis unfolding ‹c = _› by auto
qed


lemma sestoftUnGC:
  assumes "(to_gc_conf r c) ==>_G^* d" and "heap_upds_ok_conf c" and "closed c" and "r_ok r c"
  shows   "∃ r' c'. c ==>^* c' ∧ d = to_gc_conf r' c' ∧ r_ok r' c'"
using assms
proof(induction rule: rtranclp_induct)
  case base
  thus ?case by blast
next
  case (step d' d'')
  then obtain r' c' where "c ==>^* c'" and "d' = to_gc_conf r' c'" and "r_ok r' c'"  by auto

  from invariant_starE[OF ‹_ ==>^* _› heap_upds_ok_invariant]  ‹heap_upds_ok _›
  have "heap_upds_ok_conf c'".

  from invariant_starE[OF ‹_ ==>^* _› closed_invariant]  ‹closed _›
  have "closed c'".

  from step ‹d' = to_gc_conf r' c'›
  have "to_gc_conf r' c' ==>_G d''" by simp
  from this ‹heap_upds_ok_conf c'› ‹closed c'› ‹r_ok r' c'›
  have "∃ r'' c''. c' ==>^* c'' ∧ d'' = to_gc_conf r'' c'' ∧ r_ok r'' c''"
    by (rule sestoftUnGCstep)
  then obtain r'' c'' where "c' ==>^* c''" and "d'' = to_gc_conf r'' c''" and "r_ok r'' c''" by auto
  
  from ‹c' ==>^* c''› ‹c ==>^* c'›
  have "c ==>^* c''" by auto
  with ‹d'' = _› ‹r_ok r'' c''›
  show ?case by blast
qed

lemma dummies_unchanged_invariant:
  "invariant step (λ (Γ, e, S) . dummies S = V)" (is "invariant _ ?I")
proof
  fix c c'
  assume "c ==> c'" and "?I c"
  thus "?I c'" by (induction) auto
qed
  
lemma sestoftUnGC':
  assumes "([], e, []) ==>_G^* (Γ, e', map Dummy r)"
  assumes "isVal e'"
  assumes "fv e = ({}::var set)"
  shows   "∃ Γ''. ([], e, []) ==>^* (Γ'', e', []) ∧ Γ = restrictA (- set r) Γ'' ∧ set r ⊆ domA Γ''"
proof-
 from sestoftUnGC[where r = "[]" and c = "([], e, [])", simplified, OF assms(1,3)]
 obtain r' Γ' S'
  where "([], e, []) ==>^* (Γ', e', S')"
    and "Γ = restrictA (- set r') Γ'"
    and "map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')"
    and "r_ok r' (Γ', e', S')"
    by auto

  from invariant_starE[OF ‹([], e, []) ==>^* (Γ', e', S')› dummies_unchanged_invariant]
  have "dummies S' = {}" by auto
  with  ‹map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')›
  have "restr_stack (- set r') S' = []" and [simp]: "r = rev r'"
  by (induction S' rule: restr_stack.induct) (auto split: if_splits)
  
  from invariant_starE[OF ‹_ ==>^* _› heap_upds_ok_invariant]
  have "heap_upds_ok (Γ', S')" by auto
 
  from ‹isVal e'› sestoftUnGCStack[where e = e', OF ‹heap_upds_ok (Γ', S')› ]
  obtain Γ'' S''
    where "(Γ', e', S') ==>^* (Γ'', e', S'')"
    and "to_gc_conf r (Γ', e', S') = to_gc_conf r (Γ'', e', S'')"
    and "safe_hd S'' = safe_hd (restr_stack (- set r) S'')"
    by metis

  from this (2,3) ‹restr_stack (- set r') S' = []›
  have "S'' = []" by auto

  from  ‹([], e, []) ==>^* (Γ', e', S')›  and ‹(Γ', e', S') ==>^* (Γ'', e', S'')› and ‹S'' = []›
  have "([], e, []) ==>^* (Γ'', e', [])" by auto
  moreover
  have "Γ = restrictA (- set r) Γ''" using ‹to_gc_conf r _ = _› ‹Γ = _› by auto
  moreover
  from invariant_starE[OF ‹(Γ', e', S') ==>^* (Γ'', e', S'')› subset_bound_invariant ‹r_ok r' (Γ', e', S')›]
  have "set r ⊆ domA Γ''" using ‹S'' = []› by auto
  ultimately
  show ?thesis by blast
qed

end