equal
deleted
inserted
replaced
7 |
7 |
8 theory Example |
8 theory Example |
9 imports Equivalence |
9 imports Equivalence |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text \<open> |
13 |
13 |
14 \begin{verbatim} |
14 \begin{verbatim} |
15 class Nat { |
15 class Nat { |
16 |
16 |
17 Nat pred; |
17 Nat pred; |
37 System.out.println(ok != null); |
37 System.out.println(ok != null); |
38 } |
38 } |
39 } |
39 } |
40 \end{verbatim} |
40 \end{verbatim} |
41 |
41 |
42 *} |
42 \<close> |
43 |
43 |
44 axiomatization where |
44 axiomatization where |
45 This_neq_Par [simp]: "This \<noteq> Par" and |
45 This_neq_Par [simp]: "This \<noteq> Par" and |
46 Res_neq_This [simp]: "Res \<noteq> This" |
46 Res_neq_This [simp]: "Res \<noteq> This" |
47 |
47 |
60 |
60 |
61 abbreviation |
61 abbreviation |
62 one :: expr |
62 one :: expr |
63 where "one == {Nat}new Nat..suc(<>)" |
63 where "one == {Nat}new Nat..suc(<>)" |
64 |
64 |
65 text {* The following properties could be derived from a more complete |
65 text \<open>The following properties could be derived from a more complete |
66 program model, which we leave out for laziness. *} |
66 program model, which we leave out for laziness.\<close> |
67 |
67 |
68 axiomatization where Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)" |
68 axiomatization where Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)" |
69 |
69 |
70 axiomatization where method_Nat_add [simp]: "method Nat add = Some |
70 axiomatization where method_Nat_add [simp]: "method Nat add = Some |
71 \<lparr> par=Class Nat, res=Class Nat, lcl=[], |
71 \<lparr> par=Class Nat, res=Class Nat, lcl=[], |