39 } |
39 } |
40 \end{verbatim} |
40 \end{verbatim} |
41 |
41 |
42 *} |
42 *} |
43 |
43 |
44 axioms This_neq_Par [simp]: "This \<noteq> Par" |
44 axiomatization where |
45 Res_neq_This [simp]: "Res \<noteq> This" |
45 This_neq_Par [simp]: "This \<noteq> Par" and |
|
46 Res_neq_This [simp]: "Res \<noteq> This" |
46 |
47 |
47 |
48 |
48 subsection "Program representation" |
49 subsection "Program representation" |
49 |
50 |
50 consts N :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *) |
51 axiomatization |
51 consts pred :: fname |
52 N :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *) |
52 consts suc :: mname |
53 and pred :: fname |
53 add :: mname |
54 and suc add :: mname |
54 consts any :: vname |
55 and any :: vname |
55 |
56 |
56 abbreviation |
57 abbreviation |
57 dummy :: expr ("<>") |
58 dummy :: expr ("<>") |
58 where "<> == LAcc any" |
59 where "<> == LAcc any" |
59 |
60 |
62 where "one == {Nat}new Nat..suc(<>)" |
63 where "one == {Nat}new Nat..suc(<>)" |
63 |
64 |
64 text {* The following properties could be derived from a more complete |
65 text {* The following properties could be derived from a more complete |
65 program model, which we leave out for laziness. *} |
66 program model, which we leave out for laziness. *} |
66 |
67 |
67 axioms Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)" |
68 axiomatization where Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)" |
68 |
69 |
69 axioms method_Nat_add [simp]: "method Nat add = Some |
70 axiomatization where method_Nat_add [simp]: "method Nat add = Some |
70 \<lparr> par=Class Nat, res=Class Nat, lcl=[], |
71 \<lparr> par=Class Nat, res=Class Nat, lcl=[], |
71 bdy= If((LAcc This..pred)) |
72 bdy= If((LAcc This..pred)) |
72 (Res :== {Nat}(LAcc This..pred)..add({Nat}LAcc Par..suc(<>))) |
73 (Res :== {Nat}(LAcc This..pred)..add({Nat}LAcc Par..suc(<>))) |
73 Else Res :== LAcc Par \<rparr>" |
74 Else Res :== LAcc Par \<rparr>" |
74 |
75 |
75 axioms method_Nat_suc [simp]: "method Nat suc = Some |
76 axiomatization where method_Nat_suc [simp]: "method Nat suc = Some |
76 \<lparr> par=NT, res=Class Nat, lcl=[], |
77 \<lparr> par=NT, res=Class Nat, lcl=[], |
77 bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>" |
78 bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>" |
78 |
79 |
79 axioms field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)" |
80 axiomatization where field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)" |
80 |
81 |
81 lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s" |
82 lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s" |
82 by (simp add: init_locs_def init_vars_def) |
83 by (simp add: init_locs_def init_vars_def) |
83 |
84 |
84 lemma init_locs_Nat_suc [simp]: "init_locs Nat suc s = s" |
85 lemma init_locs_Nat_suc [simp]: "init_locs Nat suc s = s" |