Theory DefAss (Isabelle repository version)

(*  Title:      Jinja/DefAss.thy
    ID:         $Id: DefAss.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Definite assignment} *}

theory DefAss = BigStep:

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)"

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"

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

primrec
"\<A> (new C) = ⌊{}⌋"
"\<A> (Cast C e) = \<A> e"
"\<A> (Val v) = ⌊{}⌋"
"\<A> (e₁ «bop» e₂) = \<A> e₁ \<squnion> \<A> e₂"
"\<A> (Var V) = ⌊{}⌋"
"\<A> (LAss V e) = ⌊{V}⌋ \<squnion> \<A> e"
"\<A> (e\<bullet>F{D}) = \<A> e"
"\<A> (e₁\<bullet>F{D}:=e₂) = \<A> e₁ \<squnion> \<A> e₂"
"\<A> (e\<bullet>M(es)) = \<A> e \<squnion> \<A>s es"
"\<A> ({V:T; e}) = \<A> e \<ominus> V"
"\<A> (e₁;;e₂) = \<A> e₁ \<squnion> \<A> e₂"
"\<A> (if (e) e₁ else e₂) =  \<A> e \<squnion> (\<A> e₁ \<sqinter> \<A> e₂)"
"\<A> (while (b) e) = \<A> b"
"\<A> (throw e) = None"
"\<A> (try e₁ catch(C V) e₂) = \<A> e₁ \<sqinter> (\<A> e₂ \<ominus> V)"

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

primrec
"\<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 \<squnion> \<A> e₁))"
"\<D> (Var V) A = (V ∈∈ A)"
"\<D> (LAss V e) A = \<D> e A"
"\<D> (e\<bullet>F{D}) A = \<D> e A"
"\<D> (e₁\<bullet>F{D}:=e₂) A = (\<D> e₁ A ∧ \<D> e₂ (A \<squnion> \<A> e₁))"
"\<D> (e\<bullet>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₁;;e₂) A = (\<D> e₁ A ∧ \<D> e₂ (A \<squnion> \<A> e₁))"
"\<D> (if (e) e₁ else e₂) A =
  (\<D> e A ∧ \<D> e₁ (A \<squnion> \<A> e) ∧ \<D> e₂ (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₁ catch(C V) e₂) A = (\<D> e₁ A ∧ \<D> e₂ (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(*>*)

(* This order of the premises avoids looping of the simplifier *)
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 (rules dest:sqUn_lem)
apply (fastsimp simp add:hyperset_defs)
apply simp
apply simp
apply simp apply (rules dest:sqUn_lem)
apply simp apply (rules dest:sqUn_lem)
apply simp apply (rules dest:diff_lem)
apply simp apply (rules dest:sqUn_lem)
apply simp apply (rules dest:sqUn_lem)
apply simp apply (rules dest:sqUn_lem)
apply simp
apply simp apply (rules dest:sqUn_lem)
apply simp
apply simp apply (rules 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)(*>*)

(*
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> ⟨e,(h₀,l₀)⟩ => ⟨e',(h₁,l₁)⟩ ==> (!!A. \<A> e = ⌊A⌋ ==> A ⊆ dom l₁)"
and "P \<turnstile> ⟨es,(h₀,l₀)⟩ [=>] ⟨es',(h₁,l₁)⟩ ==> (!!A. \<A>s es = ⌊A⌋ ==> A ⊆ dom l₁)"

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(fastsimp dest!: eval_lcl_incr)
next
  case TryCatch thus ?case by(fastsimp dest!: eval_lcl_incr)
qed auto
*)
end

Hypersets

lemmas hyperset_defs:

  A \<squnion> B ==
  case A of None => None | ⌊A⌋ => case B of None => None | ⌊B⌋ => ⌊A Un B⌋

  A \<sqinter> B ==
  case A of None => B | ⌊A⌋ => case B of None => ⌊A⌋ | ⌊B⌋ => ⌊A Int B⌋

  A \<ominus> a == case A of None => None | ⌊A⌋ => ⌊A - {a}⌋

  a ∈∈ A == option_case True (op : a) A

  A \<sqsubseteq> B ==
  case B of None => True | ⌊B⌋ => case A of None => False | ⌊A⌋ => A <= B

lemma

  ⌊{}⌋ \<squnion> A = A & A \<squnion> ⌊{}⌋ = A

lemma

  ⌊A⌋ \<squnion> ⌊B⌋ = ⌊A Un B⌋ & ⌊A⌋ \<ominus> a = ⌊A - {a}⌋

lemma

  None \<squnion> A = None & A \<squnion> None = None

lemma

  a ∈∈ None & None \<ominus> a = None

lemma hyperUn_assoc:

  A \<squnion> B \<squnion> C = A \<squnion> (B \<squnion> C)

lemma hyper_insert_comm:

  A \<squnion> ⌊{a}⌋ = ⌊{a}⌋ \<squnion> A &
  A \<squnion> (⌊{a}⌋ \<squnion> B) = ⌊{a}⌋ \<squnion> (A \<squnion> B)

Definite assignment

lemma As_map_Val:

  \<A>s (map Val vs) = ⌊{}⌋

lemma D_append:

  \<D>s (es @ es') A = (\<D>s es A & \<D>s es' (A \<squnion> \<A>s es))

lemma A_fv:

  \<A> e = ⌊A⌋ ==> A <= fv e

and

  \<A>s es = ⌊A⌋ ==> A <= fvs es

lemma sqUn_lem:

  A \<sqsubseteq> A' ==> A \<squnion> B \<sqsubseteq> A' \<squnion> B

lemma diff_lem:

  A \<sqsubseteq> A' ==> A \<ominus> b \<sqsubseteq> A' \<ominus> b

lemma D_mono:

  [| A \<sqsubseteq> A'; \<D> e A |] ==> \<D> e A'

and Ds_mono:

  [| A \<sqsubseteq> A'; \<D>s es A |] ==> \<D>s es A'

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'