--- a/NEWS Mon Aug 30 10:36:55 2010 +0200
+++ b/NEWS Mon Aug 30 10:38:28 2010 +0200
@@ -62,6 +62,10 @@
*** HOL ***
+* Renamed class eq and constant eq (for code generation) to class equal
+and constant equal, plus renaming of related facts and various tuning.
+INCOMPATIBILITY.
+
* Scala (2.8 or higher) has been added to the target languages of
the code generator.
@@ -132,6 +136,7 @@
op & ~> HOL.conj
op | ~> HOL.disj
op --> ~> HOL.implies
+ op = ~> HOL.eq
Not ~> HOL.Not
The ~> HOL.The
All ~> HOL.All
--- a/doc-src/Codegen/Thy/Foundations.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Mon Aug 30 10:38:28 2010 +0200
@@ -220,12 +220,12 @@
text {*
\noindent Obviously, polymorphic equality is implemented the Haskell
way using a type class. How is this achieved? HOL introduces an
- explicit class @{class eq} with a corresponding operation @{const
- eq_class.eq} such that @{thm eq [no_vars]}. The preprocessing
- framework does the rest by propagating the @{class eq} constraints
+ explicit class @{class equal} with a corresponding operation @{const
+ HOL.equal} such that @{thm equal [no_vars]}. The preprocessing
+ framework does the rest by propagating the @{class equal} constraints
through all dependent code equations. For datatypes, instances of
- @{class eq} are implicitly derived when possible. For other types,
- you may instantiate @{text eq} manually like any other type class.
+ @{class equal} are implicitly derived when possible. For other types,
+ you may instantiate @{text equal} manually like any other type class.
*}
--- a/src/HOL/Code_Evaluation.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Mon Aug 30 10:38:28 2010 +0200
@@ -162,7 +162,7 @@
subsubsection {* Code generator setup *}
lemmas [code del] = term.recs term.cases term.size
-lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
+lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
--- a/src/HOL/Code_Numeral.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Code_Numeral.thy Mon Aug 30 10:38:28 2010 +0200
@@ -115,12 +115,12 @@
lemmas [code del] = code_numeral.recs code_numeral.cases
lemma [code]:
- "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
- by (cases k, cases l) (simp add: eq)
+ "HOL.equal k l \<longleftrightarrow> HOL.equal (nat_of k) (nat_of l)"
+ by (cases k, cases l) (simp add: equal)
lemma [code nbe]:
- "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+ "HOL.equal (k::code_numeral) k \<longleftrightarrow> True"
+ by (rule equal_refl)
subsection {* Code numerals as datatype of ints *}
@@ -301,7 +301,7 @@
(Haskell "Integer")
(Scala "BigInt")
-code_instance code_numeral :: eq
+code_instance code_numeral :: equal
(Haskell -)
setup {*
@@ -342,7 +342,7 @@
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
(Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
-code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(SML "!((_ : Int.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Aug 30 10:38:28 2010 +0200
@@ -3305,7 +3305,7 @@
(Const (@{const_name Set.member}, _) $
Free (name, _) $ _)) = name
| variable_of_bound (Const (@{const_name Trueprop}, _) $
- (Const (@{const_name "op ="}, _) $
+ (Const (@{const_name HOL.eq}, _) $
Free (name, _) $ _)) = name
| variable_of_bound t = raise TERM ("variable_of_bound", [t])
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 30 10:38:28 2010 +0200
@@ -519,9 +519,9 @@
val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
fun h x t =
case term_of t of
- Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+ Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+ | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
| b$y$z => if Term.could_unify (b, lt) then
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
@@ -771,7 +771,7 @@
in rth end
| _ => Thm.reflexive ct)
-| Const(@{const_name "op ="},_)$_$Const(@{const_name Groups.zero},_) =>
+| Const(@{const_name HOL.eq},_)$_$Const(@{const_name Groups.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -835,7 +835,7 @@
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| Const(@{const_name "op ="},_)$a$b =>
+| Const(@{const_name HOL.eq},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
@@ -844,7 +844,7 @@
(Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| @{term "Not"} $(Const(@{const_name "op ="},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
+| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
| _ => Thm.reflexive ct
end;
@@ -852,9 +852,9 @@
let
fun h x t =
case term_of t of
- Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+ Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+ | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
| Const(@{const_name Orderings.less},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Aug 30 10:38:28 2010 +0200
@@ -912,7 +912,7 @@
definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"
definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"
-definition "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
+definition eq where "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
definition "neq p = not (eq p)"
lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
@@ -2960,7 +2960,7 @@
val ifft = @{term "op = :: bool => _"}
fun llt rT = Const(@{const_name Orderings.less},rrT rT);
fun lle rT = Const(@{const_name Orderings.less},rrT rT);
-fun eqt rT = Const(@{const_name "op ="},rrT rT);
+fun eqt rT = Const(@{const_name HOL.eq},rrT rT);
fun rz rT = Const(@{const_name Groups.zero},rT);
fun dest_nat t = case t of
@@ -3021,7 +3021,7 @@
| Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
- | Const(@{const_name "op ="},ty)$p$q =>
+ | Const(@{const_name HOL.eq},ty)$p$q =>
if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
| Const(@{const_name Orderings.less},_)$p$q =>
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Mon Aug 30 10:38:28 2010 +0200
@@ -65,7 +65,7 @@
(* reification of the equation *)
val cr_sort = @{sort "comm_ring_1"};
-fun reif_eq thy (eq as Const(@{const_name "op ="}, Type("fun", [T, _])) $ lhs $ rhs) =
+fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
if Sign.of_sort thy (T, cr_sort) then
let
val fs = OldTerm.term_frees eq;
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Aug 30 10:38:28 2010 +0200
@@ -175,7 +175,7 @@
let
fun h bounds tm =
(case term_of tm of
- Const (@{const_name "op ="}, T) $ _ $ _ =>
+ Const (@{const_name HOL.eq}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
| Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
--- a/src/HOL/Decision_Procs/langford.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Mon Aug 30 10:38:28 2010 +0200
@@ -116,7 +116,7 @@
fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
fun is_eqx x eq = case term_of eq of
- Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
+ Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
| _ => false ;
local
@@ -176,7 +176,7 @@
let
fun h bounds tm =
(case term_of tm of
- Const (@{const_name "op ="}, T) $ _ $ _ =>
+ Const (@{const_name HOL.eq}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
| Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
--- a/src/HOL/HOL.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/HOL.thy Mon Aug 30 10:38:28 2010 +0200
@@ -61,14 +61,8 @@
disj :: "[bool, bool] => bool" (infixr "|" 30)
implies :: "[bool, bool] => bool" (infixr "-->" 25)
-setup Sign.root_path
+ eq :: "['a, 'a] => bool" (infixl "=" 50)
-consts
- "op =" :: "['a, 'a] => bool" (infixl "=" 50)
-
-setup Sign.local_path
-
-consts
The :: "('a => bool) => 'a"
All :: "('a => bool) => bool" (binder "ALL " 10)
Ex :: "('a => bool) => bool" (binder "EX " 10)
@@ -78,7 +72,7 @@
subsubsection {* Additional concrete syntax *}
notation (output)
- "op =" (infix "=" 50)
+ eq (infix "=" 50)
abbreviation
not_equal :: "['a, 'a] => bool" (infixl "~=" 50) where
@@ -89,15 +83,15 @@
notation (xsymbols)
Not ("\<not> _" [40] 40) and
- HOL.conj (infixr "\<and>" 35) and
- HOL.disj (infixr "\<or>" 30) and
- HOL.implies (infixr "\<longrightarrow>" 25) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ implies (infixr "\<longrightarrow>" 25) and
not_equal (infix "\<noteq>" 50)
notation (HTML output)
Not ("\<not> _" [40] 40) and
- HOL.conj (infixr "\<and>" 35) and
- HOL.disj (infixr "\<or>" 30) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
not_equal (infix "\<noteq>" 50)
abbreviation (iff)
@@ -183,8 +177,8 @@
True_or_False: "(P=True) | (P=False)"
finalconsts
- "op ="
- HOL.implies
+ eq
+ implies
The
definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
@@ -864,7 +858,7 @@
setup {*
let
- fun non_bool_eq (@{const_name "op ="}, Type (_, [T, _])) = T <> @{typ bool}
+ fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
| non_bool_eq _ = false;
val hyp_subst_tac' =
SUBGOAL (fn (goal, i) =>
@@ -930,7 +924,7 @@
(
val thy = @{theory}
type claset = Classical.claset
- val equality_name = @{const_name "op ="}
+ val equality_name = @{const_name HOL.eq}
val not_name = @{const_name Not}
val notE = @{thm notE}
val ccontr = @{thm ccontr}
@@ -1746,8 +1740,8 @@
fun eq_codegen thy defs dep thyname b t gr =
(case strip_comb t of
- (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE
- | (Const (@{const_name "op ="}, _), [t, u]) =>
+ (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
+ | (Const (@{const_name HOL.eq}, _), [t, u]) =>
let
val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
@@ -1756,7 +1750,7 @@
SOME (Codegen.parens
(Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
end
- | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen
+ | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
| _ => NONE);
@@ -1775,31 +1769,30 @@
subsubsection {* Equality *}
-class eq =
- fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
- assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
+class equal =
+ fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
begin
-lemma eq [code_unfold, code_inline del]: "eq = (op =)"
- by (rule ext eq_equals)+
+lemma equal [code_unfold, code_inline del]: "equal = (op =)"
+ by (rule ext equal_eq)+
-lemma eq_refl: "eq x x \<longleftrightarrow> True"
- unfolding eq by rule+
+lemma equal_refl: "equal x x \<longleftrightarrow> True"
+ unfolding equal by rule+
-lemma equals_eq: "(op =) \<equiv> eq"
- by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
-
-declare equals_eq [symmetric, code_post]
+lemma eq_equal: "(op =) \<equiv> equal"
+ by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
end
-declare equals_eq [code]
+declare eq_equal [symmetric, code_post]
+declare eq_equal [code]
setup {*
Code_Preproc.map_pre (fn simpset =>
- simpset addsimprocs [Simplifier.simproc_global_i @{theory} "eq" [@{term "op ="}]
+ simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
(fn thy => fn _ => fn Const (_, T) => case strip_type T
- of (Type _ :: _, _) => SOME @{thm equals_eq}
+ of (Type _ :: _, _) => SOME @{thm eq_equal}
| _ => NONE)])
*}
@@ -1839,51 +1832,49 @@
and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
-instantiation itself :: (type) eq
+instantiation itself :: (type) equal
begin
-definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
- "eq_itself x y \<longleftrightarrow> x = y"
+definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
+ "equal_itself x y \<longleftrightarrow> x = y"
instance proof
-qed (fact eq_itself_def)
+qed (fact equal_itself_def)
end
-lemma eq_itself_code [code]:
- "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
- by (simp add: eq)
+lemma equal_itself_code [code]:
+ "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
+ by (simp add: equal)
text {* Equality *}
declare simp_thms(6) [code nbe]
setup {*
- Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
+ Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
*}
-lemma equals_alias_cert: "OFCLASS('a, eq_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> eq)" (is "?ofclass \<equiv> ?eq")
+lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
proof
assume "PROP ?ofclass"
- show "PROP ?eq"
- by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm equals_eq})) *})
+ show "PROP ?equal"
+ by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm eq_equal})) *})
(fact `PROP ?ofclass`)
next
- assume "PROP ?eq"
+ assume "PROP ?equal"
show "PROP ?ofclass" proof
- qed (simp add: `PROP ?eq`)
+ qed (simp add: `PROP ?equal`)
qed
setup {*
- Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>eq \<Rightarrow> 'a \<Rightarrow> bool"})
+ Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})
*}
setup {*
- Nbe.add_const_alias @{thm equals_alias_cert}
+ Nbe.add_const_alias @{thm equal_alias_cert}
*}
-hide_const (open) eq
-
text {* Cases *}
lemma Let_case_cert:
@@ -1939,13 +1930,13 @@
text {* using built-in Haskell equality *}
-code_class eq
+code_class equal
(Haskell "Eq")
-code_const "eq_class.eq"
+code_const "HOL.equal"
(Haskell infixl 4 "==")
-code_const "op ="
+code_const HOL.eq
(Haskell infixl 4 "==")
text {* undefined *}
@@ -2134,4 +2125,6 @@
*}
+hide_const (open) eq equal
+
end
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Mon Aug 30 10:38:28 2010 +0200
@@ -53,7 +53,7 @@
F > False
ONE_ONE > HOL4Setup.ONE_ONE
ONTO > Fun.surj
- "=" > "op ="
+ "=" > HOL.eq
"==>" > HOL.implies
"/\\" > HOL.conj
"\\/" > HOL.disj
--- a/src/HOL/Import/HOLLight/hollight.imp Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Mon Aug 30 10:38:28 2010 +0200
@@ -234,7 +234,7 @@
">=" > "HOLLight.hollight.>="
">" > "HOLLight.hollight.>"
"==>" > HOL.implies
- "=" > "op ="
+ "=" > HOL.eq
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
"/\\" > HOL.conj
--- a/src/HOL/Import/hol4rews.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Mon Aug 30 10:38:28 2010 +0200
@@ -627,7 +627,7 @@
thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
|> add_hol4_type_mapping "min" "fun" false "fun"
|> add_hol4_type_mapping "min" "ind" false @{type_name ind}
- |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
+ |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq}
|> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
|> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
in
--- a/src/HOL/Import/proof_kernel.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Aug 30 10:38:28 2010 +0200
@@ -1205,7 +1205,7 @@
fun non_trivial_term_consts t = fold_aterms
(fn Const (c, _) =>
if c = @{const_name Trueprop} orelse c = @{const_name All}
- orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
+ orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name HOL.eq}
then I else insert (op =) c
| _ => I) t [];
@@ -1213,7 +1213,7 @@
let
fun add_consts (Const (c, _), cs) =
(case c of
- @{const_name "op ="} => insert (op =) "==" cs
+ @{const_name HOL.eq} => insert (op =) "==" cs
| @{const_name HOL.implies} => insert (op =) "==>" cs
| @{const_name All} => cs
| "all" => cs
@@ -1476,10 +1476,10 @@
fun mk_COMB th1 th2 thy =
let
val (f,g) = case concl_of th1 of
- _ $ (Const(@{const_name "op ="},_) $ f $ g) => (f,g)
+ _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (f,g)
| _ => raise ERR "mk_COMB" "First theorem not an equality"
val (x,y) = case concl_of th2 of
- _ $ (Const(@{const_name "op ="},_) $ x $ y) => (x,y)
+ _ $ (Const(@{const_name HOL.eq},_) $ x $ y) => (x,y)
| _ => raise ERR "mk_COMB" "Second theorem not an equality"
val fty = type_of f
val (fd,fr) = dom_rng fty
@@ -1788,7 +1788,7 @@
val cv = cterm_of thy v
val th1 = implies_elim_all (beta_eta_thm th)
val (f,g) = case concl_of th1 of
- _ $ (Const(@{const_name "op ="},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
+ _ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
| _ => raise ERR "mk_ABS" "Bad conclusion"
val (fd,fr) = dom_rng (type_of f)
val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
--- a/src/HOL/Import/shuffler.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Mon Aug 30 10:38:28 2010 +0200
@@ -60,14 +60,14 @@
fun mk_meta_eq th =
(case concl_of th of
- Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
+ Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th RS eq_reflection
| Const("==",_) $ _ $ _ => th
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make meta equality",0,[th]) (* FIXME avoid handle _ *)
fun mk_obj_eq th =
(case concl_of th of
- Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
+ Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th
| Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *)
--- a/src/HOL/Int.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Int.thy Mon Aug 30 10:38:28 2010 +0200
@@ -2222,42 +2222,42 @@
mult_bin_simps
arith_extra_simps(4) [where 'a = int]
-instantiation int :: eq
+instantiation int :: equal
begin
definition
- "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
-
-instance by default (simp add: eq_int_def)
+ "HOL.equal k l \<longleftrightarrow> k - l = (0\<Colon>int)"
+
+instance by default (simp add: equal_int_def)
end
lemma eq_number_of_int_code [code]:
- "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
- unfolding eq_int_def number_of_is_id ..
+ "HOL.equal (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> HOL.equal k l"
+ unfolding equal_int_def number_of_is_id ..
lemma eq_int_code [code]:
- "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
- "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
- "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
- "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
- "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
- "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
- "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
- "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
- "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
- "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
- "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
- "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
- "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
- "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
- "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
- "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
- unfolding eq_equals by simp_all
+ "HOL.equal Int.Pls Int.Pls \<longleftrightarrow> True"
+ "HOL.equal Int.Pls Int.Min \<longleftrightarrow> False"
+ "HOL.equal Int.Pls (Int.Bit0 k2) \<longleftrightarrow> HOL.equal Int.Pls k2"
+ "HOL.equal Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
+ "HOL.equal Int.Min Int.Pls \<longleftrightarrow> False"
+ "HOL.equal Int.Min Int.Min \<longleftrightarrow> True"
+ "HOL.equal Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
+ "HOL.equal Int.Min (Int.Bit1 k2) \<longleftrightarrow> HOL.equal Int.Min k2"
+ "HOL.equal (Int.Bit0 k1) Int.Pls \<longleftrightarrow> HOL.equal k1 Int.Pls"
+ "HOL.equal (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
+ "HOL.equal (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
+ "HOL.equal (Int.Bit1 k1) Int.Min \<longleftrightarrow> HOL.equal k1 Int.Min"
+ "HOL.equal (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> HOL.equal k1 k2"
+ "HOL.equal (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
+ "HOL.equal (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
+ "HOL.equal (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> HOL.equal k1 k2"
+ unfolding equal_eq by simp_all
lemma eq_int_refl [code nbe]:
- "eq_class.eq (k::int) k \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+ "HOL.equal (k::int) k \<longleftrightarrow> True"
+ by (rule equal_refl)
lemma less_eq_number_of_int_code [code]:
"(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
--- a/src/HOL/Lazy_Sequence.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy Mon Aug 30 10:38:28 2010 +0200
@@ -39,10 +39,14 @@
"size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
by (cases xq) auto
-lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
- (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
-apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals)
-apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
+lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
+ (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
+apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq)
+apply (cases yq) apply (auto simp add: equal_eq) done
+
+lemma [code nbe]:
+ "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
+ by (fact equal_refl)
lemma seq_case [code]:
"lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
--- a/src/HOL/Library/AssocList.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/AssocList.thy Mon Aug 30 10:38:28 2010 +0200
@@ -701,7 +701,44 @@
"Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
-lemma [code, code del]:
- "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
+lemma map_of_eqI: (*FIXME move to Map.thy*)
+ assumes set_eq: "set (map fst xs) = set (map fst ys)"
+ assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
+ shows "map_of xs = map_of ys"
+proof (rule ext)
+ fix k show "map_of xs k = map_of ys k"
+ proof (cases "map_of xs k")
+ case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
+ with set_eq have "k \<notin> set (map fst ys)" by simp
+ then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
+ with None show ?thesis by simp
+ next
+ case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
+ with map_eq show ?thesis by auto
+ qed
+qed
+
+lemma map_of_eq_dom: (*FIXME move to Map.thy*)
+ assumes "map_of xs = map_of ys"
+ shows "fst ` set xs = fst ` set ys"
+proof -
+ from assms have "dom (map_of xs) = dom (map_of ys)" by simp
+ then show ?thesis by (simp add: dom_map_of_conv_image_fst)
+qed
+
+lemma equal_Mapping [code]:
+ "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
+ (let ks = map fst xs; ls = map fst ys
+ in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
+proof -
+ have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" by (auto simp add: image_def intro!: bexI)
+ show ?thesis
+ by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
+ (auto dest!: map_of_eq_dom intro: aux)
+qed
+
+lemma [code nbe]:
+ "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
+ by (fact equal_refl)
end
--- a/src/HOL/Library/Code_Char.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy Mon Aug 30 10:38:28 2010 +0200
@@ -19,7 +19,7 @@
#> String_Code.add_literal_list_string "Haskell"
*}
-code_instance char :: eq
+code_instance char :: equal
(Haskell -)
code_reserved SML
@@ -31,7 +31,7 @@
code_reserved Scala
char
-code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
(SML "!((_ : char) = _)")
(OCaml "!((_ : char) = _)")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Code_Integer.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy Mon Aug 30 10:38:28 2010 +0200
@@ -21,7 +21,7 @@
(Scala "BigInt")
(Eval "int")
-code_instance int :: eq
+code_instance int :: equal
(Haskell -)
setup {*
@@ -96,7 +96,7 @@
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
(Eval "Integer.div'_mod/ (abs _)/ (abs _)")
-code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Code_Natural.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Mon Aug 30 10:38:28 2010 +0200
@@ -112,7 +112,7 @@
false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
*}
-code_instance code_numeral :: eq
+code_instance code_numeral :: equal
(Haskell -)
code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
@@ -131,7 +131,7 @@
(Haskell "divMod")
(Scala infixl 8 "/%")
-code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(Haskell infixl 4 "==")
(Scala infixl 5 "==")
--- a/src/HOL/Library/Dlist.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Aug 30 10:38:28 2010 +0200
@@ -109,16 +109,20 @@
text {* Equality *}
-instantiation dlist :: (eq) eq
+instantiation dlist :: (equal) equal
begin
-definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
+definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
instance proof
-qed (simp add: eq_dlist_def eq list_of_dlist_inject)
+qed (simp add: equal_dlist_def equal list_of_dlist_inject)
end
+lemma [code nbe]:
+ "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
+ by (fact equal_refl)
+
section {* Induction principle and case distinction *}
--- a/src/HOL/Library/Efficient_Nat.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Mon Aug 30 10:38:28 2010 +0200
@@ -55,12 +55,12 @@
by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
lemma eq_nat_code [code]:
- "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
- by (simp add: eq)
+ "HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
+ by (simp add: equal)
lemma eq_nat_refl [code nbe]:
- "eq_class.eq (n::nat) n \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+ "HOL.equal (n::nat) n \<longleftrightarrow> True"
+ by (rule equal_refl)
lemma less_eq_nat_code [code]:
"n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m"
@@ -332,7 +332,7 @@
(Haskell "Nat.Nat")
(Scala "Nat.Nat")
-code_instance nat :: eq
+code_instance nat :: equal
(Haskell -)
text {*
@@ -442,7 +442,7 @@
(Scala infixl 8 "/%")
(Eval "Integer.div'_mod")
-code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Enum.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Enum.thy Mon Aug 30 10:38:28 2010 +0200
@@ -35,17 +35,21 @@
subsection {* Equality and order on functions *}
-instantiation "fun" :: (enum, eq) eq
+instantiation "fun" :: (enum, equal) equal
begin
definition
- "eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
+ "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
instance proof
-qed (simp_all add: eq_fun_def enum_all expand_fun_eq)
+qed (simp_all add: equal_fun_def enum_all expand_fun_eq)
end
+lemma [code nbe]:
+ "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
+ by (fact equal_refl)
+
lemma order_fun [code]:
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
@@ -169,7 +173,7 @@
end
-lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
+lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
by (simp add: enum_fun_def Let_def)
--- a/src/HOL/Library/Fset.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Fset.thy Mon Aug 30 10:38:28 2010 +0200
@@ -227,17 +227,21 @@
"A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
by (fact less_le_not_le)
-instantiation fset :: (type) eq
+instantiation fset :: (type) equal
begin
definition
- "eq_fset A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
+ "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
instance proof
-qed (simp add: eq_fset_def set_eq [symmetric])
+qed (simp add: equal_fset_def set_eq [symmetric])
end
+lemma [code nbe]:
+ "HOL.equal (A :: 'a fset) A \<longleftrightarrow> True"
+ by (fact equal_refl)
+
subsection {* Functorial operations *}
--- a/src/HOL/Library/List_Prefix.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/List_Prefix.thy Mon Aug 30 10:38:28 2010 +0200
@@ -81,9 +81,9 @@
by (auto simp add: prefix_def)
lemma less_eq_list_code [code]:
- "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
- "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
- "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
+ "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"
+ "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False"
+ "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
by simp_all
lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
--- a/src/HOL/Library/List_lexord.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/List_lexord.thy Mon Aug 30 10:38:28 2010 +0200
@@ -103,15 +103,15 @@
end
lemma less_list_code [code]:
- "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
- "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
- "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
+ "xs < ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
+ "[] < (x\<Colon>'a\<Colon>{equal, order}) # xs \<longleftrightarrow> True"
+ "(x\<Colon>'a\<Colon>{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
by simp_all
lemma less_eq_list_code [code]:
- "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
- "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
- "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
+ "x # xs \<le> ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
+ "[] \<le> (xs\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> True"
+ "(x\<Colon>'a\<Colon>{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
by simp_all
end
--- a/src/HOL/Library/Mapping.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Mon Aug 30 10:38:28 2010 +0200
@@ -280,14 +280,14 @@
code_datatype empty update
-instantiation mapping :: (type, type) eq
+instantiation mapping :: (type, type) equal
begin
definition [code del]:
- "HOL.eq m n \<longleftrightarrow> lookup m = lookup n"
+ "HOL.equal m n \<longleftrightarrow> lookup m = lookup n"
instance proof
-qed (simp add: eq_mapping_def)
+qed (simp add: equal_mapping_def)
end
--- a/src/HOL/Library/Multiset.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Aug 30 10:38:28 2010 +0200
@@ -938,17 +938,21 @@
qed
qed
-instantiation multiset :: (eq) eq
+instantiation multiset :: (equal) equal
begin
definition
- "HOL.eq A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
+ "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
instance proof
-qed (simp add: eq_multiset_def eq_iff)
+qed (simp add: equal_multiset_def eq_iff)
end
+lemma [code nbe]:
+ "HOL.equal (A :: 'a::equal multiset) A \<longleftrightarrow> True"
+ by (fact equal_refl)
+
definition (in term_syntax)
bagify :: "('a\<Colon>typerep \<times> nat) list \<times> (unit \<Rightarrow> Code_Evaluation.term)
\<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
--- a/src/HOL/Library/Nested_Environment.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Nested_Environment.thy Mon Aug 30 10:38:28 2010 +0200
@@ -521,22 +521,21 @@
text {* Environments and code generation *}
lemma [code, code del]:
- fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
- shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
+ "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
-lemma eq_env_code [code]:
- fixes x y :: "'a\<Colon>eq"
- and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
- shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
- eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z
+lemma equal_env_code [code]:
+ fixes x y :: "'a\<Colon>equal"
+ and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
+ shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
+ HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
of None \<Rightarrow> (case g z
of None \<Rightarrow> True | Some _ \<Rightarrow> False)
| Some a \<Rightarrow> (case g z
- of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)
- and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"
- and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"
- and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"
-proof (unfold eq)
+ of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
+ and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
+ and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
+ and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
+proof (unfold equal)
have "f = g \<longleftrightarrow> (\<forall>z. case f z
of None \<Rightarrow> (case g z
of None \<Rightarrow> True | Some _ \<Rightarrow> False)
@@ -562,6 +561,10 @@
of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
qed simp_all
+lemma [code nbe]:
+ "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
+ by (fact equal_refl)
+
lemma [code, code del]:
"(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
--- a/src/HOL/Library/OptionalSugar.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Mon Aug 30 10:38:28 2010 +0200
@@ -32,7 +32,7 @@
(* deprecated, use thm with style instead, will be removed *)
(* aligning equations *)
notation (tab output)
- "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
+ "HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
"==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
(* Let *)
--- a/src/HOL/Library/Polynomial.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Aug 30 10:38:28 2010 +0200
@@ -1505,23 +1505,27 @@
declare pCons_0_0 [code_post]
-instantiation poly :: ("{zero,eq}") eq
+instantiation poly :: ("{zero, equal}") equal
begin
definition
- "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
+ "HOL.equal (p::'a poly) q \<longleftrightarrow> p = q"
-instance
- by default (rule eq_poly_def)
+instance proof
+qed (rule equal_poly_def)
end
lemma eq_poly_code [code]:
- "eq_class.eq (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
- "eq_class.eq (0::_ poly) (pCons b q) \<longleftrightarrow> eq_class.eq 0 b \<and> eq_class.eq 0 q"
- "eq_class.eq (pCons a p) (0::_ poly) \<longleftrightarrow> eq_class.eq a 0 \<and> eq_class.eq p 0"
- "eq_class.eq (pCons a p) (pCons b q) \<longleftrightarrow> eq_class.eq a b \<and> eq_class.eq p q"
-unfolding eq by simp_all
+ "HOL.equal (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
+ "HOL.equal (0::_ poly) (pCons b q) \<longleftrightarrow> HOL.equal 0 b \<and> HOL.equal 0 q"
+ "HOL.equal (pCons a p) (0::_ poly) \<longleftrightarrow> HOL.equal a 0 \<and> HOL.equal p 0"
+ "HOL.equal (pCons a p) (pCons b q) \<longleftrightarrow> HOL.equal a b \<and> HOL.equal p q"
+ by (simp_all add: equal)
+
+lemma [code nbe]:
+ "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
+ by (fact equal_refl)
lemmas coeff_code [code] =
coeff_0 coeff_pCons_0 coeff_pCons_Suc
--- a/src/HOL/Library/Product_ord.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/Product_ord.thy Mon Aug 30 10:38:28 2010 +0200
@@ -22,8 +22,8 @@
end
lemma [code]:
- "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
- "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
+ "(x1\<Colon>'a\<Colon>{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
+ "(x1\<Colon>'a\<Colon>{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
unfolding prod_le_def prod_less_def by simp_all
instance prod :: (preorder, preorder) preorder proof
--- a/src/HOL/Library/RBT.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/RBT.thy Mon Aug 30 10:38:28 2010 +0200
@@ -222,12 +222,14 @@
"Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
-lemma [code, code del]:
- "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
+lemma equal_Mapping [code]:
+ "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
+ by (simp add: equal Mapping_def entries_lookup)
-lemma eq_Mapping [code]:
- "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
- by (simp add: eq Mapping_def entries_lookup)
+lemma [code nbe]:
+ "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
+ by (fact equal_refl)
+
hide_const (open) impl_of lookup empty insert delete
entries keys bulkload map_entry map fold
--- a/src/HOL/Library/reflection.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Library/reflection.ML Mon Aug 30 10:38:28 2010 +0200
@@ -82,7 +82,7 @@
fun rearrange congs =
let
fun P (_, th) =
- let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th
+ let val @{term "Trueprop"}$(Const (@{const_name HOL.eq},_) $l$_) = concl_of th
in can dest_Var l end
val (yes,no) = List.partition P congs
in no @ yes end
--- a/src/HOL/List.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/List.thy Mon Aug 30 10:38:28 2010 +0200
@@ -4721,8 +4721,8 @@
by (simp add: null_def)
lemma equal_Nil_null [code_unfold]:
- "eq_class.eq xs [] \<longleftrightarrow> null xs"
- by (simp add: eq eq_Nil_null)
+ "HOL.equal xs [] \<longleftrightarrow> null xs"
+ by (simp add: equal eq_Nil_null)
definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
[code_post]: "maps f xs = concat (map f xs)"
@@ -4821,10 +4821,10 @@
(Haskell "[]")
(Scala "!Nil")
-code_instance list :: eq
+code_instance list :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML
--- a/src/HOL/Mutabelle/Mutabelle.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy Mon Aug 30 10:38:28 2010 +0200
@@ -4,7 +4,7 @@
begin
ML {*
-val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
+val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
val forbidden =
[(@{const_name Power.power}, "'a"),
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Aug 30 10:38:28 2010 +0200
@@ -187,7 +187,7 @@
val nitpick_mtd = ("nitpick", invoke_nitpick)
*)
-val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
+val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
val forbidden =
[(* (@{const_name "power"}, "'a"), *)
@@ -202,7 +202,7 @@
(@{const_name "top_fun_inst.top_fun"}, "'a"),
(@{const_name "Pure.term"}, "'a"),
(@{const_name "top_class.top"}, "'a"),
- (@{const_name "eq_class.eq"}, "'a"),
+ (@{const_name "HOL.equal"}, "'a"),
(@{const_name "Quotient.Quot_True"}, "'a")(*,
(@{const_name "uminus"}, "'a"),
(@{const_name "Nat.size"}, "'a"),
@@ -237,7 +237,7 @@
@{const_name "top_fun_inst.top_fun"},
@{const_name "Pure.term"},
@{const_name "top_class.top"},
- @{const_name "eq_class.eq"},
+ @{const_name "HOL.equal"},
@{const_name "Quotient.Quot_True"}]
fun is_forbidden_mutant t =
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Aug 30 10:38:28 2010 +0200
@@ -183,7 +183,7 @@
end;
fun mk_not_sym ths = maps (fn th => case prop_of th of
- _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
+ _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
| _ => [th]) ths;
fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
--- a/src/HOL/Nominal/nominal_thmdecls.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon Aug 30 10:38:28 2010 +0200
@@ -147,7 +147,7 @@
else raise EQVT_FORM "Type Implication"
end
(* case: eqvt-lemma is of the equational form *)
- | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
+ | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
(Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
(if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
--- a/src/HOL/Option.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Option.thy Mon Aug 30 10:38:28 2010 +0200
@@ -99,8 +99,8 @@
by (simp add: is_none_def)
lemma [code_unfold]:
- "eq_class.eq x None \<longleftrightarrow> is_none x"
- by (simp add: eq is_none_none)
+ "HOL.equal x None \<longleftrightarrow> is_none x"
+ by (simp add: equal is_none_none)
hide_const (open) is_none
@@ -116,10 +116,10 @@
(Haskell "Nothing" and "Just")
(Scala "!None" and "Some")
-code_instance option :: eq
+code_instance option :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML
--- a/src/HOL/Predicate.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Predicate.thy Mon Aug 30 10:38:28 2010 +0200
@@ -808,8 +808,12 @@
lemma eq_pred_code [code]:
fixes P Q :: "'a pred"
- shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
- unfolding eq by auto
+ shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
+ by (auto simp add: equal)
+
+lemma [code nbe]:
+ "HOL.equal (x :: 'a pred) x \<longleftrightarrow> True"
+ by (fact equal_refl)
lemma [code]:
"pred_case f P = f (eval P)"
--- a/src/HOL/Product_Type.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Product_Type.thy Mon Aug 30 10:38:28 2010 +0200
@@ -21,17 +21,17 @@
-- "prefer plain propositional version"
lemma
- shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
- and [code]: "eq_class.eq True P \<longleftrightarrow> P"
- and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P"
- and [code]: "eq_class.eq P True \<longleftrightarrow> P"
- and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
- by (simp_all add: eq)
+ shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
+ and [code]: "HOL.equal True P \<longleftrightarrow> P"
+ and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
+ and [code]: "HOL.equal P True \<longleftrightarrow> P"
+ and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
+ by (simp_all add: equal)
-code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
(Haskell infixl 4 "==")
-code_instance bool :: eq
+code_instance bool :: equal
(Haskell -)
@@ -92,7 +92,7 @@
end
lemma [code]:
- "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
+ "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
code_type unit
(SML "unit")
@@ -106,10 +106,10 @@
(Haskell "()")
(Scala "()")
-code_instance unit :: eq
+code_instance unit :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML
@@ -277,10 +277,10 @@
(Haskell "!((_),/ (_))")
(Scala "!((_),/ (_))")
-code_instance prod :: eq
+code_instance prod :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
(Haskell infixl 4 "==")
types_code
--- a/src/HOL/Quickcheck.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Quickcheck.thy Mon Aug 30 10:38:28 2010 +0200
@@ -97,7 +97,7 @@
\<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
"random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
-instantiation "fun" :: ("{eq, term_of}", random) random
+instantiation "fun" :: ("{equal, term_of}", random) random
begin
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
--- a/src/HOL/Quotient.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Quotient.thy Mon Aug 30 10:38:28 2010 +0200
@@ -651,6 +651,16 @@
shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
by auto
+lemma mem_rsp:
+ shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
+ by (simp add: mem_def)
+
+lemma mem_prs:
+ assumes a1: "Quotient R1 Abs1 Rep1"
+ and a2: "Quotient R2 Abs2 Rep2"
+ shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
+ by (simp add: expand_fun_eq mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
+
locale quot_type =
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -721,8 +731,8 @@
declare [[map "fun" = (fun_map, fun_rel)]]
lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp
-lemmas [quot_preserve] = if_prs o_prs let_prs
+lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp
+lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs
lemmas [quot_equiv] = identity_equivp
@@ -773,20 +783,20 @@
method_setup lifting =
{* Attrib.thms >> (fn thms => fn ctxt =>
- SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
+ SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
{* lifts theorems to quotient types *}
method_setup lifting_setup =
{* Attrib.thm >> (fn thm => fn ctxt =>
- SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *}
+ SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
{* sets up the three goals for the quotient lifting procedure *}
method_setup descending =
- {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *}
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
{* decends theorems to the raw level *}
method_setup descending_setup =
- {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt))) *}
+ {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
{* sets up the three goals for the decending theorems *}
method_setup regularize =
--- a/src/HOL/Rat.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Rat.thy Mon Aug 30 10:38:28 2010 +0200
@@ -1083,18 +1083,18 @@
by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
qed
-instantiation rat :: eq
+instantiation rat :: equal
begin
definition [code]:
- "eq_class.eq a b \<longleftrightarrow> quotient_of a = quotient_of b"
+ "HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b"
instance proof
-qed (simp add: eq_rat_def quotient_of_inject_eq)
+qed (simp add: equal_rat_def quotient_of_inject_eq)
lemma rat_eq_refl [code nbe]:
- "eq_class.eq (r::rat) r \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+ "HOL.equal (r::rat) r \<longleftrightarrow> True"
+ by (rule equal_refl)
end
--- a/src/HOL/RealDef.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/RealDef.thy Mon Aug 30 10:38:28 2010 +0200
@@ -1697,19 +1697,21 @@
"Ratreal (number_of r / number_of s) = number_of r / number_of s"
unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
-instantiation real :: eq
+instantiation real :: equal
begin
-definition "eq_class.eq (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
+definition "HOL.equal (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
-instance by default (simp add: eq_real_def)
+instance proof
+qed (simp add: equal_real_def)
-lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq x y"
- by (simp add: eq_real_def eq)
+lemma real_equal_code [code]:
+ "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
+ by (simp add: equal_real_def equal)
-lemma real_eq_refl [code nbe]:
- "eq_class.eq (x::real) x \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+lemma [code nbe]:
+ "HOL.equal (x::real) x \<longleftrightarrow> True"
+ by (rule equal_refl)
end
--- a/src/HOL/Set.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Set.thy Mon Aug 30 10:38:28 2010 +0200
@@ -268,7 +268,7 @@
fun setcompr_tr [e, idts, b] =
let
- val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
+ val eq = Syntax.const @{const_syntax HOL.eq} $ Bound (nvars idts) $ e;
val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
val exP = ex_tr [idts, P];
in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
@@ -289,7 +289,7 @@
let
fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
| check (Const (@{const_syntax HOL.conj}, _) $
- (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
+ (Const (@{const_syntax HOL.eq}, _) $ Bound m $ e) $ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
| check _ = false;
--- a/src/HOL/Statespace/distinct_tree_prover.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Mon Aug 30 10:38:28 2010 +0200
@@ -343,7 +343,7 @@
end handle Option => NONE)
fun distinctTree_tac names ctxt
- (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
+ (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)), i) =
(case get_fst_success (neq_x_y ctxt x y) names of
SOME neq => rtac neq i
| NONE => no_tac)
@@ -356,7 +356,7 @@
fun distinct_simproc names =
Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
- (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
+ (fn thy => fn ss => fn (Const (@{const_name HOL.eq},_)$x$y) =>
case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])
(get_fst_success (neq_x_y ctxt x y) names)
--- a/src/HOL/Statespace/state_fun.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Mon Aug 30 10:38:28 2010 +0200
@@ -285,7 +285,7 @@
then Bound 2
else raise TERM ("",[n]);
val sel' = lo $ d $ n' $ s;
- in (Const (@{const_name "op ="},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
+ in (Const (@{const_name HOL.eq},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
fun dest_state (s as Bound 0) = s
| dest_state (s as (Const (sel,sT)$Bound 0)) =
@@ -295,10 +295,10 @@
| dest_state s =
raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
- fun dest_sel_eq (Const (@{const_name "op ="},Teq)$
+ fun dest_sel_eq (Const (@{const_name HOL.eq},Teq)$
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
(false,Teq,lT,lo,d,n,X,dest_state s)
- | dest_sel_eq (Const (@{const_name "op ="},Teq)$X$
+ | dest_sel_eq (Const (@{const_name HOL.eq},Teq)$X$
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
(true,Teq,lT,lo,d,n,X,dest_state s)
| dest_sel_eq _ = raise TERM ("",[]);
--- a/src/HOL/Statespace/state_space.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Mon Aug 30 10:38:28 2010 +0200
@@ -223,7 +223,7 @@
fun distinctTree_tac ctxt
(Const (@{const_name Trueprop},_) $
- (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
+ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) =
(case (neq_x_y ctxt x y) of
SOME neq => rtac neq i
| NONE => no_tac)
@@ -236,7 +236,7 @@
val distinct_simproc =
Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
- (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
+ (fn thy => fn ss => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) =>
(case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
(neq_x_y ctxt x y)
--- a/src/HOL/String.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/String.thy Mon Aug 30 10:38:28 2010 +0200
@@ -183,10 +183,10 @@
fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
*}
-code_instance literal :: eq
+code_instance literal :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
(SML "!((_ : string) = _)")
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Aug 30 10:38:28 2010 +0200
@@ -416,7 +416,7 @@
fun prove_case_cong ((t, nchotomy), case_rewrites) =
let
val (Const ("==>", _) $ tm $ _) = t;
- val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ Ma)) = tm;
+ val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma)) = tm;
val cert = cterm_of thy;
val nchotomy' = nchotomy RS spec;
val [v] = Term.add_vars (concl_of nchotomy') [];
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Aug 30 10:38:28 2010 +0200
@@ -68,7 +68,7 @@
val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
Datatype_Data.the_info thy tyco;
val ty = Type (tyco, map TFree vs);
- fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
+ fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT)
$ t1 $ t2;
fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
@@ -83,7 +83,7 @@
val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps
- (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
+ (map Simpdata.mk_eq (@{thm equal} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
|> Simpdata.mk_eq;
in (map prove (triv_injects @ injects @ distincts), prove refl) end;
@@ -96,7 +96,7 @@
fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
$ Free ("x", ty) $ Free ("y", ty);
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
- (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
+ (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
val def' = Syntax.check_term lthy def;
val ((_, (_, thm)), lthy') = Specification.definition
(NONE, (Attrib.empty_binding, def')) lthy;
@@ -115,7 +115,7 @@
#> snd
in
thy
- |> Class.instantiation (tycos, vs, [HOLogic.class_eq])
+ |> Class.instantiation (tycos, vs, [HOLogic.class_equal])
|> fold_map add_def tycos
|-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
(fn _ => fn def_thms => tac def_thms) def_thms)
@@ -135,7 +135,7 @@
val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
val certs = map (mk_case_cert thy) tycos;
val tycos_eq = filter_out
- (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_eq]) tycos;
+ (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_equal]) tycos;
in
if null css then thy
else thy
--- a/src/HOL/Tools/Function/termination.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Mon Aug 30 10:38:28 2010 +0200
@@ -148,7 +148,7 @@
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+ val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
= Term.strip_qnt_body @{const_name Ex} c
in cons r o cons l end
in
@@ -185,7 +185,7 @@
val vs = Term.strip_qnt_vars @{const_name Ex} c
(* FIXME: throw error "dest_call" for malformed terms *)
- val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+ val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
= Term.strip_qnt_body @{const_name Ex} c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
--- a/src/HOL/Tools/Nitpick/minipick.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Mon Aug 30 10:38:28 2010 +0200
@@ -123,7 +123,7 @@
Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
| (t0 as Const (@{const_name Ex}, _)) $ t1 =>
to_F Ts (t0 $ eta_expand Ts t1 1)
- | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
+ | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
| Const (@{const_name ord_class.less_eq},
Type (@{type_name fun},
@@ -165,8 +165,8 @@
@{const Not} => to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name ord_class.less_eq},
Type (@{type_name fun},
[Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Aug 30 10:38:28 2010 +0200
@@ -182,7 +182,7 @@
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
val syntactic_sorts =
- @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
+ @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
@{sort number}
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
subset (op =) (S, syntactic_sorts)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 30 10:38:28 2010 +0200
@@ -408,7 +408,7 @@
(@{const_name True}, 0),
(@{const_name All}, 1),
(@{const_name Ex}, 1),
- (@{const_name "op ="}, 1),
+ (@{const_name HOL.eq}, 1),
(@{const_name HOL.conj}, 2),
(@{const_name HOL.disj}, 2),
(@{const_name HOL.implies}, 2),
@@ -1275,7 +1275,7 @@
forall is_Var args andalso not (has_duplicates (op =) args)
| _ => false
fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
- | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
+ | do_eq (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)) =
do_lhs t1
| do_eq _ = false
in do_eq end
@@ -1347,7 +1347,7 @@
@{const "==>"} $ _ $ t2 => term_under_def t2
| Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
| @{const Trueprop} $ t1 => term_under_def t1
- | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
+ | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
| Abs (_, _, t') => term_under_def t'
| t1 $ _ => term_under_def t1
| _ => t
@@ -1371,7 +1371,7 @@
val (lhs, rhs) =
case t of
Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
(t1, t2)
| _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
val args = strip_comb lhs |> snd
@@ -1453,7 +1453,7 @@
| @{const "==>"} $ _ $ t2 => lhs_of_equation t2
| @{const Trueprop} $ t1 => lhs_of_equation t1
| Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
- | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
+ | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
| @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
| _ => NONE
fun is_constr_pattern _ (Bound _) = true
@@ -1807,7 +1807,7 @@
(betapply (t2, var_t))
end
| extensional_equal _ T t1 t2 =
- Const (@{const_name "op ="}, T --> T --> bool_T) $ t1 $ t2
+ Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
fun equationalize_term ctxt tag t =
let
@@ -1816,7 +1816,7 @@
in
Logic.list_implies (prems,
case concl of
- @{const Trueprop} $ (Const (@{const_name "op ="}, Type (_, [T, _]))
+ @{const Trueprop} $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
$ t1 $ t2) =>
@{const Trueprop} $ extensional_equal j T t1 t2
| @{const Trueprop} $ t' =>
@@ -2290,7 +2290,7 @@
| simps => simps
fun is_equational_fun_surely_complete hol_ctxt x =
case equational_fun_axioms hol_ctxt x of
- [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
+ [@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)] =>
strip_comb t1 |> snd |> forall is_Var
| _ => false
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Aug 30 10:38:28 2010 +0200
@@ -590,7 +590,7 @@
if co then
Const (@{const_name The}, (T --> bool_T) --> T)
$ Abs (cyclic_co_val_name (), T,
- Const (@{const_name "op ="}, T --> T --> bool_T)
+ Const (@{const_name HOL.eq}, T --> T --> bool_T)
$ Bound 0 $ abstract_over (var, t))
else
cyclic_atom ()
@@ -849,7 +849,7 @@
(** Model reconstruction **)
fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
- $ Abs (s, T, Const (@{const_name "op ="}, _)
+ $ Abs (s, T, Const (@{const_name HOL.eq}, _)
$ Bound 0 $ t')) =
betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
| unfold_outer_the_binders t = t
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Aug 30 10:38:28 2010 +0200
@@ -222,7 +222,7 @@
| fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
| fin_fun_body dom_T ran_T
((t0 as Const (@{const_name If}, _))
- $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
+ $ (t1 as Const (@{const_name HOL.eq}, _) $ Bound 0 $ t1')
$ t2 $ t3) =
(if loose_bvar1 (t1', 0) then
NONE
@@ -650,7 +650,7 @@
Bound 0)))) accum
|>> mtype_of_mterm
end
- | @{const_name "op ="} => do_equals T accum
+ | @{const_name HOL.eq} => do_equals T accum
| @{const_name The} =>
(trace_msg (K "*** The"); raise UNSOLVABLE ())
| @{const_name Eps} =>
@@ -760,7 +760,7 @@
do_term (incr_boundvars ~1 t1') accum
else
raise SAME ()
- | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 =>
+ | (t11 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t13 =>
if not (loose_bvar1 (t13, 0)) then
do_term (incr_boundvars ~1 (t11 $ t13)) accum
else
@@ -876,7 +876,7 @@
do_term (@{const Not}
$ (HOLogic.eq_const (domain_type T0) $ t1
$ Abs (Name.uu, T1, @{const False}))) accum)
- | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
do_equals x t1 t2
| Const (@{const_name Let}, _) $ t1 $ t2 =>
do_formula sn (betapply (t2, t1)) accum
@@ -973,7 +973,7 @@
do_conjunction t0 t1 t2 accum
| (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
do_all t0 s0 T1 t1 accum
- | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
consider_general_equals mdata true x t1 t2 accum
| (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
| (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
@@ -1069,7 +1069,7 @@
Abs (Name.uu, set_T', @{const True})
| _ => Const (s, T')
else if s = @{const_name "=="} orelse
- s = @{const_name "op ="} then
+ s = @{const_name HOL.eq} then
let
val T =
case T' of
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Aug 30 10:38:28 2010 +0200
@@ -447,7 +447,7 @@
val t1 = incr_boundvars n t1
val t2 = incr_boundvars n t2
val xs = map Bound (n - 1 downto 0)
- val equation = Const (@{const_name "op ="},
+ val equation = Const (@{const_name HOL.eq},
body_T --> body_T --> bool_T)
$ betapplys (t1, xs) $ betapplys (t2, xs)
val t =
@@ -515,9 +515,9 @@
do_description_operator The @{const_name undefined_fast_The} x t1
| (Const (x as (@{const_name Eps}, _)), [t1]) =>
do_description_operator Eps @{const_name undefined_fast_Eps} x t1
- | (Const (@{const_name "op ="}, T), [t1]) =>
+ | (Const (@{const_name HOL.eq}, T), [t1]) =>
Op1 (SingletonSet, range_type T, Any, sub t1)
- | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
+ | (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2
| (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
Op2 (And, bool_T, Any, sub' t1, sub' t2)
| (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Aug 30 10:38:28 2010 +0200
@@ -41,7 +41,7 @@
fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
aux def t1 andalso aux false t2
| aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
- | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
+ | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
aux def t1 andalso aux false t2
| aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
| aux def (t1 $ t2) = aux def t1 andalso aux def t2
@@ -149,7 +149,7 @@
case t of
@{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
| Const (s0, _) $ t1 $ _ =>
- if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
+ if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
let
val (t', args) = strip_comb t1
val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
@@ -209,7 +209,7 @@
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
- | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
+ | Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 =>
do_equals new_Ts old_Ts s0 T0 t1 t2
| @{const HOL.conj} $ t1 $ t2 =>
@{const HOL.conj} $ do_term new_Ts old_Ts polar t1
@@ -332,7 +332,7 @@
do_eq_or_imp Ts true def t0 t1 t2 seen
| (t0 as @{const "==>"}) $ t1 $ t2 =>
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
- | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
| (t0 as @{const HOL.implies}) $ t1 $ t2 =>
do_eq_or_imp Ts false def t0 t1 t2 seen
@@ -399,7 +399,7 @@
aux_eq careful true t0 t1 t2
| aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
t0 $ aux false t1 $ aux careful t2
- | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
+ | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
aux_eq careful true t0 t1 t2
| aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
t0 $ aux false t1 $ aux careful t2
@@ -464,9 +464,9 @@
and aux_implies prems zs t1 t2 =
case t1 of
Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
aux_eq prems zs z t' t1 t2
- | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
aux_eq prems zs z t' t1 t2
| _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
and aux_eq prems zs z t' t1 t2 =
@@ -499,7 +499,7 @@
handle SAME () => do_term (t :: seen) ts
in
case t of
- Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
+ Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2
| _ => do_term (t :: seen) ts
end
in do_term end
@@ -653,7 +653,7 @@
fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
| params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
- | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
+ | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
snd (strip_comb t1)
| params_in_equation _ = []
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Aug 30 10:38:28 2010 +0200
@@ -179,7 +179,7 @@
fun translate_literal ctxt constant_table t =
case strip_comb t of
- (Const (@{const_name "op ="}, _), [l, r]) =>
+ (Const (@{const_name HOL.eq}, _), [l, r]) =>
let
val l' = translate_term ctxt constant_table l
val r' = translate_term ctxt constant_table r
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Aug 30 10:38:28 2010 +0200
@@ -411,7 +411,7 @@
fun conjuncts t = conjuncts_aux t [];
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
- | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
+ | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
| is_equationlike_term _ = false
val is_equationlike = is_equationlike_term o prop_of
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Aug 30 10:38:28 2010 +0200
@@ -587,7 +587,7 @@
fun preprocess_elim ctxt elimrule =
let
- fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
+ fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, T) $ lhs $ rhs)) =
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
| replace_eqs t = t
val thy = ProofContext.theory_of ctxt
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Aug 30 10:38:28 2010 +0200
@@ -111,7 +111,7 @@
fun mk_meta_equation th =
case prop_of th of
- Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
| _ => th
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -217,7 +217,7 @@
@{const_name "==>"},
@{const_name Trueprop},
@{const_name Not},
- @{const_name "op ="},
+ @{const_name HOL.eq},
@{const_name HOL.implies},
@{const_name All},
@{const_name Ex},
--- a/src/HOL/Tools/Qelim/cooper.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon Aug 30 10:38:28 2010 +0200
@@ -122,8 +122,8 @@
( case (term_of ct) of
Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
| Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
-| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
+| Const (@{const_name HOL.eq},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
+| Const (@{const_name Not},_) $ (Const (@{const_name HOL.eq},_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
| Const (@{const_name Orderings.less}, _) $ y$ z =>
if term_of x aconv y then Lt (Thm.dest_arg ct)
@@ -274,7 +274,7 @@
| lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
| lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
- | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
+ | lin (vs as x::_) ((b as Const(@{const_name HOL.eq},_))$s$t) =
(case lint vs (subC$t$s) of
(t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
@@ -345,7 +345,7 @@
case (term_of t) of
Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x aconv y andalso member (op =)
- ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
+ [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then (ins (dest_number c) acc,dacc) else (acc,dacc)
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x aconv y andalso member (op =)
@@ -387,7 +387,7 @@
| Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
| Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
- ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
+ [@{const_name HOL.eq}, @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
then cv (l div dest_number c) t else Thm.reflexive t
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x=y andalso member (op =)
--- a/src/HOL/Tools/Qelim/qelim.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Mon Aug 30 10:38:28 2010 +0200
@@ -26,7 +26,7 @@
Const(s,T)$_$_ =>
if domain_type T = HOLogic.boolT
andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
- @{const_name HOL.implies}, @{const_name "op ="}] s
+ @{const_name HOL.implies}, @{const_name HOL.eq}] s
then binop_conv (conv env) p
else atcv env p
| Const(@{const_name Not},_)$_ => arg_conv (conv env) p
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Aug 30 10:38:28 2010 +0200
@@ -12,11 +12,11 @@
val all_injection_tac: Proof.context -> int -> tactic
val clean_tac: Proof.context -> int -> tactic
- val descend_procedure_tac: Proof.context -> int -> tactic
- val descend_tac: Proof.context -> int -> tactic
+ val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
+ val descend_tac: Proof.context -> thm list -> int -> tactic
- val lift_procedure_tac: Proof.context -> thm -> int -> tactic
- val lift_tac: Proof.context -> thm list -> int -> tactic
+ val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic
+ val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic
val lifted: Proof.context -> typ list -> thm list -> thm -> thm
val lifted_attrib: attribute
@@ -338,7 +338,7 @@
=> rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
(* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
-| (Const (@{const_name "op ="},_) $
+| (Const (@{const_name HOL.eq},_) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
@@ -350,7 +350,7 @@
=> rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
(* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
-| Const (@{const_name "op ="},_) $
+| Const (@{const_name HOL.eq},_) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
@@ -370,13 +370,13 @@
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
=> rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
-| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
+| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
(rtac @{thm refl} ORELSE'
(equals_rsp_tac R ctxt THEN' RANGE [
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
(* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
+| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
(* respectfulness of constants; in particular of a simple relation *)
| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
@@ -606,9 +606,9 @@
val rtrm' = HOLogic.dest_Trueprop rtrm
val qtrm' = HOLogic.dest_Trueprop qtrm
val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
- handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
+ handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
- handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
+ handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
Drule.instantiate' []
[SOME (cterm_of thy rtrm'),
@@ -618,10 +618,21 @@
end
+(* Since we use Ball and Bex during the lifting and descending,
+ we cannot deal with lemmas containing them, unless we unfold
+ them by default. *)
+
+val default_unfolds = @{thms Ball_def Bex_def}
+
+
(** descending as tactic **)
-fun descend_procedure_tac ctxt =
- Object_Logic.full_atomize_tac
+fun descend_procedure_tac ctxt simps =
+let
+ val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
+in
+ full_simp_tac ss
+ THEN' Object_Logic.full_atomize_tac
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
let
@@ -631,11 +642,12 @@
in
rtac rule i
end)
+end
-fun descend_tac ctxt =
+fun descend_tac ctxt simps =
let
val mk_tac_raw =
- descend_procedure_tac ctxt
+ descend_procedure_tac ctxt simps
THEN' RANGE
[Object_Logic.rulify_tac THEN' (K all_tac),
regularize_tac ctxt,
@@ -650,15 +662,20 @@
(* the tactic leaves three subgoals to be proved *)
-fun lift_procedure_tac ctxt rthm =
- Object_Logic.full_atomize_tac
+fun lift_procedure_tac ctxt simps rthm =
+let
+ val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
+in
+ full_simp_tac ss
+ THEN' Object_Logic.full_atomize_tac
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
let
(* full_atomize_tac contracts eta redexes,
so we do it also in the original theorem *)
val rthm' =
- rthm |> Drule.eta_contraction_rule
+ rthm |> full_simplify ss
+ |> Drule.eta_contraction_rule
|> Thm.forall_intr_frees
|> atomize_thm
@@ -666,32 +683,29 @@
in
(rtac rule THEN' rtac rthm') i
end)
-
+end
-fun lift_single_tac ctxt rthm =
- lift_procedure_tac ctxt rthm
+fun lift_single_tac ctxt simps rthm =
+ lift_procedure_tac ctxt simps rthm
THEN' RANGE
[ regularize_tac ctxt,
all_injection_tac ctxt,
clean_tac ctxt ]
-fun lift_tac ctxt rthms =
+fun lift_tac ctxt simps rthms =
Goal.conjunction_tac
- THEN' RANGE (map (lift_single_tac ctxt) rthms)
+ THEN' RANGE (map (lift_single_tac ctxt simps) rthms)
(* automated lifting with pre-simplification of the theorems;
for internal usage *)
fun lifted ctxt qtys simps rthm =
let
- val ss = (mk_minimal_ss ctxt) addsimps simps
- val rthm' = asm_full_simplify ss rthm
-
- val ((_, [rthm'']), ctxt') = Variable.import true [rthm'] ctxt
- val goal = derive_qtrm ctxt' qtys (prop_of rthm'')
+ val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
+ val goal = derive_qtrm ctxt' qtys (prop_of rthm')
in
Goal.prove ctxt' [] [] goal
- (K (EVERY1 [asm_full_simp_tac ss, lift_single_tac ctxt' rthm'']))
+ (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
|> singleton (ProofContext.export ctxt' ctxt)
end
--- a/src/HOL/Tools/Quotient/quotient_term.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Aug 30 10:38:28 2010 +0200
@@ -267,7 +267,7 @@
map_types (Envir.subst_type ty_inst) trm
end
-fun is_eq (Const (@{const_name "op ="}, _)) = true
+fun is_eq (Const (@{const_name HOL.eq}, _)) = true
| is_eq _ = false
fun mk_rel_compose (trm1, trm2) =
@@ -539,12 +539,12 @@
end
| (* equalities need to be replaced by appropriate equivalence relations *)
- (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
+ (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
if ty = ty' then rtrm
else equiv_relation ctxt (domain_type ty, domain_type ty')
| (* in this case we just check whether the given equivalence relation is correct *)
- (rel, Const (@{const_name "op ="}, ty')) =>
+ (rel, Const (@{const_name HOL.eq}, ty')) =>
let
val rel_ty = fastype_of rel
val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
@@ -680,7 +680,7 @@
if T = T' then rtrm
else mk_repabs ctxt (T, T') rtrm
- | (_, Const (@{const_name "op ="}, _)) => rtrm
+ | (_, Const (@{const_name HOL.eq}, _)) => rtrm
| (_, Const (_, T')) =>
let
--- a/src/HOL/Tools/SMT/smt_monomorph.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML Mon Aug 30 10:38:28 2010 +0200
@@ -16,7 +16,7 @@
val ignored = member (op =) [
@{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
- @{const_name "op ="}, @{const_name zero_class.zero},
+ @{const_name HOL.eq}, @{const_name zero_class.zero},
@{const_name one_class.one}, @{const_name number_of}]
fun is_const f (n, T) = not (ignored n) andalso f T
--- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Aug 30 10:38:28 2010 +0200
@@ -252,7 +252,7 @@
fun norm_def ctxt thm =
(case Thm.prop_of thm of
- @{term Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ Abs _) =>
+ @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
norm_def ctxt (thm RS @{thm fun_cong})
| Const (@{const_name "=="}, _) $ _ $ Abs _ =>
norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Mon Aug 30 10:38:28 2010 +0200
@@ -162,12 +162,12 @@
| conn @{const_name HOL.conj} = SOME "and"
| conn @{const_name HOL.disj} = SOME "or"
| conn @{const_name HOL.implies} = SOME "implies"
- | conn @{const_name "op ="} = SOME "iff"
+ | conn @{const_name HOL.eq} = SOME "iff"
| conn @{const_name If} = SOME "if_then_else"
| conn _ = NONE
fun pred @{const_name distinct} _ = SOME "distinct"
- | pred @{const_name "op ="} _ = SOME "="
+ | pred @{const_name HOL.eq} _ = SOME "="
| pred @{const_name term_eq} _ = SOME "="
| pred @{const_name less} T = if_int_type T "<"
| pred @{const_name less_eq} T = if_int_type T "<="
--- a/src/HOL/Tools/SMT/z3_interface.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Mon Aug 30 10:38:28 2010 +0200
@@ -176,7 +176,7 @@
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
-val eq = mk_inst_pair destT1 @{cpat "op ="}
+val eq = mk_inst_pair destT1 @{cpat HOL.eq}
fun mk_eq ct cu = Thm.mk_binop (instT' ct eq) ct cu
val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Mon Aug 30 10:38:28 2010 +0200
@@ -234,7 +234,7 @@
@{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
| @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
(T.compose negIffI, lookup (iff_const $ u $ t))
- | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
+ | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
let fun rewr lit = lit COMP @{thm not_sym}
in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
| _ =>
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Aug 30 10:38:28 2010 +0200
@@ -199,7 +199,7 @@
| @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
| @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
| @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
- | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
+ | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
| Const (@{const_name distinct}, _) $ _ =>
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
else fresh_abstraction cvs ct
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 30 10:38:28 2010 +0200
@@ -83,7 +83,7 @@
(Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
fun extensionalize_theorem th =
case prop_of th of
- _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
+ _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
$ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
| _ => th
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Aug 30 10:38:28 2010 +0200
@@ -94,7 +94,7 @@
val const_trans_table =
Symtab.make [(@{type_name Product_Type.prod}, "prod"),
(@{type_name Sum_Type.sum}, "sum"),
- (@{const_name "op ="}, "equal"),
+ (@{const_name HOL.eq}, "equal"),
(@{const_name HOL.conj}, "and"),
(@{const_name HOL.disj}, "or"),
(@{const_name HOL.implies}, "implies"),
@@ -111,7 +111,7 @@
(* Invert the table of translations between Isabelle and ATPs. *)
val const_trans_table_inv =
- Symtab.update ("fequal", @{const_name "op ="})
+ Symtab.update ("fequal", @{const_name HOL.eq})
(Symtab.make (map swap (Symtab.dest const_trans_table)))
val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
@@ -185,8 +185,8 @@
SOME c' => c'
| NONE => ascii_of c
-(* "op =" MUST BE "equal" because it's built into ATPs. *)
-fun make_fixed_const @{const_name "op ="} = "equal"
+(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
+fun make_fixed_const @{const_name HOL.eq} = "equal"
| make_fixed_const c = const_prefix ^ lookup_const c
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 30 10:38:28 2010 +0200
@@ -224,7 +224,7 @@
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
-fun smart_invert_const "fequal" = @{const_name "op ="}
+fun smart_invert_const "fequal" = @{const_name HOL.eq}
| smart_invert_const s = invert_const s
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
@@ -264,7 +264,7 @@
end
| tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
and applic_to_tt ("=",ts) =
- Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
+ Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
case strip_prefix_and_unascii const_prefix a of
SOME b =>
@@ -311,7 +311,7 @@
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
- Const (@{const_name "op ="}, HOLogic.typeT)
+ Const (@{const_name HOL.eq}, HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
(case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
@@ -325,7 +325,7 @@
cvt tm1 $ cvt tm2
| cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
- list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
+ list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
(case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
@@ -480,7 +480,7 @@
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
-fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*)
+fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
| get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
@@ -529,13 +529,13 @@
" isa-term: " ^ Syntax.string_of_term ctxt tm ^
" fol-term: " ^ Metis.Term.toString t)
fun path_finder FO tm ps _ = path_finder_FO tm ps
- | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
+ | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
else path_finder_HO tm (p::ps) (*1 selects second operand*)
| path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
- | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
+ | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
(Metis.Term.Fn ("=", [t1,t2])) =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_FT tm (0::1::ps)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 30 10:38:28 2010 +0200
@@ -121,7 +121,7 @@
handled specially via "fequal". *)
val boring_consts =
[@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
- @{const_name "op ="}]
+ @{const_name HOL.eq}]
(* Add a pconstant to the table, but a [] entry means a standard
connective, which we ignore.*)
@@ -177,7 +177,7 @@
| @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const HOL.implies} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
- | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
+ | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
fold (do_term_or_formula T) [t1, t2]
| Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
$ t1 $ t2 $ t3 =>
@@ -557,7 +557,7 @@
| (_, @{const Not} $ t1) => do_formula (not pos) t1
| (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
| (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
+ | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
| (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
| _ => false
in do_formula true end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Aug 30 10:38:28 2010 +0200
@@ -315,7 +315,7 @@
| _ => raise FO_TERM us
else case strip_prefix_and_unascii const_prefix a of
SOME "equal" =>
- list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
+ list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT),
map (aux NONE []) us)
| SOME b =>
let
@@ -527,7 +527,7 @@
| is_bad_free _ _ = false
(* Vampire is keen on producing these. *)
-fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
+fun is_trivial_formula (@{const Not} $ (Const (@{const_name HOL.eq}, _)
$ t1 $ t2)) = (t1 aconv t2)
| is_trivial_formula _ = false
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 30 10:38:28 2010 +0200
@@ -73,7 +73,7 @@
| @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
| @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
| @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
- | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
+ | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
do_conn bs AIff t1 t2
| _ => (fn ts => do_term bs (Envir.eta_contract t)
|>> AAtom ||> union (op =) ts)
@@ -97,7 +97,7 @@
| aux j (t as Const (s, Type (_, [Type (_, [_, T']),
Type (_, [_, res_T])]))
$ t2 $ Abs (var_s, var_T, t')) =
- if s = @{const_name "op ="} orelse s = @{const_name "=="} then
+ if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
let val var_t = Var ((var_s, j), var_T) in
Const (s, T' --> T' --> res_T)
$ betapply (t2, var_t) $ subst_bound (var_t, t')
@@ -128,7 +128,7 @@
| (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
+ | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
$ t1 $ t2 =>
t0 $ aux Ts t1 $ aux Ts t2
| _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
--- a/src/HOL/Tools/TFL/dcterm.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Mon Aug 30 10:38:28 2010 +0200
@@ -127,7 +127,7 @@
val dest_neg = dest_monop @{const_name Not}
val dest_pair = dest_binop @{const_name Pair}
-val dest_eq = dest_binop @{const_name "op ="}
+val dest_eq = dest_binop @{const_name HOL.eq}
val dest_imp = dest_binop @{const_name HOL.implies}
val dest_conj = dest_binop @{const_name HOL.conj}
val dest_disj = dest_binop @{const_name HOL.disj}
--- a/src/HOL/Tools/TFL/post.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML Mon Aug 30 10:38:28 2010 +0200
@@ -67,7 +67,7 @@
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
fun mk_meta_eq r = case concl_of r of
Const("==",_)$_$_ => r
- | _ $(Const(@{const_name "op ="},_)$_$_) => r RS eq_reflection
+ | _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
| _ => r RS P_imp_P_eq_True
(*Is this the best way to invoke the simplifier??*)
--- a/src/HOL/Tools/TFL/usyntax.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Mon Aug 30 10:38:28 2010 +0200
@@ -244,7 +244,7 @@
end
| dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction";
-fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
+fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
| dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
--- a/src/HOL/Tools/cnf_funcs.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Mon Aug 30 10:38:28 2010 +0200
@@ -98,7 +98,7 @@
| is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
| is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
| is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
| is_atom (Const (@{const_name Not}, _) $ _) = false
| is_atom _ = true;
@@ -205,7 +205,7 @@
in
make_nnf_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -239,7 +239,7 @@
in
make_nnf_not_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
--- a/src/HOL/Tools/groebner.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Mon Aug 30 10:38:28 2010 +0200
@@ -409,7 +409,7 @@
| _ => false;
fun is_eq t =
case term_of t of
- (Const(@{const_name "op ="},_)$_$_) => true
+ (Const(@{const_name HOL.eq},_)$_$_) => true
| _ => false;
fun end_itlist f l =
@@ -923,7 +923,7 @@
fun find_term bounds tm =
(case term_of tm of
- Const (@{const_name "op ="}, T) $ _ $ _ =>
+ Const (@{const_name HOL.eq}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else dest_arg tm
| Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
@@ -985,7 +985,7 @@
local
fun lhs t = case term_of t of
- Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
+ Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
| _=> raise CTERM ("ideal_tac - lhs",[t])
fun exitac NONE = no_tac
| exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
--- a/src/HOL/Tools/hologic.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Mon Aug 30 10:38:28 2010 +0200
@@ -49,7 +49,7 @@
val exists_const: typ -> term
val mk_exists: string * typ * term -> term
val choice_const: typ -> term
- val class_eq: string
+ val class_equal: string
val mk_binop: string -> term * term -> term
val mk_binrel: string -> term * term -> term
val dest_bin: string -> typ -> term -> term * term
@@ -236,10 +236,10 @@
fun dest_not (Const ("HOL.Not", _) $ t) = t
| dest_not t = raise TERM ("dest_not", [t]);
-fun eq_const T = Const ("op =", T --> T --> boolT);
+fun eq_const T = Const ("HOL.eq", T --> T --> boolT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const ("HOL.eq", _) $ lhs $ rhs) = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
@@ -251,7 +251,7 @@
fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
-val class_eq = "HOL.eq";
+val class_equal = "HOL.equal";
(* binary operations and relations *)
--- a/src/HOL/Tools/inductive.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Mon Aug 30 10:38:28 2010 +0200
@@ -182,7 +182,7 @@
in
case concl_of thm of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
- | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm
+ | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq2mono thm
| _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
--- a/src/HOL/Tools/inductive_codegen.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon Aug 30 10:38:28 2010 +0200
@@ -52,7 +52,7 @@
fun thyname_of s = (case optmod of
NONE => Codegen.thyname_of_const thy s | SOME s => s);
in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
- SOME (Const (@{const_name "op ="}, _), [t, _]) =>
+ SOME (Const (@{const_name HOL.eq}, _), [t, _]) =>
(case head_of t of
Const (s, _) =>
CodegenData.put {intros = intros, graph = graph,
@@ -188,7 +188,7 @@
end)) (AList.lookup op = modes name)
in (case strip_comb t of
- (Const (@{const_name "op ="}, Type (_, [T, _])), _) =>
+ (Const (@{const_name HOL.eq}, Type (_, [T, _])), _) =>
[Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
(if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
| (Const (name, _), args) => the_default default (mk_modes name args)
@@ -344,7 +344,7 @@
end;
fun modename module s (iss, is) gr =
- let val (id, gr') = if s = @{const_name "op ="} then (("", "equal"), gr)
+ let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr)
else mk_const_id module s gr
in (space_implode "__"
(mk_qual_id module id ::
@@ -363,7 +363,7 @@
| compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
(case strip_comb t of
(Const (name, _), args) =>
- if name = @{const_name "op ="} orelse AList.defined op = modes name then
+ if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
let
val (args1, args2) = chop (length ms) args;
val ((ps, mode_id), gr') = gr |> fold_map
@@ -581,7 +581,7 @@
fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
Prem ([t], Envir.beta_eta_contract u, true)
- | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
+ | dest_prem (_ $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u)) =
Prem ([t, u], eq, false)
| dest_prem (_ $ t) =
(case strip_comb t of
--- a/src/HOL/Tools/inductive_set.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon Aug 30 10:38:28 2010 +0200
@@ -265,7 +265,7 @@
fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
case prop_of thm of
- Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
(case body_type T of
@{typ bool} =>
let
--- a/src/HOL/Tools/int_arith.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/int_arith.ML Mon Aug 30 10:38:28 2010 +0200
@@ -51,7 +51,7 @@
fun check (Const (@{const_name Groups.one}, @{typ int})) = false
| check (Const (@{const_name Groups.one}, _)) = true
- | check (Const (s, _)) = member (op =) [@{const_name "op ="},
+ | check (Const (s, _)) = member (op =) [@{const_name HOL.eq},
@{const_name Groups.times}, @{const_name Groups.uminus},
@{const_name Groups.minus}, @{const_name Groups.plus},
@{const_name Groups.zero},
--- a/src/HOL/Tools/lin_arith.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Mon Aug 30 10:38:28 2010 +0200
@@ -229,7 +229,7 @@
case rel of
@{const_name Orderings.less} => SOME (p, i, "<", q, j)
| @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
- | "op =" => SOME (p, i, "=", q, j)
+ | @{const_name HOL.eq} => SOME (p, i, "=", q, j)
| _ => NONE
end handle Rat.DIVZERO => NONE;
@@ -427,7 +427,7 @@
val t2' = incr_boundvars 1 t2
val t1_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
- val t1_eq_t2_plus_d = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus},
split_type --> split_type --> split_type) $ t2' $ d)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -447,7 +447,7 @@
(map (incr_boundvars 1) rev_terms)
val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
val t1' = incr_boundvars 1 t1
- val t1_eq_nat_n = Const (@{const_name "op ="}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
+ val t1_eq_nat_n = Const (@{const_name HOL.eq}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
(Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
val t1_lt_zero = Const (@{const_name Orderings.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
@@ -471,13 +471,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const (@{const_name "op ="},
+ val t2_eq_zero = Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -503,13 +503,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const (@{const_name "op ="},
+ val t2_eq_zero = Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -541,7 +541,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const (@{const_name "op ="},
+ val t2_eq_zero = Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -555,7 +555,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -595,7 +595,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const (@{const_name "op ="},
+ val t2_eq_zero = Const (@{const_name HOL.eq},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -609,7 +609,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
--- a/src/HOL/Tools/meson.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/meson.ML Mon Aug 30 10:38:28 2010 +0200
@@ -183,7 +183,7 @@
fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
(*Literals like X=X are tautologous*)
-fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
+fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
| taut_poslit (Const(@{const_name True},_)) = true
| taut_poslit _ = false;
@@ -213,7 +213,7 @@
case HOLogic.dest_Trueprop (concl_of th) of
(Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
- | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
+ | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) =>
if eliminable(t,u)
then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
@@ -222,7 +222,7 @@
fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
notequal_lits_count P + notequal_lits_count Q
- | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
+ | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1
| notequal_lits_count _ = 0;
(*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -280,7 +280,7 @@
| signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
else sum (signed_nclauses (not b) t) (signed_nclauses b u)
- | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) =
if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
(prod (signed_nclauses (not b) u) (signed_nclauses b t))
--- a/src/HOL/Tools/nat_arith.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/nat_arith.ML Mon Aug 30 10:38:28 2010 +0200
@@ -62,7 +62,7 @@
(struct
open CommonCancelSums;
val mk_bal = HOLogic.mk_eq;
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
end);
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Mon Aug 30 10:38:28 2010 +0200
@@ -168,7 +168,7 @@
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
val bal_add1 = @{thm nat_eq_add_iff1} RS trans
val bal_add2 = @{thm nat_eq_add_iff2} RS trans
);
@@ -300,7 +300,7 @@
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
val cancel = @{thm nat_mult_eq_cancel1} RS trans
val neg_exchanges = false
)
@@ -380,7 +380,7 @@
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
);
--- a/src/HOL/Tools/numeral_simprocs.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Aug 30 10:38:28 2010 +0200
@@ -222,7 +222,7 @@
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
val bal_add1 = @{thm eq_add_iff1} RS trans
val bal_add2 = @{thm eq_add_iff2} RS trans
);
@@ -401,7 +401,7 @@
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
val cancel = @{thm mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -516,7 +516,7 @@
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
fun simp_conv _ _ = SOME @{thm mult_cancel_left}
);
@@ -606,7 +606,7 @@
local
val zr = @{cpat "0"}
val zT = ctyp_of_term zr
- val geq = @{cpat "op ="}
+ val geq = @{cpat HOL.eq}
val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
@@ -676,7 +676,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -697,7 +697,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
--- a/src/HOL/Tools/recfun_codegen.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Mon Aug 30 10:38:28 2010 +0200
@@ -40,7 +40,7 @@
end
| avoid_value thy thms = thms;
-fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
+fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name HOL.eq} then ([], "") else
let
val c = AxClass.unoverload_const thy (raw_c, T);
val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
--- a/src/HOL/Tools/record.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/record.ML Mon Aug 30 10:38:28 2010 +0200
@@ -1342,7 +1342,7 @@
val eq_simproc =
Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
(fn thy => fn _ => fn t =>
- (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
+ (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
(case rec_id ~1 T of
"" => NONE
| name =>
@@ -1405,12 +1405,12 @@
else raise TERM ("", [x]);
val sel' = Const (sel, Tsel) $ Bound 0;
val (l, r) = if lr then (sel', x') else (x', sel');
- in Const (@{const_name "op ="}, Teq) $ l $ r end
+ in Const (@{const_name HOL.eq}, Teq) $ l $ r end
else raise TERM ("", [Const (sel, Tsel)]);
- fun dest_sel_eq (Const (@{const_name "op ="}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
+ fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
(true, Teq, (sel, Tsel), X)
- | dest_sel_eq (Const (@{const_name "op ="}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
+ | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
(false, Teq, (sel, Tsel), X)
| dest_sel_eq _ = raise TERM ("", []);
in
@@ -1844,8 +1844,8 @@
let
val eq =
(HOLogic.mk_Trueprop o HOLogic.mk_eq)
- (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
- Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
+ (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
+ Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
fun tac eq_def =
Class.intro_classes_tac []
THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
@@ -1853,15 +1853,15 @@
fun mk_eq thy eq_def = Simplifier.rewrite_rule
[(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
fun mk_eq_refl thy =
- @{thm HOL.eq_refl}
+ @{thm equal_refl}
|> Thm.instantiate
- ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
+ ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
|> AxClass.unoverload thy;
in
thy
|> Code.add_datatype [ext]
|> fold Code.add_default_eqn simps
- |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_eq])
+ |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition
(NONE, (Attrib.empty_binding, eq)))
--- a/src/HOL/Tools/refute.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/refute.ML Mon Aug 30 10:38:28 2010 +0200
@@ -647,7 +647,7 @@
| Const (@{const_name Hilbert_Choice.Eps}, _) => t
| Const (@{const_name All}, _) => t
| Const (@{const_name Ex}, _) => t
- | Const (@{const_name "op ="}, _) => t
+ | Const (@{const_name HOL.eq}, _) => t
| Const (@{const_name HOL.conj}, _) => t
| Const (@{const_name HOL.disj}, _) => t
| Const (@{const_name HOL.implies}, _) => t
@@ -823,7 +823,7 @@
end
| Const (@{const_name All}, T) => collect_type_axioms T axs
| Const (@{const_name Ex}, T) => collect_type_axioms T axs
- | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
+ | Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs
| Const (@{const_name HOL.conj}, _) => axs
| Const (@{const_name HOL.disj}, _) => axs
| Const (@{const_name HOL.implies}, _) => axs
@@ -1850,16 +1850,16 @@
end
| Const (@{const_name Ex}, _) =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op ="}, _) $ t1 $ t2 => (* similar to "==" (Pure) *)
+ | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *)
let
val (i1, m1, a1) = interpret thy model args t1
val (i2, m2, a2) = interpret thy m1 a1 t2
in
SOME (make_equality (i1, i2), m2, a2)
end
- | Const (@{const_name "op ="}, _) $ t1 =>
+ | Const (@{const_name HOL.eq}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op ="}, _) =>
+ | Const (@{const_name HOL.eq}, _) =>
SOME (interpret thy model args (eta_expand t 2))
| Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
(* 3-valued logic *)
--- a/src/HOL/Tools/simpdata.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Mon Aug 30 10:38:28 2010 +0200
@@ -10,7 +10,7 @@
structure Quantifier1 = Quantifier1Fun
(struct
(*abstract syntax*)
- fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
+ fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
| dest_eq _ = NONE;
fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
| dest_conj _ = NONE;
@@ -44,7 +44,7 @@
fun mk_eq th = case concl_of th
(*expects Trueprop if not == *)
of Const (@{const_name "=="},_) $ _ $ _ => th
- | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
+ | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th
| _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
| _ => th RS @{thm Eq_TrueI}
--- a/src/HOL/Typerep.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Typerep.thy Mon Aug 30 10:38:28 2010 +0200
@@ -78,9 +78,13 @@
*}
lemma [code]:
- "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
- \<and> list_all2 eq_class.eq tys1 tys2"
- by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
+ "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2
+ \<and> list_all2 HOL.equal tys1 tys2"
+ by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric])
+
+lemma [code nbe]:
+ "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
+ by (fact equal_refl)
code_type typerep
(Eval "Term.typ")
--- a/src/HOL/Word/Word.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/Word/Word.thy Mon Aug 30 10:38:28 2010 +0200
@@ -953,14 +953,14 @@
text {* Executable equality *}
-instantiation word :: ("{len0}") eq
+instantiation word :: (len0) equal
begin
-definition eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
- "eq_word k l \<longleftrightarrow> HOL.eq (uint k) (uint l)"
+definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
+ "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
instance proof
-qed (simp add: eq eq_word_def)
+qed (simp add: equal equal_word_def)
end
--- a/src/HOL/ex/Numeral.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Mon Aug 30 10:38:28 2010 +0200
@@ -845,7 +845,7 @@
"(uminus :: int \<Rightarrow> int) = uminus"
"(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
"(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
- "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
+ "(HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool) = HOL.equal"
"(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
"(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
by rule+
@@ -928,16 +928,20 @@
by simp_all
lemma eq_int_code [code]:
- "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
- "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
- "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
- "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
- "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
- "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
- "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
- "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
- "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
- by (auto simp add: eq dest: sym)
+ "HOL.equal 0 (0::int) \<longleftrightarrow> True"
+ "HOL.equal 0 (Pls l) \<longleftrightarrow> False"
+ "HOL.equal 0 (Mns l) \<longleftrightarrow> False"
+ "HOL.equal (Pls k) 0 \<longleftrightarrow> False"
+ "HOL.equal (Pls k) (Pls l) \<longleftrightarrow> HOL.equal k l"
+ "HOL.equal (Pls k) (Mns l) \<longleftrightarrow> False"
+ "HOL.equal (Mns k) 0 \<longleftrightarrow> False"
+ "HOL.equal (Mns k) (Pls l) \<longleftrightarrow> False"
+ "HOL.equal (Mns k) (Mns l) \<longleftrightarrow> HOL.equal k l"
+ by (auto simp add: equal dest: sym)
+
+lemma [code nbe]:
+ "HOL.equal (k::int) k \<longleftrightarrow> True"
+ by (fact equal_refl)
lemma less_eq_int_code [code]:
"0 \<le> (0::int) \<longleftrightarrow> True"
@@ -1078,7 +1082,7 @@
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
(Eval "Integer.div'_mod/ (abs _)/ (abs _)")
-code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/HOL/ex/SVC_Oracle.thy Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Mon Aug 30 10:38:28 2010 +0200
@@ -94,7 +94,7 @@
| fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
| fm ((c as Const(@{const_name True}, _))) = c
| fm ((c as Const(@{const_name False}, _))) = c
- | fm (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
--- a/src/HOL/ex/svc_funcs.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML Mon Aug 30 10:38:28 2010 +0200
@@ -95,7 +95,7 @@
| Const(@{const_name Not}, _) => apply c (map tag ts)
| Const(@{const_name True}, _) => (c, false)
| Const(@{const_name False}, _) => (c, false)
- | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
+ | Const(@{const_name HOL.eq}, Type ("fun", [T,_])) =>
if T = HOLogic.boolT then
(*biconditional: with int/nat comparisons below?*)
let val [t1,t2] = ts
@@ -200,7 +200,7 @@
Buildin("AND", (*unfolding uses both polarities*)
[Buildin("=>", [fm (not pos) p, fm pos q]),
Buildin("=>", [fm (not pos) q, fm pos p])])
- | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ x $ y) =
let val tx = tm x and ty = tm y
in if pos orelse T = HOLogic.realT then
Buildin("=", [tx, ty])
--- a/src/HOLCF/Tools/Domain/domain_library.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Mon Aug 30 10:38:28 2010 +0200
@@ -190,9 +190,9 @@
fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
-infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T;
-infix 0 ==; fun S == T = %%:"==" $ S $ T;
-infix 1 ===; fun S === T = %%:"op =" $ S $ T;
+infixr 0 ===>; fun S ===> T = %%: "==>" $ S $ T;
+infix 0 ==; fun S == T = %%: "==" $ S $ T;
+infix 1 ===; fun S === T = %%: @{const_name HOL.eq} $ S $ T;
infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
--- a/src/Tools/Code/code_haskell.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon Aug 30 10:38:28 2010 +0200
@@ -483,7 +483,7 @@
Code_Target.add_target
(target, { serializer = isar_serializer, literals = literals,
check = { env_var = "EXEC_GHC", make_destination = I,
- make_command = fn ghc => fn p => fn module_name =>
+ make_command = fn ghc => fn module_name =>
ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
#> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_ml.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Mon Aug 30 10:38:28 2010 +0200
@@ -966,11 +966,11 @@
Code_Target.add_target
(target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
- make_command = fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure" } })
+ make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
#> Code_Target.add_target
(target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
- make_command = fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p } })
+ make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
--- a/src/Tools/Code/code_scala.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Mon Aug 30 10:38:28 2010 +0200
@@ -444,18 +444,15 @@
(make_vars reserved) args_num is_singleton_constr;
(* print nodes *)
+ fun print_module base implicit_ps p = Pretty.chunks2
+ ([str ("object " ^ base ^ " {")]
+ @ (if null implicit_ps then [] else (single o Pretty.block)
+ (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
+ @ [p, str ("} /* object " ^ base ^ " */")]);
fun print_implicit prefix_fragments implicit =
let
val s = deresolver prefix_fragments implicit;
in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
- fun print_implicits prefix_fragments implicits =
- case map_filter (print_implicit prefix_fragments) implicits
- of [] => NONE
- | ps => (SOME o Pretty.block)
- (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
- fun print_module prefix_fragments base implicits p = Pretty.chunks2
- ([str ("object " ^ base ^ " {")] @ the_list (print_implicits prefix_fragments implicits)
- @ [p, str ("} /* object " ^ base ^ " */")]);
fun print_node _ (_, Dummy) = NONE
| print_node prefix_fragments (name, Stmt stmt) =
if null presentation_stmt_names
@@ -464,10 +461,14 @@
else NONE
| print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
if null presentation_stmt_names
- then case print_nodes (prefix_fragments @ [name_fragment]) nodes
- of NONE => NONE
- | SOME p => SOME (print_module prefix_fragments
- (Long_Name.base_name name_fragment) implicits p)
+ then
+ let
+ val prefix_fragments' = prefix_fragments @ [name_fragment];
+ in
+ Option.map (print_module name_fragment
+ (map_filter (print_implicit prefix_fragments') implicits))
+ (print_nodes prefix_fragments' nodes)
+ end
else print_nodes [] nodes
and print_nodes prefix_fragments nodes = let
val ps = map_filter (fn name => print_node prefix_fragments (name,
@@ -477,7 +478,7 @@
(* serialization *)
val p_includes = if null presentation_stmt_names
- then map (fn (base, p) => print_module [] base [] p) includes else [];
+ then map (fn (base, p) => print_module base [] p) includes else [];
val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
in
Code_Target.mk_serialization target
@@ -520,9 +521,9 @@
Code_Target.add_target
(target, { serializer = isar_serializer, literals = literals,
check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
- make_command = fn scala_home => fn p => fn _ =>
+ make_command = fn scala_home => fn _ =>
"export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
- ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " " ^ File.shell_path p } })
+ ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
#> Code_Target.add_syntax_tyco target "fun"
(SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_target.ML Mon Aug 30 10:36:55 2010 +0200
+++ b/src/Tools/Code/code_target.ML Mon Aug 30 10:38:28 2010 +0200
@@ -13,7 +13,7 @@
type literals = Code_Printer.literals
val add_target: string * { serializer: serializer, literals: literals,
check: { env_var: string, make_destination: Path.T -> Path.T,
- make_command: string -> Path.T -> string -> string } } -> theory -> theory
+ make_command: string -> string -> string } } -> theory -> theory
val extend_target: string *
(string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
-> theory -> theory
@@ -116,7 +116,7 @@
datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
check: { env_var: string, make_destination: Path.T -> Path.T,
- make_command: string -> Path.T -> string -> string } }
+ make_command: string -> string -> string } }
| Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
datatype target = Target of {
@@ -336,7 +336,7 @@
val destination = make_destination p;
val _ = file destination (serialize thy target (SOME 80)
(SOME module_name) args naming program names_cs);
- val cmd = make_command env_param destination module_name;
+ val cmd = make_command env_param module_name;
in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
then error ("Code check failed for " ^ target ^ ": " ^ cmd)
else ()