(* Time-stamp: <Sat Nov 29 2008 01:29:27 Stardate: [-28]0410.10 hwloidl>
   Rules derived from the VDM-style logic in GRUMPY.
   Main rules: ctxtWeak (and variants)
               MUTREClemma
               vdmAdapt
*)

theory VdmDerived = GRUMPY:

subsubsection {* Aux lemmas on pattern binding and constructor allocation (PConInd and ConstrInd) *}

(* aux lemmas on PConInd and ConstrInd *)
(* TODO: redefine PConInd and ConstrInd, and prove these lemmas *)

lemma env_env_notin[rule_format]: "\<forall> rs E E'. (ys, rs, E, E') \<in> PConInd \<longrightarrow> (\<forall> x . x \<notin> set ys \<longrightarrow> E x = E' x)"
(* apply (erule PConInd.induct) *)
apply (induct_tac ys)
apply clarsimp
apply (erule PConInd.cases)
apply clarsimp
apply clarsimp
apply clarsimp
apply (rename_tac y ys rs E E' x)
apply (erule PConInd.cases)
apply clarsimp
apply clarsimp
done

lemma env_env_empty[rule_format]: "([], rs, E, E') \<in> PConInd \<Longrightarrow> E=E'"
apply (erule PConInd.cases)
apply clarsimp
apply clarsimp
done

lemma match_env_notin[rule_format]: "MATCH E, h \<turnstile> PCon CONS xs @ r \<Down> (E', v ) \<Longrightarrow> (\<forall> x. x \<notin> set xs \<longrightarrow> E' x = E x)"
oops

lemma ConstrInd_h_same: "(xs,rs,E,h,h'): ConstrInd \<Longrightarrow> h=h'"
apply (erule ConstrInd.cases)
apply clarsimp
apply clarsimp
done


lemma ConstrInd_same_lengths: "\<forall> rs E h h'. (xs,rs,E,h,h'): ConstrInd \<longrightarrow> length xs = length rs"
apply (induct_tac xs)
apply clarsimp
apply (erule ConstrInd.cases)
apply clarsimp
apply clarsimp
apply clarsimp
apply (erule ConstrInd.cases)
apply clarsimp
apply (rename_tac y ys rs E h h' E'a h'a r rs'a x xs)
apply (erule_tac x="rs'a" in allE)
apply clarsimp
done

subsubsection {* Weakening lemmas for contexts *}

lemma ctxtWeak: " G \<rhd> e : P \<Longrightarrow> (G \<union> G') \<rhd> e : P"
apply (erule vdm.induct) 
apply (rule vdmValue)
apply (rule vdmVar)
apply (rule vdmConstr)
apply (rule vdmPrimBin)
apply (rule vdmRPrimBin)
apply (rule vdmIf)
apply simp apply simp
apply (rule vdmLet)
apply simp apply simp
apply (rule vdmCallFun)
apply simp
apply (rule vdmCallVar)
apply simp
apply clarsimp
apply (rule vdmCaseOne)
apply simp
apply simp
apply (rule vdmAx)
apply simp
apply (rule vdmConseq)
apply simp
apply simp
done

lemma ctxtWeakOne: " G \<rhd> e : P \<Longrightarrow> (insert (e,Q) G) \<rhd> e : P"
apply (insert ctxtWeak [of G e P "{(e,Q)}"])
apply fastsimp
done

lemma CtxtWeak: "G \<rhd> e : P \<Longrightarrow> (G \<union> D) \<rhd> e : P"
(*<*)
apply (erule vdm.induct)
apply (rule vdm_pathetic)+
apply (rule vdmIf, simp, simp)
apply (rule vdmLet, simp, simp)
apply (rule vdmCallFun, simp) 
apply (rule vdmCallVar, simp) apply fastsimp
apply (rule vdmCaseOne, simp) apply assumption
apply (rule vdmAx, simp)
apply (rule vdmConseq) apply  clarsimp apply simp
apply (rotate_tac -1)
apply (drule vdmConseq) apply simp apply assumption
done
(*>*)

lemma CtxtWeakSingleton: "G \<rhd> e : P \<Longrightarrow> (insert (ee, Q) G) \<rhd> e : P"
(*<*)by (insert CtxtWeak [of G e P "{(ee,Q)}"], simp)(*>*)

subsubsection {* Cut lemmata *}

(*
lemma cut1:
  "(DD \<rhd> e : Q) \<Longrightarrow>
  (\<forall> G ee P D . (DD = (insert (e', P') G') \<longrightarrow> G \<rhd> e' :P' \<longrightarrow> (G \<subseteq> G') \<longrightarrow> G' \<rhd> e:P))"
*)

lemma cutAux: 
  "(G'' \<rhd> e : P) \<Longrightarrow>
  (\<forall> G e' P' G' . (G'' = (insert (e', P') G') \<longrightarrow> G \<rhd> e' :P' \<longrightarrow> (G \<subseteq> G') \<longrightarrow> G' \<rhd> e:P))"
apply (erule vdm.induct) 
apply (fast intro: vdmValue)
apply (fast intro: vdmVar)
apply (fast intro: vdmConstr)
apply (fast intro: vdmPrimBin)
apply (fast intro: vdmRPrimBin)
(* IF *)
apply clarsimp
apply (erule_tac x="Ga" in allE)
apply (erule_tac x="Ga" in allE)
apply (erule_tac x="e'" in allE)
apply (erule_tac x="e'" in allE)
apply (erule_tac x="P'" in allE)
apply (erule_tac x="P'" in allE)
apply (erule_tac x="G'" in allE)
apply (erule_tac x="G'" in allE)
(*
apply (erule_tac x="insert (e', P') G'" in allE)
apply (erule_tac x="insert (e', P') G'" in allE)
*)
apply clarsimp
apply (rule vdmConseq)
prefer 2
apply (rule vdmIf)
apply simp
apply simp
apply clarsimp
(* LET *)
apply clarsimp
apply (erule_tac x="Ga" in allE)
apply (erule_tac x="Ga" in allE)
apply (erule_tac x="e'" in allE)
apply (erule_tac x="e'" in allE)
apply (erule_tac x="P'" in allE)
apply (erule_tac x="P'" in allE)
apply (erule_tac x="G'" in allE)
apply (erule_tac x="G'" in allE)
apply clarsimp
apply (rule vdmConseq)
prefer 2
apply (rule vdmLet)
apply simp
apply simp
apply clarsimp
(* CallFun *)
apply clarsimp
apply (erule_tac x="Ga" in allE)
apply (erule_tac x="e'" in allE)
apply (erule_tac x="P'" in allE)
apply (erule_tac x="insert (CallFunExp f xs, P) G'" in allE)
apply clarsimp
(*
apply (rule vdmConseq)
prefer 2
*)
apply (rule vdmCallFun)
apply clarsimp
apply (erule impE)
defer 1 (* trivial *)
apply (erule impE)
defer 1 (* trivial *)
apply simp
(* CallVar *)
apply clarsimp
apply (rule vdmCallVar)
apply (simp add: preUnderApp_def)
apply clarsimp
apply (erule_tac x="f" in allE)
apply (erule conjE)
apply (rotate_tac -1)
apply (erule_tac x="Ga" in allE)
apply (rotate_tac -1)
apply (erule_tac x="e'" in allE)
apply (rotate_tac -1)
apply (erule_tac x="P'" in allE)
apply (erule_tac x="insert (CallVarExp x xs, P) G'" in allE)
apply clarsimp
apply (erule impE)
defer 1 (* trivial *)
apply (erule impE)
defer 1 (* trivial *)
apply simp
(* Case *)
apply clarsimp
apply (erule_tac x="Ga" in allE)
apply (erule_tac x="Ga" in allE)
apply (erule_tac x="e'a" in allE)
apply (erule_tac x="e'a" in allE)
apply (erule_tac x="P'a" in allE)
apply (erule_tac x="P'a" in allE)
apply (erule_tac x="G'" in allE)
apply (erule_tac x="G'" in allE)
(*
apply (erule_tac x="insert (e', P') G'" in allE)
apply (erule_tac x="insert (e', P') G'" in allE)
*)
apply clarsimp
apply (rule vdmConseq)
prefer 2
apply (rule vdmCaseOne)
apply simp
apply simp
apply clarsimp
(* Axiom *)
apply clarsimp
apply (case_tac "(e, P) \<in> G'")
 apply simp
 apply (rule vdmAx)
 apply simp
 apply simp
 apply (erule conjE)
defer 1 (* ??? *)
(* Conseq *)
apply clarsimp
apply (rule vdmConseq)
apply clarsimp
apply simp
apply (erule_tac x="Ga" in allE)
apply (erule_tac x="e'" in allE)
apply (erule_tac x="P'" in allE)
apply (erule_tac x="G'" in allE)
apply (erule impE)
apply simp
apply (erule impE)
apply simp
apply simp
apply (drule vdmConseq)
apply (rotate_tac -1)
apply simp
apply simp
(* only trivial sub-goals of some cases above remain *)
apply auto
apply (rotate_tac -1)
apply (erule thin_rl)
apply (subgoal_tac "\<exists> Ga'. Ga \<union> Ga' = G' \<and> Ga \<inter> Ga' = {} ")
apply clarsimp
apply (rule ctxtWeak)
apply simp
apply auto
done

lemma cut: "\<lbrakk> G \<rhd> e' : P' ; (insert (e', P') G) \<rhd> e : P \<rbrakk> \<Longrightarrow> G \<rhd> e : P"
apply (insert cutAux)
apply auto
done


(* ============================================================================= *)
(* TODO: move this into a VDMDerived.thy *)

types funSpecTab_T = "FunName \<Rightarrow> VarName list \<Rightarrow>  Assertion"

consts the_funSpecTab :: "funSpecTab_T"

(* std goodContext0 def; first-order case, ie. only CallFunExp instances in context *)
constdefs goodContext0::"funSpecTab_T \<Rightarrow> Context \<Rightarrow> bool"
"goodContext0 funSpecTab G == 
  (\<forall> e P . (e,P) : G \<longrightarrow> 
    (\<exists> f xs. e = (CallFunExp f xs) \<and> (P = funSpecTab f xs) \<and> 
               (\<forall> ys . (G \<rhd> (snd (funTab f)): 
                           (\<lambda> E h hh v p . \<forall> E'.  (fst (funTab f),ys,E',E):FrameInd  \<longrightarrow>
                                                   (funSpecTab f ys) E' h hh v (p\<smile>tickExp (CallFunExp f ys) RCUndef))))))"

(* std MUTREC *)

text {*This property is preserved when elements are deleted from G.*}

lemma goodContext0_preserved: "\<lbrakk>goodContext0 the_funSpecTab G; (e,Q):G\<rbrakk> \<Longrightarrow> goodContext0 the_funSpecTab (G - {(e,Q)})"
(*<*)
apply (simp add: goodContext0_def, (rule allI)+, rule)
apply (subgoal_tac "(G - {(e,Q)}) \<rhd> e:Q")(*now use the subgoal (G - {(e,Q)}) \<rhd> e:Q to prove the goal*)
apply (subgoal_tac "G = insert (e, Q) (G - {(e, Q)})") prefer 2 apply fast
apply (erule_tac x=ea in allE, erule_tac x=P in allE)
apply (erule impE, simp)
(* apply (erule disjE) *)
(*case call*)
(*
apply (rule disjI1, clarify)
apply (rule_tac x=f in exI, clarsimp)
apply (rule cut, assumption, simp)
apply (erule disjE)
(*case invoke*)
apply (rule disjI2, rule disjI1, clarify)
apply (rule_tac x=A in exI, rule_tac x=m in exI, rule_tac x=y in exI, clarsimp)
apply (erule_tac x=B in allE)
apply (erule_tac x=x in allE)
apply (erule_tac x=C in allE)
apply (rule cut, assumption, simp)
*)
(*case invokestatic*)
apply clarsimp
(*
apply (rule disjI2)
apply (rule disjI2, clarify)
apply (rule_tac x=C in exI, rule_tac x=mn in exI, rule_tac x=y in exI, clarsimp)
*)
apply (rule cut) apply  assumption apply simp
(* now prove the subgoal (G - {(e, Q)}) \<rhd>  e : Q *)
  apply (erule_tac x=e in allE, erule_tac x=Q in allE, simp)
 (*  apply (erule disjE, clarify) *)
  (*case call*)
  apply clarify
  apply (rule vdmCallFun)
  apply (subgoal_tac "G = insert (CallFunExp f xs, the_funSpecTab f xs) (G - {(CallFunExp f xs, the_funSpecTab f xs)})", simp)
  apply fast
(*>*)
done

(* TODO: add cases for partial app to goodContext0 
  apply (erule disjE, clarify)
  (* case invoke *)
  apply (rule vdm_invoke)
  apply clarsimp
  apply (erule_tac x=A in allE, erule_tac x=y in allE, erule_tac x=C in allE)
  apply (subgoal_tac "G = insert (A\<diamondsuit>m(y), vMST A m y) G", simp)
  apply fast
  (* case invokestatic *)
  apply clarsimp
  apply (rule vdm_invokestatic) 
  apply (subgoal_tac "G = ({(C\<bullet>mn(y), sMST C mn y)} \<union> (G - {(C\<bullet>mn(y), sMST C mn y)}))", simp)
  apply fast
done
*)

lemma GoodContextCut: 
"\<lbrakk>goodContext0 the_funSpecTab G; (e,P) : G; D = G - {(e,P)}\<rbrakk> \<Longrightarrow> goodContext0 the_funSpecTab D"
(*<*)by (insert goodContext0_preserved, fast)(*>*)

lemma SetNonSingleton:
  "\<lbrakk>G \<noteq> {(e, P)}; (e, P) \<in> G\<rbrakk> \<Longrightarrow> \<exists>ee Q. (ee, Q) \<noteq> (e, P) \<and> (ee, Q) \<in> G"
by auto

lemma MUTREClemma: 
"\<forall> G . ((finite G \<and> card G = n \<and> goodContext0 the_funSpecTab G \<and> (e,P) : G) \<longrightarrow> {} \<rhd> e:P)"
apply (induct n)
(*case n=0*)
apply clarsimp
(*Case n>0*)
apply clarsimp
apply (case_tac "G = {(e,P)}")
apply clarsimp
apply (erule_tac x="{(e,P)}" in allE)
apply (clarsimp, simp add:goodContext0_def)
apply (erule disjE)? apply  clarsimp
apply (rule vdmCallFun) apply clarsimp
apply (erule disjE)? apply clarsimp?
(*
apply (rule vdm_invoke, clarsimp)
apply clarsimp
apply (rule vdm_invokestatic, clarsimp)
*)
(*Case G has more entries than (e,P)*)
apply (drule SetNonSingleton, assumption) 
(*apply (subgoal_tac "\<exists> ee Q . (ee,Q) \<noteq> (e,P) \<and> (ee,Q) : G")
prefer 2
apply (erule SetNonSingleton, assumption)
apply (rotate_tac 2)
apply ( erule thin_rl)
apply (rotate_tac 1)
apply (erule thin_rl)
apply fastsimp*)
(* use the fact that there is another pair (ee,Q):G*)
apply clarsimp
apply (subgoal_tac "(G - {(ee,Q)}) \<rhd> ee: Q")
apply (erule_tac x="G - {(ee, Q)}" in allE)
apply (rotate_tac -1) apply (erule impE) apply (simp add: goodContext0_preserved)
apply (subgoal_tac "card (G - {(ee, Q)}) = n", simp)
apply (simp add: card_Diff_singleton) 
(*the proof for (G - {(ee, Q)}) \<rhd>  ee : Q *)
apply (rotate_tac -4) apply (erule thin_rl)
apply (simp add: goodContext0_def)
apply (erule_tac x=ee in allE, erule_tac x=Q in allE, simp)
(* apply (erule disjE, clarsimp) *)
  (*case call*)
    apply clarsimp
    apply (rule vdmCallFun)
    apply (subgoal_tac "(insert (CallFunExp f xs, the_funSpecTab f xs) (G - {(CallFunExp f xs, the_funSpecTab f xs)})) = G", simp)
    apply fast
done


lemma goodAdaptCallFun: 
"\<lbrakk> (CallFunExp f ys , the_funSpecTab f ys) : G; goodContext0 the_funSpecTab  G\<rbrakk>
 \<Longrightarrow> G \<rhd> (CallFunExp f ys) :  the_funSpecTab f ys"
by (rule vdmCallFun, simp, rule CtxtWeakSingleton, simp add: goodContext0_def,fastsimp)

                   

(* std Adaptation, using goodContext0 *)

lemma AdaptCallFun[rule_format]: 
 "\<lbrakk> goodContext0 the_funSpecTab G; (CallFunExp f ys , the_funSpecTab f ys) : G \<rbrakk>
  \<Longrightarrow> (G - {(CallFunExp f ys , the_funSpecTab f ys)}) \<rhd> (CallFunExp f zs) : (the_funSpecTab f zs)"
(*<*)
apply (subgoal_tac "goodContext0 the_funSpecTab (G \<union> {(CallFunExp f zs , the_funSpecTab f zs)})")
apply (rule vdmCallFun)
apply (case_tac "ys=zs")
(*case y=z*)
apply (subgoal_tac "G = ({(CallFunExp f zs , the_funSpecTab f zs)} \<union> (G - {(CallFunExp f ys , the_funSpecTab f ys)}))", simp)
  prefer 2 apply fast
  apply (simp add: goodContext0_def)
  apply (erule_tac x="CallFunExp f zs" in allE, erule_tac x="the_funSpecTab f zs" in allE, clarsimp)
apply (rule cut)
apply (subgoal_tac "(insert (CallFunExp f zs , the_funSpecTab f zs) (G - {(CallFunExp f ys , the_funSpecTab f ys)})) \<rhd>  (CallFunExp f ys) : the_funSpecTab f ys") 
apply assumption
prefer 2 apply (erule thin_rl, simp add: goodContext0_def) 
         apply (erule_tac x="CallFunExp f zs" in allE, erule_tac x="the_funSpecTab f zs" in allE, clarsimp)
         apply (erule_tac x=zs in allE)
         apply (subgoal_tac "insert (CallFunExp f ys , the_funSpecTab f ys) (insert (CallFunExp f zs , the_funSpecTab f zs) (G -{(CallFunExp f ys , the_funSpecTab f ys)})) =
                             insert (CallFunExp f zs , the_funSpecTab f zs) G", clarsimp)
         apply fast
apply (rule vdmCallFun)
apply (subgoal_tac "(insert (CallFunExp f ys , the_funSpecTab f ys) ({(CallFunExp f zs , the_funSpecTab f zs)} \<union> (G - {(CallFunExp f ys , the_funSpecTab f ys)}))) = {(CallFunExp f zs , the_funSpecTab f zs)} \<union> G", simp) prefer 2 apply fast 
apply (erule thin_rl, simp add: goodContext0_def)
apply (subgoal_tac "insert (CallFunExp f ys , the_funSpecTab f ys) ({(CallFunExp f zs , the_funSpecTab f zs)} \<union> (G - {(CallFunExp f ys , the_funSpecTab f ys)}))=
                    insert (CallFunExp f zs , the_funSpecTab f zs) G", simp) prefer 2 apply fast 
apply fast
(*last goal*)
apply (simp add: goodContext0_def,clarsimp)
apply (rule, clarsimp)
(*2 goals*)
(*1*)
  apply (erule_tac x="CallFunExp f ys" in allE, erule_tac x="the_funSpecTab f ys" in allE, clarsimp)
  (* apply (erule impE) apply assumption  *)
  apply (erule_tac x=ysa in allE)
  apply (rule CtxtWeakSingleton)
  apply assumption
(*2*) 
apply rule
apply (erule_tac x=e in allE, erule_tac x=P in allE, erule impE, simp)
apply (erule disjE)?
(*a*) 
(*
  apply (erule exE)+ apply (erule conjE)+ apply (rule disjI1)? apply (rule_tac x=f in exI, simp)
  apply (erule CtxtWeakSingleton)
apply (erule disjE)
*)
(*b*)
 (*
  apply (erule exE)+ apply (erule conjE)+  apply (rule disjI2, rule disjI1)?
  apply (rule_tac x=f in exI, rule_tac x=ma in exI, rule_tac x=ya in exI, clarsimp)
  apply (erule_tac x=B in allE, erule_tac x=x in allE, erule_tac x=C in allE)
  apply (erule CtxtWeakSingleton)
 *)
(*c*) apply (erule exE)+ apply (erule conjE)+   apply (rule disjI2, rule disjI2)?
  apply (rule_tac x=fa in exI, rule_tac x=xs in exI, clarsimp)
  apply (erule_tac x=ysa in allE)
  apply (rule CtxtWeakSingleton)
  apply assumption
(*>*)
done

lemma EmptyProofInvs: "\<lbrakk>goodContext0 the_funSpecTab {((CallFunExp f xs), the_funSpecTab f xs)}\<rbrakk> 
                      \<Longrightarrow> {} \<rhd> (CallFunExp f ys) : the_funSpecTab f ys"
(*<*)
apply (subgoal_tac "({(CallFunExp f xs, the_funSpecTab f xs)} - {(CallFunExp f xs, the_funSpecTab f xs)}) \<rhd> (CallFunExp f ys) : the_funSpecTab f ys")
apply (simp)
apply (erule AdaptCallFun)
apply (simp)
done
(*>*)

(* wasL GCInvs_aux and GCInvs *)

lemma CallFunByGoodCtxt_aux:"\<forall> G f xs. n = card G \<longrightarrow> finite G  \<longrightarrow>  goodContext0 the_funSpecTab G \<longrightarrow> 
                  (CallFunExp f xs, the_funSpecTab f xs) : G \<longrightarrow> goodContext0 the_funSpecTab {(CallFunExp f xs, the_funSpecTab f xs)}"
apply (induct n, safe)
apply (subgoal_tac "card G = 0")
 prefer 2 apply fastsimp
apply (insert card_eq_0_iff)
apply (erule thin_rl)
apply simp
(*
apply (subgoal_tac "finite G")
apply simp
defer 1
*)
apply (case_tac "\<exists> e P. (e,P) : G - {(CallFunExp f xs, the_funSpecTab f xs)}", (erule exE)+)
  apply (erule_tac x="G - {(e,P)}" in allE)
  apply (erule_tac x=f in allE) apply (erule_tac x=xs in allE)
  apply (erule impE)
  apply simp
  apply clarify
  apply (subgoal_tac "card G = Suc n")
   prefer 2 apply simp
  apply (rotate_tac -1)
  apply (frule card_Suc_Diff1)
  apply (rotate_tac -2)
  apply simp
  apply simp
  apply (erule impE) apply simp
  apply (erule impE) apply (erule GoodContextCut) prefer 2 apply simp apply fast
  apply (erule impE) apply fast apply assumption
  (* OTW *)
apply (erule thin_rl)
apply (subgoal_tac "G = {(CallFunExp f xs, the_funSpecTab f xs)}", simp)
apply fast
done

(* ================================================== *)

text {* The adaptation rules for static and virtual methods are proven
  by combining the cut rule, the weakening lemma and the 
  VDM rules for static and virtual method invocation.*}

lemma vdmAdapt: "\<lbrakk>goodContext0 the_funSpecTab G; finite G; (CallFunExp f xs, the_funSpecTab f xs) : G\<rbrakk> \<Longrightarrow> {} \<rhd> (CallFunExp f ys) : the_funSpecTab f ys"
(*<*)
apply (rule EmptyProofInvs)
apply (subgoal_tac "\<exists> n. n = card G", safe)
apply (insert CallFunByGoodCtxt_aux, fast)
apply fastsimp
done
(*>*)

(* this is strong enough to prove the examples, but can't be proven as a derived lemma *)
lemma vdmAxAdapt[rule_format]: 
"\<lbrakk> ((CallFunExp f ys) , P ys) :  G  \<rbrakk>
 \<Longrightarrow> G \<rhd> (CallFunExp f xs) : P xs"
oops

end