added operational equality
authorhaftmann
Tue Sep 19 15:21:42 2006 +0200 (2006-09-19)
changeset 20588c847c56edf0c
parent 20587 f43a46316fa5
child 20589 24ecf9bc1a0a
added operational equality
src/HOL/Datatype.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Datatype.thy	Tue Sep 19 15:21:41 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Tue Sep 19 15:21:42 2006 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  imports Datatype_Universe
     1.5  begin
     1.6  
     1.7 +setup "DatatypeCodegen.setup2"
     1.8 +
     1.9  subsection {* Representing primitive types *}
    1.10  
    1.11  rep_datatype bool
    1.12 @@ -297,4 +299,10 @@
    1.13    (SML target_atom "NONE" and target_atom "SOME")
    1.14    (Haskell target_atom "Nothing" and target_atom "Just")
    1.15  
    1.16 +code_instance option :: eq
    1.17 +  (Haskell -)
    1.18 +
    1.19 +code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
    1.20 +  (Haskell infixl 4 "==")
    1.21 +
    1.22  end
     2.1 --- a/src/HOL/List.thy	Tue Sep 19 15:21:41 2006 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Sep 19 15:21:42 2006 +0200
     2.3 @@ -2282,7 +2282,8 @@
     2.4  
     2.5  text{* Defaults for generating efficient code for some standard functions. *}
     2.6  
     2.7 -lemmas in_set_code[code unfold] = mem_iff[symmetric, THEN eq_reflection]
     2.8 +lemmas in_set_code [code unfold] =
     2.9 +  mem_iff [symmetric, THEN eq_reflection]
    2.10  
    2.11  lemma rev_code[code unfold]: "rev xs == itrev xs []"
    2.12  by simp
    2.13 @@ -2760,6 +2761,15 @@
    2.14    (SML target_atom "(__,/ __)")
    2.15    (Haskell target_atom "(__,/ __)")
    2.16  
    2.17 +code_instance list :: eq and char :: eq
    2.18 +  (Haskell - and -)
    2.19 +
    2.20 +code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.21 +  (Haskell infixl 4 "==")
    2.22 +
    2.23 +code_const "OperationalEquality.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    2.24 +  (Haskell infixl 4 "==")
    2.25 +
    2.26  setup {*
    2.27  let
    2.28  
     3.1 --- a/src/HOL/Nat.thy	Tue Sep 19 15:21:41 2006 +0200
     3.2 +++ b/src/HOL/Nat.thy	Tue Sep 19 15:21:42 2006 +0200
     3.3 @@ -1041,10 +1041,25 @@
     3.4    apply (fastsimp dest: mult_less_mono2)
     3.5    done
     3.6  
     3.7 +
     3.8  subsection {* Code generator setup *}
     3.9  
    3.10  lemma one_is_suc_zero [code inline]:
    3.11    "1 = Suc 0"
    3.12    by simp
    3.13  
    3.14 +instance nat :: eq ..
    3.15 +
    3.16 +lemma [code func]:
    3.17 +  "OperationalEquality.eq (0\<Colon>nat) 0 = True" unfolding eq_def by auto
    3.18 +
    3.19 +lemma [code func]:
    3.20 +  "OperationalEquality.eq (Suc n) (Suc m) = OperationalEquality.eq n m" unfolding eq_def by auto
    3.21 +
    3.22 +lemma [code func]:
    3.23 +  "OperationalEquality.eq (Suc n) 0 = False" unfolding eq_def by auto
    3.24 +
    3.25 +lemma [code func]:
    3.26 +  "OperationalEquality.eq 0 (Suc m) = False" unfolding eq_def by auto
    3.27 +
    3.28  end
     4.1 --- a/src/HOL/Orderings.thy	Tue Sep 19 15:21:41 2006 +0200
     4.2 +++ b/src/HOL/Orderings.thy	Tue Sep 19 15:21:42 2006 +0200
     4.3 @@ -8,18 +8,16 @@
     4.4  header {* Type classes for $\le$ *}
     4.5  
     4.6  theory Orderings
     4.7 -imports Lattice_Locales
     4.8 +imports OperationalEquality Lattice_Locales
     4.9  uses ("antisym_setup.ML")
    4.10  begin
    4.11  
    4.12  subsection {* Order signatures and orders *}
    4.13  
    4.14 -axclass
    4.15 -  ord < type
    4.16 -
    4.17 -consts
    4.18 -  less  :: "['a::ord, 'a] => bool"
    4.19 -  less_eq  :: "['a::ord, 'a] => bool"
    4.20 +class ord = eq +
    4.21 +  constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    4.22 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    4.23 +  fixes less    :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    4.24  
    4.25  const_syntax
    4.26    less  ("op <")
     5.1 --- a/src/HOL/Product_Type.thy	Tue Sep 19 15:21:41 2006 +0200
     5.2 +++ b/src/HOL/Product_Type.thy	Tue Sep 19 15:21:42 2006 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4  
     5.5  typedef unit = "{True}"
     5.6  proof
     5.7 -  show "True : ?unit" by blast
     5.8 +  show "True : ?unit" ..
     5.9  qed
    5.10  
    5.11  constdefs
    5.12 @@ -761,6 +761,29 @@
    5.13  
    5.14  subsection {* Code generator setup *}
    5.15  
    5.16 +instance unit :: eq ..
    5.17 +
    5.18 +lemma [code func]:
    5.19 +  "OperationalEquality.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
    5.20 +
    5.21 +code_instance unit :: eq
    5.22 +  (Haskell -)
    5.23 +
    5.24 +instance * :: (eq, eq) eq ..
    5.25 +
    5.26 +lemma [code func]:
    5.27 +  "OperationalEquality.eq (x1, y1) (x2, y2) = (OperationalEquality.eq x1 x2 \<and> OperationalEquality.eq y1 y2)"
    5.28 +  unfolding eq_def by auto
    5.29 +
    5.30 +code_instance * :: eq
    5.31 +  (Haskell -)
    5.32 +
    5.33 +code_const "OperationalEquality.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    5.34 +  (Haskell infixl 4 "==")
    5.35 +
    5.36 +code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    5.37 +  (Haskell infixl 4 "==")
    5.38 +
    5.39  types_code
    5.40    "*"     ("(_ */ _)")
    5.41  attach (term_of) {*
     6.1 --- a/src/HOL/Sum_Type.thy	Tue Sep 19 15:21:41 2006 +0200
     6.2 +++ b/src/HOL/Sum_Type.thy	Tue Sep 19 15:21:42 2006 +0200
     6.3 @@ -191,6 +191,27 @@
     6.4  lemma Part_Collect: "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}"
     6.5  by blast
     6.6  
     6.7 +
     6.8 +subsection {* Code generator setup *}
     6.9 +
    6.10 +instance "+" :: (eq, eq) eq ..
    6.11 +
    6.12 +lemma [code func]:
    6.13 +  "OperationalEquality.eq (Inl x) (Inl y) = OperationalEquality.eq x y"
    6.14 +  unfolding eq_def Inl_eq ..
    6.15 +
    6.16 +lemma [code func]:
    6.17 +  "OperationalEquality.eq (Inr x) (Inr y) = OperationalEquality.eq x y"
    6.18 +  unfolding eq_def Inr_eq ..
    6.19 +
    6.20 +lemma [code func]:
    6.21 +  "OperationalEquality.eq (Inl x) (Inr y) = False"
    6.22 +  unfolding eq_def using Inl_not_Inr by auto
    6.23 +
    6.24 +lemma [code func]:
    6.25 +  "OperationalEquality.eq (Inr x) (Inl y) = False"
    6.26 +  unfolding eq_def using Inr_not_Inl by auto
    6.27 +
    6.28  ML
    6.29  {*
    6.30  val Inl_RepI = thm "Inl_RepI";