src/HOL/IMP/Abs_Int1_parity.thy
changeset 51359 00b45c7e831f
parent 51036 e7b54119c436
child 51372 d315e9a9ee72
     1.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Wed Mar 06 14:10:07 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Wed Mar 06 16:10:56 2013 +0100
     1.3 @@ -1,3 +1,5 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6  theory Abs_Int1_parity
     1.7  imports Abs_Int1
     1.8  begin
     1.9 @@ -6,29 +8,41 @@
    1.10  
    1.11  datatype parity = Even | Odd | Either
    1.12  
    1.13 -text{* Instantiation of class @{class preord} with type @{typ parity}: *}
    1.14 +text{* Instantiation of class @{class order} with type @{typ parity}: *}
    1.15  
    1.16 -instantiation parity :: preord
    1.17 +instantiation parity :: order
    1.18  begin
    1.19  
    1.20 -text{* First the definition of the interface function @{text"\<sqsubseteq>"}. Note that
    1.21 -the header of the definition must refer to the ascii name @{const le} of the
    1.22 -constants as @{text le_parity} and the definition is named @{text
    1.23 -le_parity_def}.  Inside the definition the symbolic names can be used. *}
    1.24 +text{* First the definition of the interface function @{text"\<le>"}. Note that
    1.25 +the header of the definition must refer to the ascii name @{const less_eq} of the
    1.26 +constants as @{text less_eq_parity} and the definition is named @{text
    1.27 +less_eq_parity_def}.  Inside the definition the symbolic names can be used. *}
    1.28 +
    1.29 +definition less_eq_parity where
    1.30 +"x \<le> y = (y = Either \<or> x=y)"
    1.31  
    1.32 -definition le_parity where
    1.33 -"x \<sqsubseteq> y = (y = Either \<or> x=y)"
    1.34 +text{* We also need @{text"<"}, which is defined canonically: *}
    1.35  
    1.36 -text{* Now the instance proof, i.e.\ the proof that the definition fulfills
    1.37 +definition less_parity where
    1.38 +"x < y = (x \<le> y \<and> \<not> y \<le> (x::parity))"
    1.39 +
    1.40 +text{*\noindent (The type annotation is necessary to fix the type of the polymorphic predicates.)
    1.41 +
    1.42 +Now the instance proof, i.e.\ the proof that the definition fulfills
    1.43  the axioms (assumptions) of the class. The initial proof-step generates the
    1.44  necessary proof obligations. *}
    1.45  
    1.46  instance
    1.47  proof
    1.48 -  fix x::parity show "x \<sqsubseteq> x" by(auto simp: le_parity_def)
    1.49 +  fix x::parity show "x \<le> x" by(auto simp: less_eq_parity_def)
    1.50 +next
    1.51 +  fix x y z :: parity assume "x \<le> y" "y \<le> z" thus "x \<le> z"
    1.52 +    by(auto simp: less_eq_parity_def)
    1.53  next
    1.54 -  fix x y z :: parity assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    1.55 -    by(auto simp: le_parity_def)
    1.56 +  fix x y :: parity assume "x \<le> y" "y \<le> x" thus "x = y"
    1.57 +    by(auto simp: less_eq_parity_def)
    1.58 +next
    1.59 +  fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def)
    1.60  qed
    1.61  
    1.62  end
    1.63 @@ -39,9 +53,9 @@
    1.64  begin
    1.65  
    1.66  definition join_parity where
    1.67 -"x \<squnion> y = (if x \<sqsubseteq> y then y else if y \<sqsubseteq> x then x else Either)"
    1.68 +"x \<squnion> y = (if x \<le> y then y else if y \<le> x then x else Either)"
    1.69  
    1.70 -definition Top_parity where
    1.71 +definition top_parity where
    1.72  "\<top> = Either"
    1.73  
    1.74  text{* Now the instance proof. This time we take a lazy shortcut: we do not
    1.75 @@ -52,13 +66,13 @@
    1.76  
    1.77  instance
    1.78  proof
    1.79 -  case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def)
    1.80 +  case goal1 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
    1.81  next
    1.82 -  case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def)
    1.83 +  case goal2 (*join1*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
    1.84  next
    1.85 -  case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def)
    1.86 +  case goal3 (*join2*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
    1.87  next
    1.88 -  case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def)
    1.89 +  case goal4 (*join least*) thus ?case by(auto simp: less_eq_parity_def join_parity_def)
    1.90  qed
    1.91  
    1.92  end
    1.93 @@ -92,10 +106,10 @@
    1.94  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
    1.95  proof txt{* of the locale axioms *}
    1.96    fix a b :: parity
    1.97 -  assume "a \<sqsubseteq> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
    1.98 -    by(auto simp: le_parity_def)
    1.99 +  assume "a \<le> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
   1.100 +    by(auto simp: less_eq_parity_def)
   1.101  next txt{* The rest in the lazy, implicit way *}
   1.102 -  case goal2 show ?case by(auto simp: Top_parity_def)
   1.103 +  case goal2 show ?case by(auto simp: top_parity_def)
   1.104  next
   1.105    case goal3 show ?case by auto
   1.106  next
   1.107 @@ -127,7 +141,7 @@
   1.108    ''x'' ::= N 1;
   1.109    WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
   1.110  
   1.111 -definition "steps c i = (step_parity(top(vars c)) ^^ i) (bot c)"
   1.112 +definition "steps c i = (step_parity(Top(vars c)) ^^ i) (bot c)"
   1.113  
   1.114  value "show_acom (steps test2_parity 0)"
   1.115  value "show_acom (steps test2_parity 1)"
   1.116 @@ -147,7 +161,7 @@
   1.117    case goal1 thus ?case
   1.118    proof(cases a1 a2 b1 b2
   1.119     rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *)
   1.120 -  qed (auto simp add:le_parity_def)
   1.121 +  qed (auto simp add:less_eq_parity_def)
   1.122  qed
   1.123  
   1.124  definition m_parity :: "parity \<Rightarrow> nat" where
   1.125 @@ -157,11 +171,11 @@
   1.126  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
   1.127  and m = m_parity and h = "1"
   1.128  proof
   1.129 -  case goal1 thus ?case by(auto simp add: m_parity_def le_parity_def)
   1.130 +  case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
   1.131  next
   1.132 -  case goal2 thus ?case by(auto simp add: m_parity_def le_parity_def)
   1.133 +  case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
   1.134  next
   1.135 -  case goal3 thus ?case by(auto simp add: m_parity_def le_parity_def)
   1.136 +  case goal3 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
   1.137  qed
   1.138  
   1.139  thm AI_Some_measure