Theory DefAss

(*  Title:      JinjaThreads/J/DefAss.thy
    Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Definite assignment›

theory DefAss
imports 
  Expr
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)(*>*)

lemma sqSub_mem_lem [elim]: "⟦ A ⊑ A'; a ∈∈ A ⟧ ⟹ a ∈∈ A'"
by(auto simp add: hyperset_defs)

lemma [iff]: "A ⊑ None"
by(auto simp add: hyperset_defs)

lemma [simp]: "A ⊑ A"
by(auto simp add: hyperset_defs)

lemma [iff]: "⌊A⌋ ⊑ ⌊B⌋ ⟷ A ⊆ B"
by(auto simp add: hyperset_defs)

lemma sqUn_lem2: "A ⊑ A' ⟹ B ⊔ A ⊑ B ⊔ A'"
by(simp add:hyperset_defs) blast

lemma sqSub_trans [trans, intro]: "⟦ A ⊑ B; B ⊑ C ⟧ ⟹ A ⊑ C"
by(auto simp add: hyperset_defs)

lemma hyperUn_comm: "A ⊔ B = B ⊔ A"
by(auto simp add: hyperset_defs)

lemma hyperUn_leftComm: "A ⊔ (B ⊔ C) = B ⊔ (A ⊔ C)"
by(auto simp add: hyperset_defs)

lemmas hyperUn_ac = hyperUn_comm hyperUn_leftComm hyperUn_assoc

lemma [simp]: "⌊{}⌋ ⊔ B = B"
by(auto)

lemma [simp]: "⌊{}⌋ ⊑ A"
by(auto simp add: hyperset_defs)

lemma sqInt_lem: "A ⊑ A' ⟹ A ⊓ B ⊑ A' ⊓ B"
by(auto simp add: hyperset_defs)

subsection "Definite assignment"

primrec 𝒜  :: "('a,'b,'addr) exp ⇒ 'a hyperset"
  and 𝒜s :: "('a,'b,'addr) exp list ⇒ 'a hyperset"
where
  "𝒜 (new C) = ⌊{}⌋"
| "𝒜 (newA T⌊e⌉) = 𝒜 e"
| "𝒜 (Cast C e) = 𝒜 e"
| "𝒜 (e instanceof T) = 𝒜 e"
| "𝒜 (Val v) = ⌊{}⌋"
| "𝒜 (e⇩1 «bop» e⇩2) = 𝒜 e⇩1 ⊔ 𝒜 e⇩2"
| "𝒜 (Var V) = ⌊{}⌋"
| "𝒜 (LAss V e) = ⌊{V}⌋ ⊔ 𝒜 e"
| "𝒜 (a⌊i⌉) = 𝒜 a ⊔ 𝒜 i"
| "𝒜 (a⌊i⌉ := e) = 𝒜 a ⊔ 𝒜 i ⊔ 𝒜 e"
| "𝒜 (a∙length) = 𝒜 a"
| "𝒜 (e∙F{D}) = 𝒜 e"
| "𝒜 (e⇩1∙F{D}:=e⇩2) = 𝒜 e⇩1 ⊔ 𝒜 e⇩2"
| "𝒜 (e1∙compareAndSwap(D∙F, e2, e3)) = 𝒜 e1 ⊔ 𝒜 e2 ⊔ 𝒜 e3"
| "𝒜 (e∙M(es)) = 𝒜 e ⊔ 𝒜s es"
| "𝒜 ({V:T=vo; e}) = 𝒜 e ⊖ V"
| "𝒜 (sync⇘V⇙ (o') e) = 𝒜 o' ⊔ 𝒜 e"
| "𝒜 (insync⇘V⇙ (a) e) = 𝒜 e"
| "𝒜 (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"
| "𝒜 (try e⇩1 catch(C V) e⇩2) = 𝒜 e⇩1 ⊓ (𝒜 e⇩2 ⊖ V)"

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

primrec 𝒟  :: "('a,'b,'addr) exp ⇒ 'a hyperset ⇒ bool"
  and 𝒟s :: "('a,'b,'addr) exp list ⇒ 'a hyperset ⇒ bool"
where
  "𝒟 (new C) A = True"
| "𝒟 (newA T⌊e⌉) A = 𝒟 e A"
| "𝒟 (Cast C e) A = 𝒟 e A"
| "𝒟 (e instanceof T) = 𝒟 e"
| "𝒟 (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"
| "𝒟 (a⌊i⌉) A = (𝒟 a A ∧ 𝒟 i (A ⊔ 𝒜 a))"
| "𝒟 (a⌊i⌉ := e) A = (𝒟 a A ∧ 𝒟 i (A ⊔ 𝒜 a) ∧ 𝒟 e (A ⊔ 𝒜 a ⊔ 𝒜 i))"
| "𝒟 (a∙length) A = 𝒟 a A"
| "𝒟 (e∙F{D}) A = 𝒟 e A"
| "𝒟 (e⇩1∙F{D}:=e⇩2) A = (𝒟 e⇩1 A ∧ 𝒟 e⇩2 (A ⊔ 𝒜 e⇩1))"
| "𝒟 (e1∙compareAndSwap(D∙F, e2, e3)) A = (𝒟 e1 A ∧ 𝒟 e2 (A ⊔ 𝒜 e1) ∧ 𝒟 e3 (A ⊔ 𝒜 e1 ⊔ 𝒜 e2))"
| "𝒟 (e∙M(es)) A = (𝒟 e A ∧ 𝒟s es (A ⊔ 𝒜 e))"
| "𝒟 ({V:T=vo; e}) A = (if vo = None then 𝒟 e (A ⊖ V) else 𝒟 e (A ⊔ ⌊{V}⌋))"
| "𝒟 (sync⇘V⇙ (o') e) A = (𝒟 o' A ∧ 𝒟 e (A ⊔ 𝒜 o'))"
| "𝒟 (insync⇘V⇙ (a) e) A = 𝒟 e A"
| "𝒟 (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"
| "𝒟 (try e⇩1 catch(C V) e⇩2) A = (𝒟 e⇩1 A ∧ 𝒟 e⇩2 (A ⊔ ⌊{V}⌋))"

| "𝒟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 As_append [simp]: "𝒜s (xs @ ys) = (𝒜s xs) ⊔ (𝒜s ys)"
by(induct xs, auto simp add: hyperset_defs)

lemma Ds_map_Val[simp]: "𝒟s (map Val vs) A"
(*<*)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 fixes e :: "('a,'b,'addr) exp" and es :: "('a,'b,'addr) exp list"
  shows 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 fast+
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 fixes e :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list"
  shows D_mono: "⋀A A'. A ⊑ A' ⟹ 𝒟 e A ⟹ 𝒟 e A'"
  and Ds_mono: "⋀A A'. A ⊑ A' ⟹ 𝒟s es A ⟹ 𝒟s es A'"
(*<*)
apply(induct e and es rule: 𝒟.induct 𝒟s.induct)
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp
subgoal by simp (iprover dest:sqUn_lem)
subgoal by(fastforce simp add:hyperset_defs)
subgoal by simp
subgoal by simp (iprover dest:sqUn_lem)
subgoal by simp (iprover dest:sqUn_lem)
subgoal by simp
subgoal by simp
subgoal by simp (iprover dest:sqUn_lem)
subgoal by simp (iprover dest:sqUn_lem)
subgoal by simp (iprover dest: sqUn_lem)
subgoal 
  apply(clarsimp split: if_split_asm) 
  apply (iprover dest:diff_lem) 
  apply(iprover dest: sqUn_lem)
  done
subgoal by simp (iprover dest:sqUn_lem)
subgoal by simp
subgoal by simp (iprover dest:sqUn_lem)
subgoal by simp (iprover dest:sqUn_lem)
subgoal by simp (iprover dest:sqUn_lem)
subgoal by simp
subgoal by simp (iprover dest:sqUn_lem)
subgoal by simp
subgoal by simp (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)(*>*)

declare hyperUn_comm [simp]
declare hyperUn_leftComm [simp]

end