(*  Title:      Jinja/DefAss.thy
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Definite assignment›

theory DefAss imports BigStep begin

subsection "Hypersets"

type_synonym 'a hyperset = "'a set option"

definition hyperUn :: "'a hyperset → 'a hyperset → 'a hyperset"   (infixl ‹⊔› 65)
where
  "A ⊔ B ≡ case A of None → None
                 | ⌊A⌋ → (case B of None → None | ⌊B⌋ → ⌊A ∪ B⌋)"

definition hyperInt :: "'a hyperset → 'a hyperset → 'a hyperset"   (infixl ‹⊓› 70)
where
  "A ⊓ B ≡ case A of None → B
                 | ⌊A⌋ → (case B of None → ⌊A⌋ | ⌊B⌋ → ⌊A ∩ B⌋)"

definition hyperDiff1 :: "'a hyperset → 'a → 'a hyperset"   (infixl ‹⊖› 65)
where
  "A ⊖ a ≡ case A of None → None | ⌊A⌋ → ⌊A - {a}⌋"

definition hyper_isin :: "'a → 'a hyperset → bool"   (infix ‹∈∈› 50)
where
  "a ∈∈ A ≡ case A of None → True | ⌊A⌋ → a ∈ A"

definition hyper_subset :: "'a hyperset → 'a hyperset → bool"   (infix ‹⊑› 50)
where
  "A ⊑ B ≡ case B of None → True
                 | ⌊B⌋ → (case A of None → False | ⌊A⌋ → A ⊆ B)"

lemmas hyperset_defs =
 hyperUn_def hyperInt_def hyperDiff1_def hyper_isin_def hyper_subset_def

lemma [simp]: "⌊{}⌋ ⊔ A = A ∧ A ⊔ ⌊{}⌋ = A"
(*<*)by(simp add:hyperset_defs)(*>*)

lemma [simp]: "⌊A⌋ ⊔ ⌊B⌋ = ⌊A ∪ B⌋ ∧ ⌊A⌋ ⊖ a = ⌊A - {a}⌋"
(*<*)by(simp add:hyperset_defs)(*>*)

lemma [simp]: "None ⊔ A = None ∧ A ⊔ None = None"
(*<*)by(simp add:hyperset_defs)(*>*)

lemma [simp]: "a ∈∈ None ∧ None ⊖ a = None"
(*<*)by(simp add:hyperset_defs)(*>*)

lemma hyperUn_assoc: "(A ⊔ B) ⊔ C = A ⊔ (B ⊔ C)"
(*<*)by(simp add:hyperset_defs Un_assoc)(*>*)

lemma hyper_insert_comm: "A ⊔ ⌊{a}⌋ = ⌊{a}⌋ ⊔ A ∧ A ⊔ (⌊{a}⌋ ⊔ B) = ⌊{a}⌋ ⊔ (A ⊔ B)"
(*<*)by(simp add:hyperset_defs)(*>*)


subsection "Definite assignment"

primrec
  A  :: "'a exp → 'a hyperset"
  and As :: "'a exp list → 'a hyperset"
where
  "A (new C) = ⌊{}⌋"
| "A (Cast C e) = A e"
| "A (Val v) = ⌊{}⌋"
| "A (e₁ «bop¬ e₂) = A e₁ ⊔ A e₂"
| "A (Var V) = ⌊{}⌋"
| "A (LAss V e) = ⌊{V}⌋ ⊔ A e"
| "A (e∙F{D}) = A e"
| "A (e₁∙F{D}:=e₂) = A e₁ ⊔ A e₂"
| "A (e∙M(es)) = A e ⊔ As es"
| "A ({V:T; e}) = A e ⊖ V"
| "A (e₁;;e₂) = A e₁ ⊔ A e₂"
| "A (if (e) e₁ else e₂) = A e ⊔ (A e₁ ⊓ A e₂)"
| "A (while (b) e) = A b"
| "A (throw e) = None"
| "A (try e₁ catch(C V) e₂) = A e₁ ⊓ (A e₂ ⊖ V)"

| "As ([]) = ⌊{}⌋"
| "As (e#es) = A e ⊔ As es"

primrec
  D  :: "'a exp → 'a hyperset → bool"
  and Ds :: "'a exp list → 'a hyperset → bool"
where
  "D (new C) A = True"
| "D (Cast C e) A = D e A"
| "D (Val v) A = True"
| "D (e₁ «bop¬ e₂) A = (D e₁ A ∧ D e₂ (A ⊔ A e₁))"
| "D (Var V) A = (V ∈∈ A)"
| "D (LAss V e) A = D e A"
| "D (e∙F{D}) A = D e A"
| "D (e₁∙F{D}:=e₂) A = (D e₁ A ∧ D e₂ (A ⊔ A e₁))"
| "D (e∙M(es)) A = (D e A ∧ Ds es (A ⊔ A e))"
| "D ({V:T; e}) A = D e (A ⊖ V)"
| "D (e₁;;e₂) A = (D e₁ A ∧ D e₂ (A ⊔ A e₁))"
| "D (if (e) e₁ else e₂) A =
  (D e A ∧ D e₁ (A ⊔ A e) ∧ D e₂ (A ⊔ A e))"
| "D (while (e) c) A = (D e A ∧ D c (A ⊔ A e))"
| "D (throw e) A = D e A"
| "D (try e₁ catch(C V) e₂) A = (D e₁ A ∧ D e₂ (A ⊔ ⌊{V}⌋))"

| "Ds ([]) A = True"
| "Ds (e#es) A = (D e A ∧ Ds es (A ⊔ A e))"

lemma As_map_Val[simp]: "As (map Val vs) = ⌊{}⌋"
(*<*)by (induct vs) simp_all(*>*)

lemma D_append[iff]: "∧A. Ds (es @ es') A = (Ds es A ∧ Ds es' (A ⊔ As es))"
(*<*)by (induct es type:list) (auto simp:hyperUn_assoc)(*>*)


lemma A_fv: "∧A. A e = ⌊A⌋ ==> A ⊆ fv e"
and  "∧A. As es = ⌊A⌋ ==> A ⊆ fvs es"
(*<*)
by (induct e and es rule: A.induct As.induct)
   (fastforce simp add:hyperset_defs)+
(*>*)


lemma sqUn_lem: "A ⊑ A' ==> A ⊔ B ⊑ A' ⊔ B"
(*<*)by(simp add:hyperset_defs) blast(*>*)

lemma diff_lem: "A ⊑ A' ==> A ⊖ b ⊑ A' ⊖ b"
(*<*)by(simp add:hyperset_defs) blast(*>*)

(* This order of the premises avoids looping of the simplifier *)
lemma D_mono: "∧A A'. A ⊑ A' ==> D e A ==> D (e::'a exp) A'"
and Ds_mono: "∧A A'. A ⊑ A' ==> Ds es A ==> Ds (es::'a exp list) A'"
(*<*)
proof(induct e and es rule: D.induct Ds.induct)
  case BinOp then show ?case by simp (iprover dest:sqUn_lem)
next
  case Var then show ?case by (fastforce simp add:hyperset_defs)
next
  case FAss then show ?case by simp (iprover dest:sqUn_lem)
next
  case Call then show ?case by simp (iprover dest:sqUn_lem)
next
  case Block then show ?case by simp (iprover dest:diff_lem)
next
  case Seq then show ?case by simp (iprover dest:sqUn_lem)
next
  case Cond then show ?case by simp (iprover dest:sqUn_lem)
next
  case While then show ?case by simp (iprover dest:sqUn_lem)
next
  case TryCatch then show ?case by simp (iprover dest:sqUn_lem)
next
  case Cons_exp then show ?case by simp (iprover dest:sqUn_lem)
qed simp_all
(*>*)

(* And this is the order of premises preferred during application: *)
lemma D_mono': "D e A ==> A ⊑ A' ==> D e A'"
and Ds_mono': "Ds es A ==> A ⊑ A' ==> Ds es A'"
(*<*)by(blast intro:D_mono, blast intro:Ds_mono)(*>*)

(*
text{* @{term"\<A>"} is sound w.r.t.\ the big step semantics: it
computes a conservative approximation of the variables actually
assigned to. *}

lemma "P \<turnstile> \<langle>e,(h\<^sub>0,l\<^sub>0)\<rangle> \<Rightarrow> \<langle>e',(h\<^sub>1,l\<^sub>1)\<rangle> \<Longrightarrow> (!!A. \<A> e = \<lfloor>A\<rfloor> \<Longrightarrow> A \<subseteq> dom l\<^sub>1)"
and "P \<turnstile> \<langle>es,(h\<^sub>0,l\<^sub>0)\<rangle> [\<Rightarrow>] \<langle>es',(h\<^sub>1,l\<^sub>1)\<rangle> \<Longrightarrow> (!!A. \<A>s es = \<lfloor>A\<rfloor> \<Longrightarrow> A \<subseteq> dom l\<^sub>1)"

proof (induct rule:eval_evals_induct)
  case LAss thus ?case apply(simp add:dom_def hyperset_defs) apply blast
apply blast
next
  case FAss thus ?case by simp (blast dest:eval_lcl_incr)
next
  case BinOp thus ?case by simp (blast dest:eval_lcl_incr)
next
  case Call thus  ?case by simp (blast dest:evals_lcl_incr)
next
  case Cons thus ?case by simp (blast dest:evals_lcl_incr)
next
  case Block thus ?case by(simp del: fun_upd_apply) blast
next
  case Seq thus ?case by simp (blast dest:eval_lcl_incr)
next
  case CondT thus ?case by simp (blast dest:eval_lcl_incr)
next
  case CondF thus ?case by simp (blast dest:eval_lcl_incr)
next
  case Try thus ?case by(fastforce dest!: eval_lcl_incr)
next
  case TryCatch thus ?case by(fastforce dest!: eval_lcl_incr)
qed auto
*)
end