# Theory AxExample

Up to index of Isabelle/HOL/Bali

theory AxExample
imports AxSem Example
begin

    (*  Title:      HOL/Bali/AxExample.thy
        ID:         $Id: AxExample.thy,v 1.11 2005/09/14 08:13:12 haftmann Exp $
        Author:     David von Oheimb
    *)

    header {* Example of a proof based on the Bali axiomatic semantics *}

    theory AxExample imports AxSem Example begin

    constdefs
      arr_inv :: "st => bool"
     "arr_inv ≡ λs. ∃obj a T el. globs s (Stat Base) = Some obj ∧
                                  values obj (Inl (arr, Base)) = Some (Addr a) ∧
                                  heap s a = Some (|tag=Arr T 2,values=el|)),"

    lemma arr_inv_new_obj:
    "!!a. [|arr_inv s; new_Addr (heap s)=Some a|] ==> arr_inv (gupd(Inl a\<mapsto>x) s)"
    apply (unfold arr_inv_def)
    apply (force dest!: new_AddrD2)
    done

    lemma arr_inv_set_locals [simp]: "arr_inv (set_locals l s) = arr_inv s"
    apply (unfold arr_inv_def)
    apply (simp (no_asm))
    done

    lemma arr_inv_gupd_Stat [simp]:
      "Base ≠ C ==> arr_inv (gupd(Stat C\<mapsto>obj) s) = arr_inv s"
    apply (unfold arr_inv_def)
    apply (simp (no_asm_simp))
    done

    lemma ax_inv_lupd [simp]: "arr_inv (lupd(x\<mapsto>y) s) = arr_inv s"
    apply (unfold arr_inv_def)
    apply (simp (no_asm))
    done

    declare split_if_asm [split del]
    declare lvar_def [simp]

    ML {*
    fun inst1_tac s t st = case AList.lookup (op =) (rev (term_varnames (prop_of st))) s of
      SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
    val ax_tac = REPEAT o rtac allI THEN'
                 resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
                             thm "ax_Alloc"::thm "ax_Alloc_Arr"::
                             thm "ax_SXAlloc_Normal"::
                             funpow 7 tl (thms "ax_derivs.intros"))
    *}

    theorem ax_test: "tprg,({}::'a triple set)\<turnstile>
      {Normal (λY s Z::'a. heap_free four s ∧ ¬initd Base s ∧ ¬ initd Ext s)}
      .test [Class Base].
      {λY s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"
    apply (unfold test_def arr_viewed_from_def)
    apply (tactic "ax_tac 1" (*;;*))
    defer (* We begin with the last assertion, to synthesise the intermediate
             assertions, like in the fashion of the weakest
             precondition. *)
    apply  (tactic "ax_tac 1" (* Try *))
    defer
    apply    (tactic {* inst1_tac "Q"
                     "λY s Z. arr_inv (snd s) ∧ tprg,s\<turnstile>catch SXcpt NullPointer" *})
    prefer 2
    apply    simp
    apply   (rule_tac P' = "Normal (λY s Z. arr_inv (snd s))" in conseq1)
    prefer 2
    apply    clarsimp
    apply   (rule_tac Q' = "(λY s Z. ?Q Y s Z)\<leftarrow>=False\<down>=♦" in conseq2)
    prefer 2
    apply    simp
    apply   (tactic "ax_tac 1" (* While *))
    prefer 2
    apply    (rule ax_impossible [THEN conseq1], clarsimp)
    apply   (rule_tac P' = "Normal ?P" in conseq1)
    prefer 2
    apply    clarsimp
    apply   (tactic "ax_tac 1")
    apply   (tactic "ax_tac 1" (* AVar *))
    prefer 2
    apply    (rule ax_subst_Val_allI)
    apply    (tactic {* inst1_tac "P'" "λu a. Normal (?PP a\<leftarrow>?x) u" *})
    apply    (simp del: avar_def2 peek_and_def2)
    apply    (tactic "ax_tac 1")
    apply   (tactic "ax_tac 1")
          (* just for clarification: *)
    apply   (rule_tac Q' = "Normal (λVar:(v, f) u ua. fst (snd (avar tprg (Intg 2) v u)) = Some (Xcpt (Std IndOutBound)))" in conseq2)
    prefer 2
    apply    (clarsimp simp add: split_beta)
    apply   (tactic "ax_tac 1" (* FVar *))
    apply    (tactic "ax_tac 2" (* StatRef *))
    apply   (rule ax_derivs.Done [THEN conseq1])
    apply   (clarsimp simp add: arr_inv_def inited_def in_bounds_def)
    defer
    apply  (rule ax_SXAlloc_catch_SXcpt)
    apply  (rule_tac Q' = "(λY (x, s) Z. x = Some (Xcpt (Std NullPointer)) ∧ arr_inv s) ∧. heap_free two" in conseq2)
    prefer 2
    apply   (simp add: arr_inv_new_obj)
    apply  (tactic "ax_tac 1")
    apply  (rule_tac C = "Ext" in ax_Call_known_DynT)
    apply     (unfold DynT_prop_def)
    apply     (simp (no_asm))
    apply    (intro strip)
    apply    (rule_tac P' = "Normal ?P" in conseq1)
    apply     (tactic "ax_tac 1" (* Methd *))
    apply     (rule ax_thin [OF _ empty_subsetI])
    apply     (simp (no_asm) add: body_def2)
    apply     (tactic "ax_tac 1" (* Body *))
    (* apply       (rule_tac [2] ax_derivs.Abrupt) *)
    defer
    apply      (simp (no_asm))
    apply      (tactic "ax_tac 1") (* Comp *)
                (* The first statement in the  composition
                     ((Ext)z).vee = 1; Return Null
                    will throw an exception (since z is null). So we can handle
                    Return Null with the Abrupt rule *)
    apply       (rule_tac [2] ax_derivs.Abrupt)

    apply      (rule ax_derivs.Expr) (* Expr *)
    apply      (tactic "ax_tac 1") (* Ass *)
    prefer 2
    apply       (rule ax_subst_Var_allI)
    apply       (tactic {* inst1_tac "P'" "λa vs l vf. ?PP a vs l vf\<leftarrow>?x ∧. ?p" *})
    apply       (rule allI)
    apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
    apply       (rule ax_derivs.Abrupt)
    apply      (simp (no_asm))
    apply      (tactic "ax_tac 1" (* FVar *))
    apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
    apply      (tactic "ax_tac 1")
    apply     (tactic {* inst1_tac "R" "λa'. Normal ((λVals:vs (x, s) Z. arr_inv s ∧ inited Ext (globs s) ∧ a' ≠ Null ∧ vs = [Null]) ∧. heap_free two)" *})
    apply     fastsimp
    prefer 4
    apply    (rule ax_derivs.Done [THEN conseq1],force)
    apply   (rule ax_subst_Val_allI)
    apply   (tactic {* inst1_tac "P'" "λu a. Normal (?PP a\<leftarrow>?x) u" *})
    apply   (simp (no_asm) del: peek_and_def2)
    apply   (tactic "ax_tac 1")
    prefer 2
    apply   (rule ax_subst_Val_allI)
    apply    (tactic {* inst1_tac "P'" "λaa v. Normal (?QQ aa v\<leftarrow>?y)" *})
    apply    (simp del: peek_and_def2)
    apply    (tactic "ax_tac 1")
    apply   (tactic "ax_tac 1")
    apply  (tactic "ax_tac 1")
    apply  (tactic "ax_tac 1")
    (* end method call *)
    apply (simp (no_asm))
        (* just for clarification: *)
    apply (rule_tac Q' = "Normal ((λY (x, s) Z. arr_inv s ∧ (∃a. the (locals s (VName e)) = Addr a ∧ obj_class (the (globs s (Inl a))) = Ext ∧
     invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base)
         (|name = foo, parTs = [Class Base]|)), = Ext)) ∧. initd Ext ∧. heap_free two)"
      in conseq2)
    prefer 2
    apply  clarsimp
    apply (tactic "ax_tac 1")
    apply (tactic "ax_tac 1")
    defer
    apply  (rule ax_subst_Var_allI)
    apply  (tactic {* inst1_tac "P'" "λu vf. Normal (?PP vf ∧. ?p) u" *})
    apply  (simp (no_asm) del: split_paired_All peek_and_def2)
    apply  (tactic "ax_tac 1" (* NewC *))
    apply  (tactic "ax_tac 1" (* ax_Alloc *))
         (* just for clarification: *)
    apply  (rule_tac Q' = "Normal ((λY s Z. arr_inv (store s) ∧ vf=lvar (VName e) (store s)) ∧. heap_free tree ∧. initd Ext)" in conseq2)
    prefer 2
    apply   (simp add: invocation_declclass_def dynmethd_def)
    apply   (unfold dynlookup_def)
    apply   (simp add: dynmethd_Ext_foo)
    apply   (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken)
         (* begin init *)
    apply  (rule ax_InitS)
    apply     force
    apply    (simp (no_asm))
    apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
    apply   (rule ax_Init_Skip_lemma)
    apply  (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
    apply  (rule ax_InitS [THEN conseq1] (* init Base *))
    apply      force
    apply     (simp (no_asm))
    apply    (unfold arr_viewed_from_def)
    apply    (rule allI)
    apply    (rule_tac P' = "Normal ?P" in conseq1)
    apply     (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
    apply     (tactic "ax_tac 1")
    apply     (tactic "ax_tac 1")
    apply     (rule_tac [2] ax_subst_Var_allI)
    apply      (tactic {* inst1_tac "P'" "λvf l vfa. Normal (?P vf l vfa)" *})
    apply     (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
    apply      (tactic "ax_tac 2" (* NewA *))
    apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
    apply       (tactic "ax_tac 3")
    apply      (tactic {* inst1_tac "P" "λvf l vfa. Normal (?P vf l vfa\<leftarrow>♦)" *})
    apply      (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
    apply      (tactic "ax_tac 2")
    apply     (tactic "ax_tac 1" (* FVar *))
    apply      (tactic "ax_tac 2" (* StatRef *))
    apply     (rule ax_derivs.Done [THEN conseq1])
    apply     (tactic {* inst1_tac "Q" "λvf. Normal ((λY s Z. vf=lvar (VName e) (snd s)) ∧. heap_free four ∧. initd Base ∧. initd Ext)" *})
    apply     (clarsimp split del: split_if)
    apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
    apply     (drule initedD)
    apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
    apply    force
    apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
    apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
    apply     (rule wf_tprg)
    apply    clarsimp
    apply   (tactic {* inst1_tac "P" "λvf. Normal ((λY s Z. vf = lvar (VName e) (snd s)) ∧. heap_free four ∧. initd Ext)" *})
    apply   clarsimp
    apply  (tactic {* inst1_tac "PP" "λvf. Normal ((λY s Z. vf = lvar (VName e) (snd s)) ∧. heap_free four ∧. Not o initd Base)" *})
    apply  clarsimp
         (* end init *)
    apply (rule conseq1)
    apply (tactic "ax_tac 1")
    apply clarsimp
    done

    (*
    while (true) {
      if (i) {throw xcpt;}
      else i=j
    }
    *)
    lemma Loop_Xcpt_benchmark:
     "Q = (λY (x,s) Z. x ≠ None --> the_Bool (the (locals s i))) ==>
      G,({}::'a triple set)\<turnstile>{Normal (λY s Z::'a. True)}
      .lab1• While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else
            (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}"
    apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=♦" in conseq12)
    apply  safe
    apply  (tactic "ax_tac 1" (* Loop *))
    apply   (rule ax_Normal_cases)
    prefer 2
    apply    (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
    apply   (rule conseq1)
    apply    (tactic "ax_tac 1")
    apply   clarsimp
    prefer 2
    apply  clarsimp
    apply (tactic "ax_tac 1" (* If *))
    apply  (tactic
      {* inst1_tac "P'" "Normal (λs.. (λY s Z. True)\<down>=Val (the (locals s i)))" *})
    apply  (tactic "ax_tac 1")
    apply  (rule conseq1)
    apply   (tactic "ax_tac 1")
    apply  clarsimp
    apply (rule allI)
    apply (rule ax_escape)
    apply auto
    apply  (rule conseq1)
    apply   (tactic "ax_tac 1" (* Throw *))
    apply   (tactic "ax_tac 1")
    apply   (tactic "ax_tac 1")
    apply  clarsimp
    apply (rule_tac Q' = "Normal (λY s Z. True)" in conseq2)
    prefer 2
    apply  clarsimp
    apply (rule conseq1)
    apply  (tactic "ax_tac 1")
    apply  (tactic "ax_tac 1")
    prefer 2
    apply   (rule ax_subst_Var_allI)
    apply   (tactic {* inst1_tac "P'" "λb Y ba Z vf. λY (x,s) Z. x=None ∧ snd vf = snd (lvar i s)" *})
    apply   (rule allI)
    apply   (rule_tac P' = "Normal ?P" in conseq1)
    prefer 2
    apply    clarsimp
    apply   (tactic "ax_tac 1")
    apply   (rule conseq1)
    apply    (tactic "ax_tac 1")
    apply   clarsimp
    apply  (tactic "ax_tac 1")
    apply clarsimp
    done

    end

lemma arr_inv_new_obj:

      [| arr_inv s; new_Addr (heap s) = Some a |]
      ==> arr_inv (gupd(Inl a\<mapsto>x) s)

lemma arr_inv_set_locals:

      arr_inv (set_locals l s) = arr_inv s

lemma arr_inv_gupd_Stat:

      Base ≠ C ==> arr_inv (gupd(Inr C\<mapsto>obj) s) = arr_inv s

lemma ax_inv_lupd:

      arr_inv (lupd(x\<mapsto>y) s) = arr_inv s

theorem ax_test:

      tprg,{}|-{Normal (%Y s Z. heap_free four s ∧ ¬ initd Base s ∧ ¬ initd Ext s)}
      .test [Class Base]. {%Y s Z. fst s = Some (Xcpt (Std IndOutBound))}

lemma Loop_Xcpt_benchmark:

      Q = (%Y (x, s) Z. x ≠ None --> the_Bool (the (locals s i)))
      ==> G,{}|-{Normal (%Y s Z. True)}
          .lab1• While(Lit (Bool True)) (If(Acc (LVar
          i)) Throw (Acc (LVar xcpt)) Else Expr (LVar i:=Acc (LVar j))).
          {Q}