author | wenzelm |
Sun, 17 Dec 2023 21:12:18 +0100 | |
changeset 79270 | 90c5aadcc4b2 |
parent 69597 | ff784d5a5bfb |
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 |
|
68778 | 3 |
subsection "Parity Analysis" |
4 |
||
47613 | 5 |
theory Abs_Int1_parity |
6 |
imports Abs_Int1 |
|
7 |
begin |
|
8 |
||
58310 | 9 |
datatype parity = Even | Odd | Either |
47613 | 10 |
|
69597 | 11 |
text\<open>Instantiation of class \<^class>\<open>order\<close> with type \<^typ>\<open>parity\<close>:\<close> |
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 |
||
69505 | 16 |
text\<open>First the definition of the interface function \<open>\<le>\<close>. Note that |
69597 | 17 |
the header of the definition must refer to the ascii name \<^const>\<open>less_eq\<close> of the |
69505 | 18 |
constants as \<open>less_eq_parity\<close> and the definition is named \<open>less_eq_parity_def\<close>. Inside the definition the symbolic names can be used.\<close> |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
19 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
20 |
definition less_eq_parity where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
21 |
"x \<le> y = (y = Either \<or> x=y)" |
47613 | 22 |
|
69505 | 23 |
text\<open>We also need \<open><\<close>, which is defined canonically:\<close> |
47613 | 24 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
25 |
definition less_parity where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
26 |
"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
|
27 |
|
67406 | 28 |
text\<open>\noindent(The type annotation is necessary to fix the type of the polymorphic predicates.) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
29 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
30 |
Now the instance proof, i.e.\ the proof that the definition fulfills |
47613 | 31 |
the axioms (assumptions) of the class. The initial proof-step generates the |
67406 | 32 |
necessary proof obligations.\<close> |
47613 | 33 |
|
34 |
instance |
|
35 |
proof |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
36 |
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
|
37 |
next |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
38 |
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
|
39 |
by(auto simp: less_eq_parity_def) |
47613 | 40 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
41 |
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
|
42 |
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
|
43 |
next |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
44 |
fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def) |
47613 | 45 |
qed |
46 |
||
47 |
end |
|
48 |
||
69597 | 49 |
text\<open>Instantiation of class \<^class>\<open>semilattice_sup_top\<close> with type \<^typ>\<open>parity\<close>:\<close> |
47613 | 50 |
|
51826 | 51 |
instantiation parity :: semilattice_sup_top |
47613 | 52 |
begin |
53 |
||
51389 | 54 |
definition sup_parity where |
51624 | 55 |
"x \<squnion> y = (if x = y then x else Either)" |
47613 | 56 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
57 |
definition top_parity where |
47613 | 58 |
"\<top> = Either" |
59 |
||
67406 | 60 |
text\<open>Now the instance proof. This time we take a shortcut with the help of |
69505 | 61 |
proof method \<open>goal_cases\<close>: it creates cases 1 ... n for the subgoals |
61179 | 62 |
1 ... n; in case i, i is also the name of the assumptions of subgoal i and |
69505 | 63 |
\<open>case?\<close> refers to the conclusion of subgoal i. |
67406 | 64 |
The class axioms are presented in the same order as in the class definition.\<close> |
47613 | 65 |
|
66 |
instance |
|
61179 | 67 |
proof (standard, goal_cases) |
68 |
case 1 (*sup1*) show ?case by(auto simp: less_eq_parity_def sup_parity_def) |
|
47613 | 69 |
next |
61179 | 70 |
case 2 (*sup2*) show ?case by(auto simp: less_eq_parity_def sup_parity_def) |
47613 | 71 |
next |
61179 | 72 |
case 3 (*sup least*) thus ?case by(auto simp: less_eq_parity_def sup_parity_def) |
47613 | 73 |
next |
61179 | 74 |
case 4 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def) |
47613 | 75 |
qed |
76 |
||
77 |
end |
|
78 |
||
79 |
||
67406 | 80 |
text\<open>Now we define the functions used for instantiating the abstract |
47613 | 81 |
interpretation locales. Note that the Isabelle terminology is |
82 |
\emph{interpretation}, not \emph{instantiation} of locales, but we use |
|
67406 | 83 |
instantiation to avoid confusion with abstract interpretation.\<close> |
47613 | 84 |
|
85 |
fun \<gamma>_parity :: "parity \<Rightarrow> val set" where |
|
86 |
"\<gamma>_parity Even = {i. i mod 2 = 0}" | |
|
87 |
"\<gamma>_parity Odd = {i. i mod 2 = 1}" | |
|
88 |
"\<gamma>_parity Either = UNIV" |
|
89 |
||
90 |
fun num_parity :: "val \<Rightarrow> parity" where |
|
91 |
"num_parity i = (if i mod 2 = 0 then Even else Odd)" |
|
92 |
||
93 |
fun plus_parity :: "parity \<Rightarrow> parity \<Rightarrow> parity" where |
|
94 |
"plus_parity Even Even = Even" | |
|
95 |
"plus_parity Odd Odd = Even" | |
|
96 |
"plus_parity Even Odd = Odd" | |
|
97 |
"plus_parity Odd Even = Odd" | |
|
98 |
"plus_parity Either y = Either" | |
|
99 |
"plus_parity x Either = Either" |
|
100 |
||
67406 | 101 |
text\<open>First we instantiate the abstract value interface and prove that the |
69597 | 102 |
functions on type \<^typ>\<open>parity\<close> have all the necessary properties:\<close> |
47613 | 103 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61671
diff
changeset
|
104 |
global_interpretation Val_semilattice |
47613 | 105 |
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
67406 | 106 |
proof (standard, goal_cases) txt\<open>subgoals are the locale axioms\<close> |
61179 | 107 |
case 1 thus ?case by(auto simp: less_eq_parity_def) |
47613 | 108 |
next |
61179 | 109 |
case 2 show ?case by(auto simp: top_parity_def) |
47613 | 110 |
next |
61179 | 111 |
case 3 show ?case by auto |
112 |
next |
|
113 |
case (4 _ a1 _ a2) thus ?case |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
61890
diff
changeset
|
114 |
by (induction a1 a2 rule: plus_parity.induct) |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
61890
diff
changeset
|
115 |
(auto simp add: mod_add_eq [symmetric]) |
47613 | 116 |
qed |
117 |
||
67406 | 118 |
text\<open>In case 4 we needed to refer to particular variables. |
61179 | 119 |
Writing (i x y z) fixes the names of the variables in case i to be x, y and z |
120 |
in the left-to-right order in which the variables occur in the subgoal. |
|
67406 | 121 |
Underscores are anonymous placeholders for variable names we don't care to fix.\<close> |
61179 | 122 |
|
67406 | 123 |
text\<open>Instantiating the abstract interpretation locale requires no more |
47613 | 124 |
proofs (they happened in the instatiation above) but delivers the |
69505 | 125 |
instantiated abstract interpreter which we call \<open>AI_parity\<close>:\<close> |
47613 | 126 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61671
diff
changeset
|
127 |
global_interpretation Abs_Int |
47613 | 128 |
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
61671
20d4cd2ceab2
prefer "rewrites" and "defines" to note rewrite morphisms
haftmann
parents:
61179
diff
changeset
|
129 |
defines aval_parity = aval' and step_parity = step' and AI_parity = AI |
47613 | 130 |
.. |
131 |
||
132 |
||
133 |
subsubsection "Tests" |
|
134 |
||
135 |
definition "test1_parity = |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51826
diff
changeset
|
136 |
''x'' ::= N 1;; |
47613 | 137 |
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)" |
56927 | 138 |
value "show_acom (the(AI_parity test1_parity))" |
47613 | 139 |
|
140 |
definition "test2_parity = |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51826
diff
changeset
|
141 |
''x'' ::= N 1;; |
47613 | 142 |
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)" |
143 |
||
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51625
diff
changeset
|
144 |
definition "steps c i = ((step_parity \<top>) ^^ 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 |
||
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61671
diff
changeset
|
158 |
global_interpretation Abs_Int_mono |
47613 | 159 |
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
61179 | 160 |
proof (standard, goal_cases) |
161 |
case (1 _ a1 _ a2) thus ?case |
|
52525 | 162 |
by(induction a1 a2 rule: plus_parity.induct) |
163 |
(auto simp add:less_eq_parity_def) |
|
47613 | 164 |
qed |
165 |
||
166 |
definition m_parity :: "parity \<Rightarrow> nat" where |
|
51389 | 167 |
"m_parity x = (if x = Either then 0 else 1)" |
47613 | 168 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61671
diff
changeset
|
169 |
global_interpretation Abs_Int_measure |
47613 | 170 |
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
49433 | 171 |
and m = m_parity and h = "1" |
61179 | 172 |
proof (standard, goal_cases) |
173 |
case 1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def) |
|
47613 | 174 |
next |
61179 | 175 |
case 2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def) |
47613 | 176 |
qed |
177 |
||
178 |
thm AI_Some_measure |
|
179 |
||
180 |
end |