Theory DefAss

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

header {* \isaheader{Definite assignment} *}

theory DefAss imports Expr begin

subsection "Hypersets"

types 'a hyperset = "'a set option"

constdefs
  hyperUn :: "'a hyperset => 'a hyperset => 'a hyperset"   (infixl "\<squnion>" 65)
  "A \<squnion> B  ≡  case A of None => None
                 | ⌊A⌋ => (case B of None => None | ⌊B⌋ => ⌊A ∪ B⌋)"

  hyperInt :: "'a hyperset => 'a hyperset => 'a hyperset"   (infixl "\<sqinter>" 70)
  "A \<sqinter> B  ≡  case A of None => B
                 | ⌊A⌋ => (case B of None => ⌊A⌋ | ⌊B⌋ => ⌊A ∩ B⌋)"

  hyperDiff1 :: "'a hyperset => 'a => 'a hyperset"   (infixl "\<ominus>" 65)
  "A \<ominus> a  ≡  case A of None => None | ⌊A⌋ => ⌊A - {a}⌋"

 hyper_isin :: "'a => 'a hyperset => bool"   (infix "∈∈" 50)
 "a ∈∈ A  ≡  case A of None => True | ⌊A⌋ => a ∈ A"

  hyper_subset :: "'a hyperset => 'a hyperset => bool"   (infix "\<sqsubseteq>" 50)
  "A \<sqsubseteq> B  ≡  case B of None => True
                 | ⌊B⌋ => (case A of None => False | ⌊A⌋ => A ⊆ B)"

  hyperRestrict :: "'a hyperset => 'a set => 'a hyperset" (infixl "¡" 65)
  "A ¡ B ≡ case A of None => None
                   | ⌊A'⌋ => ⌊A' ∩ B⌋"

lemmas hyperset_defs =
 hyperUn_def hyperInt_def hyperDiff1_def hyper_isin_def hyper_subset_def hyperRestrict_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)(*>*)

lemma [simp]: "None ¡ B = None"
by(simp add: hyperRestrict_def)

lemma [simp]: "⌊A⌋ ¡ B = ⌊A ∩ B⌋"
by(simp add: hyperRestrict_def)

lemma sqSub_lem: "A \<sqsubseteq> A' ==> A ¡ B \<sqsubseteq> A' ¡ B"
by(auto simp add: hyperset_defs)

lemma sqSub_mem_lem [elim]: "[| A \<sqsubseteq> A'; a ∈∈ A |] ==> a ∈∈ A'"
by(auto simp add: hyperset_defs)

lemma [iff]: "A \<sqsubseteq> None"
by(auto simp add: hyperset_defs)

lemma [simp]: "A \<sqsubseteq> A"
by(auto simp add: hyperset_defs)

lemma [iff]: "⌊A⌋ \<sqsubseteq> ⌊B⌋ <-> A ⊆ B"
by(auto simp add: hyperset_defs)

lemma sqUn_lem2: "A \<sqsubseteq> A' ==> B \<squnion> A \<sqsubseteq> B \<squnion> A'"
by(simp add:hyperset_defs) blast

lemma sqSub_trans [trans, intro]: "[| A \<sqsubseteq> B; B \<sqsubseteq> C |] ==> A \<sqsubseteq> C"
by(auto simp add: hyperset_defs)

lemma hyperUn_comm: "A \<squnion> B = B \<squnion> A"
by(auto simp add: hyperset_defs)

lemma hyperUn_leftComm: "A \<squnion> (B \<squnion> C) = B \<squnion> (A \<squnion> C)"
by(auto simp add: hyperset_defs)

lemmas hyperUn_ac = hyperUn_comm hyperUn_leftComm hyperUn_assoc

lemma [simp]: "⌊{}⌋ \<squnion> B = B"
by(auto)

lemma [simp]: "A ¡ B \<sqsubseteq> A"
by(auto simp add: hyperset_defs)

lemma [simp]: "⌊{}⌋ \<sqsubseteq> A"
by(auto simp add: hyperset_defs)

lemma [simp]: "A ¡ B ¡ C = A ¡ (B ∩ C)"
by(auto simp add: hyperRestrict_def)

lemma restrict_lem: "C ⊆ D ==> A \<squnion> B ¡ C \<sqsubseteq> B \<squnion> (A ¡ D)"
by(auto simp add: hyperset_defs)

lemma restrict_lem2: "A ⊆ B ==> C ¡ A \<sqsubseteq> C ¡ B"
by(auto simp add: hyperRestrict_def)

lemma restrict_lem3: "D ⊆ E ==> A \<squnion> (B \<squnion> C) ¡ D \<sqsubseteq> B \<squnion> (C \<squnion> (A ¡ E))"
by(auto simp add: hyperset_defs)

lemma sqInt_lem: "A \<sqsubseteq> A' ==> A \<sqinter> B \<sqsubseteq> A' \<sqinter> B"
by(auto simp add: hyperset_defs)

subsection "Definite assignment"

consts
 \<A>  :: "('a,'b) exp => 'a hyperset"
 \<A>s :: "('a,'b) exp list => 'a hyperset"
 \<D>  :: "('a,'b) exp => 'a hyperset => bool"
 \<D>s :: "('a,'b) exp list => 'a hyperset => bool"

primrec
"\<A> (new C) = ⌊{}⌋"
"\<A> (newA T⌊e⌉) = \<A> e"
"\<A> (Cast C e) = \<A> e"
"\<A> (Val v) = ⌊{}⌋"
"\<A> (e1 «bop» e2) = \<A> e1 \<squnion> \<A> e2"
"\<A> (Var V) = ⌊{}⌋"
"\<A> (LAss V e) = ⌊{V}⌋ \<squnion> \<A> e"
"\<A> (a⌊i⌉) = \<A> a \<squnion> \<A> i"
"\<A> (a⌊i⌉ := e) = \<A> a \<squnion> \<A> i \<squnion> \<A> e"
"\<A> (a•length) = \<A> a"
"\<A> (e•F{D}) = \<A> e"
"\<A> (e1•F{D}:=e2) = \<A> e1 \<squnion> \<A> e2"
"\<A> (e•M(es)) = \<A> e \<squnion> \<A>s es"
"\<A> ({V:T=vo; e}) = \<A> e \<ominus> V"
"\<A> (syncV (o') e) = \<A> o' \<squnion> \<A> e"
"\<A> (insyncV (a) e) = \<A> e"
"\<A> (e1;;e2) = \<A> e1 \<squnion> \<A> e2"
"\<A> (if (e) e1 else e2) =  \<A> e \<squnion> (\<A> e1 \<sqinter> \<A> e2)"
"\<A> (while (b) e) = \<A> b"
"\<A> (throw e) = None"
"\<A> (try e1 catch(C V) e2) = \<A> e1 \<sqinter> (\<A> e2 \<ominus> V)"

"\<A>s ([]) = ⌊{}⌋"
"\<A>s (e#es) = \<A> e \<squnion> \<A>s es"

primrec
"\<D> (new C) A = True"
"\<D> (newA T⌊e⌉) A = \<D> e A"
"\<D> (Cast C e) A = \<D> e A"
"\<D> (Val v) A = True"
"\<D> (e1 «bop» e2) A = (\<D> e1 A ∧ \<D> e2 (A \<squnion> \<A> e1))"
"\<D> (Var V) A = (V ∈∈ A)"
"\<D> (LAss V e) A = \<D> e A"
"\<D> (a⌊i⌉) A = (\<D> a A ∧ \<D> i (A \<squnion> \<A> a))"
"\<D> (a⌊i⌉ := e) A = (\<D> a A ∧ \<D> i (A \<squnion> \<A> a) ∧ \<D> e (A \<squnion> \<A> a \<squnion> \<A> i))"
"\<D> (a•length) A = \<D> a A"
"\<D> (e•F{D}) A = \<D> e A"
"\<D> (e1•F{D}:=e2) A = (\<D> e1 A ∧ \<D> e2 (A \<squnion> \<A> e1))"
"\<D> (e•M(es)) A = (\<D> e A ∧ \<D>s es (A \<squnion> \<A> e))"
"\<D> ({V:T=vo; e}) A = (if vo = None then \<D> e (A \<ominus> V) else \<D> e (A \<squnion> ⌊{V}⌋))"
"\<D> (syncV (o') e) A = (\<D> o' A ∧ \<D> e (A \<squnion> \<A> o'))"
"\<D> (insyncV (a) e) A = \<D> e A"
"\<D> (e1;;e2) A = (\<D> e1 A ∧ \<D> e2 (A \<squnion> \<A> e1))"
"\<D> (if (e) e1 else e2) A =
  (\<D> e A ∧ \<D> e1 (A \<squnion> \<A> e) ∧ \<D> e2 (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 e1 catch(C V) e2) A = (\<D> e1 A ∧ \<D> e2 (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 As_append [simp]: "\<A>s (xs @ ys) = (\<A>s xs) \<squnion> (\<A>s ys)"
by(induct xs, auto simp add: hyperset_defs)

lemma Ds_map_Val[simp]: "\<D>s (map Val vs) A"
(*<*)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
  fixes e :: "('a,'b) exp"
  fixes es :: "('a,'b) exp list"
  shows 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 fast+
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(*>*)

(* This order of the premises avoids looping of the simplifier *)
lemma D_mono: "!!A A'. A \<sqsubseteq> A' ==> \<D> e A ==> \<D> (e::('a,'b) exp) A'"
  and Ds_mono: "!!A A'. A \<sqsubseteq> A' ==> \<D>s es A ==> \<D>s (es::('a,'b) exp list) A'"
(*<*)
apply(induct e and es)
apply simp
apply simp
apply simp
apply simp
apply simp apply (iprover dest:sqUn_lem)
apply (fastsimp simp add:hyperset_defs)
apply simp
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)
apply simp apply (iprover dest:sqUn_lem)
apply(clarsimp split: split_if_asm) apply (iprover dest:diff_lem) apply(iprover dest: sqUn_lem)
apply simp apply (iprover dest:sqUn_lem)
apply simp
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
(*>*)

(* And this is the order of premises preferred during application: *)
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)(*>*)

declare hyperUn_comm [simp]
declare hyperUn_leftComm [simp]

lemma fixes e :: "('a,'b) exp"
  and es :: "('a,'b) exp list"
  shows D_fv: "\<D> e A ==> \<D> e (A ¡ (fv e))"
  and Ds_fvs: "\<D>s es A ==> \<D>s es (A ¡ (fvs es))"
proof(induct e and es arbitrary: A and A)
  case Var thus ?case by(simp add: hyperset_defs)
next
  case Block thus ?case
    by(fastsimp simp add: hyperset_defs simp del: hyperRestrict_def intro: D_mono')
next
  case Synchronized thus ?case by(fastsimp simp add: hyperset_defs simp del: hyperRestrict_def intro: D_mono')
next
  case InSynchronized thus ?case by(fastsimp simp add: hyperset_defs simp del: hyperRestrict_def intro: D_mono')
next
  case TryCatch thus ?case by(fastsimp simp add: hyperset_defs simp del: hyperRestrict_def intro: D_mono')
qed (simp_all, (blast intro: D_mono' Ds_mono' restrict_lem2 restrict_lem restrict_lem3)+)


end