equal
deleted
inserted
replaced
3 Copyright 2001 Technische Universitaet Muenchen |
3 Copyright 2001 Technische Universitaet Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header "Example" |
6 header "Example" |
7 |
7 |
8 theory Example imports Equivalence begin |
8 theory Example |
|
9 imports Equivalence |
|
10 begin |
9 |
11 |
10 text {* |
12 text {* |
11 |
13 |
12 \begin{verbatim} |
14 \begin{verbatim} |
13 class Nat { |
15 class Nat { |
87 by (simp add: new_obj_def init_vars_def upd_obj_def Let_def) |
89 by (simp add: new_obj_def init_vars_def upd_obj_def Let_def) |
88 |
90 |
89 |
91 |
90 subsection "``atleast'' relation for interpretation of Nat ``values''" |
92 subsection "``atleast'' relation for interpretation of Nat ``values''" |
91 |
93 |
92 consts Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50) |
94 primrec Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50) where |
93 primrec "s:x\<ge>0 = (x\<noteq>Null)" |
95 "s:x\<ge>0 = (x\<noteq>Null)" |
94 "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)" |
96 | "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)" |
95 |
97 |
96 lemma Nat_atleast_lupd [rule_format, simp]: |
98 lemma Nat_atleast_lupd [rule_format, simp]: |
97 "\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)" |
99 "\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)" |
98 apply (induct n) |
100 apply (induct n) |
99 by auto |
101 by auto |