Theory DefAss

(*  Title:       CoreC++
    Author:      Tobias Nipkow, Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Definite assignment›

theory DefAss
imports BigStep
begin


subsection ‹Hypersets›

type_synonym hyperset = "vname set option"

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

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

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

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

definition hyper_subset :: "hyperset ⇒ 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 𝒜 :: "expr ⇒ hyperset" and 𝒜s :: "expr list ⇒ hyperset" where
"𝒜 (new C) = ⌊{}⌋" |
"𝒜 (Cast C e) = 𝒜 e" |
"𝒜 (⦇C⦈e) = 𝒜 e" |
"𝒜 (Val v) = ⌊{}⌋" |
"𝒜 (e⇩1 «bop» e⇩2) = 𝒜 e⇩1 ⊔ 𝒜 e⇩2" |
"𝒜 (Var V) = ⌊{}⌋" |
"𝒜 (LAss V e) = ⌊{V}⌋ ⊔ 𝒜 e" |
"𝒜 (e∙F{Cs}) = 𝒜 e" |
"𝒜 (e⇩1∙F{Cs}:=e⇩2) = 𝒜 e⇩1 ⊔ 𝒜 e⇩2" |
"𝒜 (Call e Copt M es) = 𝒜 e ⊔ 𝒜s es" |
"𝒜 ({V:T; e}) = 𝒜 e ⊖ V" |
"𝒜 (e⇩1;;e⇩2) = 𝒜 e⇩1 ⊔ 𝒜 e⇩2" |
"𝒜 (if (e) e⇩1 else e⇩2) =  𝒜 e ⊔ (𝒜 e⇩1 ⊓ 𝒜 e⇩2)" |
"𝒜 (while (b) e) = 𝒜 b" |
"𝒜 (throw e) = None" |

"𝒜s ([]) = ⌊{}⌋" |
"𝒜s (e#es) = 𝒜 e ⊔ 𝒜s es"

primrec 𝒟 :: "expr ⇒ hyperset ⇒ bool" and 𝒟s :: "expr list ⇒ hyperset ⇒ bool" where
"𝒟 (new C) A = True" |
"𝒟 (Cast C e) A = 𝒟 e A" |
"𝒟 (⦇C⦈e) A = 𝒟 e A" |
"𝒟 (Val v) A = True" |
"𝒟 (e⇩1 «bop» e⇩2) A = (𝒟 e⇩1 A ∧ 𝒟 e⇩2 (A ⊔ 𝒜 e⇩1))" |
"𝒟 (Var V) A = (V ∈∈ A)" |
"𝒟 (LAss V e) A = 𝒟 e A" |
"𝒟 (e∙F{Cs}) A = 𝒟 e A" |
"𝒟 (e⇩1∙F{Cs}:=e⇩2) A = (𝒟 e⇩1 A ∧ 𝒟 e⇩2 (A ⊔ 𝒜 e⇩1))" |
"𝒟 (Call e Copt M es) A = (𝒟 e A ∧ 𝒟s es (A ⊔ 𝒜 e))" |
"𝒟 ({V:T; e}) A = 𝒟 e (A ⊖ V)" |
"𝒟 (e⇩1;;e⇩2) A = (𝒟 e⇩1 A ∧ 𝒟 e⇩2 (A ⊔ 𝒜 e⇩1))" |
"𝒟 (if (e) e⇩1 else e⇩2) A =
  (𝒟 e A ∧ 𝒟 e⇩1 (A ⊔ 𝒜 e) ∧ 𝒟 e⇩2 (A ⊔ 𝒜 e))" |
"𝒟 (while (e) c) A = (𝒟 e A ∧ 𝒟 c (A ⊔ 𝒜 e))" |
"𝒟 (throw e) A = 𝒟 e A" |

"𝒟s ([]) A = True" |
"𝒟s (e#es) A = (𝒟 e A ∧ 𝒟s es (A ⊔ 𝒜 e))"

lemma As_map_Val[simp]: "𝒜s (map Val vs) = ⌊{}⌋"
by (induct vs) simp_all

lemma D_append[iff]: "⋀A. 𝒟s (es @ es') A = (𝒟s es A ∧ 𝒟s es' (A ⊔ 𝒜s es))"
by (induct es type:list) (auto simp:hyperUn_assoc)


lemma A_fv: "⋀A. 𝒜 e = ⌊A⌋ ⟹ A ⊆ fv e"
and  "⋀A. 𝒜s es = ⌊A⌋ ⟹ A ⊆ fvs es"

apply(induct e and es rule: 𝒜.induct 𝒜s.induct)
apply (simp_all add:hyperset_defs)
apply blast+
done



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' ⟹ 𝒟 e A ⟹ 𝒟 (e::expr) A'"
and Ds_mono: "⋀A A'. A ⊑ A' ⟹ 𝒟s es A ⟹ 𝒟s (es::expr list) A'"

apply(induct e and es rule: 𝒟.induct 𝒟s.induct)
apply simp
apply simp
apply simp
apply simp
apply simp apply (iprover dest:sqUn_lem)
apply (fastforce simp add:hyperset_defs)
apply simp
apply simp
apply simp apply (iprover dest:sqUn_lem)
apply simp apply (iprover dest:sqUn_lem)
apply simp apply (iprover dest:diff_lem)
apply simp apply (iprover dest:sqUn_lem)
apply simp apply (iprover dest:sqUn_lem)
apply simp apply (iprover dest:sqUn_lem)
apply simp
apply simp 
apply simp
apply (iprover dest:sqUn_lem)
done


(* And this is the order of premises preferred during application: *)
lemma D_mono': "𝒟 e A ⟹ A ⊑ A' ⟹ 𝒟 e A'"
and Ds_mono': "𝒟s es A ⟹ A ⊑ A' ⟹ 𝒟s es A'"
by(blast intro:D_mono, blast intro:Ds_mono)

end