(* Author: Tobias Nipkow *) theory tut12_2 imports "~~/src/HOL/IMP/Abs_Int1" begin subsection "Parity Analysis" datatype sign = Neg | Zero | Pos | Any text{* Instantiation of class @{class order} with type @{typ sign}: *} instantiation sign :: order begin text{* First the definition of the interface function @{text"\"}. Note that the header of the definition must refer to the ascii name @{const less_eq} of the constants as @{text less_eq_sign} and the definition is named @{text less_eq_sign_def}. Inside the definition the symbolic names can be used. *} definition less_eq_sign where "x \ y = (y = Any \ x=y)" text{* We also need @{text"<"}, which is defined canonically: *} definition less_sign where "x < y = (x \ y \ \ y \ (x::sign))" text{*\noindent(The type annotation is necessary to fix the type of the polymorphic predicates.) Now the instance proof, i.e.\ the proof that the definition fulfills the axioms (assumptions) of the class. The initial proof-step generates the necessary proof obligations. *} instance proof fix x::sign show "x \ x" by(auto simp: less_eq_sign_def) next fix x y z :: sign assume "x \ y" "y \ z" thus "x \ z" by(auto simp: less_eq_sign_def) next fix x y :: sign assume "x \ y" "y \ x" thus "x = y" by(auto simp: less_eq_sign_def) next fix x y :: sign show "(x < y) = (x \ y \ \ y \ x)" by(rule less_sign_def) qed end text{* Instantiation of class @{class semilattice_sup_top} with type @{typ sign}: *} instantiation sign :: semilattice_sup_top begin definition sup_sign where "x \ y = (if x = y then x else Any)" definition top_sign where "\ = Any" text{* Now the instance proof. This time we take a lazy shortcut: we do not write out the proof obligations but use the @{text goali} primitive to refer to the assumptions of subgoal i and @{text "case?"} to refer to the conclusion of subgoal i. The class axioms are presented in the same order as in the class definition. Warning: this is brittle! *} instance proof case goal1 (*sup1*) show ?case by(auto simp: less_eq_sign_def sup_sign_def) next case goal2 (*sup2*) show ?case by(auto simp: less_eq_sign_def sup_sign_def) next case goal3 (*sup least*) thus ?case by(auto simp: less_eq_sign_def sup_sign_def) next case goal4 (*top*) show ?case by(auto simp: less_eq_sign_def top_sign_def) qed end text{* Now we define the functions used for instantiating the abstract interpretation locales. Note that the Isabelle terminology is \emph{interpretation}, not \emph{instantiation} of locales, but we use instantiation to avoid confusion with abstract interpretation. *} fun \_sign :: "sign \ val set" where "\_sign Neg = {i. i < 0}" | "\_sign Zero = {0}" | "\_sign Pos = {i. i > 0}" | "\_sign Any = UNIV" fun num_sign :: "val \ sign" where "num_sign i = (if i > 0 then Pos else if i=0 then Zero else Neg)" fun plus_sign :: "sign \ sign \ sign" where "plus_sign Zero x = x" | "plus_sign x Zero = x" | "plus_sign Pos Pos = Pos" | "plus_sign Neg Neg = Neg" | "plus_sign _ _ = Any" text{* First we instantiate the abstract value interface and prove that the functions on type @{typ sign} have all the necessary properties: *} interpretation Val_semilattice where \ = \_sign and num' = num_sign and plus' = plus_sign proof txt{* of the locale axioms *} fix a b :: sign assume "a \ b" thus "\_sign a \ \_sign b" by(auto simp: less_eq_sign_def) next txt{* The rest in the lazy, implicit way *} case goal2 show ?case by(auto simp: top_sign_def) next case goal3 show ?case by auto next txt{* Warning: this subproof refers to the names @{text a1} and @{text a2} from the statement of the axiom. *} case goal4 thus ?case by (cases "(a1,a2)" rule: plus_sign.cases) (auto simp add:mod_add_eq) (*by (induction a1 a2 rule: plus_sign.induct) (auto simp add:mod_add_eq)*) qed text{* Instantiating the abstract interpretation locale requires no more proofs (they happened in the instatiation above) but delivers the instantiated abstract interpreter which we call @{text AI_sign}: *} interpretation Abs_Int where \ = \_sign and num' = num_sign and plus' = plus_sign defines aval_sign is aval' and step_sign is step' and AI_sign is AI .. subsubsection "Tests" definition "test1_sign = ''x'' ::= N 1;; WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)" value [code] "show_acom (the(AI_sign test1_sign))" definition "test2_sign = ''x'' ::= N 1;; WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N -3)" definition "steps c i = ((step_sign \) ^^ i) (bot c)" thm AI_correct value "show_acom (steps test2_sign 0)" value "show_acom (steps test2_sign 1)" value "show_acom (steps test2_sign 2)" value "show_acom (steps test2_sign 3)" value "show_acom (steps test2_sign 4)" value "show_acom (steps test2_sign 5)" value "show_acom (steps test2_sign 6)" value "show_acom (steps test2_sign 7)" value "show_acom (steps test2_sign 8)" value "show_acom (steps test2_sign 9)" value "show_acom (steps test2_sign 10)" value "show_acom (the(AI_sign test2_sign))" subsubsection "Termination" lemma [simp]: "plus_sign x Any = Any" "plus_sign Any x = Any" by (cases x, simp_all)+ interpretation Abs_Int_mono where \ = \_sign and num' = num_sign and plus' = plus_sign proof case goal1 thus ?case by(induction a1 a2 rule: plus_sign.induct) (auto simp add:less_eq_sign_def) qed definition m_sign :: "sign \ nat" where "m_sign x = (if x = Any then 0 else 1)" interpretation Abs_Int_measure where \ = \_sign and num' = num_sign and plus' = plus_sign and m = m_sign and h = "1" proof case goal1 thus ?case by(auto simp add: m_sign_def less_eq_sign_def) next case goal2 thus ?case by(auto simp add: m_sign_def less_eq_sign_def less_sign_def) qed thm AI_Some_measure end