theory PG imports Main Nat List
begin


(*********************************** PROGRAMS **********************************)

types node = nat


datatype field = ff | fg | fh | Field nat
datatype var = vx | vy | vz | Var nat

datatype st = Copy var var node           ("[_:=_,_]")
            | FLoad var var field node    ("[_=_.._,_]")
            | FStore var field var node   ("[_.._=_,_]")
            | New var node                ("[_=new,_]")
            | Branch node node            ("[?,_,_]")

types prog = "node ~=> st"


(*********************************** RUNTIME ***********************************)

types addr = nat

datatype val = Null
             | Addr addr  ("$_")

types heap = "addr ~=> field \<Rightarrow> val"
types stack = "var ~=> val"


(********************************** SEMANTICS **********************************)

types action = "addr option"

consts filter_addr :: "addr \<Rightarrow> (action list) \<Rightarrow> (action list)"
defs filter_addr[simp]: "filter_addr a A == (map (\<lambda>x. if x=Some a then None else x) A)"

consts accesses :: "(prog *  heap * stack * node * (action list)) \<Rightarrow> bool"
recdef accesses "measure(\<lambda>(P,h,s,n,A). length A)"
       "accesses (P, h, s, n, []) = True"
       "accesses (P, h, s, n, (act#A)) = (case P n of
        Some st \<Rightarrow> (case st of
                [x:=y, n'] \<Rightarrow> (case s y of
                        Some v \<Rightarrow> (act=None) & accesses (P,h,(s(x:=Some v)),n',A)
                      | None \<Rightarrow> False
                )
              | [x=y .. f, n'] \<Rightarrow> (case s y of
                        Some u \<Rightarrow> (case u of
                                $a \<Rightarrow> (case h a of
                                        Some fs \<Rightarrow> ((act=Some a) & accesses (P,h,(s(x:=Some (fs f))),n',A))
                                      | None \<Rightarrow> False
                                )
                              | Null \<Rightarrow> False
                        )
                      | None \<Rightarrow> False
               ) 
              | [x .. f=y, n'] \<Rightarrow> (case s y of
                        Some y' \<Rightarrow> (case s x of
                                Some x' \<Rightarrow> (case x' of
                                        $a \<Rightarrow> (case h a of
                                                Some fs \<Rightarrow> ( (act=Some a) & accesses (P,(h(a:=Some(fs(f:=y')))),s,n',A) )
                                              | None \<Rightarrow> False
                                        )
                                      | Null \<Rightarrow> False
                                )
                              | None \<Rightarrow> False
                        )
                      | None \<Rightarrow> False
                )
              | [x=new,n'] \<Rightarrow> (
                        (act = None) &
                        (\<exists>a.
                                ((h a) = None) &
                                (\<exists>A'.
                                    accesses (P, (h(a:=Some (\<lambda>f. Null))), (s(x:=Some $a)), n', A')
                                    & A = filter_addr a A')


                        )
                )
              | [?,n',n''] \<Rightarrow> (
                        (act = None) &
                        (accesses (P, h, s, n', A) | accesses (P, h, s, n'', A))
                )
        )
      | None \<Rightarrow> False
)" 
(hints recdef_cong: rev_conj_cong)



(* sanity *)

consts MyProg :: prog
defs MyProg_def[simp]: "MyProg == [1\<mapsto>[vx=new,2], 2\<mapsto>[vx:=vy,3], 3\<mapsto>[vz .. ff=vz,4]]"

lemma "(b~=Some a & c~=Some a) \<longrightarrow> (filter_addr a [b,c] = [b,c])"
by simp

lemma "(b~=Some a) \<longrightarrow> (filter_addr a [b,Some a] = [b,None])"
by (simp)

lemma "accesses (MyProg,[a\<mapsto>(\<lambda>f. Null)],[vz\<mapsto>$a],3,[Some a])"
by (simp)

lemma always_another_address1[simp]: "(EX aa::addr . a ~= aa)"
apply(rule_tac x = "Suc(a)" in exI)
apply(simp)
done

lemma always_another_address2[simp]: "(EX aa::addr . aa ~= a)"
apply(rule_tac x = "Suc(a)" in exI)
by (simp)

lemma "accesses (MyProg,[a\<mapsto>(\<lambda>f. Null)],[vz\<mapsto>$a,vy\<mapsto>$b],1,[None,None,Some a])"
apply(auto)
apply(rule_tac ?x="Suc(a)" in exI)
apply(auto)
apply(rule_tac ?x="[None, Some a]" in exI)
apply(simp)
done




(*********************************** ANALYSIS ***********************************)

datatype edge = VarEdge var node           (infix "\<rightarrow>" 100)
              | FieldEdge node field node  ("_\<rightarrow>_\<rightarrow>_" 100)

types pgraph = "edge set"

types analysis = "node \<Rightarrow> pgraph"

consts access:: "node \<Rightarrow> st \<Rightarrow> pgraph"
defs access_def[simp]: "access n st == case st of
        [x:=y,n'] \<Rightarrow> {}
      | [x=y .. f,n'] \<Rightarrow> {y\<rightarrow>n}
      | [x .. f=y,n'] \<Rightarrow> {x\<rightarrow>n}
      | [x=new,n'] \<Rightarrow> {}
      | [?,n',n''] \<Rightarrow> {}"

consts translate:: "node \<Rightarrow> st \<Rightarrow> analysis \<Rightarrow> pgraph"
defs translate_def[simp]: "translate n st X == case st of
        [x:=y,next] \<Rightarrow>    ((X next) - {x\<rightarrow>n' | n'. x\<rightarrow>n'\<in>(X next)})
                                  \<union> {y\<rightarrow>n' | n'. x\<rightarrow>n'\<in>(X next)}

      | [x=y .. f,next] \<Rightarrow> ((X next) - {x\<rightarrow>n' | n'. x\<rightarrow>n'\<in>(X next)})
                                  \<union> {n\<rightarrow>f\<rightarrow>n' | n'. x\<rightarrow>n'\<in>(X next)}

      | [x .. f=y,next] \<Rightarrow> ((X next) - {e. \<exists>n' n''. (e=(n'\<rightarrow>f\<rightarrow>n'')) & x\<rightarrow>n'\<in>(X next)
                                                                    & \<not>(\<exists>z.(z~=x) & z\<rightarrow>n'\<in>(X next))
                                                                    & \<not>(\<exists>n''' f. (n'''\<rightarrow>f\<rightarrow>n')\<in>(X next))})
                                  \<union> {y\<rightarrow>n' | n'. (\<exists>n'' . (n''\<rightarrow>f\<rightarrow>n')\<in>(X next))}

      | [x=new,next] \<Rightarrow>   (X next) - {x\<rightarrow>n' | n'. x\<rightarrow>n'\<in>(X next)}

      | [?,tnext,fnext] \<Rightarrow>   (X tnext) \<union> (X fnext)
" 


consts wfpgraph:: "prog \<Rightarrow> analysis \<Rightarrow> node \<Rightarrow> bool"
defs wfpgraph_def[simp]: "wfpgraph P X n == case P n of
        Some st \<Rightarrow> (X n) = (access n st) \<union> (translate n st X)
      | None \<Rightarrow> True"


consts wfanalysis:: "prog \<Rightarrow> analysis \<Rightarrow> bool"  (infix "\<turnstile>" 95)
defs wfanalysis_def: "P\<turnstile>X == \<forall>n. wfpgraph P X n"


(*
(* sanity *)

consts anal0:: analysis
defs anal0[simp]: "anal0 == \<lambda>n.{}"

lemma "wfanalysis MyProg (anal0(1:={vz\<rightarrow>3}, 2:={vz\<rightarrow>3}, 3:={vz\<rightarrow>3}))"
by (simp add: wfanalysis_def)


lemma "wfanalysis [1\<mapsto>[vy=new,2], 2\<mapsto>[vx:=vy,3], 3\<mapsto>[vx .. f=vz,4]] (anal0(2:={vy\<rightarrow>3}, 3:={vx\<rightarrow>3}))"
by (simp add: wfanalysis_def)


lemma "wfanalysis [1\<mapsto>[vx=new,2], 2\<mapsto>[vx:=vy,3], 3\<mapsto>[vx .. f=vz,4]] (anal0(1:={vy\<rightarrow>3}, 2:={vy\<rightarrow>3}, 3:={vx\<rightarrow>3}))"
by (simp add: wfanalysis_def)
*)



(*********************************** SOUNDNESS ***********************************)

types pgass = "node \<Rightarrow> (addr set)"

consts pgassle :: "pgass \<Rightarrow> pgass \<Rightarrow> bool" (infixl "\<sqsubseteq>" 65 )
defs pgassle_def: "\<phi> \<sqsubseteq> \<phi>' == \<forall>n. (\<phi> n) \<subseteq> (\<phi>' n)"

consts pgassinter :: "pgass \<Rightarrow> pgass \<Rightarrow> pgass" (infixl "\<sqinter>" 65 )
defs pgassinter_def: "\<phi> \<sqinter> \<phi>' == \<lambda>n. (\<phi> n) \<inter> (\<phi>' n)"

consts pgassInter :: "pgass set \<Rightarrow> pgass" ("\<Sqinter> _" 65 )
defs pgassInter_def: "\<Sqinter> \<phi>s == \<lambda>n. \<Inter> { (\<phi> n) | \<phi>. \<phi>\<in>\<phi>s }"

constdefs \<phi>0:: "pgass" 
               "\<phi>0 == \<lambda>n. {}"

lemma \<phi>0_le[simp]: "\<phi>0 \<sqsubseteq> \<phi>"
apply(simp add: pgassle_def \<phi>0_def)
done

lemma \<phi>0_union1[simp]: "\<phi> \<sqinter> \<phi>' \<sqsubseteq> \<phi>"
apply(simp add: pgassinter_def subset_def pgassle_def)
done

lemma \<phi>0_union2[simp]: "\<phi> \<sqinter> \<phi>' \<sqsubseteq> \<phi>'"
apply(simp add: pgassinter_def subset_def pgassle_def)
done

lemma \<phi>0_union_id[simp]: "\<phi> \<sqinter> \<phi> = \<phi>"
apply(simp add: pgassinter_def subset_def)
done

lemma pgass_ref[simp]: "\<phi> \<sqsubseteq> \<phi>"
apply(simp add: pgassle_def)
done

lemma pgass_id[simp]: "\<phi> \<sqsubseteq> \<phi>0 \<Longrightarrow> \<phi>=\<phi>0"
apply(simp add: \<phi>0_def pgassle_def)
apply(rule ext)
apply(auto)
done

consts pgassaddr :: "pgass \<Rightarrow> (addr set)"
defs pgassaddr_def: "pgassaddr \<phi> == {a. \<exists>n. a\<in>(\<phi> n)}"


consts wfpgass :: "heap \<Rightarrow> stack \<Rightarrow> pgraph \<Rightarrow> pgass \<Rightarrow> bool" ("(_,_\<turnstile>_:_)")

defs wfpgass_def: "wfpgass h s G \<phi> ==
    (\<forall>x. \<forall>n. (x\<rightarrow>n)\<in>G \<longrightarrow> (\<exists>x'.((s x) = x') & (\<forall>a.(x'=Some $a)\<longrightarrow>a\<in>(\<phi> n))))
  & (\<forall>f. \<forall>n. \<forall>n'. (n\<rightarrow>f\<rightarrow>n')\<in>G \<longrightarrow>
                        {a. \<exists>a'. a'\<in>(\<phi> n) & (\<exists>fs. ((h a')=Some fs) & ((fs f)=$a))} \<subseteq> (\<phi> n'))"


consts minpgass :: "heap \<Rightarrow> stack \<Rightarrow> pgraph \<Rightarrow> pgass" ("(\<Phi> _ _ _)")
defs minpgass_def: "\<Phi> h s G == \<Sqinter> { \<phi>. wfpgass h s G \<phi> }"


(* sanity *)


lemma "wfpgass [100\<mapsto>(\<lambda>f. Null)(f:=$100)] [vx\<mapsto>$100] {vx\<rightarrow>1,1\<rightarrow>f\<rightarrow>1} ((\<lambda>n.{})(1:={100}))"
apply(simp add:wfpgass_def)
done

lemma "wfpgass [100\<mapsto>((\<lambda>f. Null)(ff:=$101))] empty {1\<rightarrow>ff\<rightarrow>2} ((\<lambda>n.{})(1:={100},2:={101}))"
apply(simp add:wfpgass_def)
done



consts actionlistaddr:: "(action list) \<Rightarrow> (addr set)"
defs actionlistaddr_def: "actionlistaddr A == {a. (Some a) mem A}"



(* sanity *)

lemma "actionlistaddr [Some a, None, Some b, Some b] = {a,b}"
apply(simp add:actionlistaddr_def)
apply(auto)
done




lemma noaction [simp]: "actionlistaddr (None#A) = actionlistaddr A"
apply(simp add: actionlistaddr_def)
done

lemma someaction [simp]: "actionlistaddr ((Some a)#A) = {a} \<union> actionlistaddr A"
apply(simp add: actionlistaddr_def)
apply(auto)
done


lemma wfpgass_preserved_over_subset: "\<lbrakk> G'\<subseteq>G ; wfpgass h s G \<phi> \<rbrakk> \<Longrightarrow> wfpgass h s G' \<phi>"
apply(simp add: wfpgass_def)
apply(blast)
done

(* wellformed assignments can be joined to form another assignment
   ultimately this can help us find a minimal assignment *)
lemma wfpgass_inter: "\<lbrakk> \<forall> \<phi>\<in>\<phi>s. wfpgass h s G \<phi> \<rbrakk> \<Longrightarrow> wfpgass h s G (\<Sqinter> \<phi>s)"
apply(simp add: pgassInter_def subset_def wfpgass_def)
apply(safe)
apply(blast)
apply(blast)
done


(* clearly the smallest valid assignment is valid *)
lemma minpgass_sufficient: "wfpgass h s G (minpgass h s G)"
apply(simp add: minpgass_def)
apply(insert wfpgass_inter)
apply(blast)
done


lemma wfpgass_always_le: "wfpgass h s G \<phi> \<Longrightarrow> (\<exists>\<phi>'. minpgass h s G = \<phi>' \<and> \<phi>'\<sqsubseteq>\<phi>)"
apply(simp add: minpgass_def pgassInter_def pgassle_def)
apply(blast)
done

lemma wfpgass_shrink: "wfpgass h s G \<phi> \<Longrightarrow> (minpgass h s G) \<sqsubseteq> \<phi>"
apply(drule wfpgass_always_le)
apply(blast)
done

lemma source_aux: "\<lbrakk> \<forall>x. x \<rightarrow> n \<in> G \<longrightarrow> s x \<noteq> Some $a;
                   \<forall>n' f. (n'\<rightarrow>f\<rightarrow>n) \<in> G \<longrightarrow> (\<forall>a' fs. h a' = Some fs \<longrightarrow> fs f \<noteq> $a) \<rbrakk> \<Longrightarrow> \<exists>\<phi>. a\<notin>\<phi> n \<and> wfpgass h s G \<phi>"
apply (rule_tac ?x="(\<lambda>n . UNIV)(n:=UNIV-{a})" in exI)
apply (simp add: wfpgass_def)
apply(auto)
done


lemma source: "a\<in>(minpgass h s G) n \<Longrightarrow> (\<exists>x. x\<rightarrow>n\<in>G \<and> (s x = Some $a)) \<or> (\<exists>n' f a' fs. (n'\<rightarrow>f\<rightarrow>n)\<in>G \<and> (h a'=Some fs) \<and> (fs f = $a))"
apply (subgoal_tac "\<forall>h s G n a. a\<in>(minpgass h s G) n \<longrightarrow> (\<exists>x. x\<rightarrow>n\<in>G \<and> (s x = Some $a)) \<or> (\<exists>n' f a' fs. (n'\<rightarrow>f\<rightarrow>n)\<in>G \<and> (h a'=Some fs) \<and> (fs f = $a))")
apply(blast)
apply(thin_tac "a \<in> minpgass h s G n")
apply(simp add: minpgass_def pgassInter_def)
apply(rule classical)
apply(simp)
apply(clarify)
apply(simp)
apply(drule_tac ?h="h" and ?s="s" and ?G="G" in source_aux)
apply(auto)
done


lemma thinactionlistaddr: " actionlistaddr L - {a} \<subseteq> S \<Longrightarrow> actionlistaddr (map ((\<lambda>x. x)(Some a := None)) L) \<subseteq> S"
apply(subgoal_tac "actionlistaddr (map ((\<lambda>x. x)(Some a := None)) L) = actionlistaddr L - {a}")
apply(simp)
apply(simp add: actionlistaddr_def)
apply(thin_tac "{a. Some a mem L} - {a} \<subseteq> S")
apply(induct_tac L)
apply(simp)
apply(simp,blast)
done

theorem soundness: "(accesses (P,h,s,n,A)) \<and> (wfanalysis P X)\<longrightarrow> (actionlistaddr A \<subseteq> pgassaddr (minpgass h s (X n)))"

apply(induct_tac P h s n A rule: accesses.induct)
apply(simp add: actionlistaddr_def)
apply(rule impI|rule allI|erule conjE|rule conjI)+
apply(case_tac "P n")
apply(simp)
apply(rename_tac st)
apply(case_tac st)




(*** x=y ***)
apply(rename_tac x y n')
apply(simp)
apply(fold fun_upd_def)
apply(case_tac "s y")
apply(simp)
apply(rename_tac v)
apply(simp)
apply(erule conjE)
apply(simp add: wfanalysis_def)
apply(drule_tac ?x="n" in spec)
apply(simp)
apply(simp only:minpgass_def pgassInter_def)
apply(erule subset_trans)
apply(simp only:subset_def Ball_def pgassaddr_def wfpgass_def Inter_def)
apply(clarify)
apply(rename_tac a n'')
apply(rule_tac ?x="n''" in exI)
apply(simp)
apply(clarify)
apply(rename_tac z \<phi>)
apply(drule_tac ?x="\<phi> n''" in spec)
apply(erule impE)
apply(rule_tac ?x="\<phi>" in exI)
apply(simp add: wfpgass_def)
apply(rule impI|rule allI|rule conjI|erule conjE)+
apply(rename_tac z n'' a)
apply(case_tac "y=x")
apply(simp)
apply(case_tac "z=x")
apply(simp)
apply(drule_tac ?x="z" in spec)
apply(drule_tac ?x="n''" in spec)
apply(simp)
apply(drule_tac ?x="z" in spec)
apply(drule_tac ?x="n''" in spec)
apply(simp)
apply(assumption)




(*** case x=y.f ***)

apply(simp)
apply(fold fun_upd_def)
apply(rename_tac x y f n')
apply(case_tac "s y")
apply(simp)
apply(simp)
apply(rename_tac yv)
apply(case_tac yv)
apply(simp)
apply(rename_tac targ)
apply(simp)
apply(case_tac "h targ")
apply(simp)
apply(rename_tac fs)
apply(simp)
apply(erule conjE)
apply(subgoal_tac "actionlistaddr A \<subseteq> pgassaddr (minpgass h s (X n))")
apply(rule conjI)
apply(thin_tac "accesses (P, h, s(x \<mapsto> fs f), n', A)")
apply(thin_tac "actionlistaddr A \<subseteq> pgassaddr \<Phi> h s (X n)")
apply(thin_tac "act = Some targ")
apply(thin_tac "actionlistaddr A \<subseteq> pgassaddr (\<Phi> h s(x \<mapsto> fs f) (X n'))")
apply(thin_tac "yv = $targ")
apply(thin_tac "st = [x=y.. f,n']")
apply(thin_tac "h targ = Some fs")
apply(simp add: minpgass_def pgassInter_def wfpgass_def wfanalysis_def pgassaddr_def)
apply(drule_tac ?x="n" in spec)
apply(rule_tac ?x="n" in exI)
apply(simp)
apply(rule allI)
apply(rename_tac addrs)
apply(rule impI)
apply(erule exE)
apply(erule conjE)+
apply(drule_tac ?x="y" in spec)
apply(drule_tac ?x="n" in spec)
apply(erule conjE)+
apply(drule mp)
apply(simp)
apply(simp)
apply(simp)
apply(erule subset_trans)
apply(thin_tac "st = [x=y.. f,n']")
apply(thin_tac "yv = $targ")
apply(thin_tac "act = Some targ")
apply(thin_tac "accesses (P, h, s(x \<mapsto> fs f), n', A)")
apply(simp add: minpgass_def pgassInter_def subset_def pgassaddr_def)
apply(rule allI)
apply(rename_tac a)
apply(rule impI)
apply(erule exE)
apply(rename_tac n'')
apply(rule_tac ?x="n''" in exI)
apply(rule allI)
apply(rename_tac addrs)
apply(rule impI)
apply(drule_tac ?x="addrs" in spec)
apply(erule exE)
apply(rename_tac \<phi>)
apply(drule mp)
apply(rule_tac ?x="\<phi>" in exI)
apply(erule conjE)
apply(erule conjI)
apply(simp add: wfanalysis_def wfpgass_def)
apply(drule_tac ?x="n" in spec,simp)
apply(clarify)
apply(rename_tac z)
apply(rule conjI)
apply(rule impI)
apply(rule allI)
apply(rename_tac n'')
apply(clarify)
apply(drule_tac ?x="f" in spec)
apply(drule_tac ?x="n" in spec)
apply(drule_tac ?x="n''" in spec)
apply(erule conjE)
apply(drule mp)
back
apply(simp)
apply(simp add: subset_def)
apply(drule_tac ?x="a" in spec)
apply(drule mp)
apply(rule_tac ?x="targ" in exI)
apply(rule conjI)
apply(blast)
apply(blast)
apply(assumption)
apply(blast)
apply(assumption)




(*** case x.f=y ***)

apply(rename_tac x f y n')
apply(simp)
apply(fold fun_upd_def)
apply(thin_tac "st = [x..f=y,n']")
apply(case_tac "s y")
apply(simp)
apply(rename_tac yv)
apply(case_tac "s x")
apply(simp)
apply(rename_tac xv)
apply(simp)
apply(case_tac xv)
apply(simp)
apply(rename_tac a)
apply(case_tac "h a")
apply(simp)
apply(rename_tac fs)
apply(simp)
apply(thin_tac "xv = $a")
apply(erule conjE)
apply(subgoal_tac "actionlistaddr A \<subseteq> pgassaddr (minpgass h s (X n)) ")
apply(simp)
apply(simp add: pgassaddr_def minpgass_def pgassInter_def)
apply(rule_tac ?x="n" in exI)
apply(rule allI)
apply(rename_tac addrs)
apply(rule impI)
apply(erule exE)
apply(thin_tac "actionlistaddr A \<subseteq> {aa. \<exists>n. \<forall>x. (\<exists>\<phi>. x = \<phi> n \<and> wfpgass (h(a \<mapsto> fs(f := yv))) s (X n') \<phi>) \<longrightarrow> aa \<in> x}")
apply(thin_tac "s y = Some yv")
apply(thin_tac "h a = Some fs")
apply(thin_tac "act = Some a")
apply(thin_tac "accesses (P,(h(a \<mapsto> fs(f := yv))),s,n',A)")
apply(thin_tac "actionlistaddr A \<subseteq> {a. \<exists>na. \<forall>x. (\<exists>\<phi>. x = \<phi> na \<and> wfpgass h s (X n) \<phi>) \<longrightarrow> a \<in> x}")
apply(erule conjE)
apply(simp add: wfpgass_def wfanalysis_def)
apply(drule_tac ?x="n" in spec)
apply(simp)
apply(blast)
apply(thin_tac "act = Some a")
apply(thin_tac "accesses(P,(h(a \<mapsto> fs(f := yv))),s,n',A)")
apply(erule subset_trans)
apply(simp add:subset_def)
apply(clarify)
apply(rename_tac a')
apply(simp add: pgassaddr_def)
apply(clarify)
apply(rename_tac n'')
apply(rule_tac ?x="n''" in exI)
apply(simp add: minpgass_def pgassInter_def)
apply(clarify)
apply(rename_tac addrs \<phi>)
apply(simp)
apply(drule_tac ?x="(minpgass h s (X n)) n''" in spec)
apply(drule mp)
apply(rule_tac ?x="minpgass h s (X n)" in exI)
apply(simp)
prefer 2
apply(drule wfpgass_shrink)
apply(unfold pgassle_def)
apply(blast)
apply(thin_tac "h,s\<turnstile>X n:\<phi>")
apply(subgoal_tac "h,s\<turnstile>X n:(minpgass h s (X n))")
prefer 2
apply(rule minpgass_sufficient)
apply(simp only: wfanalysis_def wfpgraph_def)
apply(drule_tac ?x="n" in spec)
apply(simp|clarify)+
apply(thin_tac "X n = insert (x \<rightarrow> n)
         (X n' -
          {e. \<exists>n'a. (\<exists>n''. e = (n'a\<rightarrow>f\<rightarrow>n'')) \<and>
                    x \<rightarrow> n'a \<in> X n' \<and> (\<forall>z. z = x \<or> z \<rightarrow> n'a \<notin> X n') \<and> (\<forall>n''' f. (n'''\<rightarrow>f\<rightarrow>n'a) \<notin> X n')} \<union>
          {y \<rightarrow> n'a |n'a. \<exists>n''. (n''\<rightarrow>f\<rightarrow>n'a) \<in> X n'})")
apply(thin_tac "P n = Some [x..f=y,n']")
apply(simp (no_asm_simp) only: wfpgass_def)
apply(clarify|simp)+
apply(intro conjI impI allI)
apply(simp only: wfpgass_def)
apply(clarify|simp)+
apply(rename_tac n1 n2 a2 a1)

apply(case_tac "a1 = a")
apply(simp)
apply(clarify)
apply(simp (no_asm) add: minpgass_def pgassInter_def)
apply(simp (no_asm) only: wfpgass_def)
apply(clarify)
apply(simp (no_asm_simp))
apply(drule_tac ?x="y" in spec)
apply(drule_tac ?x="n2" in spec)
apply(drule mp)
apply(blast)
apply(blast)

apply(simp|clarify)+
apply(rename_tac "fs1")
apply(frule source)
apply(simp|clarify)+
apply(erule disjE)
apply(simp|clarify)+
apply(rename_tac z)
apply(erule disjE)
apply(simp|clarify)+
apply(erule disjE)
apply(simp only: wfpgass_def)
apply(simp|clarify)+
apply(drule_tac ?x="f" in spec)
apply(drule_tac ?x="n1" in spec)
apply(drule_tac ?x="n2" in spec)
apply(simp|clarify)+
apply(drule mp)
apply(subgoal_tac "z\<noteq>x")
apply(blast)
apply(simp|clarify)+
apply(drule_tac ?x="z" in spec)
apply(drule_tac ?x="n1" in spec)
apply(simp|clarify)+
apply(blast)
apply(simp|clarify)+
apply(rename_tac n3)
apply(simp only: wfpgass_def)
apply(simp|clarify)+
apply(drule_tac ?x="f" in spec)
apply(drule_tac ?x="n1" in spec)
apply(drule_tac ?x="n2" in spec)
apply(simp|clarify)+
apply(drule mp)
apply(blast)
apply(blast)
apply(simp|clarify)+
apply(rename_tac n3 f3 a9 fs9)
apply(simp only: wfpgass_def)
apply(erule conjE)
apply(drule_tac ?x="f" in spec)
apply(drule_tac ?x="n1" in spec)
apply(drule_tac ?x="n2" in spec)
apply(drule mp)
back
apply(blast)
apply(simp only: subset_def)
apply(simp only: Ball_def)
apply(drule_tac ?x="a2" in spec)
apply(blast)


apply(rename_tac f0  n1 n2)
apply(clarify|simp)+
apply(rename_tac a2 a1) 
apply(subgoal_tac "a1 \<in> minpgass h s
              (insert (x \<rightarrow> n)
                (X n' -
                 {e. \<exists>n'a. (\<exists>n''. e = (n'a\<rightarrow>f\<rightarrow>n'')) \<and>
                           x \<rightarrow> n'a \<in> X n' \<and>
                           (\<forall>z. z = x \<or> z \<rightarrow> n'a \<notin> X n') \<and> (\<forall>n''' f. (n'''\<rightarrow>f\<rightarrow>n'a) \<notin> X n')} \<union>
                 {y \<rightarrow> n'a |n'a. \<exists>n''. (n''\<rightarrow>f\<rightarrow>n'a) \<in> X n'}))
              n1 \<and>
        (\<exists>fs. (h a1 = Some fs) \<and> (fs f0 = $a2))")

apply(simp|clarify)+
apply(rename_tac fs1)
apply(simp only: wfpgass_def)
apply(simp|clarify)+
apply(drule_tac ?x="f0" in spec)
apply(drule_tac ?x="n1" in spec)
apply(drule_tac ?x="n2" in spec)
apply(blast)
apply(blast)




(*** new ***)

apply(rename_tac x n')
apply(simp)
apply(fold fun_upd_def)
apply(erule conjE)
apply(erule exE)
apply(erule conjE)
apply(erule exE)
apply(rename_tac "A'")
apply(drule_tac ?x="a" in spec)
apply(drule_tac ?x="A'" in spec)
apply(simp)
apply(thin_tac "st = [x=new,n']")
apply(thin_tac "act = None")
apply(thin_tac "h a = None")
apply(erule conjE)
apply(thin_tac "A = map ((\<lambda>x. x)(Some a := None)) A'")
apply(thin_tac "accesses (P, h(a \<mapsto> \<lambda>f. Null), s(x \<mapsto> $a), n', A')")
apply(simp add: wfanalysis_def)
apply(drule_tac ?x="n" in spec)
apply(simp)
apply(thin_tac "P n = Some [x=new,n']")
apply(thin_tac "X n = X n' - {x \<rightarrow> n'a |n'a. x \<rightarrow> n'a \<in> X n'}")
apply(simp)
apply(rule thinactionlistaddr)
apply(simp add: minpgass_def actionlistaddr_def pgassInter_def pgassaddr_def)
apply(simp add: subset_def Ball_def)
apply(intro allI impI)
apply(rename_tac a')
apply(erule conjE)
apply(drule_tac ?x="a'" in spec)
apply(simp)
apply(thin_tac "Some a' mem A'")
apply(erule exE)
apply(rename_tac "n")
apply(rule_tac ?x="n" in exI)
apply(rule allI)
apply(rename_tac "addrs")
apply(rule impI)
apply(drule_tac ?x="addrs \<union> {a}" in spec)
apply(drule mp)
apply(erule exE)
apply(erule conjE)
apply(thin_tac "a' \<noteq> a")
apply(simp)
apply(rule_tac ?x="\<lambda>n.{a} \<union> \<phi> n" in exI)
apply(simp)
apply(clarify)
apply(simp)
apply(unfold wfpgass_def)
apply(rule conjI)
apply(clarify)
apply(simp)
apply(blast)
apply(simp)
apply(blast)
apply(simp)



(*** if ***)

apply(rename_tac n' n'')
apply(simp)
apply(erule conjE)
apply(erule disjE)
apply(thin_tac "accesses (P, h, s, n'', A) \<longrightarrow> actionlistaddr A \<subseteq> pgassaddr \<Phi> h s (X n'')")
apply(simp)
apply(simp add: wfanalysis_def pgassaddr_def)
apply(drule_tac ?x="n" in spec)
apply(simp)
apply(subgoal_tac "{a. \<exists>n. a \<in> (\<Phi> h s (X n')) n} \<subseteq> {a. \<exists>n. a \<in> (\<Phi> h s ((X n') \<union> (X n''))) n}")
apply(blast)
apply(thin_tac "accesses (P, h, s, n', A)")
apply(thin_tac "act = None")
apply(thin_tac "X n = X n' \<union> X n''")
apply(thin_tac "P n = Some [?,n',n'']")
apply(thin_tac "actionlistaddr A \<subseteq> {a. \<exists>n. a \<in> (\<Phi> h s (X n')) n}")
apply(thin_tac "st = [?,n',n'']")
apply(simp add: minpgass_def subset_def pgassInter_def)
apply(clarify)
apply(rule_tac ?x="n" in exI)
apply(clarify)
apply(drule_tac ?x="\<phi> n" in spec)
apply(drule mp)
apply(simp add: subset_def Ball_def)
apply(rule_tac ?x="\<phi>" in exI)
apply(insert wfpgass_preserved_over_subset)
apply(blast)
apply(blast)

apply(thin_tac "accesses (P, h, s, n', A) \<longrightarrow> actionlistaddr A \<subseteq> pgassaddr \<Phi> h s (X n')")
apply(simp)
apply(simp add: wfanalysis_def pgassaddr_def)
apply(drule_tac ?x="n" in spec)
apply(simp)
apply(subgoal_tac "{a. \<exists>n. a \<in> (\<Phi> h s (X n'')) n} \<subseteq> {a. \<exists>n. a \<in> (\<Phi> h s ((X n') \<union> (X n''))) n}")
apply(blast)
apply(thin_tac "accesses (P, h, s, n'', A)")
apply(thin_tac "act = None")
apply(thin_tac "X n = X n' \<union> X n''")
apply(thin_tac "P n = Some [?,n',n'']")
apply(thin_tac "actionlistaddr A \<subseteq> {a. \<exists>n. a \<in> (\<Phi> h s (X n'')) n}")
apply(thin_tac "st = [?,n',n'']")
apply(simp add: minpgass_def subset_def pgassInter_def)
apply(clarify)
apply(rule_tac ?x="n" in exI)
apply(clarify)
apply(drule_tac ?x="\<phi> n" in spec)
apply(drule mp)
apply(simp add: subset_def Ball_def)
apply(rule_tac ?x="\<phi>" in exI)
apply(insert wfpgass_preserved_over_subset)
apply(blast)
apply(blast)

done


end