src/HOL/NanoJava/Example.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 44375 dfc2e722fe47
child 58963 26bf09b95dda
permissions -rw-r--r--
modernized header uniformly as section;
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
oheimb@11565
    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
oheimb@11565
    42
*}
oheimb@11565
    43
krauss@44375
    44
axiomatization where
krauss@44375
    45
  This_neq_Par [simp]: "This \<noteq> Par" and
krauss@44375
    46
  Res_neq_This [simp]: "Res  \<noteq> 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
oheimb@11565
    65
text {* The following properties could be derived from a more complete
oheimb@11565
    66
        program model, which we leave out for laziness. *}
oheimb@11565
    67
krauss@44375
    68
axiomatization where Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)"
oheimb@11565
    69
krauss@44375
    70
axiomatization where method_Nat_add [simp]: "method Nat add = Some 
oheimb@11565
    71
  \<lparr> 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 \<rparr>"
oheimb@11565
    75
krauss@44375
    76
axiomatization where method_Nat_suc [simp]: "method Nat suc = Some 
oheimb@11565
    77
  \<lparr> par=NT, res=Class Nat, lcl=[], 
oheimb@11565
    78
   bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>"
oheimb@11565
    79
krauss@44375
    80
axiomatization where field_Nat [simp]: "field Nat = empty(pred\<mapsto>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\<mapsto>(Nat, empty(pred\<mapsto>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 \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50) where
haftmann@39758
    96
  "s:x\<ge>0     = (x\<noteq>Null)"
haftmann@39758
    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)"
oheimb@11565
    98
oheimb@11565
    99
lemma Nat_atleast_lupd [rule_format, simp]: 
berghofe@21020
   100
 "\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> 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
 "\<forall>s v::val. set_locs l s:v \<ge> n = (s:v \<ge> 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
 "\<forall>s v::val. del_locs s:v \<ge> n = (s:v \<ge> 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 \<ge> n \<longrightarrow> 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 \<Longrightarrow> s:Addr a \<ge> n \<longrightarrow> 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
"\<forall>a. s:get_field s a pred \<ge> n \<longrightarrow> heap s a \<noteq> None \<longrightarrow> s:Addr a \<ge> 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 \<Longrightarrow> \<forall>v::val. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> 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
oheimb@11565
   134
apply (tactic "smp_tac 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
  "{} \<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}"
oheimb@12742
   144
apply (rule hoare_ehoare.Meth) (* 1 *)
oheimb@11565
   145
apply clarsimp
oheimb@11565
   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 
oheimb@12934
   147
        Q'= "\<lambda>Z s. s:s<Res> \<ge> 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 = "\<lambda>Z Cm s. s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> 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 = "\<lambda>v s. (s:s<This> \<ge> n \<and> s:s<Par> \<ge> m) \<and> 
oheimb@11565
   156
        (\<exists>a. s<This> = Addr a \<and> 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 = "\<lambda>v   s. (\<forall>m. n = Suc m \<longrightarrow> s:v \<ge> m) \<and> s:s<Par> \<ge> m" and 
oheimb@11565
   170
    R = "\<lambda>T P s. (\<forall>m. n = Suc m \<longrightarrow> s:T \<ge> m) \<and> s:P  \<ge> 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 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+)
oheimb@11565
   187
apply  (clarsimp split add: 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