--- a/src/HOL/Tools/Lifting/lifting_info.ML Sat Mar 22 20:42:16 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Sat Mar 22 21:40:19 2014 +0100
@@ -446,30 +446,35 @@
let
val assms = map (perhaps (try HOLogic.dest_Trueprop)) (prems_of rule)
val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of rule);
- val (lhs, rhs) = case concl of
- Const ("Orderings.ord_class.less_eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs =>
- (lhs, rhs)
- | Const ("Orderings.ord_class.less_eq", _) $ rhs $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) =>
- (lhs, rhs)
- | Const ("HOL.eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => (lhs, rhs)
- | _ => error "The rule has a wrong format."
+ val (lhs, rhs) =
+ (case concl of
+ Const (@{const_name less_eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs =>
+ (lhs, rhs)
+ | Const (@{const_name less_eq}, _) $ rhs $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) =>
+ (lhs, rhs)
+ | Const (@{const_name HOL.eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs =>
+ (lhs, rhs)
+ | _ => error "The rule has a wrong format.")
val lhs_vars = Term.add_vars lhs []
val rhs_vars = Term.add_vars rhs []
val assms_vars = fold Term.add_vars assms [];
- val _ = if has_duplicates op= lhs_vars then error "Left-hand side has variable duplicates" else ()
- val _ = if subset op= (rhs_vars, lhs_vars) then ()
+ val _ =
+ if has_duplicates op= lhs_vars
+ then error "Left-hand side has variable duplicates" else ()
+ val _ =
+ if subset op= (rhs_vars, lhs_vars) then ()
else error "Extra variables in the right-hand side of the rule"
- val _ = if subset op= (assms_vars, lhs_vars) then ()
+ val _ =
+ if subset op= (assms_vars, lhs_vars) then ()
else error "Extra variables in the assumptions of the rule"
val rhs_args = (snd o strip_comb) rhs;
- fun check_comp t = case t of
- Const ("Relation.relcompp", _) $ Var (_, _) $ Var (_,_) => ()
- | _ => error "There is an argument on the rhs that is not a composition."
+ fun check_comp t =
+ (case t of
+ Const (@{const_name relcompp}, _) $ Var _ $ Var _ => ()
+ | _ => error "There is an argument on the rhs that is not a composition.")
val _ = map check_comp rhs_args
- in
- ()
- end
+ in () end
in
fun add_distr_rule distr_rule ctxt =
@@ -477,13 +482,13 @@
val _ = sanity_check distr_rule
val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of distr_rule)
in
- case concl of
- Const ("Orderings.ord_class.less_eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>
+ (case concl of
+ Const (@{const_name less_eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
add_pos_distr_rule distr_rule ctxt
- | Const ("Orderings.ord_class.less_eq", _) $ _ $ (Const ("Relation.relcompp",_) $ _ $ _) =>
+ | Const (@{const_name less_eq}, _) $ _ $ (Const (@{const_name relcompp},_) $ _ $ _) =>
add_neg_distr_rule distr_rule ctxt
- | Const ("HOL.eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>
- add_eq_distr_rule distr_rule ctxt
+ | Const (@{const_name HOL.eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
+ add_eq_distr_rule distr_rule ctxt)
end
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Sat Mar 22 20:42:16 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sat Mar 22 21:40:19 2014 +0100
@@ -85,16 +85,16 @@
val eq_OO_meta = mk_meta_eq @{thm eq_OO}
fun print_generate_pcr_cr_eq_error ctxt term =
- let
- val goal = (Const ("HOL.eq", dummyT)) $ term $ Const ("HOL.eq", dummyT)
- val error_msg = cat_lines
- ["Generation of a pcr_cr_eq failed.",
- (Pretty.string_of (Pretty.block
- [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
- "Most probably a relator_eq rule for one of the involved types is missing."]
- in
- error error_msg
- end
+ let
+ val goal = Const (@{const_name HOL.eq}, dummyT) $ term $ Const (@{const_name HOL.eq}, dummyT)
+ val error_msg = cat_lines
+ ["Generation of a pcr_cr_eq failed.",
+ (Pretty.string_of (Pretty.block
+ [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
+ "Most probably a relator_eq rule for one of the involved types is missing."]
+ in
+ error error_msg
+ end
in
fun define_pcr_cr_eq lthy pcr_rel_def =
let
@@ -121,15 +121,15 @@
(Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy))))
in
case (term_of o Thm.rhs_of) pcr_cr_eq of
- Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ =>
+ Const (@{const_name "relcompp"}, _) $ Const (@{const_name HOL.eq}, _) $ _ =>
let
val thm =
pcr_cr_eq
|> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
|> mk_HOL_eq
|> singleton (Variable.export lthy orig_lthy)
- val ((_, [thm]), lthy) = Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []),
- [thm]) lthy
+ val ((_, [thm]), lthy) =
+ Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) lthy
in
(thm, lthy)
end
@@ -626,7 +626,7 @@
val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
(**)
val quot_thm = case typedef_set of
- Const ("Orderings.top_class.top", _) =>
+ Const (@{const_name top}, _) =>
[typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
[typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
@@ -638,7 +638,7 @@
fun qualify suffix = Binding.qualified true suffix qty_name
val opt_reflp_thm =
case typedef_set of
- Const ("Orderings.top_class.top", _) =>
+ Const (@{const_name top}, _) =>
SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
| _ => NONE
val dom_thm = get_Domainp_thm quot_thm
@@ -819,7 +819,7 @@
Pretty.brk 1,
Display.pretty_thm ctxt pcr_cr_eq]]
val (pcr_const_eq, eqs) = strip_comb eq_lhs
- fun is_eq (Const ("HOL.eq", _)) = true
+ fun is_eq (Const (@{const_name HOL.eq}, _)) = true
| is_eq _ = false
fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
| eq_Const _ _ = false
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Mar 22 20:42:16 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Mar 22 21:40:19 2014 +0100
@@ -176,8 +176,10 @@
val (Ts, fns) = split_list xs
val constr = Const (c, Ts ---> simpleT)
val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
- val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
- val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
+ val Eval_App =
+ Const (@{const_name Code_Evaluation.App}, HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
+ val Eval_Const =
+ Const (@{const_name Code_Evaluation.Const}, HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
val start_term = test_function simpleT $
--- a/src/HOL/Transitive_Closure.thy Sat Mar 22 20:42:16 2014 +0100
+++ b/src/HOL/Transitive_Closure.thy Sat Mar 22 21:40:19 2014 +0100
@@ -1239,8 +1239,8 @@
fun decomp (@{const Trueprop} $ t) =
let fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
- let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
- | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
+ let fun decr (Const (@{const_name rtrancl}, _ ) $ r) = (r,"r*")
+ | decr (Const (@{const_name trancl}, _ ) $ r) = (r,"r+")
| decr r = (r,"r");
val (rel,r) = decr (Envir.beta_eta_contract rel);
in SOME (a,b,rel,r) end
@@ -1262,8 +1262,8 @@
fun decomp (@{const Trueprop} $ t) =
let fun dec (rel $ a $ b) =
- let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*")
- | decr (Const ("Transitive_Closure.tranclp", _ ) $ r) = (r,"r+")
+ let fun decr (Const (@{const_name rtranclp}, _ ) $ r) = (r,"r*")
+ | decr (Const (@{const_name tranclp}, _ ) $ r) = (r,"r+")
| decr r = (r,"r");
val (rel,r) = decr rel;
in SOME (a, b, rel, r) end