Quelle  Sestoft.thy

theory Sestoft 
imports SestoftConf
begin

inductive step :: "conf ==> conf ==> bool" (infix ‹==>› 50) where
  app₁:  "(Γ, App e x, S) ==> (Γ, e , Arg x # S)"
| app₂:  "(Γ, Lam [y]. e, Arg x # S) ==> (Γ, e[y ::= x] , S)"
| var₁:  "map_of Γ x = Some e ==> (Γ, Var x, S) ==> (delete x Γ, e , Upd x # S)"
| var₂:  "x ∉ domA Γ ==> isVal e ==> (Γ, e, Upd x # S) ==> ((x,e)# Γ, e , S)"
| let₁:  "atom ` domA Δ ♯* Γ ==> atom ` domA Δ ♯* S
                           ==> (Γ, Let Δ e, S) ==> (Δ@Γ, e , S)"
| if₁:  "(Γ, scrut ? e1 : e2, S) ==> (Γ, scrut, Alts e1 e2 # S)"
| if₂:  "(Γ, Bool b, Alts e1 e2 # S) ==> (Γ, if b then e1 else e2, S)"

abbreviation steps (infix ‹==>^*› 50) where "steps ≡ step^**"

lemma SmartLet_stepI:
   "atom ` domA Δ ♯* Γ ==> atom ` domA Δ ♯* S ==> (Γ, SmartLet Δ e, S) ==>^* (Δ@Γ, e , S)"
unfolding SmartLet_def by (auto intro: let₁)

lemma lambda_var: "map_of Γ x = Some e ==> isVal e ==> (Γ, Var x, S) ==>^* ((x,e) # delete x Γ, e , S)"
  by (rule rtranclp_trans[OF r_into_rtranclp r_into_rtranclp])
     (auto intro: var₁ var₂)

lemma let₁_closed:
  assumes "closed (Γ, Let Δ e, S)"
  assumes "domA Δ ∩ domA Γ = {}"
  assumes "domA Δ ∩ upds S = {}"
  shows "(Γ, Let Δ e, S) ==> (Δ@Γ, e , S)"
proof
  from ‹domA Δ ∩ domA Γ = {}› and ‹domA Δ ∩ upds S = {}›
  have "domA Δ ∩ (domA Γ ∪ upds S) = {}" by auto
  with ‹closed _›
  have "domA Δ ∩ fv (Γ, S) = {}" by auto
  hence "atom ` domA Δ ♯* (Γ, S)"
    by (auto simp add: fresh_star_def fv_def fresh_def)
  thus "atom` domA Δ ♯* Γ" and "atom ` domA Δ ♯* S" by (auto simp add: fresh_star_Pair)
qed
  
text ‹An induction rule that skips the annoying case of a lambda taken off the heap›

lemma step_invariant_induction[consumes 4, case_names app₁ app₂ thunk lamvar var₂ let₁ if₁ if₂ refl trans]:
  assumes "c ==>^* c'"
  assumes "¬ boring_step c'"
  assumes "invariant (==>) I"
  assumes "I c"
  assumes app₁:  "∧ Γ e x S . I (Γ, App e x, S) ==> P (Γ, App e x, S) (Γ, e , Arg x # S)"
  assumes app₂:  "∧ Γ y e x S . I (Γ, Lam [y]. e, Arg x # S) ==> P (Γ, Lam [y]. e, Arg x # S) (Γ, e[y ::= x] , S)"
  assumes thunk:  "∧ Γ x e S . map_of Γ x = Some e ==> ¬ isVal e ==> I (Γ, Var x, S) ==> P (Γ, Var x, S) (delete x Γ, e , Upd x # S)"
  assumes lamvar:  "∧ Γ x e S . map_of Γ x = Some e ==> isVal e ==> I (Γ, Var x, S) ==> P (Γ, Var x, S) ((x,e) # delete x Γ, e , S)"
  assumes var₂:  "∧ Γ x e S . x ∉ domA Γ ==> isVal e ==> I (Γ, e, Upd x # S) ==> P (Γ, e, Upd x # S) ((x,e)# Γ, e , S)"
  assumes let₁:  "∧ Δ Γ e S . atom ` domA Δ ♯* Γ ==> atom ` domA Δ ♯* S ==> I (Γ, Let Δ e, S) ==> P (Γ, Let Δ e, S) (Δ@Γ, e, S)"
  assumes if₁:   "∧Γ scrut e1 e2 S. I (Γ, scrut ? e1 : e2, S) ==> P (Γ, scrut ? e1 : e2, S) (Γ, scrut, Alts e1 e2 # S)"
  assumes if₂:   "∧Γ b e1 e2 S. I (Γ, Bool b, Alts e1 e2 # S) ==> P (Γ, Bool b, Alts e1 e2 # S) (Γ, if b then e1 else e2, S)"
  assumes refl: "∧ c. P c c"
  assumes trans[trans]: "∧ c c' c''. c ==>^* c' ==> c' ==>^* c'' ==> P c c' ==> P c' c'' ==> P c c''"
  shows "P c c'"
proof-
  from assms(1,3,4)
  have "P c c' ∨ (boring_step c' ∧ (∀ c''. c' ==> c'' ⟶ P c c''))"
  proof(induction rule: rtranclp_invariant_induct)
  case base
    have "P c c" by (rule refl)
    thus ?case..
  next
  case (step y z)
    from step(5)
    show ?case
    proof
      assume "P c y"

      note t = trans[OF ‹c ==>^* y› r_into_rtranclp[where r = step, OF ‹y ==> z›]]
      
      from ‹y ==> z›
      show ?thesis
      proof (cases)
        case app₁ hence "P y z" using assms(5) ‹I y› by metis
        with ‹P c y› show ?thesis by (metis t)
      next
        case app₂ hence "P y z" using assms(6) ‹I y› by metis
        with ‹P c y› show ?thesis by (metis t)
      next
        case (var₁ Γ x e S)
        show ?thesis
        proof (cases "isVal e")
          case False with var₁ have "P y z" using assms(7) ‹I y› by metis
          with ‹P c y› show ?thesis by (metis t)
        next
          case True
          have *: "y ==>^* ((x,e) # delete x Γ, e , S)" using var₁ True lambda_var by metis

          have "boring_step (delete x Γ, e, Upd x # S)" using True ..
          moreover
          have "P y ((x,e) # delete x Γ, e , S)" using var₁ True assms(8) ‹I y› by metis
          with ‹P c y› have "P c ((x,e) # delete x Γ, e , S)" by (rule trans[OF ‹c ==>^* y› *])
          ultimately
          show ?thesis using var₁(2,3) True by (auto elim!: step.cases)
        qed
      next
        case var₂ hence "P y z" using assms(9) ‹I y› by metis
        with ‹P c y› show ?thesis by (metis t)
      next
        case let₁ hence "P y z" using assms(10) ‹I y› by metis
        with ‹P c y› show ?thesis by (metis t)
      next
        case if₁ hence "P y z" using assms(11) ‹I y› by metis
        with ‹P c y› show ?thesis by (metis t)
      next
        case if₂ hence "P y z" using assms(12) ‹I y› by metis
        with ‹P c y› show ?thesis by (metis t)
      qed
    next
      assume "boring_step y ∧ (∀c''. y ==> c'' ⟶ P c c'')"
      with ‹y ==> z›
      have "P c z" by blast
      thus ?thesis..
    qed
  qed
  with assms(2)
  show ?thesis by auto
qed


lemma step_induction[consumes 2, case_names app₁ app₂ thunk lamvar var₂ let₁ if₁ if₂ refl trans]:
  assumes "c ==>^* c'"
  assumes "¬ boring_step c'"
  assumes app₁:  "∧ Γ e x S . P (Γ, App e x, S) (Γ, e , Arg x # S)"
  assumes app₂:  "∧ Γ y e x S . P (Γ, Lam [y]. e, Arg x # S) (Γ, e[y ::= x] , S)"
  assumes thunk:  "∧ Γ x e S . map_of Γ x = Some e ==> ¬ isVal e ==> P (Γ, Var x, S) (delete x Γ, e , Upd x # S)"
  assumes lamvar:  "∧ Γ x e S . map_of Γ x = Some e ==> isVal e ==> P (Γ, Var x, S) ((x,e) # delete x Γ, e , S)"
  assumes var₂:  "∧ Γ x e S . x ∉ domA Γ ==> isVal e ==> P (Γ, e, Upd x # S) ((x,e)# Γ, e , S)"
  assumes let₁:  "∧ Δ Γ e S . atom ` domA Δ ♯* Γ ==> atom ` domA Δ ♯* S ==> P (Γ, Let Δ e, S) (Δ@Γ, e, S)"
  assumes if₁:   "∧Γ scrut e1 e2 S. P (Γ, scrut ? e1 : e2, S) (Γ, scrut, Alts e1 e2 # S)"
  assumes if₂:   "∧Γ b e1 e2 S. P (Γ, Bool b, Alts e1 e2 # S) (Γ, if b then e1 else e2, S)"
  assumes refl: "∧ c. P c c"
  assumes trans[trans]: "∧ c c' c''. c ==>^* c' ==> c' ==>^* c'' ==> P c c' ==> P c' c'' ==> P c c''"
  shows "P c c'"
by (rule step_invariant_induction[OF _ _ invariant_True, simplified, OF assms])

subsubsection ‹Equivariance›

lemma step_eqvt[eqvt]: "step x y ==> step (π ∙ x) (π ∙ y)"
  apply (induction  rule: step.induct)
  apply (perm_simp, rule step.intros)
  apply (perm_simp, rule step.intros)
  apply (perm_simp, rule step.intros)
  apply (rule permute_boolE[where p = "-π"], simp add: pemute_minus_self)
  apply (perm_simp, rule step.intros)
  apply (rule permute_boolE[where p = "-π"], simp add: pemute_minus_self)
  apply (rule permute_boolE[where p = "-π"], simp add: pemute_minus_self)
  apply (perm_simp, rule step.intros)
  apply (rule permute_boolE[where p = "-π"], simp add: pemute_minus_self)
  apply (rule permute_boolE[where p = "-π"], simp add: pemute_minus_self)
  apply (perm_simp, rule step.intros)
  apply (perm_simp, rule step.intros)
  done  

subsubsection ‹Invariants›

lemma closed_invariant:
  "invariant step closed"
proof
  fix c c'
  assume "c ==> c'" and "closed c"
  thus "closed c'"
  by (induction rule: step.induct) (auto simp add: fv_subst_eq dest!: subsetD[OF fv_delete_subset] dest: subsetD[OF map_of_Some_fv_subset])
qed

lemma heap_upds_ok_invariant:
  "invariant step heap_upds_ok_conf"
proof
  fix c c'
  assume "c ==> c'" and "heap_upds_ok_conf c"
  thus "heap_upds_ok_conf c'"
  by (induction rule: step.induct) auto
qed

end