header {* \isaheader{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 "\<squnion>" 65)
where
"A \<squnion> B ≡ case A of None => None
| ⌊A⌋ => (case B of None => None | ⌊B⌋ => ⌊A ∪ B⌋)"
definition hyperInt :: "'a hyperset => 'a hyperset => 'a hyperset" (infixl "\<sqinter>" 70)
where
"A \<sqinter> B ≡ case A of None => B
| ⌊A⌋ => (case B of None => ⌊A⌋ | ⌊B⌋ => ⌊A ∩ B⌋)"
definition hyperDiff1 :: "'a hyperset => 'a => 'a hyperset" (infixl "\<ominus>" 65)
where
"A \<ominus> 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 "\<sqsubseteq>" 50)
where
"A \<sqsubseteq> 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]: "⌊{}⌋ \<squnion> A = A ∧ A \<squnion> ⌊{}⌋ = A"
by(simp add:hyperset_defs)
lemma [simp]: "⌊A⌋ \<squnion> ⌊B⌋ = ⌊A ∪ B⌋ ∧ ⌊A⌋ \<ominus> a = ⌊A - {a}⌋"
by(simp add:hyperset_defs)
lemma [simp]: "None \<squnion> A = None ∧ A \<squnion> None = None"
by(simp add:hyperset_defs)
lemma [simp]: "a ∈∈ None ∧ None \<ominus> a = None"
by(simp add:hyperset_defs)
lemma hyperUn_assoc: "(A \<squnion> B) \<squnion> C = A \<squnion> (B \<squnion> C)"
by(simp add:hyperset_defs Un_assoc)
lemma hyper_insert_comm: "A \<squnion> ⌊{a}⌋ = ⌊{a}⌋ \<squnion> A ∧ A \<squnion> (⌊{a}⌋ \<squnion> B) = ⌊{a}⌋ \<squnion> (A \<squnion> B)"
by(simp add:hyperset_defs)
subsection "Definite assignment"
primrec
\<A> :: "'a exp => 'a hyperset"
and \<A>s :: "'a exp list => 'a hyperset"
where
"\<A> (new C) = ⌊{}⌋"
| "\<A> (Cast C e) = \<A> e"
| "\<A> (Val v) = ⌊{}⌋"
| "\<A> (e⇣1 «bop» e⇣2) = \<A> e⇣1 \<squnion> \<A> e⇣2"
| "\<A> (Var V) = ⌊{}⌋"
| "\<A> (LAss V e) = ⌊{V}⌋ \<squnion> \<A> e"
| "\<A> (e•F{D}) = \<A> e"
| "\<A> (e⇣1•F{D}:=e⇣2) = \<A> e⇣1 \<squnion> \<A> e⇣2"
| "\<A> (e•M(es)) = \<A> e \<squnion> \<A>s es"
| "\<A> ({V:T; e}) = \<A> e \<ominus> V"
| "\<A> (e⇣1;;e⇣2) = \<A> e⇣1 \<squnion> \<A> e⇣2"
| "\<A> (if (e) e⇣1 else e⇣2) = \<A> e \<squnion> (\<A> e⇣1 \<sqinter> \<A> e⇣2)"
| "\<A> (while (b) e) = \<A> b"
| "\<A> (throw e) = None"
| "\<A> (try e⇣1 catch(C V) e⇣2) = \<A> e⇣1 \<sqinter> (\<A> e⇣2 \<ominus> V)"
| "\<A>s ([]) = ⌊{}⌋"
| "\<A>s (e#es) = \<A> e \<squnion> \<A>s es"
primrec
\<D> :: "'a exp => 'a hyperset => bool"
and \<D>s :: "'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⇣1 «bop» e⇣2) A = (\<D> e⇣1 A ∧ \<D> e⇣2 (A \<squnion> \<A> e⇣1))"
| "\<D> (Var V) A = (V ∈∈ A)"
| "\<D> (LAss V e) A = \<D> e A"
| "\<D> (e•F{D}) A = \<D> e A"
| "\<D> (e⇣1•F{D}:=e⇣2) A = (\<D> e⇣1 A ∧ \<D> e⇣2 (A \<squnion> \<A> e⇣1))"
| "\<D> (e•M(es)) A = (\<D> e A ∧ \<D>s es (A \<squnion> \<A> e))"
| "\<D> ({V:T; e}) A = \<D> e (A \<ominus> V)"
| "\<D> (e⇣1;;e⇣2) A = (\<D> e⇣1 A ∧ \<D> e⇣2 (A \<squnion> \<A> e⇣1))"
| "\<D> (if (e) e⇣1 else e⇣2) A =
(\<D> e A ∧ \<D> e⇣1 (A \<squnion> \<A> e) ∧ \<D> e⇣2 (A \<squnion> \<A> e))"
| "\<D> (while (e) c) A = (\<D> e A ∧ \<D> c (A \<squnion> \<A> e))"
| "\<D> (throw e) A = \<D> e A"
| "\<D> (try e⇣1 catch(C V) e⇣2) A = (\<D> e⇣1 A ∧ \<D> e⇣2 (A \<squnion> ⌊{V}⌋))"
| "\<D>s ([]) A = True"
| "\<D>s (e#es) A = (\<D> e A ∧ \<D>s es (A \<squnion> \<A> e))"
lemma As_map_Val[simp]: "\<A>s (map Val vs) = ⌊{}⌋"
by (induct vs) simp_all
lemma D_append[iff]: "!!A. \<D>s (es @ es') A = (\<D>s es A ∧ \<D>s es' (A \<squnion> \<A>s es))"
by (induct es type:list) (auto simp:hyperUn_assoc)
lemma A_fv: "!!A. \<A> e = ⌊A⌋ ==> A ⊆ fv e"
and "!!A. \<A>s es = ⌊A⌋ ==> A ⊆ fvs es"
apply(induct e and es)
apply (simp_all add:hyperset_defs)
apply blast+
done
lemma sqUn_lem: "A \<sqsubseteq> A' ==> A \<squnion> B \<sqsubseteq> A' \<squnion> B"
by(simp add:hyperset_defs) blast
lemma diff_lem: "A \<sqsubseteq> A' ==> A \<ominus> b \<sqsubseteq> A' \<ominus> b"
by(simp add:hyperset_defs) blast
lemma D_mono: "!!A A'. A \<sqsubseteq> A' ==> \<D> e A ==> \<D> (e::'a exp) A'"
and Ds_mono: "!!A A'. A \<sqsubseteq> A' ==> \<D>s es A ==> \<D>s (es::'a exp list) A'"
apply(induct e and es)
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 (iprover dest:sqUn_lem)
apply simp
apply simp apply (iprover dest:sqUn_lem)
done
lemma D_mono': "\<D> e A ==> A \<sqsubseteq> A' ==> \<D> e A'"
and Ds_mono': "\<D>s es A ==> A \<sqsubseteq> A' ==> \<D>s es A'"
by(blast intro:D_mono, blast intro:Ds_mono)
end