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