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