author | nipkow |
Fri, 08 Mar 2013 11:28:04 +0100 | |
changeset 51372 | d315e9a9ee72 |
parent 51359 | 00b45c7e831f |
child 51389 | 8a9f0503b1c0 |
permissions | -rw-r--r-- |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
1 |
(* Author: Tobias Nipkow *) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
2 |
|
47613 | 3 |
theory Abs_Int1_parity |
4 |
imports Abs_Int1 |
|
5 |
begin |
|
6 |
||
7 |
subsection "Parity Analysis" |
|
8 |
||
9 |
datatype parity = Even | Odd | Either |
|
10 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
11 |
text{* Instantiation of class @{class order} with type @{typ parity}: *} |
47613 | 12 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
13 |
instantiation parity :: order |
47613 | 14 |
begin |
15 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
16 |
text{* First the definition of the interface function @{text"\<le>"}. Note that |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
17 |
the header of the definition must refer to the ascii name @{const less_eq} of the |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
18 |
constants as @{text less_eq_parity} and the definition is named @{text |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
19 |
less_eq_parity_def}. Inside the definition the symbolic names can be used. *} |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
20 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
21 |
definition less_eq_parity where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
22 |
"x \<le> y = (y = Either \<or> x=y)" |
47613 | 23 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
24 |
text{* We also need @{text"<"}, which is defined canonically: *} |
47613 | 25 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
26 |
definition less_parity where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
27 |
"x < y = (x \<le> y \<and> \<not> y \<le> (x::parity))" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
28 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
29 |
text{*\noindent (The type annotation is necessary to fix the type of the polymorphic predicates.) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
30 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
31 |
Now the instance proof, i.e.\ the proof that the definition fulfills |
47613 | 32 |
the axioms (assumptions) of the class. The initial proof-step generates the |
33 |
necessary proof obligations. *} |
|
34 |
||
35 |
instance |
|
36 |
proof |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
37 |
fix x::parity show "x \<le> x" by(auto simp: less_eq_parity_def) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
38 |
next |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
39 |
fix x y z :: parity assume "x \<le> y" "y \<le> z" thus "x \<le> z" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
40 |
by(auto simp: less_eq_parity_def) |
47613 | 41 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
42 |
fix x y :: parity assume "x \<le> y" "y \<le> x" thus "x = y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
43 |
by(auto simp: less_eq_parity_def) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
44 |
next |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
45 |
fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def) |
47613 | 46 |
qed |
47 |
||
48 |
end |
|
49 |
||
49396 | 50 |
text{* Instantiation of class @{class semilattice} with type @{typ parity}: *} |
47613 | 51 |
|
49396 | 52 |
instantiation parity :: semilattice |
47613 | 53 |
begin |
54 |
||
55 |
definition join_parity where |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
56 |
"x \<squnion> y = (if x \<le> y then y else if y \<le> x then x else Either)" |
47613 | 57 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
58 |
definition top_parity where |
47613 | 59 |
"\<top> = Either" |
60 |
||
61 |
text{* Now the instance proof. This time we take a lazy shortcut: we do not |
|
62 |
write out the proof obligations but use the @{text goali} primitive to refer |
|
63 |
to the assumptions of subgoal i and @{text "case?"} to refer to the |
|
64 |
conclusion of subgoal i. The class axioms are presented in the same order as |
|
65 |
in the class definition. *} |
|
66 |
||
67 |
instance |
|
68 |
proof |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
69 |
case goal1 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def) |
47613 | 70 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
71 |
case goal2 (*join1*) show ?case by(auto simp: less_eq_parity_def join_parity_def) |
47613 | 72 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
73 |
case goal3 (*join2*) show ?case by(auto simp: less_eq_parity_def join_parity_def) |
47613 | 74 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
75 |
case goal4 (*join least*) thus ?case by(auto simp: less_eq_parity_def join_parity_def) |
47613 | 76 |
qed |
77 |
||
78 |
end |
|
79 |
||
80 |
||
81 |
text{* Now we define the functions used for instantiating the abstract |
|
82 |
interpretation locales. Note that the Isabelle terminology is |
|
83 |
\emph{interpretation}, not \emph{instantiation} of locales, but we use |
|
84 |
instantiation to avoid confusion with abstract interpretation. *} |
|
85 |
||
86 |
fun \<gamma>_parity :: "parity \<Rightarrow> val set" where |
|
87 |
"\<gamma>_parity Even = {i. i mod 2 = 0}" | |
|
88 |
"\<gamma>_parity Odd = {i. i mod 2 = 1}" | |
|
89 |
"\<gamma>_parity Either = UNIV" |
|
90 |
||
91 |
fun num_parity :: "val \<Rightarrow> parity" where |
|
92 |
"num_parity i = (if i mod 2 = 0 then Even else Odd)" |
|
93 |
||
94 |
fun plus_parity :: "parity \<Rightarrow> parity \<Rightarrow> parity" where |
|
95 |
"plus_parity Even Even = Even" | |
|
96 |
"plus_parity Odd Odd = Even" | |
|
97 |
"plus_parity Even Odd = Odd" | |
|
98 |
"plus_parity Odd Even = Odd" | |
|
99 |
"plus_parity Either y = Either" | |
|
100 |
"plus_parity x Either = Either" |
|
101 |
||
102 |
text{* First we instantiate the abstract value interface and prove that the |
|
103 |
functions on type @{typ parity} have all the necessary properties: *} |
|
104 |
||
105 |
interpretation Val_abs |
|
106 |
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
|
107 |
proof txt{* of the locale axioms *} |
|
108 |
fix a b :: parity |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
109 |
assume "a \<le> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
110 |
by(auto simp: less_eq_parity_def) |
47613 | 111 |
next txt{* The rest in the lazy, implicit way *} |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
112 |
case goal2 show ?case by(auto simp: top_parity_def) |
47613 | 113 |
next |
114 |
case goal3 show ?case by auto |
|
115 |
next |
|
116 |
txt{* Warning: this subproof refers to the names @{text a1} and @{text a2} |
|
117 |
from the statement of the axiom. *} |
|
118 |
case goal4 thus ?case |
|
119 |
proof(cases a1 a2 rule: parity.exhaust[case_product parity.exhaust]) |
|
120 |
qed (auto simp add:mod_add_eq) |
|
121 |
qed |
|
122 |
||
123 |
text{* Instantiating the abstract interpretation locale requires no more |
|
124 |
proofs (they happened in the instatiation above) but delivers the |
|
49344 | 125 |
instantiated abstract interpreter which we call @{text AI_parity}: *} |
47613 | 126 |
|
127 |
interpretation Abs_Int |
|
128 |
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
|
129 |
defines aval_parity is aval' and step_parity is step' and AI_parity is AI |
|
130 |
.. |
|
131 |
||
132 |
||
133 |
subsubsection "Tests" |
|
134 |
||
135 |
definition "test1_parity = |
|
136 |
''x'' ::= N 1; |
|
137 |
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)" |
|
50995 | 138 |
value [code] "show_acom (the(AI_parity test1_parity))" |
47613 | 139 |
|
140 |
definition "test2_parity = |
|
141 |
''x'' ::= N 1; |
|
142 |
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)" |
|
143 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
144 |
definition "steps c i = (step_parity(Top(vars c)) ^^ i) (bot c)" |
47613 | 145 |
|
146 |
value "show_acom (steps test2_parity 0)" |
|
147 |
value "show_acom (steps test2_parity 1)" |
|
148 |
value "show_acom (steps test2_parity 2)" |
|
149 |
value "show_acom (steps test2_parity 3)" |
|
150 |
value "show_acom (steps test2_parity 4)" |
|
151 |
value "show_acom (steps test2_parity 5)" |
|
49188 | 152 |
value "show_acom (steps test2_parity 6)" |
50995 | 153 |
value "show_acom (the(AI_parity test2_parity))" |
47613 | 154 |
|
155 |
||
156 |
subsubsection "Termination" |
|
157 |
||
158 |
interpretation Abs_Int_mono |
|
159 |
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
|
160 |
proof |
|
161 |
case goal1 thus ?case |
|
162 |
proof(cases a1 a2 b1 b2 |
|
163 |
rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *) |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
164 |
qed (auto simp add:less_eq_parity_def) |
47613 | 165 |
qed |
166 |
||
167 |
definition m_parity :: "parity \<Rightarrow> nat" where |
|
168 |
"m_parity x = (if x=Either then 0 else 1)" |
|
169 |
||
170 |
interpretation Abs_Int_measure |
|
171 |
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
|
49433 | 172 |
and m = m_parity and h = "1" |
47613 | 173 |
proof |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
174 |
case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def) |
47613 | 175 |
next |
51372 | 176 |
case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def) |
47613 | 177 |
qed |
178 |
||
179 |
thm AI_Some_measure |
|
180 |
||
181 |
end |