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