# Theory Example

Up to index of Isabelle/HOL/NanoJava

theory Example
imports Equivalence
begin

    (*  Title:      HOL/NanoJava/Example.thy
        ID:         $Id: Example.thy,v 1.5 2005/06/17 14:13:09 haftmann Exp $
        Author:     David von Oheimb
        Copyright   2001 Technische Universitaet Muenchen
    *)

    header "Example"

    theory Example imports Equivalence begin

    text {*

    \begin{verbatim}
    class Nat {

      Nat pred;

      Nat suc()
        { Nat n = new Nat(); n.pred = this; return n; }

      Nat eq(Nat n)
        { if (this.pred != null) if (n.pred != null) return this.pred.eq(n.pred);
                                 else return n.pred; // false
          else if (n.pred != null) return this.pred; // false
               else return this.suc(); // true
        }

      Nat add(Nat n)
        { if (this.pred != null) return this.pred.add(n.suc()); else return n; }

      public static void main(String[] args) // test x+1=1+x
        {
            Nat one = new Nat().suc();
            Nat x   = new Nat().suc().suc().suc().suc();
            Nat ok = x.suc().eq(x.add(one));
            System.out.println(ok != null);
        }
    }
    \end{verbatim}

    *}

    axioms This_neq_Par [simp]: "This ≠ Par"
           Res_neq_This [simp]: "Res  ≠ This"

    subsection "Program representation"

    consts N    :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *)
    consts pred :: fname
    consts suc  :: mname
           add  :: mname
    consts any  :: vname
    syntax dummy:: expr ("<>")
           one  :: expr
    translations
          "<>"  == "LAcc any"
          "one" == "{Nat}new Nat..suc(<>)"

    text {* The following properties could be derived from a more complete
            program model, which we leave out for laziness. *}

    axioms Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)"

    axioms method_Nat_add [simp]: "method Nat add = Some
      (| par=Class Nat, res=Class Nat, lcl=[],
       bdy= If((LAcc This..pred))
              (Res :== {Nat}(LAcc This..pred)..add({Nat}LAcc Par..suc(<>)))
            Else Res :== LAcc Par |)),"

    axioms method_Nat_suc [simp]: "method Nat suc = Some
      (| par=NT, res=Class Nat, lcl=[],
       bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This |)),"

    axioms field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)"

    lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s"
    by (simp add: init_locs_def init_vars_def)

    lemma init_locs_Nat_suc [simp]: "init_locs Nat suc s = s"
    by (simp add: init_locs_def init_vars_def)

    lemma upd_obj_new_obj_Nat [simp]:
      "upd_obj a pred v (new_obj a Nat s) = hupd(a\<mapsto>(Nat, empty(pred\<mapsto>v))) s"
    by (simp add: new_obj_def init_vars_def upd_obj_def Let_def)

    subsection "``atleast'' relation for interpretation of Nat ``values''"

    consts Nat_atleast :: "state => val => nat => bool" ("_:_ ≥ _" [51, 51, 51] 50)
    primrec "s:x≥0     = (x≠Null)"
            "s:x≥Suc n = (∃a. x=Addr a ∧ heap s a ≠ None ∧ s:get_field s a pred≥n)"

    lemma Nat_atleast_lupd [rule_format, simp]:
     "∀s v. lupd(x\<mapsto>y) s:v ≥ n = (s:v ≥ n)"
    apply (induct n)
    by  auto

    lemma Nat_atleast_set_locs [rule_format, simp]:
     "∀s v. set_locs l s:v ≥ n = (s:v ≥ n)"
    apply (induct n)
    by auto

    lemma Nat_atleast_del_locs [rule_format, simp]:
     "∀s v. del_locs s:v ≥ n = (s:v ≥ n)"
    apply (induct n)
    by auto

    lemma Nat_atleast_NullD [rule_format]: "s:Null ≥ n --> False"
    apply (induct n)
    by auto

    lemma Nat_atleast_pred_NullD [rule_format]:
    "Null = get_field s a pred ==> s:Addr a ≥ n --> n = 0"
    apply (induct n)
    by (auto dest: Nat_atleast_NullD)

    lemma Nat_atleast_mono [rule_format]:
    "∀a. s:get_field s a pred ≥ n --> heap s a ≠ None --> s:Addr a ≥ n"
    apply (induct n)
    by auto

    lemma Nat_atleast_newC [rule_format]:
      "heap s aa = None ==> ∀v. s:v ≥ n --> hupd(aa\<mapsto>obj) s:v ≥ n"
    apply (induct n)
    apply  auto
    apply  (case_tac "aa=a")
    apply   auto
    apply (tactic "smp_tac 1 1")
    apply (case_tac "aa=a")
    apply  auto
    done

    subsection "Proof(s) using the Hoare logic"

    theorem add_homomorph_lb:
      "{} \<turnstile> {λs. s:s<This> ≥ X ∧ s:s<Par> ≥ Y} Meth(Nat,add) {λs. s:s<Res> ≥ X+Y}"
    apply (rule hoare_ehoare.Meth) (* 1 *)
    apply clarsimp
    apply (rule_tac P'= "λZ s. (s:s<This> ≥ fst Z ∧ s:s<Par> ≥ snd Z) ∧ D=Nat" and
            Q'= "λZ s. s:s<Res> ≥ fst Z+snd Z" in AxSem.Conseq)
    prefer 2
    apply  (clarsimp simp add: init_locs_def init_vars_def)
    apply rule
    apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
    apply (rule_tac P = "λZ Cm s. s:s<This> ≥ fst Z ∧ s:s<Par> ≥ snd Z" in AxSem.Impl1)
    apply (clarsimp simp add: body_def)  (* 4 *)
    apply (rename_tac n m)
    apply (rule_tac Q = "λv s. (s:s<This> ≥ n ∧ s:s<Par> ≥ m) ∧
            (∃a. s<This> = Addr a ∧ v = get_field s a pred)" in hoare_ehoare.Cond)
    apply  (rule hoare_ehoare.FAcc)
    apply  (rule eConseq1)
    apply   (rule hoare_ehoare.LAcc)
    apply  fast
    apply auto
    prefer 2
    apply  (rule hoare_ehoare.LAss)
    apply  (rule eConseq1)
    apply   (rule hoare_ehoare.LAcc)
    apply  (auto dest: Nat_atleast_pred_NullD)
    apply (rule hoare_ehoare.LAss)
    apply (rule_tac
        Q = "λv   s. (∀m. n = Suc m --> s:v ≥ m) ∧ s:s<Par> ≥ m" and
        R = "λT P s. (∀m. n = Suc m --> s:T ≥ m) ∧ s:P  ≥ Suc m"
        in hoare_ehoare.Call) (* 13 *)
    apply   (rule hoare_ehoare.FAcc)
    apply   (rule eConseq1)
    apply    (rule hoare_ehoare.LAcc)
    apply   clarify
    apply   (drule sym, rotate_tac -1, frule (1) trans)
    apply   simp
    prefer 2
    apply  clarsimp
    apply  (rule hoare_ehoare.Meth) (* 17 *)
    apply  clarsimp
    apply  (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
    apply  (rule AxSem.Conseq)
    apply   rule
    apply   (rule hoare_ehoare.Asm) (* 20 *)
    apply   (rule_tac a = "((case n of 0 => 0 | Suc m => m),m+1)" in UN_I, rule+)
    apply  (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono)
    apply rule
    apply (rule hoare_ehoare.Call) (* 21 *)
    apply   (rule hoare_ehoare.LAcc)
    apply  rule
    apply  (rule hoare_ehoare.LAcc)
    apply clarify
    apply (rule hoare_ehoare.Meth) (* 24 *)
    apply clarsimp
    apply  (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
    apply (rule AxSem.Impl1)
    apply (clarsimp simp add: body_def)
    apply (rule hoare_ehoare.Comp) (* 26 *)
    prefer 2
    apply  (rule hoare_ehoare.FAss)
    prefer 2
    apply   rule
    apply   (rule hoare_ehoare.LAcc)
    apply  (rule hoare_ehoare.LAcc)
    apply (rule hoare_ehoare.LAss)
    apply (rule eConseq1)
    apply  (rule hoare_ehoare.NewC) (* 32 *)
    apply (auto dest!: new_AddrD elim: Nat_atleast_newC)
    done

    end

### Program representation

lemma init_locs_Nat_add:

      init_locs Nat add s = s

lemma init_locs_Nat_suc:

      init_locs Nat suc s = s

lemma upd_obj_new_obj_Nat:

      upd_obj a pred v (new_obj a Nat s) = hupd(a|->(Nat, [pred |-> v])) s

### ``atleast'' relation for interpretation of Nat ``values''

lemma Nat_atleast_lupd:

      (lupd(x|->y) s:v ≥ n) = (s:v ≥ n)

lemma Nat_atleast_set_locs:

      (set_locs l s:v ≥ n) = (s:v ≥ n)

lemma Nat_atleast_del_locs:

      (del_locs s:v ≥ n) = (s:v ≥ n)

lemma Nat_atleast_NullD:

      s:Null ≥ n ==> False

lemma Nat_atleast_pred_NullD:

      [| Null = get_field s a pred; s:Addr a ≥ n |] ==> n = 0

lemma Nat_atleast_mono:

      [| s:get_field s a pred ≥ n; heap s a ≠ None |] ==> s:Addr a ≥ n

lemma Nat_atleast_newC:

      [| heap s aa = None; s:v ≥ n |] ==> hupd(aa|->obj) s:v ≥ n

### Proof(s) using the Hoare logic

theorem add_homomorph_lb:

      {} |- {%s. s:s<This> ≥ X ∧ s:s<Par> ≥ Y} Meth (Nat, add) {%s. s:s<Res> ≥ X + Y}