1(* Author: Tobias Nipkow *)
2
3theory Abs_Int1_parity
4imports Abs_Int1
5begin
6
7subsection "Parity Analysis"
8
9datatype parity = Even | Odd | Either
10
11text\<open>Instantiation of class @{class order} with type @{typ parity}:\<close>
12
13instantiation parity :: order
14begin
15
16text\<open>First the definition of the interface function @{text"\<le>"}. Note that
17the header of the definition must refer to the ascii name @{const less_eq} of the
18constants as @{text less_eq_parity} and the definition is named @{text
19less_eq_parity_def}.  Inside the definition the symbolic names can be used.\<close>
20
21definition less_eq_parity where
22"x \<le> y = (y = Either \<or> x=y)"
23
24text\<open>We also need @{text"<"}, which is defined canonically:\<close>
25
26definition less_parity where
27"x < y = (x \<le> y \<and> \<not> y \<le> (x::parity))"
28
29text\<open>\noindent(The type annotation is necessary to fix the type of the polymorphic predicates.)
30
31Now the instance proof, i.e.\ the proof that the definition fulfills
32the axioms (assumptions) of the class. The initial proof-step generates the
33necessary proof obligations.\<close>
34
35instance
36proof
37  fix x::parity show "x \<le> x" by(auto simp: less_eq_parity_def)
38next
39  fix x y z :: parity assume "x \<le> y" "y \<le> z" thus "x \<le> z"
40    by(auto simp: less_eq_parity_def)
41next
42  fix x y :: parity assume "x \<le> y" "y \<le> x" thus "x = y"
43    by(auto simp: less_eq_parity_def)
44next
45  fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def)
46qed
47
48end
49
50text\<open>Instantiation of class @{class semilattice_sup_top} with type @{typ parity}:\<close>
51
52instantiation parity :: semilattice_sup_top
53begin
54
55definition sup_parity where
56"x \<squnion> y = (if x = y then x else Either)"
57
58definition top_parity where
59"\<top> = Either"
60
61text\<open>Now the instance proof. This time we take a shortcut with the help of
62proof method @{text goal_cases}: it creates cases 1 ... n for the subgoals
631 ... n; in case i, i is also the name of the assumptions of subgoal i and
64@{text "case?"} refers to the conclusion of subgoal i.
65The class axioms are presented in the same order as in the class definition.\<close>
66
67instance
68proof (standard, goal_cases)
69  case 1 (*sup1*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
70next
71  case 2 (*sup2*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
72next
73  case 3 (*sup least*) thus ?case by(auto simp: less_eq_parity_def sup_parity_def)
74next
75  case 4 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
76qed
77
78end
79
80
81text\<open>Now we define the functions used for instantiating the abstract
82interpretation locales. Note that the Isabelle terminology is
83\emph{interpretation}, not \emph{instantiation} of locales, but we use
84instantiation to avoid confusion with abstract interpretation.\<close>
85
86fun \<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
91fun num_parity :: "val \<Rightarrow> parity" where
92"num_parity i = (if i mod 2 = 0 then Even else Odd)"
93
94fun 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
102text\<open>First we instantiate the abstract value interface and prove that the
103functions on type @{typ parity} have all the necessary properties:\<close>
104
105global_interpretation Val_semilattice
106where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
107proof (standard, goal_cases) txt\<open>subgoals are the locale axioms\<close>
108  case 1 thus ?case by(auto simp: less_eq_parity_def)
109next
110  case 2 show ?case by(auto simp: top_parity_def)
111next
112  case 3 show ?case by auto
113next
114  case (4 _ a1 _ a2) thus ?case
115    by (induction a1 a2 rule: plus_parity.induct)
116      (auto simp add: mod_add_eq [symmetric])
117qed
118
119text\<open>In case 4 we needed to refer to particular variables.
120Writing (i x y z) fixes the names of the variables in case i to be x, y and z
121in the left-to-right order in which the variables occur in the subgoal.
122Underscores are anonymous placeholders for variable names we don't care to fix.\<close>
123
124text\<open>Instantiating the abstract interpretation locale requires no more
125proofs (they happened in the instatiation above) but delivers the
126instantiated abstract interpreter which we call @{text AI_parity}:\<close>
127
128global_interpretation Abs_Int
129where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
130defines aval_parity = aval' and step_parity = step' and AI_parity = AI
131..
132
133
134subsubsection "Tests"
135
136definition "test1_parity =
137  ''x'' ::= N 1;;
138  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
139value "show_acom (the(AI_parity test1_parity))"
140
141definition "test2_parity =
142  ''x'' ::= N 1;;
143  WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
144
145definition "steps c i = ((step_parity \<top>) ^^ i) (bot c)"
146
147value "show_acom (steps test2_parity 0)"
148value "show_acom (steps test2_parity 1)"
149value "show_acom (steps test2_parity 2)"
150value "show_acom (steps test2_parity 3)"
151value "show_acom (steps test2_parity 4)"
152value "show_acom (steps test2_parity 5)"
153value "show_acom (steps test2_parity 6)"
154value "show_acom (the(AI_parity test2_parity))"
155
156
157subsubsection "Termination"
158
159global_interpretation Abs_Int_mono
160where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
161proof (standard, goal_cases)
162  case (1 _ a1 _ a2) thus ?case
163    by(induction a1 a2 rule: plus_parity.induct)
164      (auto simp add:less_eq_parity_def)
165qed
166
167definition m_parity :: "parity \<Rightarrow> nat" where
168"m_parity x = (if x = Either then 0 else 1)"
169
170global_interpretation Abs_Int_measure
171where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
172and m = m_parity and h = "1"
173proof (standard, goal_cases)
174  case 1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
175next
176  case 2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
177qed
178
179thm AI_Some_measure
180
181end
182