Theory Sestoft

theory Sestoft 
imports SestoftConf
begin

inductive step :: "conf ⇒ conf ⇒ bool" (infix "⇒" 50) where
  app⇩1:  "(Γ, App e x, S) ⇒ (Γ, e , Arg x # S)"
| app⇩2:  "(Γ, Lam [y]. e, Arg x # S) ⇒ (Γ, e[y ::= x] , S)"
| var⇩1:  "map_of Γ x = Some e ⟹ (Γ, Var x, S) ⇒ (delete x Γ, e , Upd x # S)"
| var⇩2:  "x ∉ domA Γ ⟹ isVal e ⟹ (Γ, e, Upd x # S) ⇒ ((x,e)# Γ, e , S)"
| let⇩1:  "atom ` domA Δ ♯* Γ ⟹ atom ` domA Δ ♯* S
                           ⟹ (Γ, Let Δ e, S) ⇒ (Δ@Γ, e , S)"
| if⇩1:  "(Γ, scrut ? e1 : e2, S) ⇒ (Γ, scrut, Alts e1 e2 # S)"
| if⇩2:  "(Γ, 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⇩1)

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⇩1 var⇩2)

lemma let⇩1_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⇩1 app⇩2 thunk lamvar var⇩2 let⇩1 if⇩1 if⇩2 refl trans]:
  assumes "c ⇒⇧* c'"
  assumes "¬ boring_step c'"
  assumes "invariant op ⇒ I"
  assumes "I c"
  assumes app⇩1:  "⋀ Γ e x S . I (Γ, App e x, S) ⟹ P (Γ, App e x, S)  (Γ, e , Arg x # S)"
  assumes app⇩2:  "⋀ Γ 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⇩2:  "⋀ Γ x e S . x ∉ domA Γ ⟹ isVal e ⟹ I (Γ, e, Upd x # S) ⟹ P (Γ, e, Upd x # S) ((x,e)# Γ, e , S)"
  assumes let⇩1:  "⋀ Δ Γ e S . atom ` domA Δ ♯* Γ ⟹ atom ` domA Δ ♯* S ⟹ I (Γ, Let Δ e, S) ⟹ P (Γ, Let Δ e, S) (Δ@Γ, e, S)"
  assumes if⇩1:   "⋀Γ scrut e1 e2 S. I  (Γ, scrut ? e1 : e2, S) ⟹ P (Γ, scrut ? e1 : e2, S) (Γ, scrut, Alts e1 e2 # S)"
  assumes if⇩2:   "⋀Γ 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⇩1 hence "P y z" using assms(5) `I y` by metis
        with `P c y` show ?thesis by (metis t)
      next
        case app⇩2 hence "P y z" using assms(6) `I y` by metis
        with `P c y` show ?thesis by (metis t)
      next
        case (var⇩1 Γ x e S)
        show ?thesis
        proof (cases "isVal e")
          case False with var⇩1 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⇩1 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⇩1 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⇩1(2,3) True by (auto elim!: step.cases)
        qed
      next
        case var⇩2 hence "P y z" using assms(9) `I y` by metis
        with `P c y` show ?thesis by (metis t)
      next
        case let⇩1 hence "P y z" using assms(10) `I y` by metis
        with `P c y` show ?thesis by (metis t)
      next
        case if⇩1 hence "P y z" using assms(11) `I y` by metis
        with `P c y` show ?thesis by (metis t)
      next
        case if⇩2 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⇩1 app⇩2 thunk lamvar var⇩2 let⇩1 if⇩1 if⇩2 refl trans]:
  assumes "c ⇒⇧* c'"
  assumes "¬ boring_step c'"
  assumes app⇩1:  "⋀ Γ e x S . P (Γ, App e x, S)  (Γ, e , Arg x # S)"
  assumes app⇩2:  "⋀ Γ 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⇩2:  "⋀ Γ x e S . x ∉ domA Γ ⟹ isVal e ⟹ P (Γ, e, Upd x # S) ((x,e)# Γ, e , S)"
  assumes let⇩1:  "⋀ Δ Γ e S . atom ` domA Δ ♯* Γ ⟹ atom ` domA Δ ♯* S ⟹ P (Γ, Let Δ e, S) (Δ@Γ, e, S)"
  assumes if⇩1:   "⋀Γ scrut e1 e2 S. P (Γ, scrut ? e1 : e2, S) (Γ, scrut, Alts e1 e2 # S)"
  assumes if⇩2:   "⋀Γ 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!: set_mp[OF fv_delete_subset] dest: set_mp[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