|
1 theory Abs_Int0_parity |
|
2 imports Abs_Int0 |
|
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 |
|
42 definition join_parity where |
|
43 "x \<squnion> y = (if x \<sqsubseteq> y then y else if y \<sqsubseteq> x then x else Either)" |
|
44 |
|
45 definition Top_parity where |
|
46 "\<top> = Either" |
|
47 |
|
48 text{* Now the instance proof. This time we take a lazy shortcut: we do not |
|
49 write out the proof obligations but use the @{text goali} primitive to refer |
|
50 to the assumptions of subgoal i and @{text "case?"} to refer to the |
|
51 conclusion of subgoal i. The class axioms are presented in the same order as |
|
52 in the class definition. *} |
|
53 |
|
54 instance |
|
55 proof |
|
56 case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def) |
|
57 next |
|
58 case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def) |
|
59 next |
|
60 case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def) |
|
61 next |
|
62 case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def) |
|
63 qed |
|
64 |
|
65 end |
|
66 |
|
67 |
|
68 text{* Now we define the functions used for instantiating the abstract |
|
69 interpretation locales. Note that the Isabelle terminology is |
|
70 \emph{interpretation}, not \emph{instantiation} of locales, but we use |
|
71 instantiation to avoid confusion with abstract interpretation. *} |
|
72 |
|
73 fun \<gamma>_parity :: "parity \<Rightarrow> val set" where |
|
74 "\<gamma>_parity Even = {i. i mod 2 = 0}" | |
|
75 "\<gamma>_parity Odd = {i. i mod 2 = 1}" | |
|
76 "\<gamma>_parity Either = UNIV" |
|
77 |
|
78 fun num_parity :: "val \<Rightarrow> parity" where |
|
79 "num_parity i = (if i mod 2 = 0 then Even else Odd)" |
|
80 |
|
81 fun plus_parity :: "parity \<Rightarrow> parity \<Rightarrow> parity" where |
|
82 "plus_parity Even Even = Even" | |
|
83 "plus_parity Odd Odd = Even" | |
|
84 "plus_parity Even Odd = Odd" | |
|
85 "plus_parity Odd Even = Odd" | |
|
86 "plus_parity Either y = Either" | |
|
87 "plus_parity x Either = Either" |
|
88 |
|
89 text{* First we instantiate the abstract value interface and prove that the |
|
90 functions on type @{typ parity} have all the necessary properties: *} |
|
91 |
|
92 interpretation Val_abs |
|
93 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
|
94 defines aval_parity is aval' |
|
95 proof txt{* of the locale axioms *} |
|
96 fix a b :: parity |
|
97 assume "a \<sqsubseteq> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b" |
|
98 by(auto simp: le_parity_def) |
|
99 next txt{* The rest in the lazy, implicit way *} |
|
100 case goal2 show ?case by(auto simp: Top_parity_def) |
|
101 next |
|
102 case goal3 show ?case by auto |
|
103 next |
|
104 txt{* Warning: this subproof refers to the names @{text a1} and @{text a2} |
|
105 from the statement of the axiom. *} |
|
106 case goal4 thus ?case |
|
107 proof(cases a1 a2 rule: parity.exhaust[case_product parity.exhaust]) |
|
108 qed (auto simp add:mod_add_eq) |
|
109 qed |
|
110 |
|
111 text{* Instantiating the abstract interpretation locale requires no more |
|
112 proofs (they happened in the instatiation above) but delivers the |
|
113 instantiated abstract interpreter which we call AI: *} |
|
114 |
|
115 interpretation Abs_Int |
|
116 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
|
117 defines step_parity is step' and AI_parity is AI |
|
118 proof qed |
|
119 |
|
120 |
|
121 subsubsection "Tests" |
|
122 |
|
123 definition "test1_parity = |
|
124 ''x'' ::= N 1; |
|
125 WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)" |
|
126 |
|
127 value "show_acom_opt (AI_parity test1_parity)" |
|
128 |
|
129 definition "test2_parity = |
|
130 ''x'' ::= N 1; |
|
131 WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)" |
|
132 |
|
133 value "show_acom ((step_parity \<top> ^^1) (anno None test2_parity))" |
|
134 value "show_acom ((step_parity \<top> ^^2) (anno None test2_parity))" |
|
135 value "show_acom ((step_parity \<top> ^^3) (anno None test2_parity))" |
|
136 value "show_acom ((step_parity \<top> ^^4) (anno None test2_parity))" |
|
137 value "show_acom ((step_parity \<top> ^^5) (anno None test2_parity))" |
|
138 value "show_acom_opt (AI_parity test2_parity)" |
|
139 |
|
140 |
|
141 subsubsection "Termination" |
|
142 |
|
143 interpretation Abs_Int_mono |
|
144 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
|
145 proof |
|
146 case goal1 thus ?case |
|
147 proof(cases a1 a2 b1 b2 |
|
148 rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *) |
|
149 qed (auto simp add:le_parity_def) |
|
150 qed |
|
151 |
|
152 |
|
153 definition m_parity :: "parity \<Rightarrow> nat" where |
|
154 "m_parity x = (if x=Either then 0 else 1)" |
|
155 |
|
156 lemma measure_parity: |
|
157 "(strict{(x::parity,y). x \<sqsubseteq> y})^-1 \<subseteq> measure m_parity" |
|
158 by(auto simp add: m_parity_def le_parity_def) |
|
159 |
|
160 lemma measure_parity_eq: |
|
161 "\<forall>x y::parity. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m_parity x = m_parity y" |
|
162 by(auto simp add: m_parity_def le_parity_def) |
|
163 |
|
164 lemma AI_parity_Some: "\<exists>c'. AI_parity c = Some c'" |
|
165 by(rule AI_Some_measure[OF measure_parity measure_parity_eq]) |
|
166 |
|
167 end |