src/HOL/NanoJava/Example.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63648 f9f3006a5579
child 68451 c34aa23a1fb6
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/NanoJava/Example.thy
     2     Author:     David von Oheimb
     3     Copyright   2001 Technische Universitaet Muenchen
     4 *)
     5 
     6 section "Example"
     7 
     8 theory Example
     9 imports Equivalence
    10 begin
    11 
    12 text \<open>
    13 
    14 \begin{verbatim}
    15 class Nat {
    16 
    17   Nat pred;
    18 
    19   Nat suc() 
    20     { Nat n = new Nat(); n.pred = this; return n; }
    21 
    22   Nat eq(Nat n)
    23     { if (this.pred != null) if (n.pred != null) return this.pred.eq(n.pred);
    24                              else return n.pred; // false
    25       else if (n.pred != null) return this.pred; // false
    26            else return this.suc(); // true
    27     }
    28 
    29   Nat add(Nat n)
    30     { if (this.pred != null) return this.pred.add(n.suc()); else return n; }
    31 
    32   public static void main(String[] args) // test x+1=1+x
    33     {
    34         Nat one = new Nat().suc();
    35         Nat x   = new Nat().suc().suc().suc().suc();
    36         Nat ok = x.suc().eq(x.add(one));
    37         System.out.println(ok != null);
    38     }
    39 }
    40 \end{verbatim}
    41 
    42 \<close>
    43 
    44 axiomatization where
    45   This_neq_Par [simp]: "This \<noteq> Par" and
    46   Res_neq_This [simp]: "Res  \<noteq> This"
    47 
    48 
    49 subsection "Program representation"
    50 
    51 axiomatization 
    52   N    :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *)
    53   and pred :: fname
    54   and suc add :: mname
    55   and any  :: vname
    56 
    57 abbreviation
    58   dummy :: expr ("<>")
    59   where "<> == LAcc any"
    60 
    61 abbreviation
    62   one :: expr
    63   where "one == {Nat}new Nat..suc(<>)"
    64 
    65 text \<open>The following properties could be derived from a more complete
    66         program model, which we leave out for laziness.\<close>
    67 
    68 axiomatization where Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)"
    69 
    70 axiomatization where method_Nat_add [simp]: "method Nat add = Some 
    71   \<lparr> par=Class Nat, res=Class Nat, lcl=[], 
    72    bdy= If((LAcc This..pred)) 
    73           (Res :== {Nat}(LAcc This..pred)..add({Nat}LAcc Par..suc(<>))) 
    74         Else Res :== LAcc Par \<rparr>"
    75 
    76 axiomatization where method_Nat_suc [simp]: "method Nat suc = Some 
    77   \<lparr> par=NT, res=Class Nat, lcl=[], 
    78    bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>"
    79 
    80 axiomatization where field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)"
    81 
    82 lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s"
    83 by (simp add: init_locs_def init_vars_def)
    84 
    85 lemma init_locs_Nat_suc [simp]: "init_locs Nat suc s = s"
    86 by (simp add: init_locs_def init_vars_def)
    87 
    88 lemma upd_obj_new_obj_Nat [simp]: 
    89   "upd_obj a pred v (new_obj a Nat s) = hupd(a\<mapsto>(Nat, empty(pred\<mapsto>v))) s"
    90 by (simp add: new_obj_def init_vars_def upd_obj_def Let_def)
    91 
    92 
    93 subsection "``atleast'' relation for interpretation of Nat ``values''"
    94 
    95 primrec Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50) where
    96   "s:x\<ge>0     = (x\<noteq>Null)"
    97 | "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
    98 
    99 lemma Nat_atleast_lupd [rule_format, simp]: 
   100  "\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
   101 apply (induct n)
   102 by  auto
   103 
   104 lemma Nat_atleast_set_locs [rule_format, simp]: 
   105  "\<forall>s v::val. set_locs l s:v \<ge> n = (s:v \<ge> n)"
   106 apply (induct n)
   107 by auto
   108 
   109 lemma Nat_atleast_del_locs [rule_format, simp]: 
   110  "\<forall>s v::val. del_locs s:v \<ge> n = (s:v \<ge> n)"
   111 apply (induct n)
   112 by auto
   113 
   114 lemma Nat_atleast_NullD [rule_format]: "s:Null \<ge> n \<longrightarrow> False"
   115 apply (induct n)
   116 by auto
   117 
   118 lemma Nat_atleast_pred_NullD [rule_format]: 
   119 "Null = get_field s a pred \<Longrightarrow> s:Addr a \<ge> n \<longrightarrow> n = 0"
   120 apply (induct n)
   121 by (auto dest: Nat_atleast_NullD)
   122 
   123 lemma Nat_atleast_mono [rule_format]: 
   124 "\<forall>a. s:get_field s a pred \<ge> n \<longrightarrow> heap s a \<noteq> None \<longrightarrow> s:Addr a \<ge> n"
   125 apply (induct n)
   126 by auto
   127 
   128 lemma Nat_atleast_newC [rule_format]: 
   129   "heap s aa = None \<Longrightarrow> \<forall>v::val. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> n"
   130 apply (induct n)
   131 apply  auto
   132 apply  (case_tac "aa=a")
   133 apply   auto
   134 apply (tactic "smp_tac @{context} 1 1")
   135 apply (case_tac "aa=a")
   136 apply  auto
   137 done
   138 
   139 
   140 subsection "Proof(s) using the Hoare logic"
   141 
   142 theorem add_homomorph_lb: 
   143   "{} \<turnstile> {\<lambda>s. s:s<This> \<ge> X \<and> s:s<Par> \<ge> Y} Meth(Nat,add) {\<lambda>s. s:s<Res> \<ge> X+Y}"
   144 apply (rule hoare_ehoare.Meth) (* 1 *)
   145 apply clarsimp
   146 apply (rule_tac P'= "\<lambda>Z s. (s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z) \<and> D=Nat" and 
   147         Q'= "\<lambda>Z s. s:s<Res> \<ge> fst Z+snd Z" in AxSem.Conseq)
   148 prefer 2
   149 apply  (clarsimp simp add: init_locs_def init_vars_def)
   150 apply rule
   151 apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
   152 apply (rule_tac P = "\<lambda>Z Cm s. s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z" in AxSem.Impl1)
   153 apply (clarsimp simp add: body_def)  (* 4 *)
   154 apply (rename_tac n m)
   155 apply (rule_tac Q = "\<lambda>v s. (s:s<This> \<ge> n \<and> s:s<Par> \<ge> m) \<and> 
   156         (\<exists>a. s<This> = Addr a \<and> v = get_field s a pred)" in hoare_ehoare.Cond)
   157 apply  (rule hoare_ehoare.FAcc)
   158 apply  (rule eConseq1)
   159 apply   (rule hoare_ehoare.LAcc)
   160 apply  fast
   161 apply auto
   162 prefer 2
   163 apply  (rule hoare_ehoare.LAss)
   164 apply  (rule eConseq1)
   165 apply   (rule hoare_ehoare.LAcc)
   166 apply  (auto dest: Nat_atleast_pred_NullD)
   167 apply (rule hoare_ehoare.LAss)
   168 apply (rule_tac 
   169     Q = "\<lambda>v   s. (\<forall>m. n = Suc m \<longrightarrow> s:v \<ge> m) \<and> s:s<Par> \<ge> m" and 
   170     R = "\<lambda>T P s. (\<forall>m. n = Suc m \<longrightarrow> s:T \<ge> m) \<and> s:P  \<ge> Suc m" 
   171     in hoare_ehoare.Call) (* 13 *)
   172 apply   (rule hoare_ehoare.FAcc)
   173 apply   (rule eConseq1)
   174 apply    (rule hoare_ehoare.LAcc)
   175 apply   clarify
   176 apply   (drule sym, rotate_tac -1, frule (1) trans)
   177 apply   simp
   178 prefer 2
   179 apply  clarsimp
   180 apply  (rule hoare_ehoare.Meth) (* 17 *)
   181 apply  clarsimp
   182 apply  (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
   183 apply  (rule AxSem.Conseq)
   184 apply   rule
   185 apply   (rule hoare_ehoare.Asm) (* 20 *)
   186 apply   (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+)
   187 apply  (clarsimp split: nat.split_asm dest!: Nat_atleast_mono)
   188 apply rule
   189 apply (rule hoare_ehoare.Call) (* 21 *)
   190 apply   (rule hoare_ehoare.LAcc)
   191 apply  rule
   192 apply  (rule hoare_ehoare.LAcc)
   193 apply clarify
   194 apply (rule hoare_ehoare.Meth) (* 24 *)
   195 apply clarsimp
   196 apply  (case_tac "D = Nat", simp_all, rule_tac [2] cFalse)
   197 apply (rule AxSem.Impl1)
   198 apply (clarsimp simp add: body_def)
   199 apply (rule hoare_ehoare.Comp) (* 26 *)
   200 prefer 2
   201 apply  (rule hoare_ehoare.FAss)
   202 prefer 2
   203 apply   rule
   204 apply   (rule hoare_ehoare.LAcc)
   205 apply  (rule hoare_ehoare.LAcc)
   206 apply (rule hoare_ehoare.LAss)
   207 apply (rule eConseq1)
   208 apply  (rule hoare_ehoare.NewC) (* 32 *)
   209 apply (auto dest!: new_AddrD elim: Nat_atleast_newC)
   210 done
   211 
   212 
   213 end