# HG changeset patch # User nipkow # Date 1327671044 -3600 # Node ID 202f8b8086a3a79e7658cc2206c1c56a241b3b5b # Parent b6fbdd3d0915d870309763790646b1d33bf785d5 added parity analysis diff -r b6fbdd3d0915 -r 202f8b8086a3 src/HOL/IMP/Abs_Int0_parity.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IMP/Abs_Int0_parity.thy Fri Jan 27 14:30:44 2012 +0100 @@ -0,0 +1,167 @@ +theory Abs_Int0_parity +imports Abs_Int0 +begin + +subsection "Parity Analysis" + +datatype parity = Even | Odd | Either + +text{* Instantiation of class @{class preord} with type @{typ parity}: *} + +instantiation parity :: preord +begin + +text{* First the definition of the interface function @{text"\"}. Note that +the header of the definition must refer to the ascii name @{const le} of the +constants as @{text le_parity} and the definition is named @{text +le_parity_def}. Inside the definition the symbolic names can be used. *} + +definition le_parity where +"x \ y = (y = Either \ x=y)" + +text{* 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::parity show "x \ x" by(auto simp: le_parity_def) +next + fix x y z :: parity assume "x \ y" "y \ z" thus "x \ z" + by(auto simp: le_parity_def) +qed + +end + +text{* Instantiation of class @{class SL_top} with type @{typ parity}: *} + +instantiation parity :: SL_top +begin + + +definition join_parity where +"x \ y = (if x \ y then y else if y \ x then x else Either)" + +definition Top_parity where +"\ = Either" + +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. *} + +instance +proof + case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def) +next + case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def) +next + case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def) +next + case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_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 \_parity :: "parity \ val set" where +"\_parity Even = {i. i mod 2 = 0}" | +"\_parity Odd = {i. i mod 2 = 1}" | +"\_parity Either = UNIV" + +fun num_parity :: "val \ parity" where +"num_parity i = (if i mod 2 = 0 then Even else Odd)" + +fun plus_parity :: "parity \ parity \ parity" where +"plus_parity Even Even = Even" | +"plus_parity Odd Odd = Even" | +"plus_parity Even Odd = Odd" | +"plus_parity Odd Even = Odd" | +"plus_parity Either y = Either" | +"plus_parity x Either = Either" + +text{* First we instantiate the abstract value interface and prove that the +functions on type @{typ parity} have all the necessary properties: *} + +interpretation Val_abs +where \ = \_parity and num' = num_parity and plus' = plus_parity +defines aval_parity is aval' +proof txt{* of the locale axioms *} + fix a b :: parity + assume "a \ b" thus "\_parity a \ \_parity b" + by(auto simp: le_parity_def) +next txt{* The rest in the lazy, implicit way *} + case goal2 show ?case by(auto simp: Top_parity_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 + proof(cases a1 a2 rule: parity.exhaust[case_product parity.exhaust]) + qed (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 AI: *} + +interpretation Abs_Int +where \ = \_parity and num' = num_parity and plus' = plus_parity +defines step_parity is step' and AI_parity is AI +proof qed + + +subsubsection "Tests" + +definition "test1_parity = + ''x'' ::= N 1; + WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)" + +value "show_acom_opt (AI_parity test1_parity)" + +definition "test2_parity = + ''x'' ::= N 1; + WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)" + +value "show_acom ((step_parity \ ^^1) (anno None test2_parity))" +value "show_acom ((step_parity \ ^^2) (anno None test2_parity))" +value "show_acom ((step_parity \ ^^3) (anno None test2_parity))" +value "show_acom ((step_parity \ ^^4) (anno None test2_parity))" +value "show_acom ((step_parity \ ^^5) (anno None test2_parity))" +value "show_acom_opt (AI_parity test2_parity)" + + +subsubsection "Termination" + +interpretation Abs_Int_mono +where \ = \_parity and num' = num_parity and plus' = plus_parity +proof + case goal1 thus ?case + proof(cases a1 a2 b1 b2 + rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *) + qed (auto simp add:le_parity_def) +qed + + +definition m_parity :: "parity \ nat" where +"m_parity x = (if x=Either then 0 else 1)" + +lemma measure_parity: + "(strict{(x::parity,y). x \ y})^-1 \ measure m_parity" +by(auto simp add: m_parity_def le_parity_def) + +lemma measure_parity_eq: + "\x y::parity. x \ y \ y \ x \ m_parity x = m_parity y" +by(auto simp add: m_parity_def le_parity_def) + +lemma AI_parity_Some: "\c'. AI_parity c = Some c'" +by(rule AI_Some_measure[OF measure_parity measure_parity_eq]) + +end diff -r b6fbdd3d0915 -r 202f8b8086a3 src/HOL/IMP/ROOT.ML --- a/src/HOL/IMP/ROOT.ML Fri Jan 27 10:31:31 2012 +0100 +++ b/src/HOL/IMP/ROOT.ML Fri Jan 27 14:30:44 2012 +0100 @@ -19,9 +19,12 @@ "Hoare_Examples", "VC", "HoareT", - "Abs_Int2", "Collecting1", "Collecting_list", + "Abs_Int0", + "Abs_Int0_parity", + "Abs_Int0_const", + "Abs_Int2", "Abs_Int_Den/Abs_Int_den2", "Procs_Dyn_Vars_Dyn", "Procs_Stat_Vars_Dyn",