--- a/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -45,17 +45,21 @@
val disc_corecsN: string
val dtorN: string
val dtor_coinductN: string
- val dtor_mapN: string
- val dtor_relN: string
val dtor_corecN: string
val dtor_corecsN: string
val dtor_ctorN: string
val dtor_exhaustN: string
val dtor_injectN: string
+ val dtor_mapN: string
val dtor_map_uniqueN: string
+ val dtor_relN: string
+ val dtor_rel_coinductN: string
+ val dtor_rel_strong_coinductN: string
val dtor_set_inclN: string
val dtor_set_set_inclN: string
val dtor_srelN: string
+ val dtor_srel_coinductN: string
+ val dtor_srel_strong_coinductN: string
val dtor_strong_coinductN: string
val dtor_unfoldN: string
val dtor_unfold_uniqueN: string
@@ -75,8 +79,6 @@
val nchotomyN: string
val recN: string
val recsN: string
- val rel_coinductN: string
- val rel_strong_coinductN: string
val relsN: string
val rvN: string
val sel_corecsN: string
@@ -85,8 +87,6 @@
val set_inclN: string
val set_set_inclN: string
val simpsN: string
- val srel_coinductN: string
- val srel_strong_coinductN: string
val strTN: string
val str_initN: string
val strongN: string
@@ -235,21 +235,21 @@
val ctor_exhaustN = mk_exhaustN ctorN
val dtor_injectN = mk_injectN dtorN
val dtor_exhaustN = mk_exhaustN dtorN
+val ctor_relN = ctorN ^ "_" ^ relN
+val dtor_relN = dtorN ^ "_" ^ relN
+val ctor_srelN = ctorN ^ "_" ^ srelN
+val dtor_srelN = dtorN ^ "_" ^ srelN
val inductN = "induct"
val coinductN = coN ^ inductN
val ctor_inductN = ctorN ^ "_" ^ inductN
val ctor_induct2N = ctor_inductN ^ "2"
val dtor_coinductN = dtorN ^ "_" ^ coinductN
-val rel_coinductN = relN ^ "_" ^ coinductN
-val srel_coinductN = srelN ^ "_" ^ coinductN
-val ctor_srelN = ctorN ^ "_" ^ srelN
-val dtor_srelN = dtorN ^ "_" ^ srelN
-val ctor_relN = ctorN ^ "_" ^ relN
-val dtor_relN = dtorN ^ "_" ^ relN
+val dtor_rel_coinductN = dtor_relN ^ "_" ^ coinductN
+val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN
val strongN = "strong_"
val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN
-val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN
-val srel_strong_coinductN = srelN ^ "_" ^ strongN ^ coinductN
+val dtor_rel_strong_coinductN = dtor_relN ^ "_" ^ strongN ^ coinductN
+val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strongN ^ coinductN
val hsetN = "Hset"
val hset_recN = hsetN ^ "_rec"
val set_inclN = "set_incl"
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -2178,8 +2178,8 @@
val timer = time (timer "corec definitions & thms");
- val (dtor_coinduct_thm, coinduct_params, srel_coinduct_thm, rel_coinduct_thm,
- dtor_strong_coinduct_thm, srel_strong_coinduct_thm, rel_strong_coinduct_thm) =
+ val (dtor_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_rel_coinduct_thm,
+ dtor_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, dtor_rel_strong_coinduct_thm) =
let
val zs = Jzs1 @ Jzs2;
val frees = phis @ zs;
@@ -2213,12 +2213,13 @@
val srel_prems = map5 (mk_srel_prem false) phis dtors srels Jzs Jzs_copy;
val srel_upto_prems = map5 (mk_srel_prem true) phis dtors srels Jzs Jzs_copy;
- val srel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl));
- val coinduct_params = rev (Term.add_tfrees srel_coinduct_goal []);
-
- val srel_coinduct = unfold_thms lthy @{thms diag_UNIV}
- (Skip_Proof.prove lthy [] [] srel_coinduct_goal
- (K (mk_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
+ val dtor_srel_coinduct_goal =
+ fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl));
+ val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []);
+
+ val dtor_srel_coinduct = unfold_thms lthy @{thms diag_UNIV}
+ (Skip_Proof.prove lthy [] [] dtor_srel_coinduct_goal
+ (K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
|> Thm.close_derivation);
fun mk_dtor_prem upto_eq phi dtor map_nth sets Jz Jz_copy FJz =
@@ -2256,10 +2257,10 @@
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 srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
+ val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] []
(fold_rev Logic.all zs (Logic.list_implies (srel_upto_prems, concl)))
- (K (mk_srel_strong_coinduct_tac m cTs cts srel_coinduct srel_monos srel_Ids)))
+ (K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids)))
|> Thm.close_derivation;
val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
@@ -2272,11 +2273,12 @@
val rel_of_srel_thms =
srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
- val rel_coinduct = unfold_thms lthy rel_of_srel_thms srel_coinduct;
- val rel_strong_coinduct = unfold_thms lthy rel_of_srel_thms srel_strong_coinduct;
+ val dtor_rel_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_coinduct;
+ val dtor_rel_strong_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_strong_coinduct;
in
- (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), srel_coinduct, rel_coinduct,
- dtor_strong_coinduct, srel_strong_coinduct, rel_strong_coinduct)
+ (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), dtor_srel_coinduct,
+ dtor_rel_coinduct, dtor_strong_coinduct, dtor_srel_strong_coinduct,
+ dtor_rel_strong_coinduct)
end;
val timer = time (timer "coinduction");
@@ -2957,10 +2959,10 @@
val common_notes =
[(dtor_coinductN, [dtor_coinduct_thm]),
(dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
- (rel_coinductN, [rel_coinduct_thm]),
- (rel_strong_coinductN, [rel_strong_coinduct_thm]),
- (srel_coinductN, [srel_coinduct_thm]),
- (srel_strong_coinductN, [srel_strong_coinduct_thm])]
+ (dtor_rel_coinductN, [dtor_rel_coinduct_thm]),
+ (dtor_rel_strong_coinductN, [dtor_rel_strong_coinduct_thm]),
+ (dtor_srel_coinductN, [dtor_srel_coinduct_thm]),
+ (dtor_srel_strong_coinductN, [dtor_srel_strong_coinduct_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
@@ -38,6 +38,9 @@
val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic
+ val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
+ val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
+ thm list -> thm list -> tactic
val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
thm list -> thm list -> thm list list -> tactic
val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
@@ -108,9 +111,6 @@
val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
thm list list -> thm list list -> tactic
val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic
- val mk_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
- val mk_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
- thm list -> thm list -> tactic
val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
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
@@ -1123,7 +1123,7 @@
REPEAT_DETERM_N m o rtac refl,
EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
-fun mk_srel_coinduct_tac ks raw_coind bis_srel =
+fun mk_dtor_srel_coinduct_tac ks raw_coind bis_srel =
EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI,
CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI,
@@ -1132,8 +1132,8 @@
CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
-fun mk_srel_strong_coinduct_tac m cTs cts srel_coinduct srel_monos srel_Ids =
- EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts srel_coinduct),
+fun mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
+ EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_srel_coinduct),
EVERY' (map2 (fn srel_mono => fn srel_Id =>
EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp),
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -1784,9 +1784,9 @@
val Ibnf_notes =
[(ctor_mapN, map single folded_ctor_map_thms),
(ctor_relN, map single ctor_Irel_thms),
- (ctor_srelN, map single ctor_Isrel_thms),
(ctor_set_inclN, ctor_set_incl_thmss),
- (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @
+ (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss),
+ (ctor_srelN, map single ctor_Isrel_thms)] @
map2 (fn i => fn thms => (mk_ctor_setsN i, map single thms)) ls' folded_set_simp_thmss
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>