--- a/src/HOL/Tools/BNF/bnf_def.ML Sun Aug 17 22:27:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Aug 18 13:46:22 2014 +0200
@@ -73,7 +73,7 @@
val rel_cong_of_bnf: bnf -> thm
val rel_conversep_of_bnf: bnf -> thm
val rel_mono_of_bnf: bnf -> thm
- val rel_mono_strong_of_bnf: bnf -> thm
+ val rel_mono_strong0_of_bnf: bnf -> thm
val rel_eq_of_bnf: bnf -> thm
val rel_flip_of_bnf: bnf -> thm
val set_bd_of_bnf: bnf -> thm list
@@ -234,7 +234,7 @@
rel_cong: thm lazy,
rel_map: thm list lazy,
rel_mono: thm lazy,
- rel_mono_strong: thm lazy,
+ rel_mono_strong0: thm lazy,
rel_Grp: thm lazy,
rel_conversep: thm lazy,
rel_OO: thm lazy
@@ -242,7 +242,7 @@
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
- rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
+ rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
@@ -264,7 +264,7 @@
rel_cong = rel_cong,
rel_map = rel_map,
rel_mono = rel_mono,
- rel_mono_strong = rel_mono_strong,
+ rel_mono_strong0 = rel_mono_strong0,
rel_Grp = rel_Grp,
rel_conversep = rel_conversep,
rel_OO = rel_OO};
@@ -291,7 +291,7 @@
rel_cong,
rel_map,
rel_mono,
- rel_mono_strong,
+ rel_mono_strong0,
rel_Grp,
rel_conversep,
rel_OO} =
@@ -316,7 +316,7 @@
rel_cong = Lazy.map f rel_cong,
rel_map = Lazy.map (map f) rel_map,
rel_mono = Lazy.map f rel_mono,
- rel_mono_strong = Lazy.map f rel_mono_strong,
+ rel_mono_strong0 = Lazy.map f rel_mono_strong0,
rel_Grp = Lazy.map f rel_Grp,
rel_conversep = Lazy.map f rel_conversep,
rel_OO = Lazy.map f rel_OO};
@@ -445,7 +445,7 @@
val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
-val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
+val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
@@ -615,7 +615,7 @@
val rel_conversepN = "rel_conversep";
val rel_mapN = "rel_map"
val rel_monoN = "rel_mono"
-val rel_mono_strongN = "rel_mono_strong"
+val rel_mono_strong0N = "rel_mono_strong0"
val rel_comppN = "rel_compp";
val rel_compp_GrpN = "rel_compp_Grp";
@@ -655,7 +655,7 @@
(inj_mapN, [Lazy.force (#inj_map facts)]),
(map_comp0N, [#map_comp0 axioms]),
(map_transferN, [Lazy.force (#map_transfer facts)]),
- (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
+ (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
(set_map0N, #set_map0 axioms),
(set_bdN, #set_bd axioms)] @
(witNs ~~ wit_thmss_of_bnf bnf)
@@ -1299,7 +1299,7 @@
val rel_flip = Lazy.lazy mk_rel_flip;
- fun mk_rel_mono_strong () =
+ fun mk_rel_mono_strong0 () =
let
fun mk_prem setA setB R S a b =
HOLogic.mk_Trueprop
@@ -1312,12 +1312,12 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
- (fn {context = ctxt, prems = _} => mk_rel_mono_strong_tac ctxt (Lazy.force in_rel)
+ (fn {context = ctxt, prems = _} => mk_rel_mono_strong0_tac ctxt (Lazy.force in_rel)
(map Lazy.force set_map))
|> Thm.close_derivation
end;
- val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
+ val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
fun mk_rel_map () =
let
@@ -1368,7 +1368,7 @@
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
- rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
+ rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO;
val wits = map2 mk_witness bnf_wits wit_thms;
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Sun Aug 17 22:27:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Aug 18 13:46:22 2014 +0200
@@ -25,7 +25,7 @@
val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
val mk_rel_mono_tac: thm list -> thm -> tactic
- val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic
+ val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
@@ -211,7 +211,7 @@
in_tac @{thm sndOp_in}] 1
end;
-fun mk_rel_mono_strong_tac ctxt in_rel set_maps =
+fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
if null set_maps then atac 1
else
unfold_tac ctxt [in_rel] THEN
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Sun Aug 17 22:27:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Aug 18 13:46:22 2014 +0200
@@ -167,7 +167,7 @@
val map_id0s = map map_id0_of_bnf bnfs;
val map_ids = map map_id_of_bnf bnfs;
val set_mapss = map set_map_of_bnf bnfs;
- val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs;
+ val rel_mono_strong0s = map rel_mono_strong0_of_bnf bnfs;
val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
val timer = time (timer "Extracted terms & thms");
@@ -1691,7 +1691,7 @@
in
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
- ctor_Irel_thms rel_mono_strongs le_rel_OOs)
+ ctor_Irel_thms rel_mono_strong0s le_rel_OOs)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy)
end;
@@ -1762,7 +1762,7 @@
val Irel_induct_thm =
mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
(fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
- ctor_Irel_thms rel_mono_strongs) lthy;
+ ctor_Irel_thms rel_mono_strong0s) lthy;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
val ctor_fold_transfer_thms =
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sun Aug 17 22:27:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Aug 18 13:46:22 2014 +0200
@@ -582,7 +582,7 @@
(induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
end;
-fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs =
+fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs =
EVERY' (rtac induct ::
map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
@@ -592,7 +592,7 @@
REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac],
REPEAT_DETERM_N (length le_rel_OOs) o
EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]])
- ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs) 1;
+ ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
(* BNF tactics *)
@@ -701,19 +701,19 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
-fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strongs =
+fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
let val n = length ks;
in
unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
- EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
+ EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
- etac rel_mono_strong,
+ etac rel_mono_strong0,
REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
EVERY' (map (fn j =>
EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]},
Goal.assume_rule_tac ctxt]) ks)])
- IHs ctor_rels rel_mono_strongs)] 1
+ IHs ctor_rels rel_mono_strong0s)] 1
end;
fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds =