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