--- a/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -54,13 +54,13 @@
val morN: string
val nchotomyN: string
val pred_coinductN: string
- val pred_coinduct_uptoN: string
val pred_simpN: string
+ val pred_strong_coinductN: string
val recN: string
val recsN: string
val rel_coinductN: string
- val rel_coinduct_uptoN: string
val rel_simpN: string
+ val rel_strong_coinductN: string
val rvN: string
val sel_coitersN: string
val sel_corecsN: string
@@ -69,11 +69,11 @@
val simpsN: string
val strTN: string
val str_initN: string
+ val strongN: string
val sum_bdN: string
val sum_bdTN: string
val unfN: string
val unf_coinductN: string
- val unf_coinduct_uptoN: string
val unf_coiterN: string
val unf_coiter_uniqueN: string
val unf_coitersN: string
@@ -82,8 +82,8 @@
val unf_exhaustN: string
val unf_fldN: string
val unf_injectN: string
+ val unf_strong_coinductN: string
val uniqueN: string
- val uptoN: string
val mk_exhaustN: string -> string
val mk_injectN: string -> string
@@ -226,10 +226,10 @@
val simpN = "_simp";
val rel_simpN = relN ^ simpN;
val pred_simpN = predN ^ simpN;
-val uptoN = "upto"
-val unf_coinduct_uptoN = unf_coinductN ^ "_" ^ uptoN
-val rel_coinduct_uptoN = rel_coinductN ^ "_" ^ uptoN
-val pred_coinduct_uptoN = pred_coinductN ^ "_" ^ uptoN
+val strongN = "strong_"
+val unf_strong_coinductN = unfN ^ "_" ^ strongN ^ coinductN
+val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN
+val pred_strong_coinductN = predN ^ "_" ^ strongN ^ coinductN
val hsetN = "Hset"
val hset_recN = hsetN ^ "_rec"
val set_inclN = "set_incl"
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -2176,7 +2176,7 @@
val timer = time (timer "corec definitions & thms");
val (unf_coinduct_thm, coinduct_params, rel_coinduct_thm, pred_coinduct_thm,
- unf_coinduct_upto_thm, rel_coinduct_upto_thm, pred_coinduct_upto_thm) =
+ unf_strong_coinduct_thm, rel_strong_coinduct_thm, pred_strong_coinduct_thm) =
let
val zs = Jzs1 @ Jzs2;
val frees = phis @ zs;
@@ -2253,16 +2253,16 @@
val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
- val rel_coinduct_upto = singleton (Proof_Context.export names_lthy lthy)
+ val rel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] []
(fold_rev Logic.all zs (Logic.list_implies (rel_upto_prems, concl)))
- (K (mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids)))
+ (K (mk_rel_strong_coinduct_tac m cTs cts rel_coinduct rel_monos rel_Ids)))
|> Thm.close_derivation;
- val unf_coinduct_upto = singleton (Proof_Context.export names_lthy lthy)
+ val unf_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] []
(fold_rev Logic.all zs (Logic.list_implies (unf_upto_prems, concl)))
- (K (mk_unf_coinduct_upto_tac ks cTs cts unf_coinduct bis_def
+ (K (mk_unf_strong_coinduct_tac ks cTs cts unf_coinduct bis_def
(tcoalg_thm RS bis_diag_thm))))
|> Thm.close_derivation;
@@ -2270,10 +2270,10 @@
rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct;
- val pred_coinduct_upto = unfold_defs lthy pred_of_rel_thms rel_coinduct_upto;
+ val pred_strong_coinduct = unfold_defs lthy pred_of_rel_thms rel_strong_coinduct;
in
(unf_coinduct, rev (Term.add_tfrees unf_coinduct_goal []), rel_coinduct, pred_coinduct,
- unf_coinduct_upto, rel_coinduct_upto, pred_coinduct_upto)
+ unf_strong_coinduct, rel_strong_coinduct, pred_strong_coinduct)
end;
val timer = time (timer "coinduction");
@@ -2955,9 +2955,9 @@
[(unf_coinductN, [unf_coinduct_thm]),
(rel_coinductN, [rel_coinduct_thm]),
(pred_coinductN, [pred_coinduct_thm]),
- (unf_coinduct_uptoN, [unf_coinduct_upto_thm]),
- (rel_coinduct_uptoN, [rel_coinduct_upto_thm]),
- (pred_coinduct_uptoN, [pred_coinduct_upto_thm])]
+ (unf_strong_coinductN, [unf_strong_coinduct_thm]),
+ (rel_strong_coinductN, [rel_strong_coinduct_thm]),
+ (pred_strong_coinductN, [pred_strong_coinduct_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -88,7 +88,7 @@
val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
thm list -> thm list -> thm -> thm list -> tactic
val mk_rel_coinduct_tac: 'a list -> thm -> thm -> tactic
- val mk_rel_coinduct_upto_tac: int -> ctyp option list -> cterm option list -> thm -> thm list ->
+ val mk_rel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm -> thm list ->
thm list -> tactic
val mk_rel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
thm list -> thm list -> thm list list -> tactic
@@ -111,7 +111,7 @@
cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
thm list list -> thm list list -> thm -> thm list list -> tactic
val mk_unf_coinduct_tac: int -> int list -> thm -> thm -> tactic
- val mk_unf_coinduct_upto_tac: int list -> ctyp option list -> cterm option list -> thm -> thm ->
+ val mk_unf_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> thm ->
thm -> tactic
val mk_unf_o_fld_tac: thm -> thm -> thm -> thm -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
@@ -1132,7 +1132,7 @@
CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
-fun mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids =
+fun mk_rel_strong_coinduct_tac m cTs cts rel_coinduct rel_monos rel_Ids =
EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts rel_coinduct),
EVERY' (map2 (fn rel_mono => fn rel_Id =>
EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
@@ -1165,7 +1165,7 @@
rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
end;
-fun mk_unf_coinduct_upto_tac ks cTs cts unf_coinduct bis_def bis_diag =
+fun mk_unf_strong_coinduct_tac ks cTs cts unf_coinduct bis_def bis_diag =
EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts unf_coinduct),
EVERY' (map (fn i =>
EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp},