--- a/NEWS Fri Mar 21 15:12:03 2014 +0100
+++ b/NEWS Fri Mar 21 20:33:56 2014 +0100
@@ -71,6 +71,34 @@
*** Pure ***
+* Basic constants of Pure use more conventional names and are always
+qualified. Rare INCOMPATIBILITY, but with potentially serious
+consequences, notably for tools in Isabelle/ML. The following
+renaming needs to be applied:
+
+ == ~> Pure.eq
+ ==> ~> Pure.imp
+ all ~> Pure.all
+ TYPE ~> Pure.type
+ dummy_pattern ~> Pure.dummy_pattern
+
+Systematic porting works by using the following theory setup on a
+*previous* Isabelle version to introduce the new name accesses for the
+old constants:
+
+setup {*
+ fn thy => thy
+ |> Sign.root_path
+ |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
+ |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
+ |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
+ |> Sign.restore_naming thy
+*}
+
+Thus ML antiquotations like @{const_name Pure.eq} may be used already.
+Later the application is moved to the current Isabelle version, and
+the auxiliary aliases are deleted.
+
* Low-level type-class commands 'classes', 'classrel', 'arities' have
been discontinued to avoid the danger of non-trivial axiomatization
that is not immediately visible. INCOMPATIBILITY, use regular
--- a/src/CCL/Wfd.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/CCL/Wfd.thy Fri Mar 21 20:33:56 2014 +0100
@@ -423,10 +423,10 @@
@{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
@{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
-fun bvars (Const(@{const_name all},_) $ Abs(s,_,t)) l = bvars t (s::l)
+fun bvars (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) l = bvars t (s::l)
| bvars _ l = l
-fun get_bno l n (Const(@{const_name all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
+fun get_bno l n (Const(@{const_name Pure.all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
| get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t
| get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
| get_bno l n (Const(@{const_name mem},_) $ t $ _) = get_bno l n t
--- a/src/Doc/ProgProve/LaTeXsugar.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Doc/ProgProve/LaTeXsugar.thy Fri Mar 21 20:33:56 2014 +0100
@@ -13,7 +13,7 @@
(* THEOREMS *)
notation (Rule output)
- "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+ Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
syntax (Rule output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
@@ -28,7 +28,7 @@
"Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
notation (IfThen output)
- "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThen output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
@@ -36,7 +36,7 @@
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
notation (IfThenNoBox output)
- "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThenNoBox output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
--- a/src/FOL/simpdata.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/FOL/simpdata.ML Fri Mar 21 20:33:56 2014 +0100
@@ -14,7 +14,7 @@
error("conclusion must be a =-equality or <->");;
fun mk_eq th = case concl_of th of
- Const("==",_)$_$_ => th
+ Const(@{const_name Pure.eq},_)$_$_ => th
| _ $ (Const(@{const_name eq},_)$_$_) => mk_meta_eq th
| _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th
| _ $ (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
--- a/src/FOLP/hypsubst.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/FOLP/hypsubst.ML Fri Mar 21 20:33:56 2014 +0100
@@ -58,8 +58,8 @@
assumption. Returns the number of intervening assumptions, paried with
the rule asm_rl (resp. sym). *)
fun eq_var bnd =
- let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
- | eq_var_aux k (Const("==>",_) $ A $ B) =
+ let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
+ | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
((k, inspect_pair bnd (dest_eq A))
(*Exception Match comes from inspect_pair or dest_eq*)
handle Match => eq_var_aux (k+1) B)
--- a/src/FOLP/simp.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/FOLP/simp.ML Fri Mar 21 20:33:56 2014 +0100
@@ -405,10 +405,10 @@
else ();
(* Skip the first n hyps of a goal, and return the rest in generalized form *)
-fun strip_varify(Const("==>", _) $ H $ B, n, vs) =
+fun strip_varify(Const(@{const_name Pure.imp}, _) $ H $ B, n, vs) =
if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
else strip_varify(B,n-1,vs)
- | strip_varify(Const("all",_)$Abs(_,T,t), n, vs) =
+ | strip_varify(Const(@{const_name Pure.all},_)$Abs(_,T,t), n, vs) =
strip_varify(t,n,Var(("?",length vs),T)::vs)
| strip_varify _ = [];
--- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 21 20:33:56 2014 +0100
@@ -84,7 +84,7 @@
(* The result of the quantifier elimination *)
val (th, tac) =
(case (prop_of pre_thm) of
- Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
+ Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let
val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
in
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri Mar 21 20:33:56 2014 +0100
@@ -64,7 +64,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case prop_of pre_thm of
- Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
+ Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
in
((pth RS iffD2) RS pre_thm,
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Mar 21 20:33:56 2014 +0100
@@ -184,9 +184,9 @@
| Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
- | Const ("==>", _) $ _ $ _ => find_args bounds tm
- | Const ("==", _) $ _ $ _ => find_args bounds tm
- | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
--- a/src/HOL/Decision_Procs/langford.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Fri Mar 21 20:33:56 2014 +0100
@@ -204,13 +204,13 @@
else Thm.dest_fun2 tm
| Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
| Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Pure.all}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
- | Const ("==>", _) $ _ $ _ => find_args bounds tm
- | Const ("==", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name Pure.imp}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name Pure.eq}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
@@ -230,7 +230,7 @@
fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
let
- fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
+ fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
val p' = fold_rev gen ts p
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 21 20:33:56 2014 +0100
@@ -112,7 +112,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
- Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
+ Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
if Config.get ctxt quick_and_dirty
--- a/src/HOL/Library/LaTeXsugar.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Fri Mar 21 20:33:56 2014 +0100
@@ -67,7 +67,7 @@
(* THEOREMS *)
notation (Rule output)
- "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+ Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
syntax (Rule output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
@@ -82,7 +82,7 @@
"Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
notation (IfThen output)
- "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThen output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
@@ -90,7 +90,7 @@
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
notation (IfThenNoBox output)
- "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThenNoBox output)
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
--- a/src/HOL/Library/OptionalSugar.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Library/OptionalSugar.thy Fri Mar 21 20:33:56 2014 +0100
@@ -33,7 +33,7 @@
(* aligning equations *)
notation (tab output)
"HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
- "==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
+ "Pure.eq" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
(* Let *)
translations
--- a/src/HOL/Library/refute.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Library/refute.ML Fri Mar 21 20:33:56 2014 +0100
@@ -545,9 +545,9 @@
fun unfold_loop t =
case t of
(* Pure *)
- Const (@{const_name all}, _) => t
- | Const (@{const_name "=="}, _) => t
- | Const (@{const_name "==>"}, _) => t
+ Const (@{const_name Pure.all}, _) => t
+ | Const (@{const_name Pure.eq}, _) => t
+ | Const (@{const_name Pure.imp}, _) => t
| Const (@{const_name Pure.type}, _) => t (* axiomatic type classes *)
(* HOL *)
| Const (@{const_name Trueprop}, _) => t
@@ -709,9 +709,9 @@
and collect_term_axioms t axs =
case t of
(* Pure *)
- Const (@{const_name all}, _) => axs
- | Const (@{const_name "=="}, _) => axs
- | Const (@{const_name "==>"}, _) => axs
+ Const (@{const_name Pure.all}, _) => axs
+ | Const (@{const_name Pure.eq}, _) => axs
+ | Const (@{const_name Pure.imp}, _) => axs
(* axiomatic type classes *)
| Const (@{const_name Pure.type}, T) => collect_type_axioms T axs
(* HOL *)
@@ -1183,7 +1183,7 @@
(* interpretation which includes values for the (formerly) *)
(* quantified variables. *)
(* maps !!x1...xn. !xk...xm. t to t *)
- fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) =
+ fun strip_all_body (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) =
strip_all_body t
| strip_all_body (Const (@{const_name Trueprop}, _) $ t) =
strip_all_body t
@@ -1191,7 +1191,7 @@
strip_all_body t
| strip_all_body t = t
(* maps !!x1...xn. !xk...xm. t to [x1, ..., xn, xk, ..., xm] *)
- fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) =
+ fun strip_all_vars (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) =
(a, T) :: strip_all_vars t
| strip_all_vars (Const (@{const_name Trueprop}, _) $ t) =
strip_all_vars t
@@ -1569,7 +1569,7 @@
fun Pure_interpreter ctxt model args t =
case t of
- Const (@{const_name all}, _) $ t1 =>
+ Const (@{const_name Pure.all}, _) $ t1 =>
let
val (i, m, a) = interpret ctxt model args t1
in
@@ -1584,11 +1584,11 @@
end
| _ =>
raise REFUTE ("Pure_interpreter",
- "\"all\" is followed by a non-function")
+ "\"Pure.all\" is followed by a non-function")
end
- | Const (@{const_name all}, _) =>
+ | Const (@{const_name Pure.all}, _) =>
SOME (interpret ctxt model args (eta_expand t 1))
- | Const (@{const_name "=="}, _) $ t1 $ t2 =>
+ | Const (@{const_name Pure.eq}, _) $ t1 $ t2 =>
let
val (i1, m1, a1) = interpret ctxt model args t1
val (i2, m2, a2) = interpret ctxt m1 a1 t2
@@ -1597,11 +1597,11 @@
SOME ((if #def_eq args then make_def_equality else make_equality)
(i1, i2), m2, a2)
end
- | Const (@{const_name "=="}, _) $ _ =>
+ | Const (@{const_name Pure.eq}, _) $ _ =>
SOME (interpret ctxt model args (eta_expand t 1))
- | Const (@{const_name "=="}, _) =>
+ | Const (@{const_name Pure.eq}, _) =>
SOME (interpret ctxt model args (eta_expand t 2))
- | Const (@{const_name "==>"}, _) $ t1 $ t2 =>
+ | Const (@{const_name Pure.imp}, _) $ t1 $ t2 =>
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret ctxt model args t1
@@ -1611,9 +1611,9 @@
in
SOME (Leaf [fmTrue, fmFalse], m2, a2)
end
- | Const (@{const_name "==>"}, _) $ _ =>
+ | Const (@{const_name Pure.imp}, _) $ _ =>
SOME (interpret ctxt model args (eta_expand t 1))
- | Const (@{const_name "==>"}, _) =>
+ | Const (@{const_name Pure.imp}, _) =>
SOME (interpret ctxt model args (eta_expand t 2))
| _ => NONE;
@@ -1632,7 +1632,7 @@
(* redundant, since 'False' is also an IDT constructor *)
| Const (@{const_name False}, _) =>
SOME (FF, model, args)
- | Const (@{const_name All}, _) $ t1 => (* similar to "all" (Pure) *)
+ | Const (@{const_name All}, _) $ t1 => (* similar to "Pure.all" *)
let
val (i, m, a) = interpret ctxt model args t1
in
@@ -1670,7 +1670,7 @@
end
| Const (@{const_name Ex}, _) =>
SOME (interpret ctxt model args (eta_expand t 1))
- | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to "==" (Pure) *)
+ | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => (* similar to Pure.eq *)
let
val (i1, m1, a1) = interpret ctxt model args t1
val (i2, m2, a2) = interpret ctxt m1 a1 t2
@@ -1715,7 +1715,7 @@
(* this would make "undef" propagate, even for formulae like *)
(* "True | undef": *)
(* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
- | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *)
+ | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to Pure.imp *)
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret ctxt model args t1
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Fri Mar 21 20:33:56 2014 +0100
@@ -435,7 +435,8 @@
val ty = type_of a
val (encoding, a) = remove_types encoding a
val (encoding, b) = remove_types encoding b
- val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding
+ val (eq, encoding) =
+ Encode.insert (Const (@{const_name Pure.eq}, ty --> ty --> @{typ "prop"})) encoding
in
(encoding, EqPrem (a, b, ty, eq))
end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 21 20:33:56 2014 +0100
@@ -275,7 +275,7 @@
@{const_name Quickcheck_Random.catch_match},
@{const_name Quickcheck_Exhaustive.unknown},
@{const_name Num.Bit0}, @{const_name Num.Bit1}
- (*@{const_name "==>"}, @{const_name "=="}*)]
+ (*@{const_name Pure.imp}, @{const_name Pure.eq}*)]
val forbidden_mutant_consts =
[
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Mar 21 20:33:56 2014 +0100
@@ -292,7 +292,7 @@
subsection {* Known Constants *}
-lemma "x \<equiv> all \<Longrightarrow> False"
+lemma "x \<equiv> Pure.all \<Longrightarrow> False"
nitpick [card = 1, expect = genuine]
nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
nitpick [card = 6, expect = genuine]
@@ -306,15 +306,15 @@
nitpick [expect = genuine]
oops
-lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
+lemma "Pure.all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
nitpick [expect = none]
by auto
-lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
+lemma "Pure.all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
nitpick [expect = genuine]
oops
-lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))"
+lemma "I = (\<lambda>x. x) \<Longrightarrow> Pure.all P \<equiv> Pure.all (\<lambda>x. P (I x))"
nitpick [expect = none]
by auto
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Mar 21 20:33:56 2014 +0100
@@ -326,7 +326,7 @@
nitpick [expect = genuine]
oops
-lemma "(x \<equiv> all) \<Longrightarrow> False"
+lemma "(x \<equiv> Pure.all) \<Longrightarrow> False"
nitpick [expect = genuine]
oops
--- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 21 20:33:56 2014 +0100
@@ -32,8 +32,8 @@
fun unquantify t =
let
- val (vs, Ts) = split_list (strip_qnt_vars "all" t);
- val body = strip_qnt_body "all" t;
+ val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} t);
+ val body = strip_qnt_body @{const_name Pure.all} t;
val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
(fn Free (v, _) => insert (op =) v | _ => I) body []))
in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
--- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Mar 21 20:33:56 2014 +0100
@@ -134,7 +134,7 @@
val thy = Context.theory_of context
val thms_to_be_added = (case (prop_of orig_thm) of
(* case: eqvt-lemma is of the implicational form *)
- (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
+ (Const(@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
let
val (pi,typi) = get_pi concl thy
in
--- a/src/HOL/Product_Type.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Product_Type.thy Fri Mar 21 20:33:56 2014 +0100
@@ -457,7 +457,7 @@
ML {*
(* replace parameters of product type by individual component parameters *)
local (* filtering with exists_paired_all is an essential optimization *)
- fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
+ fun exists_paired_all (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) =
can HOLogic.dest_prodT T orelse exists_paired_all t
| exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
| exists_paired_all (Abs (_, _, t)) = exists_paired_all t
--- a/src/HOL/Prolog/prolog.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Prolog/prolog.ML Fri Mar 21 20:33:56 2014 +0100
@@ -13,9 +13,9 @@
Const(@{const_name Trueprop},_)$t => isD t
| Const(@{const_name HOL.conj} ,_)$l$r => isD l andalso isD r
| Const(@{const_name HOL.implies},_)$l$r => isG l andalso isD r
- | Const( "==>",_)$l$r => isG l andalso isD r
+ | Const(@{const_name Pure.imp},_)$l$r => isG l andalso isD r
| Const(@{const_name All},_)$Abs(s,_,t) => isD t
- | Const("all",_)$Abs(s,_,t) => isD t
+ | Const(@{const_name Pure.all},_)$Abs(s,_,t) => isD t
| Const(@{const_name HOL.disj},_)$_$_ => false
| Const(@{const_name Ex} ,_)$_ => false
| Const(@{const_name Not},_)$_ => false
@@ -33,9 +33,9 @@
| Const(@{const_name HOL.conj} ,_)$l$r => isG l andalso isG r
| Const(@{const_name HOL.disj} ,_)$l$r => isG l andalso isG r
| Const(@{const_name HOL.implies},_)$l$r => isD l andalso isG r
- | Const( "==>",_)$l$r => isD l andalso isG r
+ | Const(@{const_name Pure.imp},_)$l$r => isD l andalso isG r
| Const(@{const_name All},_)$Abs(_,_,t) => isG t
- | Const("all",_)$Abs(_,_,t) => isG t
+ | Const(@{const_name Pure.all},_)$Abs(_,_,t) => isG t
| Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t
| Const(@{const_name True},_) => true
| Const(@{const_name Not},_)$_ => false
@@ -79,8 +79,8 @@
| ap (Const(@{const_name HOL.implies},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
| ap t = (0,false,t);
(*
- fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
- | rep_goal (Const ("==>",_)$s$t) =
+ fun rep_goal (Const (@{const_name Pure.all},_)$Abs (_,_,t)) = rep_goal t
+ | rep_goal (Const (@{const_name Pure.imp},_)$s$t) =
(case rep_goal t of (l,t) => (s::l,t))
| rep_goal t = ([] ,t);
val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Mar 21 20:33:56 2014 +0100
@@ -320,7 +320,7 @@
|> apfst the_single
end
-(*like strip_top_All_vars but for "all" instead of "All"*)
+(*like strip_top_All_vars but for "Pure.all" instead of "HOL.All"*)
fun strip_top_all_vars acc t =
if Logic.is_all t then
let
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 21 20:33:56 2014 +0100
@@ -1670,7 +1670,7 @@
(* @{const_name HOL.not_equal}, *)
@{const_name HOL.False},
@{const_name HOL.True},
- @{const_name "==>"}]
+ @{const_name Pure.imp}]
fun strip_qtfrs_tac ctxt =
REPEAT_DETERM (HEADGOAL (rtac @{thm allI}))
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Mar 21 20:33:56 2014 +0100
@@ -404,8 +404,9 @@
(* These are ignored anyway by the relevance filter (unless they appear in
higher-order places) but not by the monomorphizer. *)
val atp_logical_consts =
- [@{const_name Pure.prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"},
- @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
+ [@{const_name Pure.prop}, @{const_name Pure.conjunction},
+ @{const_name Pure.all}, @{const_name Pure.imp}, @{const_name Pure.eq},
+ @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
@{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
(* These are either simplified away by "Meson.presimplify" (most of the time) or
@@ -1879,8 +1880,8 @@
in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
- | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
- | s_not_prop t = @{const "==>"} $ t $ @{prop False}
+ | s_not_prop (@{const Pure.imp} $ t $ @{prop False}) = t
+ | s_not_prop t = @{const Pure.imp} $ t $ @{prop False}
fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
concl_t facts =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Mar 21 20:33:56 2014 +0100
@@ -46,7 +46,7 @@
fun hhf_concl_conv cv ctxt ct =
(case Thm.term_of ct of
- Const (@{const_name all}, _) $ Abs _ =>
+ Const (@{const_name Pure.all}, _) $ Abs _ =>
Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct
| _ => Conv.concl_conv ~1 cv ct);
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Fri Mar 21 20:33:56 2014 +0100
@@ -86,8 +86,8 @@
| retype_free _ t = raise TERM ("retype_free", [t]);
fun drop_all t =
- subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
- strip_qnt_body @{const_name all} t);
+ subst_bounds (strip_qnt_vars @{const_name Pure.all} t |> map Free |> rev,
+ strip_qnt_body @{const_name Pure.all} t);
fun permute_args n t =
list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n);
--- a/src/HOL/Tools/Datatype/primrec.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Datatype/primrec.ML Fri Mar 21 20:33:56 2014 +0100
@@ -34,8 +34,8 @@
fun process_eqn is_fixed spec rec_fns =
let
- val (vs, Ts) = split_list (strip_qnt_vars "all" spec);
- val body = strip_qnt_body "all" spec;
+ val (vs, Ts) = split_list (strip_qnt_vars @{const_name Pure.all} spec);
+ val body = strip_qnt_body @{const_name Pure.all} spec;
val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
(fn Free (v, _) => insert (op =) v | _ => I) body []));
val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 21 20:33:56 2014 +0100
@@ -434,7 +434,7 @@
let
fun prove_case_cong ((t, nchotomy), case_rewrites) =
let
- val Const ("==>", _) $ tm $ _ = t;
+ val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
val cert = cterm_of thy;
val nchotomy' = nchotomy RS spec;
--- a/src/HOL/Tools/Function/function_common.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Fri Mar 21 20:33:56 2014 +0100
@@ -280,8 +280,8 @@
fun split_def ctxt check_head geq =
let
fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
- val qs = Term.strip_qnt_vars "all" geq
- val imp = Term.strip_qnt_body "all" geq
+ val qs = Term.strip_qnt_vars @{const_name Pure.all} geq
+ val imp = Term.strip_qnt_body @{const_name Pure.all} geq
val (gs, eq) = Logic.strip_horn imp
val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
--- a/src/HOL/Tools/Function/function_lib.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Fri Mar 21 20:33:56 2014 +0100
@@ -40,7 +40,7 @@
(* Removes all quantifiers from a term, replacing bound variables by frees. *)
-fun dest_all_all (t as (Const ("all",_) $ _)) =
+fun dest_all_all (t as (Const (@{const_name Pure.all},_) $ _)) =
let
val (v,b) = Logic.dest_all t |> apfst Free
val (vs, b') = dest_all_all b
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Mar 21 20:33:56 2014 +0100
@@ -547,11 +547,11 @@
fun rename_to_tnames ctxt term =
let
- fun all_typs (Const ("all", _) $ Abs (_, T, t)) = T :: all_typs t
+ fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t
| all_typs _ = []
- fun rename (Const ("all", T1) $ Abs (_, T2, t)) (new_name :: names) =
- (Const ("all", T1) $ Abs (new_name, T2, rename t names))
+ fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) =
+ (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names))
| rename t _ = t
val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
--- a/src/HOL/Tools/Meson/meson.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Fri Mar 21 20:33:56 2014 +0100
@@ -105,7 +105,7 @@
try (fn () =>
let val thy = theory_of_thm thA
val tmA = concl_of thA
- val Const("==>",_) $ tmB $ _ = prop_of thB
+ val Const(@{const_name Pure.imp},_) $ tmB $ _ = prop_of thB
val tenv =
Pattern.first_order_match thy (tmB, tmA)
(Vartab.empty, Vartab.empty) |> snd
@@ -472,7 +472,7 @@
(***** MESON PROOF PROCEDURE *****)
-fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
+fun rhyps (Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
As) = rhyps(phi, A::As)
| rhyps (_, As) = As;
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Mar 21 20:33:56 2014 +0100
@@ -242,7 +242,7 @@
fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
case t of
(t1 as Const (s, _)) $ Abs (s', T, t') =>
- if s = @{const_name all} orelse s = @{const_name All} orelse
+ if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
s = @{const_name Ex} then
let
val skolem = (pos = (s = @{const_name Ex}))
@@ -254,7 +254,7 @@
else
t
| (t1 as Const (s, _)) $ t2 $ t3 =>
- if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then
+ if s = @{const_name Pure.imp} orelse s = @{const_name HOL.implies} then
t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
else if s = @{const_name HOL.conj} orelse
s = @{const_name HOL.disj} then
@@ -275,13 +275,13 @@
ct
|> (case term_of ct of
Const (s, _) $ Abs (s', _, _) =>
- if s = @{const_name all} orelse s = @{const_name All} orelse
+ if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
s = @{const_name Ex} then
Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
else
Conv.all_conv
| Const (s, _) $ _ $ _ =>
- if s = @{const_name "==>"} orelse s = @{const_name implies} then
+ if s = @{const_name Pure.imp} orelse s = @{const_name implies} then
Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
else if s = @{const_name conj} orelse s = @{const_name disj} then
Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 21 20:33:56 2014 +0100
@@ -1062,7 +1062,7 @@
end
fun is_fixed_equation ctxt
- (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
+ (Const (@{const_name Pure.eq}, _) $ Free (s, _) $ Const _) =
Variable.is_fixed ctxt s
| is_fixed_equation _ _ = false
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Mar 21 20:33:56 2014 +0100
@@ -363,9 +363,9 @@
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
well. *)
val built_in_consts =
- [(@{const_name all}, 1),
- (@{const_name "=="}, 2),
- (@{const_name "==>"}, 2),
+ [(@{const_name Pure.all}, 1),
+ (@{const_name Pure.eq}, 2),
+ (@{const_name Pure.imp}, 2),
(@{const_name Pure.conjunction}, 2),
(@{const_name Trueprop}, 1),
(@{const_name Not}, 1),
@@ -973,7 +973,7 @@
fold (fn (z as ((s, _), T)) => fn t' =>
Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
(take (length zs' - length zs) zs')
- fun aux zs (@{const "==>"} $ t1 $ t2) =
+ fun aux zs (@{const Pure.imp} $ t1 $ t2) =
let val zs' = Term.add_vars t1 zs in
close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
end
@@ -1178,7 +1178,7 @@
| loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
| loose_bvar1_count _ = 0
-fun s_betapply _ (t1 as Const (@{const_name "=="}, _) $ t1', t2) =
+fun s_betapply _ (t1 as Const (@{const_name Pure.eq}, _) $ t1', t2) =
if t1' aconv t2 then @{prop True} else t1 $ t2
| s_betapply _ (t1 as Const (@{const_name HOL.eq}, _) $ t1', t2) =
if t1' aconv t2 then @{term True} else t1 $ t2
@@ -1422,8 +1422,8 @@
simplification rules (equational specifications). *)
fun term_under_def t =
case t of
- @{const "==>"} $ _ $ t2 => term_under_def t2
- | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
+ @{const Pure.imp} $ _ $ t2 => term_under_def t2
+ | Const (@{const_name Pure.eq}, _) $ t1 $ _ => term_under_def t1
| @{const Trueprop} $ t1 => term_under_def t1
| Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
| Abs (_, _, t') => term_under_def t'
@@ -1448,7 +1448,7 @@
| aux _ _ = NONE
val (lhs, rhs) =
case t of
- Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
+ Const (@{const_name Pure.eq}, _) $ t1 $ t2 => (t1, t2)
| @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
(t1, t2)
| _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
@@ -1527,9 +1527,9 @@
fun lhs_of_equation t =
case t of
- Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
- | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
- | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
+ Const (@{const_name Pure.all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
+ | Const (@{const_name Pure.eq}, _) $ t1 $ _ => SOME t1
+ | @{const Pure.imp} $ _ $ 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 HOL.eq}, _) $ t1 $ _ => SOME t1
@@ -1947,7 +1947,7 @@
@{const Trueprop} $ extensional_equal j T t1 t2
| @{const Trueprop} $ t' =>
@{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
- | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
+ | Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 =>
@{const Trueprop} $ extensional_equal j T t1 t2
| _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
quote (Syntax.string_of_term ctxt t) ^ ".");
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Mar 21 20:33:56 2014 +0100
@@ -844,8 +844,8 @@
if not (could_exist_alpha_subtype alpha_T T) then
(mtype_for T, accum)
else case s of
- @{const_name all} => do_all T accum
- | @{const_name "=="} => do_equals T accum
+ @{const_name Pure.all} => do_all T accum
+ | @{const_name Pure.eq} => do_equals T accum
| @{const_name All} => do_all T accum
| @{const_name Ex} =>
let val set_T = domain_type T in
@@ -1057,9 +1057,9 @@
" \<turnstile> " ^ Syntax.string_of_term ctxt t ^
" : o\<^sup>" ^ string_for_sign sn ^ "?");
case t of
- Const (s as @{const_name all}, _) $ Abs (_, T1, t1) =>
+ Const (s as @{const_name Pure.all}, _) $ Abs (_, T1, t1) =>
do_quantifier s T1 t1
- | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
+ | Const (@{const_name Pure.eq}, _) $ t1 $ t2 => do_equals t1 t2
| @{const Trueprop} $ t1 => do_formula sn t1 accum
| Const (s as @{const_name All}, _) $ Abs (_, T1, t1) =>
do_quantifier s T1 t1
@@ -1076,7 +1076,7 @@
do_formula sn (betapply (t2, t1)) accum
| @{const Pure.conjunction} $ t1 $ t2 =>
do_connect meta_conj_spec false t1 t2 accum
- | @{const "==>"} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
+ | @{const Pure.imp} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
| @{const Not} $ t1 => do_connect imp_spec true t1 @{const False} accum
| @{const conj} $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
| @{const disj} $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
@@ -1122,11 +1122,11 @@
and do_implies t1 t2 = do_term t1 #> do_formula t2
and do_formula t accum =
case t of
- Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
+ Const (@{const_name Pure.all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
| @{const Trueprop} $ t1 => do_formula t1 accum
- | Const (@{const_name "=="}, _) $ t1 $ t2 =>
+ | Const (@{const_name Pure.eq}, _) $ t1 $ t2 =>
consider_general_equals mdata true t1 t2 accum
- | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
+ | @{const Pure.imp} $ t1 $ t2 => do_implies t1 t2 accum
| @{const Pure.conjunction} $ t1 $ t2 =>
fold (do_formula) [t1, t2] accum
| Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Mar 21 20:33:56 2014 +0100
@@ -474,12 +474,12 @@
| k => sub (eta_expand Ts t k)
in
case strip_comb t of
- (Const (@{const_name all}, _), [Abs (s, T, t1)]) =>
+ (Const (@{const_name Pure.all}, _), [Abs (s, T, t1)]) =>
do_quantifier All s T t1
- | (t0 as Const (@{const_name all}, _), [t1]) =>
+ | (t0 as Const (@{const_name Pure.all}, _), [t1]) =>
sub' (t0 $ eta_expand Ts t1 1)
- | (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2
- | (Const (@{const_name "==>"}, _), [t1, t2]) =>
+ | (Const (@{const_name Pure.eq}, T), [t1, t2]) => sub_equals T t1 t2
+ | (Const (@{const_name Pure.imp}, _), [t1, t2]) =>
Op2 (Or, prop_T, Any, Op1 (Not, prop_T, Any, sub t1), sub' t2)
| (Const (@{const_name Pure.conjunction}, _), [t1, t2]) =>
Op2 (And, prop_T, Any, sub' t1, sub' t2)
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 21 20:33:56 2014 +0100
@@ -36,9 +36,9 @@
val may_use_binary_ints =
let
- fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
+ fun aux def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) =
aux def t1 andalso aux false t2
- | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
+ | aux def (@{const Pure.imp} $ t1 $ t2) = aux false t1 andalso aux def 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
@@ -145,7 +145,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 HOL.eq} then
+ if s0 = @{const_name Pure.eq} 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')
@@ -187,12 +187,12 @@
end
and do_term new_Ts old_Ts polar t =
case t of
- Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
+ Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
- | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
+ | Const (s0 as @{const_name Pure.eq}, T0) $ t1 $ t2 =>
do_equals new_Ts old_Ts s0 T0 t1 t2
- | @{const "==>"} $ t1 $ t2 =>
- @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ | @{const Pure.imp} $ t1 $ t2 =>
+ @{const Pure.imp} $ do_term new_Ts old_Ts (flip_polarity polar) t1
$ do_term new_Ts old_Ts polar t2
| @{const Pure.conjunction} $ t1 $ t2 =>
@{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
@@ -334,9 +334,9 @@
val k = maxidx_of_term t + 1
fun do_term Ts def t args seen =
case t of
- (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
+ (t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as @{const "==>"}) $ t1 $ t2 =>
+ | (t0 as @{const Pure.imp}) $ t1 $ t2 =>
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
| (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
@@ -401,9 +401,9 @@
val num_occs_of_var =
fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
| _ => I) t (K 0)
- fun aux Ts careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
+ fun aux Ts careful ((t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2) =
aux_eq Ts careful true t0 t1 t2
- | aux Ts careful ((t0 as @{const "==>"}) $ t1 $ t2) =
+ | aux Ts careful ((t0 as @{const Pure.imp}) $ t1 $ t2) =
t0 $ aux Ts false t1 $ aux Ts careful t2
| aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
aux_eq Ts careful true t0 t1 t2
@@ -455,22 +455,22 @@
(** Destruction of universal and existential equalities **)
-fun curry_assms (@{const "==>"} $ (@{const Trueprop}
+fun curry_assms (@{const Pure.imp} $ (@{const Trueprop}
$ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
- | curry_assms (@{const "==>"} $ t1 $ t2) =
- @{const "==>"} $ curry_assms t1 $ curry_assms t2
+ | curry_assms (@{const Pure.imp} $ t1 $ t2) =
+ @{const Pure.imp} $ curry_assms t1 $ curry_assms t2
| curry_assms t = t
val destroy_universal_equalities =
let
fun aux prems zs t =
case t of
- @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
+ @{const Pure.imp} $ t1 $ t2 => aux_implies prems zs t1 t2
| _ => Logic.list_implies (rev prems, t)
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 (@{const_name Pure.eq}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
| @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
aux_eq prems zs z t' t1 t2
| @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
@@ -591,10 +591,10 @@
not (is_higher_order_type abs_T)) polar t)
in
case t of
- Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
+ Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
- | @{const "==>"} $ t1 $ t2 =>
- @{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
+ | @{const Pure.imp} $ t1 $ t2 =>
+ @{const Pure.imp} $ aux ss Ts js skolemizable (flip_polarity polar) t1
$ aux ss Ts js skolemizable polar t2
| @{const Pure.conjunction} $ t1 $ t2 =>
@{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1
@@ -654,7 +654,7 @@
(** Function specialization **)
-fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
+fun params_in_equation (@{const Pure.imp} $ _ $ t2) = params_in_equation t2
| params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
| params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
snd (strip_comb t1)
@@ -866,7 +866,7 @@
if exists_subterm (curry (op aconv) u) def then NONE else SOME u
in
case t of
- Const (@{const_name "=="}, _) $ (u as Free _) $ def => do_equals u def
+ Const (@{const_name Pure.eq}, _) $ (u as Free _) $ def => do_equals u def
| @{const Trueprop}
$ (Const (@{const_name HOL.eq}, _) $ (u as Free _) $ def) =>
do_equals u def
@@ -918,7 +918,7 @@
and add_def_axiom depth = add_axiom fst apfst true depth
and add_nondef_axiom depth = add_axiom snd apsnd false depth
and add_maybe_def_axiom depth t =
- (if head_of t <> @{const "==>"} then add_def_axiom
+ (if head_of t <> @{const Pure.imp} then add_def_axiom
else add_nondef_axiom) depth t
and add_eq_axiom depth t =
(if is_constr_pattern_formula ctxt t then add_def_axiom
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 21 20:33:56 2014 +0100
@@ -307,7 +307,8 @@
fun imp_prems_conv cv ct =
(case Thm.term_of ct of
- Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
+ Const (@{const_name Pure.imp}, _) $ _ $ _ =>
+ Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
| _ => Conv.all_conv ct)
fun preprocess_intro thy rule =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Mar 21 20:33:56 2014 +0100
@@ -460,14 +460,14 @@
(* general syntactic functions *)
-fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
+fun is_equationlike_term (Const (@{const_name Pure.eq}, _) $ _ $ _) = 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
-fun is_pred_equation_term (Const ("==", _) $ u $ v) =
+fun is_pred_equation_term (Const (@{const_name Pure.eq}, _) $ u $ v) =
(fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
| is_pred_equation_term _ = false
@@ -620,7 +620,7 @@
(*
fun equals_conv lhs_cv rhs_cv ct =
case Thm.term_of ct of
- Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
+ Const (@{const_name Pure.eq}, _) $ _ $ _ => Conv.arg_conv cv ct
| _ => error "equals_conv"
*)
@@ -973,7 +973,8 @@
fun imp_prems_conv cv ct =
(case Thm.term_of ct of
- Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
+ Const (@{const_name Pure.imp}, _) $ _ $ _ =>
+ Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
| _ => Conv.all_conv ct)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Mar 21 20:33:56 2014 +0100
@@ -84,7 +84,7 @@
val is_introlike = is_introlike_term o prop_of
-fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
+fun check_equation_format_term (t as (Const (@{const_name Pure.eq}, _) $ u $ _)) =
(case strip_comb u of
(Const (_, T), args) =>
if (length (binder_types T) = length args) then
@@ -98,7 +98,7 @@
val check_equation_format = check_equation_format_term o prop_of
-fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u)
+fun defining_term_of_equation_term (Const (@{const_name Pure.eq}, _) $ u $ _) = fst (strip_comb u)
| defining_term_of_equation_term t =
raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
@@ -224,8 +224,8 @@
end
val logic_operator_names =
- [@{const_name "=="},
- @{const_name "==>"},
+ [@{const_name Pure.eq},
+ @{const_name Pure.imp},
@{const_name Trueprop},
@{const_name Not},
@{const_name HOL.eq},
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Mar 21 20:33:56 2014 +0100
@@ -795,7 +795,7 @@
fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
let
- fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
+ fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "Pure.all"}
fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
val p' = fold_rev gen ts p
--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 21 20:33:56 2014 +0100
@@ -52,7 +52,7 @@
(case Thm.prop_of thm of
@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
norm_def (thm RS @{thm fun_cong})
- | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
+ | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ =>
norm_def (thm RS @{thm meta_eq_to_obj_eq})
| _ => thm)
@@ -61,20 +61,20 @@
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
- @{const "==>"} $ _ $ _ =>
+ @{const Pure.imp} $ _ $ _ =>
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_imp}
- | Const (@{const_name "=="}, _) $ _ $ _ =>
+ | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_eq}
- | Const (@{const_name all}, _) $ Abs _ =>
+ | Const (@{const_name Pure.all}, _) $ Abs _ =>
Conv.binder_conv (atomize_conv o snd) ctxt then_conv
Conv.rewr_conv @{thm atomize_all}
| _ => Conv.all_conv) ct
val setup_atomize =
- fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
- @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
+ fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp},
+ @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}]
(** unfold special quantifiers **)
--- a/src/HOL/Tools/SMT/smt_utils.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML Fri Mar 21 20:33:56 2014 +0100
@@ -188,7 +188,7 @@
@{const Trueprop} $ _ => Thm.dest_arg ct
| _ => raise CTERM ("not a property", [ct]))
-val equals = mk_const_pat @{theory} @{const_name "=="} destT1
+val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Mar 21 20:33:56 2014 +0100
@@ -614,7 +614,7 @@
(* |- (EX x. P x) = P c |- ~(ALL x. P x) = ~ P c *)
local
val forall =
- SMT_Utils.mk_const_pat @{theory} @{const_name all}
+ SMT_Utils.mk_const_pat @{theory} @{const_name Pure.all}
(SMT_Utils.destT1 o SMT_Utils.destT1)
fun mk_forall cv ct =
Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct)
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Mar 21 20:33:56 2014 +0100
@@ -199,7 +199,7 @@
and abstr (dcvs as (d, cvs)) ct =
(case Thm.term_of ct of
@{const Trueprop} $ _ => abstr1 dcvs ct
- | @{const "==>"} $ _ $ _ => abstr2 dcvs ct
+ | @{const Pure.imp} $ _ $ _ => abstr2 dcvs ct
| @{const True} => pair ct
| @{const False} => pair ct
| @{const Not} $ _ => abstr1 dcvs ct
@@ -229,7 +229,7 @@
| _ => fresh_abstraction dcvs ct cx)))
in abstr (depth, []) end
-val cimp = Thm.cterm_of @{theory} @{const "==>"}
+val cimp = Thm.cterm_of @{theory} @{const Pure.imp}
fun deepen depth f x =
if depth = 0 then f depth x
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML Fri Mar 21 20:33:56 2014 +0100
@@ -48,7 +48,7 @@
(case Thm.prop_of thm of
@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
norm_def (thm RS @{thm fun_cong})
- | Const (@{const_name "=="}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
+ | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
| _ => thm)
@@ -56,17 +56,17 @@
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
- @{const "==>"} $ _ $ _ =>
+ @{const Pure.imp} $ _ $ _ =>
Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
- | Const (@{const_name "=="}, _) $ _ $ _ =>
+ | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
- | Const (@{const_name all}, _) $ Abs _ =>
+ | Const (@{const_name Pure.all}, _) $ Abs _ =>
Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
| _ => Conv.all_conv) ct
val setup_atomize =
- fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
- @{const_name all}, @{const_name Trueprop}]
+ fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq},
+ @{const_name Pure.all}, @{const_name Trueprop}]
(** unfold special quantifiers **)
--- a/src/HOL/Tools/SMT2/smt2_util.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_util.ML Fri Mar 21 20:33:56 2014 +0100
@@ -185,7 +185,7 @@
@{const Trueprop} $ _ => Thm.dest_arg ct
| _ => raise CTERM ("not a property", [ct]))
-val equals = mk_const_pat @{theory} @{const_name "=="} destT1
+val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
--- a/src/HOL/Tools/SMT2/z3_new_proof.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_proof.ML Fri Mar 21 20:33:56 2014 +0100
@@ -463,7 +463,7 @@
val match = Sign.typ_match (Proof_Context.theory_of ctxt)
val t' = singleton (Variable.polymorphic ctxt) t
- val patTs = map snd (Term.strip_qnt_vars @{const_name all} t')
+ val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t')
val objTs = map (the o Symtab.lookup env) bounds
val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end
@@ -501,7 +501,7 @@
SOME (tyenv, _) => subst_of tyenv
| NONE => strip_match ctxt pat (i + 1) (dest_quant i obj))
-fun dest_all i (Const (@{const_name all}, _) $ (a as Abs (_, T, _))) =
+fun dest_all i (Const (@{const_name Pure.all}, _) $ (a as Abs (_, T, _))) =
dest_all (i + 1) (Term.betapply (a, Var (("", i), T)))
| dest_all i t = (i, t)
@@ -517,7 +517,7 @@
| SOME subst =>
let
val applyT = Same.commit (substTs_same subst)
- val patTs = map snd (Term.strip_qnt_vars @{const_name all} t'')
+ val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t'')
in SOME (Symtab.make (bs' ~~ map applyT patTs)) end)
end
--- a/src/HOL/Tools/SMT2/z3_new_replay.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Fri Mar 21 20:33:56 2014 +0100
@@ -14,7 +14,7 @@
structure Z3_New_Replay: Z3_NEW_REPLAY =
struct
-fun params_of t = Term.strip_qnt_vars @{const_name all} t
+fun params_of t = Term.strip_qnt_vars @{const_name Pure.all} t
fun varify ctxt thm =
let
@@ -32,7 +32,7 @@
fun mk (n, T) n' = (n, SMT2_Util.certify ctxt' (Free (n', T)))
in (ctxt', Symtab.make (map2 mk nTs ns)) end
-fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) =
+fun forall_elim_term ct (Const (@{const_name Pure.all}, _) $ (a as Abs _)) =
Term.betapply (a, Thm.term_of ct)
| forall_elim_term _ qt = raise TERM ("forall_elim'", [qt])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Mar 21 20:33:56 2014 +0100
@@ -85,8 +85,8 @@
fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
- | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
- | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
+ | is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2
+ | is_rec_def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
| is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
| is_rec_def _ = false
@@ -260,13 +260,13 @@
else
Interesting
fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t
- | interest_of_prop Ts (@{const "==>"} $ t $ u) =
+ | interest_of_prop Ts (@{const Pure.imp} $ t $ u) =
combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
- | interest_of_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
+ | interest_of_prop Ts (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) =
if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
- | interest_of_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
+ | interest_of_prop Ts ((t as Const (@{const_name Pure.all}, _)) $ u) =
interest_of_prop Ts (t $ eta_expand Ts u 1)
- | interest_of_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
+ | interest_of_prop _ (Const (@{const_name Pure.eq}, _) $ t $ u) =
combine_interests (interest_of_bool t) (interest_of_bool u)
| interest_of_prop _ _ = Deal_Breaker
val t = prop_of th
@@ -351,7 +351,7 @@
| normalize_eq (@{const Trueprop} $ (t as @{const Not}
$ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1)
- | normalize_eq (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
+ | normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) =
(if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1))
|> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2)
| normalize_eq t = t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Mar 21 20:33:56 2014 +0100
@@ -187,9 +187,9 @@
if T = HOLogic.boolT then do_formula else do_term ext_arg
and do_formula t =
(case t of
- Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t'
- | @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2
- | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
+ Const (@{const_name Pure.all}, _) $ Abs (_, _, t') => do_formula t'
+ | @{const Pure.imp} $ t1 $ t2 => do_formula t1 #> do_formula t2
+ | Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 =>
do_term_or_formula false T t1 #> do_term_or_formula true T t2
| @{const Trueprop} $ t1 => do_formula t1
| @{const False} => I
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 21 20:33:56 2014 +0100
@@ -77,10 +77,10 @@
fun do_formula pos t =
(case (pos, t) of
(_, @{const Trueprop} $ t1) => do_formula pos t1
- | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => do_formula pos t'
+ | (true, Const (@{const_name Pure.all}, _) $ Abs (_, _, t')) => do_formula pos t'
| (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => do_formula pos t'
| (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => do_formula pos t'
- | (_, @{const "==>"} $ t1 $ t2) =>
+ | (_, @{const Pure.imp} $ t1 $ t2) =>
do_formula (not pos) t1 andalso (t2 = @{prop False} orelse do_formula pos t2)
| (_, @{const HOL.implies} $ t1 $ t2) =>
do_formula (not pos) t1 andalso (t2 = @{const False} orelse do_formula pos t2)
@@ -88,7 +88,7 @@
| (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 HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
- | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
+ | (true, Const (@{const_name Pure.eq}, _) $ t1 $ t2) => do_equals t1 t2
| _ => false)
in do_formula true end
--- a/src/HOL/Tools/TFL/post.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML Fri Mar 21 20:33:56 2014 +0100
@@ -63,7 +63,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 Pure.eq},_)$_$_ => r
| _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
| _ => r RS P_imp_P_eq_True
--- a/src/HOL/Tools/TFL/rules.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Fri Mar 21 20:33:56 2014 +0100
@@ -293,7 +293,7 @@
fun GEN v th =
let val gth = Thm.forall_intr v th
val thy = Thm.theory_of_thm gth
- val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
+ val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
val allI2 = Drule.instantiate_normalize (certify thy theta) allI
@@ -441,21 +441,22 @@
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
fun is_cong thm =
- case (Thm.prop_of thm)
- of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
- (Const("==",_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) => false
- | _ => true;
+ case (Thm.prop_of thm) of
+ (Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $
+ (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) =>
+ false
+ | _ => true;
-fun dest_equal(Const ("==",_) $
+fun dest_equal(Const (@{const_name Pure.eq},_) $
(Const (@{const_name Trueprop},_) $ lhs)
$ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
- | dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
+ | dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
| dest_equal tm = USyntax.dest_eq tm;
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
-fun dest_all used (Const("all",_) $ (a as Abs _)) = USyntax.dest_abs used a
+fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a
| dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
val is_all = can (dest_all []);
@@ -468,10 +469,10 @@
end
else ([], fm, used);
-fun break_all(Const("all",_) $ Abs (_,_,body)) = body
+fun break_all(Const(@{const_name Pure.all},_) $ Abs (_,_,body)) = body
| break_all _ = raise RULES_ERR "break_all" "not a !!";
-fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
+fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) =
let val (L,core) = list_break_all body
in ((s,ty)::L, core)
end
@@ -725,7 +726,7 @@
fun eliminate thm =
case Thm.prop_of thm
- of Const("==>",_) $ imp $ _ =>
+ of Const(@{const_name Pure.imp},_) $ imp $ _ =>
eliminate
(if not(is_all imp)
then uq_eliminate (thm, imp, Thm.theory_of_thm thm)
@@ -740,7 +741,8 @@
val cntxt = rev (Simplifier.prems_of ctxt)
val dummy = print_thms ctxt "cntxt:" cntxt
val thy = Thm.theory_of_thm thm
- val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
+ val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
+ Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
(Misc_Legacy.add_term_frees(tm,[]))
in fold_rev Forall vlist tm
--- a/src/HOL/Tools/TFL/tfl.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Fri Mar 21 20:33:56 2014 +0100
@@ -357,7 +357,7 @@
(*For Isabelle, the lhs of a definition must be a constant.*)
fun const_def sign (c, Ty, rhs) =
singleton (Syntax.check_terms (Proof_Context.init_global sign))
- (Const("==",dummyT) $ Const(c,Ty) $ rhs);
+ (Const(@{const_name Pure.eq},dummyT) $ Const(c,Ty) $ rhs);
(*Make all TVars available for instantiation by adding a ? to the front*)
fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
--- a/src/HOL/Tools/code_evaluation.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/code_evaluation.ML Fri Mar 21 20:33:56 2014 +0100
@@ -193,7 +193,7 @@
val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
val t = Thm.term_of ct;
val T = fastype_of t;
- val mk_eq = Thm.mk_binop (cert (Const ("==", T --> T --> propT)));
+ val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
in case value ctxt t
of NONE => Thm.reflexive ct
| SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
@@ -206,9 +206,9 @@
fun static_conv ctxt consts Ts =
let
- val eqs = "==" :: @{const_name HOL.eq} ::
+ val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
- (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*)
+ (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
val value = static_value ctxt consts Ts;
val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
in
--- a/src/HOL/Tools/inductive.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Mar 21 20:33:56 2014 +0100
@@ -258,7 +258,7 @@
handle THM _ => thm RS @{thm le_boolD}
in
(case concl_of thm of
- Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
+ Const (@{const_name Pure.eq}, _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
| _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm
| _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
--- a/src/HOL/Tools/inductive_realizer.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Mar 21 20:33:56 2014 +0100
@@ -31,20 +31,21 @@
val pred_of = fst o dest_Const o head_of;
-fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
+fun strip_all' used names (Const (@{const_name Pure.all}, _) $ Abs (s, T, t)) =
let val (s', names') = (case names of
[] => (singleton (Name.variant_list used) s, [])
| name :: names' => (name, names'))
in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
- | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
+ | strip_all' used names ((t as Const (@{const_name Pure.imp}, _) $ P) $ Q) =
t $ strip_all' used names Q
| strip_all' _ _ t = t;
fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
-fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
+fun strip_one name
+ (Const (@{const_name Pure.all}, _) $ Abs (s, T, Const (@{const_name Pure.imp}, _) $ P $ Q)) =
(subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
- | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
+ | strip_one _ (Const (@{const_name Pure.imp}, _) $ P $ Q) = (P, Q);
fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
(case strip_type T of
@@ -145,8 +146,8 @@
val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
- fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
- | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
+ fun is_meta (Const (@{const_name Pure.all}, _) $ Abs (s, _, P)) = is_meta P
+ | is_meta (Const (@{const_name Pure.imp}, _) $ _ $ Q) = is_meta Q
| is_meta (Const (@{const_name Trueprop}, _) $ t) =
(case head_of t of
Const (s, _) => can (Inductive.the_inductive ctxt) s
--- a/src/HOL/Tools/inductive_set.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/inductive_set.ML Fri Mar 21 20:33:56 2014 +0100
@@ -50,7 +50,7 @@
addsimps [@{thm split_paired_all}, @{thm split_conv}]) 1
in
SOME (Goal.prove ctxt [] []
- (Const ("==", T --> T --> propT) $ S $ S')
+ (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
(K (EVERY
[rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
rtac subsetI 1, dtac CollectD 1, simp,
--- a/src/HOL/Tools/record.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/record.ML Fri Mar 21 20:33:56 2014 +0100
@@ -1287,7 +1287,7 @@
(fn ctxt => fn t =>
(case t of
Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
- if quantifier = @{const_name all} orelse
+ if quantifier = @{const_name Pure.all} orelse
quantifier = @{const_name All} orelse
quantifier = @{const_name Ex}
then
@@ -1301,7 +1301,7 @@
| SOME (all_thm, All_thm, Ex_thm, _) =>
SOME
(case quantifier of
- @{const_name all} => all_thm
+ @{const_name Pure.all} => all_thm
| @{const_name All} => All_thm RS @{thm eq_reflection}
| @{const_name Ex} => Ex_thm RS @{thm eq_reflection}
| _ => raise Fail "split_simproc"))
@@ -1368,8 +1368,8 @@
val has_rec = exists_Const
(fn (s, Type (_, [Type (_, [T, _]), _])) =>
- (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
- is_recT T
+ (s = @{const_name Pure.all} orelse s = @{const_name All} orelse s = @{const_name Ex})
+ andalso is_recT T
| _ => false);
fun mk_split_free_tac free induct_thm i =
@@ -1418,10 +1418,10 @@
val has_rec = exists_Const
(fn (s, Type (_, [Type (_, [T, _]), _])) =>
- (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
+ (s = @{const_name Pure.all} orelse s = @{const_name All}) andalso is_recT T
| _ => false);
- fun is_all (Const (@{const_name all}, _) $ _) = ~1
+ fun is_all (Const (@{const_name Pure.all}, _) $ _) = ~1
| is_all (Const (@{const_name All}, _) $ _) = ~1
| is_all _ = 0;
in
--- a/src/HOL/Tools/simpdata.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML Fri Mar 21 20:33:56 2014 +0100
@@ -43,7 +43,7 @@
fun mk_eq th = case concl_of th
(*expects Trueprop if not == *)
- of Const (@{const_name "=="},_) $ _ $ _ => th
+ of Const (@{const_name Pure.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/ex/Refute_Examples.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Fri Mar 21 20:33:56 2014 +0100
@@ -325,7 +325,7 @@
refute [expect = genuine]
oops
-lemma "(x == all) \<Longrightarrow> False"
+lemma "(x == Pure.all) \<Longrightarrow> False"
refute [expect = genuine]
oops
--- a/src/HOL/ex/SVC_Oracle.thy Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Mar 21 20:33:56 2014 +0100
@@ -100,7 +100,7 @@
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
- | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
+ | mt ((c as Const(@{const_name Pure.imp}, _)) $ p $ q) = c $ (mt p) $ (mt q)
| mt t = fm t (*it might be a formula*)
in (Logic.list_all (params, mt body), !pairs) end;
--- a/src/HOL/ex/svc_funcs.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/ex/svc_funcs.ML Fri Mar 21 20:33:56 2014 +0100
@@ -232,7 +232,7 @@
| fm pos t = var(t,[]);
(*entry point, and translation of a meta-formula*)
fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p)
- | mt pos ((c as Const("==>", _)) $ p $ q) =
+ | mt pos ((c as Const(@{const_name Pure.imp}, _)) $ p $ q) =
Buildin("=>", [mt (not pos) p, mt pos q])
| mt pos t = fm pos (iff_tag t) (*it might be a formula*)
--- a/src/Provers/blast.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Provers/blast.ML Fri Mar 21 20:33:56 2014 +0100
@@ -419,11 +419,12 @@
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *)
-fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B
+fun strip_imp_prems (Const (@{const_name Pure.imp}, _) $ A $ B) =
+ strip_Trueprop A :: strip_imp_prems B
| strip_imp_prems _ = [];
(* A1==>...An==>B goes to B, where B is not an implication *)
-fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const (@{const_name Pure.imp}, _) $ A $ B) = strip_imp_concl B
| strip_imp_concl A = strip_Trueprop A;
@@ -443,7 +444,7 @@
else P :: delete_concl Ps
| _ => P :: delete_concl Ps);
-fun skoPrem state vars (Const ("all", _) $ Abs (_, P)) =
+fun skoPrem state vars (Const (@{const_name Pure.all}, _) $ Abs (_, P)) =
skoPrem state vars (subst_bound (Skolem (gensym state "S", vars), P))
| skoPrem _ _ P = P;
@@ -1177,7 +1178,7 @@
(*Make a list of all the parameters in a subgoal, even if nested*)
local open Term
in
-fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
+fun discard_foralls (Const(@{const_name Pure.all},_)$Abs(a,T,t)) = discard_foralls t
| discard_foralls t = t;
end;
--- a/src/Provers/hypsubst.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Provers/hypsubst.ML Fri Mar 21 20:33:56 2014 +0100
@@ -104,8 +104,8 @@
(*Locates a substitutable variable on the left (resp. right) of an equality
assumption. Returns the number of intervening assumptions. *)
fun eq_var bnd novars =
- let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
- | eq_var_aux k (Const("==>",_) $ A $ B) =
+ let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
+ | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
((k, inspect_pair bnd novars
(Data.dest_eq (Data.dest_Trueprop A)))
handle TERM _ => eq_var_aux (k+1) B
--- a/src/Provers/splitter.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Provers/splitter.ML Fri Mar 21 20:33:56 2014 +0100
@@ -57,7 +57,7 @@
fun split_format_err () = error "Wrong format for split rule";
fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
- Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of
+ Const(@{const_name Pure.eq}, _) $ (Var _ $ t) $ c => (case strip_comb t of
(Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
| _ => split_format_err ())
| _ => split_format_err ();
@@ -393,9 +393,9 @@
fun tac (t,i) =
let val n = find_index (exists_Const (member (op =) cname_list o #1))
(Logic.strip_assums_hyp t);
- fun first_prem_is_disj (Const ("==>", _) $ (Const (c, _)
+ fun first_prem_is_disj (Const (@{const_name Pure.imp}, _) $ (Const (c, _)
$ (Const (s, _) $ _ $ _ )) $ _ ) = c = const_Trueprop andalso s = const_or
- | first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
+ | first_prem_is_disj (Const(@{const_name Pure.all},_)$Abs(_,_,t)) =
first_prem_is_disj t
| first_prem_is_disj _ = false;
(* does not work properly if the split variable is bound by a quantifier *)
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 21 20:33:56 2014 +0100
@@ -63,7 +63,7 @@
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
(PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
- (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
+ (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
(PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) =
let
val _ $ A $ C = Envir.beta_norm X;
@@ -78,7 +78,7 @@
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
(PAxm ("Pure.symmetric", _, _) % _ % _ %%
(PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
- (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
+ (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
(PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) =
let
val _ $ A $ C = Envir.beta_norm Y;
@@ -91,7 +91,7 @@
end
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
- (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
+ (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
(PAxm ("Pure.reflexive", _, _) % _) %%
(PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) =
let
@@ -104,7 +104,7 @@
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
(PAxm ("Pure.symmetric", _, _) % _ % _ %%
- (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
+ (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
(PAxm ("Pure.reflexive", _, _) % _) %%
(PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) =
let
@@ -140,7 +140,7 @@
| rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
(PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
(PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
- (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
+ (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
(PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
SOME (equal_elim_axm %> C %> D %% prf2 %%
(equal_elim_axm %> A %> C %% prf3 %%
@@ -150,7 +150,7 @@
(PAxm ("Pure.symmetric", _, _) % _ % _ %%
(PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
(PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
- (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
+ (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
(PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
SOME (equal_elim_axm %> A %> B %% prf1 %%
(equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
@@ -160,7 +160,7 @@
(PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
(PAxm ("Pure.symmetric", _, _) % _ % _ %%
(PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
- (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
+ (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
(PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
(equal_elim_axm %> B %> D %% prf3 %%
@@ -171,14 +171,14 @@
(PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
(PAxm ("Pure.symmetric", _, _) % _ % _ %%
(PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
- (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
+ (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
(PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
(equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
(equal_elim_axm %> C %> D %% prf2 %% prf4)))
| rew' ((prf as PAxm ("Pure.combination", _, _) %
- SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
+ SOME ((eq as Const ("Pure.eq", T)) $ t) % _ % _ % _) %%
(PAxm ("Pure.reflexive", _, _) % _)) =
let val (U, V) = (case T of
Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
@@ -307,9 +307,9 @@
val Hs' = Logic.strip_assums_hyp Q;
val k = length Hs;
val l = length params;
- fun mk_prf i j Hs Hs' (Const ("all", _) $ Abs (_, _, P)) prf =
+ fun mk_prf i j Hs Hs' (Const ("Pure.all", _) $ Abs (_, _, P)) prf =
mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
- | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("==>", _) $ _ $ P) prf =
+ | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("Pure.imp", _) $ _ $ P) prf =
mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
| mk_prf _ _ _ _ _ prf = prf
in
@@ -324,9 +324,9 @@
val Hs' = Logic.strip_assums_hyp Q;
val k = length Hs;
val l = length params;
- fun mk_prf (Const ("all", _) $ Abs (s, T, P)) prf =
+ fun mk_prf (Const ("Pure.all", _) $ Abs (s, T, P)) prf =
Abst (s, SOME T, mk_prf P prf)
- | mk_prf (Const ("==>", _) $ P $ Q) prf =
+ | mk_prf (Const ("Pure.imp", _) $ P $ Q) prf =
AbsP ("H", SOME P, mk_prf Q prf)
| mk_prf _ prf = prf
in
--- a/src/Pure/Proof/reconstruct.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/Proof/reconstruct.ML Fri Mar 21 20:33:56 2014 +0100
@@ -155,7 +155,7 @@
| SOME T => (T, env));
val (t, prf, cnstrts, env'', vTs') =
mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
- in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
+ in (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
cnstrts, env'', vTs')
end
| mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) =
@@ -173,7 +173,7 @@
| mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) =
let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2
in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of
- (Const ("==>", _) $ u' $ t', prf1, cnstrts', env'', vTs'') =>
+ (Const ("Pure.imp", _) $ u' $ t', prf1, cnstrts', env'', vTs'') =>
add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts)
env'' vTs'' (u, u')
| (t, prf1, cnstrts', env'', vTs'') =>
@@ -185,7 +185,7 @@
| mk_cnstrts env Ts Hs vTs (cprf % SOME t) =
let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t
in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of
- (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
+ (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
prf, cnstrts, env2, vTs2) =>
let val env3 = unifyT thy env2 T U
in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2)
@@ -194,12 +194,12 @@
let val (v, env3) = mk_var env2 Ts (U --> propT);
in
add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2
- (u, Const ("all", (U --> propT) --> propT) $ v)
+ (u, Const ("Pure.all", (U --> propT) --> propT) $ v)
end)
end
| mk_cnstrts env Ts Hs vTs (cprf % NONE) =
(case head_norm (mk_cnstrts env Ts Hs vTs cprf) of
- (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
+ (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
prf, cnstrts, env', vTs') =>
let val (t, env'') = mk_var env' Ts T
in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs')
@@ -211,7 +211,7 @@
val (t, env3) = mk_var env2 Ts T
in
add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs'
- (u, Const ("all", (T --> propT) --> propT) $ v)
+ (u, Const ("Pure.all", (T --> propT) --> propT) $ v)
end)
| mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs), _))) =
mk_cnstrts_atom env vTs prop opTs prf
@@ -309,10 +309,10 @@
| prop_of0 Hs (AbsP (s, SOME t, prf)) =
Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
| prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
- Const ("all", _) $ f => f $ t
+ Const ("Pure.all", _) $ f => f $ t
| _ => error "prop_of: all expected")
| prop_of0 Hs (prf1 %% prf2) = (case head_norm (prop_of0 Hs prf1) of
- Const ("==>", _) $ P $ Q => Q
+ Const ("Pure.imp", _) $ P $ Q => Q
| _ => error "prop_of: ==> expected")
| prop_of0 Hs (Hyp t) = t
| prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
--- a/src/Pure/Syntax/simple_syntax.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML Fri Mar 21 20:33:56 2014 +0100
@@ -107,12 +107,12 @@
(enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies ||
term2 env T) x
and term2 env T x =
- (equal env "==" ||
+ (equal env ||
term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
term3 env T) x
-and equal env eq x =
- (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>
- Const (eq, Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
+and equal env x =
+ (term3 env dummyT -- ($$ "==" |-- term2 env dummyT) >> (fn (t, u) =>
+ Const ("Pure.eq", Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
and term3 env T x =
(idt >> Free ||
var -- constraint >> Var ||
--- a/src/Pure/Syntax/syntax_trans.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Fri Mar 21 20:33:56 2014 +0100
@@ -174,7 +174,7 @@
(case Ast.unfold_ast_p "_asms" asms of
(asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
| _ => raise Ast.AST ("bigimpl_ast_tr", asts))
- in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
+ in Ast.fold_ast_p "\\<^const>Pure.imp" (prems, concl) end
| bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
@@ -382,7 +382,8 @@
fun impl_ast_tr' asts =
if no_brackets () then raise Match
else
- (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
+ (case Ast.unfold_ast_p "\\<^const>Pure.imp"
+ (Ast.Appl (Ast.Constant "\\<^const>Pure.imp" :: asts)) of
(prems as _ :: _ :: _, concl) =>
let
val (asms, asm) = split_last prems;
@@ -498,7 +499,7 @@
("_abs", fn _ => abs_ast_tr'),
("_idts", fn _ => idtyp_ast_tr' "_idts"),
("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
- ("\\<^const>==>", fn _ => impl_ast_tr'),
+ ("\\<^const>Pure.imp", fn _ => impl_ast_tr'),
("_index", fn _ => index_ast_tr')];
end;
--- a/src/Pure/conv.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/conv.ML Fri Mar 21 20:33:56 2014 +0100
@@ -140,17 +140,17 @@
fun forall_conv cv ctxt ct =
(case Thm.term_of ct of
- Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
+ Const ("Pure.all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
| _ => raise CTERM ("forall_conv", [ct]));
fun implies_conv cv1 cv2 ct =
(case Thm.term_of ct of
- Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
+ Const ("Pure.imp", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
| _ => raise CTERM ("implies_conv", [ct]));
fun implies_concl_conv cv ct =
(case Thm.term_of ct of
- Const ("==>", _) $ _ $ _ => arg_conv cv ct
+ Const ("Pure.imp", _) $ _ $ _ => arg_conv cv ct
| _ => raise CTERM ("implies_concl_conv", [ct]));
--- a/src/Pure/drule.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/drule.ML Fri Mar 21 20:33:56 2014 +0100
@@ -126,7 +126,7 @@
(* A1==>...An==>B goes to B, where B is not an implication *)
fun strip_imp_concl ct =
(case Thm.term_of ct of
- Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
+ Const ("Pure.imp", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
| _ => ct);
(*The premises of a theorem, as a cterm list*)
@@ -706,7 +706,7 @@
val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq];
fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false
- | is_norm_hhf (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false
+ | is_norm_hhf (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false
| is_norm_hhf (Abs _ $ _) = false
| is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u
| is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t
--- a/src/Pure/goal.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/goal.ML Fri Mar 21 20:33:56 2014 +0100
@@ -327,8 +327,8 @@
(* non-atomic goal assumptions *)
-fun non_atomic (Const ("==>", _) $ _ $ _) = true
- | non_atomic (Const ("all", _) $ _) = true
+fun non_atomic (Const ("Pure.imp", _) $ _ $ _) = true
+ | non_atomic (Const ("Pure.all", _) $ _) = true
| non_atomic _ = false;
fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
--- a/src/Pure/logic.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/logic.ML Fri Mar 21 20:33:56 2014 +0100
@@ -93,14 +93,14 @@
(** all **)
-fun all_const T = Const ("all", (T --> propT) --> propT);
+fun all_const T = Const ("Pure.all", (T --> propT) --> propT);
fun all v t = all_const (Term.fastype_of v) $ lambda v t;
-fun is_all (Const ("all", _) $ Abs _) = true
+fun is_all (Const ("Pure.all", _) $ Abs _) = true
| is_all _ = false;
-fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) =
+fun dest_all (Const ("Pure.all", _) $ Abs (abs as (_, T, _))) =
let val (x, b) = Term.dest_abs abs (*potentially slow*)
in ((x, T), b) end
| dest_all t = raise TERM ("dest_all", [t]);
@@ -113,19 +113,19 @@
fun mk_equals (t, u) =
let val T = Term.fastype_of t
- in Const ("==", T --> T --> propT) $ t $ u end;
+ in Const ("Pure.eq", T --> T --> propT) $ t $ u end;
-fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
+fun dest_equals (Const ("Pure.eq", _) $ t $ u) = (t, u)
| dest_equals t = raise TERM ("dest_equals", [t]);
(** implies **)
-val implies = Const ("==>", propT --> propT --> propT);
+val implies = Const ("Pure.imp", propT --> propT --> propT);
fun mk_implies (A, B) = implies $ A $ B;
-fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
+fun dest_implies (Const ("Pure.imp", _) $ A $ B) = (A, B)
| dest_implies A = raise TERM ("dest_implies", [A]);
@@ -136,28 +136,28 @@
| list_implies (A::As, B) = implies $ A $ list_implies(As,B);
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *)
-fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems B
| strip_imp_prems _ = [];
(* A1==>...An==>B goes to B, where B is not an implication *)
-fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B
| strip_imp_concl A = A : term;
(*Strip and return premises: (i, [], A1==>...Ai==>B)
goes to ([Ai, A(i-1),...,A1] , B) (REVERSED)
if i<0 or else i too big then raises TERM*)
fun strip_prems (0, As, B) = (As, B)
- | strip_prems (i, As, Const("==>", _) $ A $ B) =
+ | strip_prems (i, As, Const("Pure.imp", _) $ A $ B) =
strip_prems (i-1, A::As, B)
| strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
(*Count premises -- quicker than (length o strip_prems) *)
-fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
+fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B
| count_prems _ = 0;
(*Select Ai from A1 ==>...Ai==>B*)
-fun nth_prem (1, Const ("==>", _) $ A $ _) = A
- | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
+fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A
+ | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B)
| nth_prem (_, A) = raise TERM ("nth_prem", [A]);
(*strip a proof state (Horn clause):
@@ -395,46 +395,46 @@
fun lift_abs inc =
let
- fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
- | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
+ fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t
+ | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
| lift Ts _ t = incr_indexes (rev Ts, inc) t;
in lift [] end;
fun lift_all inc =
let
- fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
- | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
+ fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t
+ | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
| lift Ts _ t = incr_indexes (rev Ts, inc) t;
in lift [] end;
(*Strips assumptions in goal, yielding list of hypotheses. *)
fun strip_assums_hyp B =
let
- fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
- | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
+ fun strip Hs (Const ("Pure.imp", _) $ H $ B) = strip (H :: Hs) B
+ | strip Hs (Const ("Pure.all", _) $ Abs (a, T, t)) =
strip (map (incr_boundvars 1) Hs) t
| strip Hs B = rev Hs
in strip [] B end;
(*Strips assumptions in goal, yielding conclusion. *)
-fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
- | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
+fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B
+ | strip_assums_concl (Const("Pure.all",_)$Abs(a,T,t)) = strip_assums_concl t
| strip_assums_concl B = B;
(*Make a list of all the parameters in a subgoal, even if nested*)
-fun strip_params (Const("==>", _) $ H $ B) = strip_params B
- | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
+fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B
+ | strip_params (Const("Pure.all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
| strip_params B = [];
(*test for nested meta connectives in prems*)
val has_meta_prems =
let
- fun is_meta (Const ("==", _) $ _ $ _) = true
- | is_meta (Const ("==>", _) $ _ $ _) = true
- | is_meta (Const ("all", _) $ _) = true
+ fun is_meta (Const ("Pure.eq", _) $ _ $ _) = true
+ | is_meta (Const ("Pure.imp", _) $ _ $ _) = true
+ | is_meta (Const ("Pure.all", _) $ _) = true
| is_meta _ = false;
- fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
- | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
+ fun ex_meta (Const ("Pure.imp", _) $ A $ B) = is_meta A orelse ex_meta B
+ | ex_meta (Const ("Pure.all", _) $ Abs (_, _, B)) = ex_meta B
| ex_meta _ = false;
in ex_meta end;
@@ -444,10 +444,10 @@
fun remove_params j n A =
if j=0 andalso n<=0 then A (*nothing left to do...*)
else case A of
- Const("==>", _) $ H $ B =>
+ Const("Pure.imp", _) $ H $ B =>
if n=1 then (remove_params j (n-1) B)
else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
- | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
+ | Const("Pure.all",_)$Abs(a,T,t) => remove_params (j-1) n t
| _ => if n>0 then raise TERM("remove_params", [A])
else A;
@@ -460,9 +460,9 @@
in list_all (vars, remove_params (length vars) n A) end;
(*Makes parameters in a goal have the names supplied by the list cs.*)
-fun list_rename_params cs (Const ("==>", _) $ A $ B) =
+fun list_rename_params cs (Const ("Pure.imp", _) $ A $ B) =
implies $ A $ list_rename_params cs B
- | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) =
+ | list_rename_params (c :: cs) ((a as Const ("Pure.all", _)) $ Abs (_, T, t)) =
a $ Abs (c, T, list_rename_params cs t)
| list_rename_params cs B = B;
@@ -480,12 +480,12 @@
Unless nasms<0, it can terminate the recursion early; that allows
erule to work on assumptions of the form P==>Q.*)
fun strip_assums_imp (0, Hs, B) = (Hs, B) (*recursion terminated by nasms*)
- | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
+ | strip_assums_imp (nasms, Hs, Const("Pure.imp", _) $ H $ B) =
strip_assums_imp (nasms-1, H::Hs, B)
| strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
(*Strips OUTER parameters only.*)
-fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
+fun strip_assums_all (params, Const("Pure.all",_)$Abs(a,T,t)) =
strip_assums_all ((a,T)::params, t)
| strip_assums_all (params, B) = (params, B);
--- a/src/Pure/more_thm.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/more_thm.ML Fri Mar 21 20:33:56 2014 +0100
@@ -127,7 +127,7 @@
let
val cert = Thm.cterm_of (Thm.theory_of_cterm t);
val T = #T (Thm.rep_cterm t);
- in Thm.apply (cert (Const ("all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
+ in Thm.apply (cert (Const ("Pure.all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
fun all t A = all_name ("", t) A;
@@ -136,22 +136,22 @@
fun dest_implies ct =
(case Thm.term_of ct of
- Const ("==>", _) $ _ $ _ => dest_binop ct
+ Const ("Pure.imp", _) $ _ $ _ => dest_binop ct
| _ => raise TERM ("dest_implies", [Thm.term_of ct]));
fun dest_equals ct =
(case Thm.term_of ct of
- Const ("==", _) $ _ $ _ => dest_binop ct
+ Const ("Pure.eq", _) $ _ $ _ => dest_binop ct
| _ => raise TERM ("dest_equals", [Thm.term_of ct]));
fun dest_equals_lhs ct =
(case Thm.term_of ct of
- Const ("==", _) $ _ $ _ => Thm.dest_arg1 ct
+ Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct
| _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct]));
fun dest_equals_rhs ct =
(case Thm.term_of ct of
- Const ("==", _) $ _ $ _ => Thm.dest_arg ct
+ Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct
| _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct]));
val lhs_of = dest_equals_lhs o Thm.cprop_of;
@@ -337,7 +337,7 @@
fun forall_elim_var i th =
forall_elim_vars_aux
- (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
+ (fn Const ("Pure.all", _) $ Abs (a, T, _) => [(a, T)]
| _ => raise THM ("forall_elim_vars", i, [th])) i th;
end;
--- a/src/Pure/proofterm.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/proofterm.ML Fri Mar 21 20:33:56 2014 +0100
@@ -865,9 +865,9 @@
fun mk_app b (i, j, prf) =
if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
- fun lift Us bs i j (Const ("==>", _) $ A $ B) =
+ fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) =
AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
- | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
+ | lift Us bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) =
Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
| lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
@@ -886,9 +886,9 @@
fun mk_asm_prf t i m =
let
fun imp_prf _ i 0 = PBound i
- | imp_prf (Const ("==>", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
+ | imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
| imp_prf _ i _ = PBound i;
- fun all_prf (Const ("all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
+ fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
| all_prf t = imp_prf t (~i) m
in all_prf t end;
@@ -899,9 +899,9 @@
(***** Composition of object rule with proof state *****)
-fun flatten_params_proof i j n (Const ("==>", _) $ A $ B, k) =
+fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) =
AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k))
- | flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) =
+ | flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) =
Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k))
| flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
@@ -1091,9 +1091,9 @@
if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
else vs;
-fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) =
+fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) =
add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u)
- | add_npvars q p Ts (vs, Const ("all", Type (_, [Type (_, [T, _]), _])) $ t) =
+ | add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) =
add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
| add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
| add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
@@ -1105,8 +1105,8 @@
| (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
| (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
-fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
- | prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
+fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
+ | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t
| prop_vars t = (case strip_comb t of
(Var (ixn, _), _) => [ixn] | _ => []);
@@ -1196,7 +1196,7 @@
(fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
| (_, x) => (false, x)) insts
in ([], false, insts' @ map (pair false) ts'', prf) end
- and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
+ and needed (Const ("Pure.imp", _) $ t $ u) ts ((b, _, _, _)::prfs) =
union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs)
| needed (Var (ixn, _)) (_::_) _ = [ixn]
| needed _ _ _ = [];
--- a/src/Pure/pure_thy.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/pure_thy.ML Fri Mar 21 20:33:56 2014 +0100
@@ -169,7 +169,7 @@
("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"),
("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
- (const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
+ (const "Pure.imp", typ "prop => prop => prop", Delimfix "op ==>"),
(const "Pure.dummy_pattern", typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
(const "Pure.term", typ "logic => prop", Delimfix "TERM _"),
@@ -184,9 +184,9 @@
("_idtyp", typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
- (const "==", typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
- (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
- (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
+ (const "Pure.eq", typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
+ (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
+ (const "Pure.imp", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Delimfix "\\<dots>")]
@@ -195,15 +195,15 @@
#> Sign.add_syntax ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts
- [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
- (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
- (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
+ [(qualify (Binding.name "eq"), typ "'a => 'a => prop", Infix ("==", 2)),
+ (qualify (Binding.name "imp"), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
+ (qualify (Binding.name "all"), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
(qualify (Binding.name "prop"), typ "prop => prop", NoSyn),
(qualify (Binding.name "type"), typ "'a itself", NoSyn),
(qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
- #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
- #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
- #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
+ #> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") []
+ #> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") []
+ #> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") []
#> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") []
#> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") []
#> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
--- a/src/Pure/raw_simplifier.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/raw_simplifier.ML Fri Mar 21 20:33:56 2014 +0100
@@ -599,7 +599,7 @@
| is_full_cong_prems [] _ = false
| is_full_cong_prems (p :: prems) varpairs =
(case Logic.strip_assums_concl p of
- Const ("==", _) $ lhs $ rhs =>
+ Const ("Pure.eq", _) $ lhs $ rhs =>
let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
is_Var x andalso forall is_Bound xs andalso
not (has_duplicates (op =) xs) andalso xs = ys andalso
@@ -981,7 +981,7 @@
let
fun is_simple ({thm, ...}: rrule) =
(case Thm.prop_of thm of
- Const ("==", _) $ _ $ _ => true
+ Const ("Pure.eq", _) $ _ $ _ => true
| _ => false);
fun sort [] (re1, re2) = re1 @ re2
| sort (rr :: rrs) (re1, re2) =
@@ -1099,7 +1099,7 @@
end
| t $ _ =>
(case t of
- Const ("==>", _) $ _ => impc t0 ctxt
+ Const ("Pure.imp", _) $ _ => impc t0 ctxt
| Abs _ =>
let val thm = Thm.beta_conversion false t0
in
--- a/src/Pure/term.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/term.ML Fri Mar 21 20:33:56 2014 +0100
@@ -579,11 +579,11 @@
val propT : typ = Type ("prop",[]);
(* maps !!x1...xn. t to t *)
-fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t
+fun strip_all_body (Const("Pure.all",_)$Abs(_,_,t)) = strip_all_body t
| strip_all_body t = t;
(* maps !!x1...xn. t to [x1, ..., xn] *)
-fun strip_all_vars (Const("all",_)$Abs(a,T,t)) =
+fun strip_all_vars (Const("Pure.all",_)$Abs(a,T,t)) =
(a,T) :: strip_all_vars t
| strip_all_vars t = [] : (string*typ) list;
--- a/src/Pure/thm.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/thm.ML Fri Mar 21 20:33:56 2014 +0100
@@ -687,7 +687,7 @@
fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
in
case prop of
- Const ("==>", _) $ A $ B =>
+ Const ("Pure.imp", _) $ A $ B =>
if A aconv propA then
Thm (deriv_rule2 (curry Proofterm.%%) der derA,
{thy = merge_thys2 thAB thA,
@@ -741,7 +741,7 @@
(ct as Cterm {t, T, maxidx = maxt, sorts, ...})
(th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
(case prop of
- Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
+ Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
if T <> qary then
raise THM ("forall_elim: type mismatch", 0, [th])
else
@@ -778,7 +778,7 @@
*)
fun symmetric (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) =
(case prop of
- (eq as Const ("==", _)) $ t $ u =>
+ (eq as Const ("Pure.eq", _)) $ t $ u =>
Thm (deriv_rule1 Proofterm.symmetric der,
{thy = thy,
tags = [],
@@ -803,7 +803,7 @@
fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
in
case (prop1, prop2) of
- ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>
+ ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
if not (u aconv u') then err "middle term"
else
Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
@@ -911,8 +911,8 @@
| _ => raise THM ("combination: not function type", 0, [th1, th2]));
in
(case (prop1, prop2) of
- (Const ("==", Type ("fun", [fT, _])) $ f $ g,
- Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
+ (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
+ Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
(chktypes fT tT;
Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
{thy = merge_thys2 th1 th2,
@@ -939,7 +939,7 @@
fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
in
(case (prop1, prop2) of
- (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
+ (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
if A aconv A' andalso B aconv B' then
Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
{thy = merge_thys2 th1 th2,
@@ -967,7 +967,7 @@
fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
in
(case prop1 of
- Const ("==", _) $ A $ B =>
+ Const ("Pure.eq", _) $ A $ B =>
if prop2 aconv A then
Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
{thy = merge_thys2 th1 th2,
@@ -1472,17 +1472,17 @@
(* strip_apply f B A strips off all assumptions/parameters from A
introduced by lifting over B, and applies f to remaining part of A*)
fun strip_apply f =
- let fun strip (Const ("==>", _) $ _ $ B1)
- (Const ("==>", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
- | strip ((c as Const ("all", _)) $ Abs (_, _, t1))
- ( Const ("all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
+ let fun strip (Const ("Pure.imp", _) $ _ $ B1)
+ (Const ("Pure.imp", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
+ | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1))
+ ( Const ("Pure.all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
| strip _ A = f A
in strip end;
-fun strip_lifted (Const ("==>", _) $ _ $ B1)
- (Const ("==>", _) $ _ $ B2) = strip_lifted B1 B2
- | strip_lifted (Const ("all", _) $ Abs (_, _, t1))
- (Const ("all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
+fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1)
+ (Const ("Pure.imp", _) $ _ $ B2) = strip_lifted B1 B2
+ | strip_lifted (Const ("Pure.all", _) $ Abs (_, _, t1))
+ (Const ("Pure.all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
| strip_lifted _ A = A;
(*Use the alist to rename all bound variables and some unknowns in a term
@@ -1532,10 +1532,10 @@
(*strip off pairs of assumptions/parameters in parallel -- they are
identical because of lifting*)
-fun strip_assums2 (Const("==>", _) $ _ $ B1,
- Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
- | strip_assums2 (Const("all",_)$Abs(a,T,t1),
- Const("all",_)$Abs(_,_,t2)) =
+fun strip_assums2 (Const("Pure.imp", _) $ _ $ B1,
+ Const("Pure.imp", _) $ _ $ B2) = strip_assums2 (B1,B2)
+ | strip_assums2 (Const("Pure.all",_)$Abs(a,T,t1),
+ Const("Pure.all",_)$Abs(_,_,t2)) =
let val (B1,B2) = strip_assums2 (t1,t2)
in (Abs(a,T,B1), Abs(a,T,B2)) end
| strip_assums2 BB = BB;
@@ -1543,13 +1543,13 @@
(*Faster normalization: skip assumptions that were lifted over*)
fun norm_term_skip env 0 t = Envir.norm_term env t
- | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
+ | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) =
let
val T' = Envir.subst_type (Envir.type_env env) T
(*Must instantiate types of parameters because they are flattened;
this could be a NEW parameter*)
in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end
- | norm_term_skip env n (Const ("==>", _) $ A $ B) =
+ | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) =
Logic.mk_implies (A, norm_term_skip env (n - 1) B)
| norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
--- a/src/Sequents/simpdata.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Sequents/simpdata.ML Fri Mar 21 20:33:56 2014 +0100
@@ -29,7 +29,7 @@
(*Make meta-equalities.*)
fun mk_meta_eq ctxt th = case concl_of th of
- Const("==",_)$_$_ => th
+ Const(@{const_name Pure.eq},_)$_$_ => th
| Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
(case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
([], [p]) =>
--- a/src/Tools/Code/code_runtime.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML Fri Mar 21 20:33:56 2014 +0100
@@ -163,7 +163,7 @@
val _ = if fastype_of t <> propT
then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
else ();
- val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
+ val iff = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
of SOME Holds => true
| _ => false;
--- a/src/Tools/Code/code_symbol.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Tools/Code/code_symbol.ML Fri Mar 21 20:33:56 2014 +0100
@@ -88,8 +88,8 @@
in
fun default_base (Constant "") = "value"
- | default_base (Constant "==>") = "follows"
- | default_base (Constant "==") = "meta_eq"
+ | default_base (Constant @{const_name Pure.imp}) = "follows"
+ | default_base (Constant @{const_name Pure.eq}) = "meta_eq"
| default_base (Constant c) = base c
| default_base (Type_Constructor tyco) = base tyco
| default_base (Type_Class class) = base class
--- a/src/Tools/induct.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Tools/induct.ML Fri Mar 21 20:33:56 2014 +0100
@@ -162,7 +162,7 @@
| SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
val rearrange_eqs_simproc =
- Simplifier.simproc_global Pure.thy "rearrange_eqs" ["all t"]
+ Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
(fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t));
@@ -644,14 +644,16 @@
local
-fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
+fun goal_prefix k ((c as Const (@{const_name Pure.all}, _)) $ Abs (a, T, B)) =
+ c $ Abs (a, T, goal_prefix k B)
| goal_prefix 0 _ = Term.dummy_prop
- | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
+ | goal_prefix k ((c as Const (@{const_name Pure.imp}, _)) $ A $ B) =
+ c $ A $ goal_prefix (k - 1) B
| goal_prefix _ _ = Term.dummy_prop;
-fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
+fun goal_params k (Const (@{const_name Pure.all}, _) $ Abs (_, _, B)) = goal_params k B + 1
| goal_params 0 _ = 0
- | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
+ | goal_params k (Const (@{const_name Pure.imp}, _) $ _ $ B) = goal_params (k - 1) B
| goal_params _ _ = 0;
fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
@@ -670,11 +672,13 @@
[(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
(cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
- fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
+ fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) =
+ goal_concl k ((a, T) :: xs) B
| goal_concl 0 xs B =
if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
else SOME (xs, absfree (x, T) (Term.incr_boundvars 1 B))
- | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
+ | goal_concl k xs (Const (@{const_name Pure.imp}, _) $ _ $ B) =
+ goal_concl (k - 1) xs B
| goal_concl _ _ _ = NONE;
in
(case goal_concl n [] goal of
--- a/src/Tools/misc_legacy.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Tools/misc_legacy.ML Fri Mar 21 20:33:56 2014 +0100
@@ -130,9 +130,9 @@
H1,...,Hn are the hypotheses; x1...xm are variants of the parameters.
Main difference from strip_assums concerns parameters:
it replaces the bound variables by free variables. *)
-fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) =
+fun strip_context_aux (params, Hs, Const (@{const_name Pure.imp}, _) $ H $ B) =
strip_context_aux (params, H :: Hs, B)
- | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) =
+ | strip_context_aux (params, Hs, Const (@{const_name Pure.all},_) $ Abs (a, T, t)) =
let val (b, u) = Syntax_Trans.variant_abs (a, T, t)
in strip_context_aux ((b, T) :: params, Hs, u) end
| strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
--- a/src/Tools/nbe.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Tools/nbe.ML Fri Mar 21 20:33:56 2014 +0100
@@ -586,7 +586,7 @@
let
val thy = Proof_Context.theory_of ctxt;
val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
- val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT));
+ val eq = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
val rhs = Thm.cterm_of thy raw_rhs;
in Thm.mk_binop eq lhs rhs end;
--- a/src/Tools/quickcheck.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Tools/quickcheck.ML Fri Mar 21 20:33:56 2014 +0100
@@ -358,7 +358,7 @@
val lthy = Proof.context_of state;
val thy = Proof.theory_of state;
val _ = message lthy "Quickchecking..."
- fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
+ fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t
| strip t = t;
val {goal = st, ...} = Proof.raw_goal state;
val (gi, frees) = Logic.goal_params (prop_of st) i;