# HG changeset patch # User wenzelm # Date 1395430436 -3600 # Node ID 84fc7dfa3cd439a5eace985db3c7fa84b241b83d # Parent 3298b7a2795a63dc415e94c8c2c3e6e3246e6ba3 more qualified names; diff -r 3298b7a2795a -r 84fc7dfa3cd4 NEWS --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/CCL/Wfd.thy --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Doc/ProgProve/LaTeXsugar.thy --- 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 \ prop \ 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 \ prop \ prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") @@ -36,7 +36,7 @@ "_asm" :: "prop \ 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 \ prop \ prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/FOL/simpdata.ML --- 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} diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/FOLP/hypsubst.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/FOLP/simp.ML --- 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 _ = []; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Decision_Procs/cooper_tac.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Decision_Procs/ferrack_tac.ML --- 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, diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Decision_Procs/ferrante_rackoff.ML --- 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 = diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Decision_Procs/langford.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Decision_Procs/mir_tac.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Library/LaTeXsugar.thy --- 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 \ prop \ 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 \ prop \ prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") @@ -90,7 +90,7 @@ "_asm" :: "prop \ 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 \ prop \ prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Library/OptionalSugar.thy --- 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{\ >\\<^raw:}\putisatab\isa{> (_)") + "Pure.eq" ("(_) \<^raw:}\putisatab\isa{\ >\\<^raw:}\putisatab\isa{> (_)") (* Let *) translations diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Library/refute.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Matrix_LP/Compute_Oracle/compute.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Mutabelle/mutabelle_extra.ML --- 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 = [ diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Nitpick_Examples/Core_Nits.thy --- 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 \ all \ False" +lemma "x \ Pure.all \ False" nitpick [card = 1, expect = genuine] nitpick [card = 1, box "('a \ prop) \ prop", expect = genuine] nitpick [card = 6, expect = genuine] @@ -306,15 +306,15 @@ nitpick [expect = genuine] oops -lemma "all (\x. Trueprop (f x y = f x y)) \ Trueprop True" +lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop True" nitpick [expect = none] by auto -lemma "all (\x. Trueprop (f x y = f x y)) \ Trueprop False" +lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop False" nitpick [expect = genuine] oops -lemma "I = (\x. x) \ all P \ all (\x. P (I x))" +lemma "I = (\x. x) \ Pure.all P \ Pure.all (\x. P (I x))" nitpick [expect = none] by auto diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Nitpick_Examples/Refute_Nits.thy --- 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 \ all) \ False" +lemma "(x \ Pure.all) \ False" nitpick [expect = genuine] oops diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Nominal/nominal_primrec.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Nominal/nominal_thmdecls.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Product_Type.thy --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Prolog/prolog.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- 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})) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 = diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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); diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- 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); diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Datatype/primrec.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Datatype/rep_datatype.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Function/function_common.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Function/function_lib.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Lifting/lifting_def.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Meson/meson.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Meson/meson_clausify.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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) ^ "."); diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 @@ " \ " ^ 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 = diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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}, diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/SMT/smt_normalize.ML --- 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 **) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/SMT/smt_utils.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/SMT/z3_proof_tools.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/SMT2/smt2_normalize.ML --- 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 **) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/SMT2/smt2_util.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/SMT2/z3_new_proof.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/SMT2/z3_new_replay.ML --- 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]) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/TFL/post.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/TFL/rules.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/TFL/tfl.ML --- 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) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/code_evaluation.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/inductive.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/inductive_realizer.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/inductive_set.ML --- 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, diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/record.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/simpdata.ML --- 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} diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/ex/Refute_Examples.thy --- 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) \ False" +lemma "(x == Pure.all) \ False" refute [expect = genuine] oops diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/ex/SVC_Oracle.thy --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/ex/svc_funcs.ML --- 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*) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Provers/blast.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Provers/hypsubst.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Provers/splitter.ML --- 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 *) diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/Proof/proof_rewrite_rules.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/Proof/reconstruct.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/Syntax/simple_syntax.ML --- 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 || diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/Syntax/syntax_trans.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/conv.ML --- 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])); diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/drule.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/goal.ML --- 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) => diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/logic.ML --- 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); diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/more_thm.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/proofterm.ML --- 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 _ _ _ = []; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/pure_thy.ML --- 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 ("_\\_", [], 0)), ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), - (const "==", typ "'a => 'a => prop", Infix ("\\", 2)), - (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), - (const "==>", typ "prop => prop => prop", Infixr ("\\", 1)), + (const "Pure.eq", typ "'a => 'a => prop", Infix ("\\", 2)), + (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), + (const "Pure.imp", typ "prop => prop => prop", Infixr ("\\", 1)), ("_DDDOT", typ "aprop", Delimfix "\\"), ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_DDDOT", typ "logic", Delimfix "\\")] @@ -195,15 +195,15 @@ #> Sign.add_syntax ("HTML", false) [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/raw_simplifier.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/term.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Pure/thm.ML --- 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??"; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Sequents/simpdata.ML --- 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]) => diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Tools/Code/code_runtime.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Tools/Code/code_symbol.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Tools/induct.ML --- 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 diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Tools/misc_legacy.ML --- 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); diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Tools/nbe.ML --- 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; diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/Tools/quickcheck.ML --- 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;