discontinued special treatment of op = vs. eq_class.eq
authorhaftmann
Thu Sep 25 09:28:03 2008 +0200 (2008-09-25)
changeset 28346b8390cd56b8f
parent 28345 4562584d9d66
child 28347 3cb64932ac77
discontinued special treatment of op = vs. eq_class.eq
src/HOL/Code_Eval.thy
src/HOL/Code_Setup.thy
src/HOL/Datatype.thy
src/HOL/HOL.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Code_Message.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/RType.thy
src/HOL/List.thy
src/HOL/Product_Type.thy
src/Pure/Isar/code_unit.ML
src/Tools/code/code_name.ML
     1.1 --- a/src/HOL/Code_Eval.thy	Wed Sep 24 19:39:25 2008 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Thu Sep 25 09:28:03 2008 +0200
     1.3 @@ -135,7 +135,7 @@
     1.4  subsubsection {* Code generator setup *}
     1.5  
     1.6  lemmas [code func del] = term.recs term.cases term.size
     1.7 -lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
     1.8 +lemma [code func, code func del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
     1.9  
    1.10  lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
    1.11  lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
     2.1 --- a/src/HOL/Code_Setup.thy	Wed Sep 24 19:39:25 2008 +0200
     2.2 +++ b/src/HOL/Code_Setup.thy	Thu Sep 25 09:28:03 2008 +0200
     2.3 @@ -77,7 +77,10 @@
     2.4  text {* using built-in Haskell equality *}
     2.5  
     2.6  code_class eq
     2.7 -  (Haskell "Eq" where "op =" \<equiv> "(==)")
     2.8 +  (Haskell "Eq" where "eq_class.eq" \<equiv> "(==)")
     2.9 +
    2.10 +code_const "eq_class.eq"
    2.11 +  (Haskell infixl 4 "==")
    2.12  
    2.13  code_const "op ="
    2.14    (Haskell infixl 4 "==")
     3.1 --- a/src/HOL/Datatype.thy	Wed Sep 24 19:39:25 2008 +0200
     3.2 +++ b/src/HOL/Datatype.thy	Thu Sep 25 09:28:03 2008 +0200
     3.3 @@ -686,7 +686,7 @@
     3.4  code_instance option :: eq
     3.5    (Haskell -)
     3.6  
     3.7 -code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
     3.8 +code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
     3.9    (Haskell infixl 4 "==")
    3.10  
    3.11  code_reserved SML
     4.1 --- a/src/HOL/HOL.thy	Wed Sep 24 19:39:25 2008 +0200
     4.2 +++ b/src/HOL/HOL.thy	Thu Sep 25 09:28:03 2008 +0200
     4.3 @@ -1710,16 +1710,24 @@
     4.4  
     4.5  class eq = type +
     4.6    fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     4.7 -  assumes eq: "eq x y \<longleftrightarrow> x = y "
     4.8 +  assumes eq_equals: "eq x y \<longleftrightarrow> x = y "
     4.9  begin
    4.10  
    4.11 +lemma eq: "eq = (op =)"
    4.12 +  by (rule ext eq_equals)+
    4.13 +
    4.14  lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
    4.15 -  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
    4.16 +  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    4.17  
    4.18  declare equals_eq [symmetric, code post]
    4.19  
    4.20 +lemma eq_refl: "eq x x \<longleftrightarrow> True"
    4.21 +  unfolding eq by rule+
    4.22 +
    4.23  end
    4.24  
    4.25 +declare simp_thms(6) [code nbe]
    4.26 +
    4.27  hide (open) const eq
    4.28  hide const eq
    4.29  
     5.1 --- a/src/HOL/Library/Code_Char.thy	Wed Sep 24 19:39:25 2008 +0200
     5.2 +++ b/src/HOL/Library/Code_Char.thy	Thu Sep 25 09:28:03 2008 +0200
     5.3 @@ -28,7 +28,7 @@
     5.4  code_reserved OCaml
     5.5    char
     5.6  
     5.7 -code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
     5.8 +code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
     5.9    (SML "!((_ : char) = _)")
    5.10    (OCaml "!((_ : char) = _)")
    5.11    (Haskell infixl 4 "==")
     6.1 --- a/src/HOL/Library/Code_Index.thy	Wed Sep 24 19:39:25 2008 +0200
     6.2 +++ b/src/HOL/Library/Code_Index.thy	Thu Sep 25 09:28:03 2008 +0200
     6.3 @@ -111,8 +111,8 @@
     6.4  qed
     6.5  
     6.6  lemma [code func]:
     6.7 -  "k = l \<longleftrightarrow> nat_of_index k = nat_of_index l"
     6.8 -  by (cases k, cases l) simp
     6.9 +  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
    6.10 +  by (cases k, cases l) (simp add: eq)
    6.11  
    6.12  
    6.13  subsection {* Indices as datatype of ints *}
    6.14 @@ -319,7 +319,7 @@
    6.15    (OCaml "(fun n -> fun m ->/ (n '/ m, n mod m))")
    6.16    (Haskell "divMod")
    6.17  
    6.18 -code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
    6.19 +code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
    6.20    (SML "!((_ : Int.int) = _)")
    6.21    (OCaml "!((_ : int) = _)")
    6.22    (Haskell infixl 4 "==")
     7.1 --- a/src/HOL/Library/Code_Integer.thy	Wed Sep 24 19:39:25 2008 +0200
     7.2 +++ b/src/HOL/Library/Code_Integer.thy	Thu Sep 25 09:28:03 2008 +0200
     7.3 @@ -72,7 +72,7 @@
     7.4    (OCaml "Big'_int.mult'_big'_int")
     7.5    (Haskell infixl 7 "*")
     7.6  
     7.7 -code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
     7.8 +code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
     7.9    (SML "!((_ : IntInf.int) = _)")
    7.10    (OCaml "Big'_int.eq'_big'_int")
    7.11    (Haskell infixl 4 "==")
     8.1 --- a/src/HOL/Library/Code_Message.thy	Wed Sep 24 19:39:25 2008 +0200
     8.2 +++ b/src/HOL/Library/Code_Message.thy	Thu Sep 25 09:28:03 2008 +0200
     8.3 @@ -50,7 +50,7 @@
     8.4  code_instance message_string :: eq
     8.5    (Haskell -)
     8.6  
     8.7 -code_const "op = \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
     8.8 +code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
     8.9    (SML "!((_ : string) = _)")
    8.10    (OCaml "!((_ : string) = _)")
    8.11    (Haskell infixl 4 "==")
     9.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 24 19:39:25 2008 +0200
     9.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Sep 25 09:28:03 2008 +0200
     9.3 @@ -400,7 +400,7 @@
     9.4    (OCaml "Big'_int.quomod'_big'_int")
     9.5    (Haskell "divMod")
     9.6  
     9.7 -code_const "op = \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
     9.8 +code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
     9.9    (SML "!((_ : IntInf.int) = _)")
    9.10    (OCaml "Big'_int.eq'_big'_int")
    9.11    (Haskell infixl 4 "==")
    10.1 --- a/src/HOL/Library/RType.thy	Wed Sep 24 19:39:25 2008 +0200
    10.2 +++ b/src/HOL/Library/RType.thy	Thu Sep 25 09:28:03 2008 +0200
    10.3 @@ -91,9 +91,9 @@
    10.4  *}
    10.5  
    10.6  lemma [code func]:
    10.7 -  "Typerep tyco1 tys1 = Typerep tyco2 tys2 \<longleftrightarrow> tyco1 = tyco2
    10.8 -     \<and> list_all2 (op =) tys1 tys2"
    10.9 -  by (auto simp add: list_all2_eq [symmetric])
   10.10 +  "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
   10.11 +     \<and> list_all2 eq_class.eq tys1 tys2"
   10.12 +  by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
   10.13  
   10.14  code_type typerep
   10.15    (SML "Term.typ")
    11.1 --- a/src/HOL/List.thy	Wed Sep 24 19:39:25 2008 +0200
    11.2 +++ b/src/HOL/List.thy	Thu Sep 25 09:28:03 2008 +0200
    11.3 @@ -3625,7 +3625,7 @@
    11.4  code_instance list :: eq
    11.5    (Haskell -)
    11.6  
    11.7 -code_const "op = \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
    11.8 +code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
    11.9    (Haskell infixl 4 "==")
   11.10  
   11.11  setup {*
    12.1 --- a/src/HOL/Product_Type.thy	Wed Sep 24 19:39:25 2008 +0200
    12.2 +++ b/src/HOL/Product_Type.thy	Thu Sep 25 09:28:03 2008 +0200
    12.3 @@ -22,13 +22,15 @@
    12.4  declare case_split [cases type: bool]
    12.5    -- "prefer plain propositional version"
    12.6  
    12.7 -lemma [code func]:
    12.8 -  shows "False = P \<longleftrightarrow> \<not> P"
    12.9 -    and "True = P \<longleftrightarrow> P" 
   12.10 -    and "P = False \<longleftrightarrow> \<not> P" 
   12.11 -    and "P = True \<longleftrightarrow> P" by simp_all
   12.12 +lemma
   12.13 +  shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
   12.14 +    and [code func]: "eq_class.eq True P \<longleftrightarrow> P" 
   12.15 +    and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
   12.16 +    and [code func]: "eq_class.eq P True \<longleftrightarrow> P"
   12.17 +    and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
   12.18 +  by (simp_all add: eq)
   12.19  
   12.20 -code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   12.21 +code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   12.22    (Haskell infixl 4 "==")
   12.23  
   12.24  code_instance bool :: eq
   12.25 @@ -88,7 +90,7 @@
   12.26  instance unit :: eq ..
   12.27  
   12.28  lemma [code func]:
   12.29 -  "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
   12.30 +  "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
   12.31  
   12.32  code_type unit
   12.33    (SML "unit")
   12.34 @@ -98,7 +100,7 @@
   12.35  code_instance unit :: eq
   12.36    (Haskell -)
   12.37  
   12.38 -code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   12.39 +code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   12.40    (Haskell infixl 4 "==")
   12.41  
   12.42  code_const Unity
   12.43 @@ -916,7 +918,7 @@
   12.44  instance * :: (eq, eq) eq ..
   12.45  
   12.46  lemma [code func]:
   12.47 -  "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
   12.48 +  "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
   12.49  
   12.50  lemma split_case_cert:
   12.51    assumes "CASE \<equiv> split f"
   12.52 @@ -935,7 +937,7 @@
   12.53  code_instance * :: eq
   12.54    (Haskell -)
   12.55  
   12.56 -code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   12.57 +code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   12.58    (Haskell infixl 4 "==")
   12.59  
   12.60  code_const Pair
    13.1 --- a/src/Pure/Isar/code_unit.ML	Wed Sep 24 19:39:25 2008 +0200
    13.2 +++ b/src/Pure/Isar/code_unit.ML	Thu Sep 25 09:28:03 2008 +0200
    13.3 @@ -20,9 +20,8 @@
    13.4  
    13.5    (*constant aliasses*)
    13.6    val add_const_alias: thm -> theory -> theory
    13.7 -  val subst_alias: theory -> string -> string
    13.8 +  val triv_classes: theory -> class list
    13.9    val resubst_alias: theory -> string -> string
   13.10 -  val triv_classes: theory -> class list
   13.11  
   13.12    (*constants*)
   13.13    val string_of_typ: theory -> typ -> string
   13.14 @@ -39,7 +38,7 @@
   13.15    (*defining equations*)
   13.16    val assert_rew: thm -> thm
   13.17    val mk_rew: thm -> thm
   13.18 -  val mk_func: thm -> thm
   13.19 +  val mk_func: bool -> thm -> thm
   13.20    val head_func: thm -> string * ((string * sort) list * typ)
   13.21    val expand_eta: int -> thm -> thm
   13.22    val rewrite_func: simpset -> thm -> thm
   13.23 @@ -223,6 +222,7 @@
   13.24      |> map Drule.zero_var_indexes
   13.25    end;
   13.26  
   13.27 +
   13.28  (* const aliasses *)
   13.29  
   13.30  structure ConstAlias = TheoryDataFun
   13.31 @@ -252,16 +252,6 @@
   13.32        ((c_c', thm) :: alias, fold (insert (op =)) some_class classes))
   13.33    end;
   13.34  
   13.35 -fun rew_alias thm =
   13.36 -  let
   13.37 -    val thy = Thm.theory_of_thm thm;
   13.38 -  in rewrite_head ((map snd o fst o ConstAlias.get) thy) thm end;
   13.39 -
   13.40 -fun subst_alias thy c = ConstAlias.get thy
   13.41 -  |> fst
   13.42 -  |> get_first (fn ((c', c''), _) => if c = c' then SOME c'' else NONE)
   13.43 -  |> the_default c;
   13.44 -
   13.45  fun resubst_alias thy =
   13.46    let
   13.47      val alias = fst (ConstAlias.get thy);
   13.48 @@ -275,19 +265,18 @@
   13.49  
   13.50  val triv_classes = snd o ConstAlias.get;
   13.51  
   13.52 +
   13.53  (* reading constants as terms *)
   13.54  
   13.55  fun check_bare_const thy t = case try dest_Const t
   13.56   of SOME c_ty => c_ty
   13.57    | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
   13.58  
   13.59 -fun check_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
   13.60 -  o check_bare_const thy;
   13.61 +fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
   13.62  
   13.63  fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
   13.64  
   13.65 -fun read_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
   13.66 -  o read_bare_const thy;
   13.67 +fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
   13.68  
   13.69  
   13.70  (* constructor sets *)
   13.71 @@ -372,7 +361,7 @@
   13.72  
   13.73  (* defining equations *)
   13.74  
   13.75 -fun assert_func thm =
   13.76 +fun assert_func linear thm =
   13.77    let
   13.78      val thy = Thm.theory_of_thm thm;
   13.79      val (head, args) = (strip_comb o fst o Logic.dest_equals
   13.80 @@ -380,7 +369,7 @@
   13.81      val _ = case head of Const _ => () | _ =>
   13.82        bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
   13.83      val _ =
   13.84 -      if has_duplicates (op =)
   13.85 +      if linear andalso has_duplicates (op =)
   13.86          ((fold o fold_aterms) (fn Var (v, _) => cons v
   13.87            | _ => I
   13.88          ) args [])
   13.89 @@ -403,7 +392,7 @@
   13.90      val _ = map (check 0) args;
   13.91    in thm end;
   13.92  
   13.93 -val mk_func = rew_alias o assert_func o mk_rew;
   13.94 +fun mk_func linear = assert_func linear o mk_rew;
   13.95  
   13.96  fun head_func thm =
   13.97    let
   13.98 @@ -454,6 +443,6 @@
   13.99  
  13.100  fun case_cert thm = case_certificate thm
  13.101    handle Bind => error "bad case certificate"
  13.102 -      | TERM _ => error "bad case certificate";
  13.103 +       | TERM _ => error "bad case certificate";
  13.104  
  13.105  end;
    14.1 --- a/src/Tools/code/code_name.ML	Wed Sep 24 19:39:25 2008 +0200
    14.2 +++ b/src/Tools/code/code_name.ML	Thu Sep 25 09:28:03 2008 +0200
    14.3 @@ -45,9 +45,8 @@
    14.4          val thy' = case some_thyname
    14.5           of SOME thyname => ThyInfo.the_theory thyname thy
    14.6            | NONE => thy;
    14.7 -        val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
    14.8 +        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
    14.9            ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
   14.10 -        val cs = map (Code_Unit.subst_alias thy') raw_cs;
   14.11          fun belongs_here c =
   14.12            not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
   14.13        in case some_thyname