--- a/src/HOL/BNF/Tools/bnf_fp.ML Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Fri Sep 21 18:25:17 2012 +0200
@@ -39,15 +39,16 @@
val disc_corecsN: string
val dtorN: string
val dtor_coinductN: string
- val dtor_unfoldN: string
- val dtor_unfold_uniqueN: string
- val dtor_unfoldsN: string
+ val dtor_relN: string
val dtor_corecN: string
val dtor_corecsN: string
val dtor_exhaustN: string
val dtor_ctorN: string
val dtor_injectN: string
val dtor_strong_coinductN: string
+ val dtor_unfoldN: string
+ val dtor_unfold_uniqueN: string
+ val dtor_unfoldsN: string
val exhaustN: string
val foldN: string
val foldsN: string
@@ -65,7 +66,6 @@
val recN: string
val recsN: string
val rel_coinductN: string
- val rel_simpN: string
val rel_strong_coinductN: string
val rvN: string
val sel_unfoldsN: string
@@ -74,7 +74,7 @@
val set_set_inclN: string
val simpsN: string
val srel_coinductN: string
- val srel_simpN: string
+ val dtor_srelN: string
val srel_strong_coinductN: string
val strTN: string
val str_initN: string
@@ -225,8 +225,8 @@
val rel_coinductN = relN ^ "_" ^ coinductN
val srel_coinductN = srelN ^ "_" ^ coinductN
val simpN = "_simp";
-val srel_simpN = srelN ^ simpN;
-val rel_simpN = relN ^ simpN;
+val dtor_srelN = dtorN ^ "_" ^ srelN
+val dtor_relN = dtorN ^ "_" ^ relN
val strongN = "strong_"
val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN
val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Sep 21 18:25:17 2012 +0200
@@ -2899,7 +2899,7 @@
val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
- val Jsrel_simp_thms =
+ val dtor_Jsrel_thms =
let
fun mk_goal Jz Jz' dtor dtor' JsrelR srelR = fold_rev Logic.all (Jz :: Jz' :: JRs)
(mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JsrelR),
@@ -2910,24 +2910,24 @@
fn map_simp => fn set_simps => fn dtor_inject => fn dtor_ctor =>
fn set_naturals => fn set_incls => fn set_set_inclss =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps
+ (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps
dtor_inject dtor_ctor set_naturals set_incls set_set_inclss))
|> Thm.close_derivation)
ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
end;
- val Jrel_simp_thms =
+ val dtor_Jrel_thms =
let
fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
(mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz')));
val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
in
- map3 (fn goal => fn srel_def => fn Jsrel_simp =>
+ map3 (fn goal => fn srel_def => fn dtor_Jsrel =>
Skip_Proof.prove lthy [] [] goal
- (mk_rel_simp_tac srel_def Jrel_defs Jsrel_defs Jsrel_simp)
+ (mk_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel)
|> Thm.close_derivation)
- goals srel_defs Jsrel_simp_thms
+ goals srel_defs dtor_Jsrel_thms
end;
val timer = time (timer "additional properties");
@@ -2941,11 +2941,11 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val Jbnf_notes =
- [(map_simpsN, map single folded_map_simp_thms),
- (rel_simpN, map single Jrel_simp_thms),
+ [(dtor_relN, map single dtor_Jrel_thms),
+ (dtor_srelN, map single dtor_Jsrel_thms),
+ (map_simpsN, map single folded_map_simp_thms),
(set_inclN, set_incl_thmss),
- (set_set_inclN, map flat set_set_incl_thmsss),
- (srel_simpN, map single Jsrel_simp_thms)] @
+ (set_set_inclN, map flat set_set_incl_thmsss)] @
map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Fri Sep 21 18:25:17 2012 +0200
@@ -38,6 +38,8 @@
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_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 ->
thm -> thm -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
@@ -109,8 +111,6 @@
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_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
- thm list -> thm list -> thm list 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
@@ -1494,7 +1494,7 @@
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
-fun mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
+fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
set_naturals set_incls set_set_inclss =
let
val m = length set_incls;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Sep 21 18:25:17 2012 +0200
@@ -1742,7 +1742,7 @@
val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
- val Isrel_simp_thms =
+ val dtor_Isrel_thms =
let
fun mk_goal xF yF ctor ctor' IsrelR srelR = fold_rev Logic.all (xF :: yF :: IRs)
(mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IsrelR),
@@ -1753,24 +1753,24 @@
fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor =>
fn set_naturals => fn set_incls => fn set_set_inclss =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_srel_simp_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps
+ (K (mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps
ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
|> Thm.close_derivation)
ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
end;
- val Irel_simp_thms =
+ val dtor_Irel_thms =
let
fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
(mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF));
val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
in
- map3 (fn goal => fn srel_def => fn Isrel_simp =>
+ map3 (fn goal => fn srel_def => fn dtor_Isrel =>
Skip_Proof.prove lthy [] [] goal
- (mk_rel_simp_tac srel_def Irel_defs Isrel_defs Isrel_simp)
+ (mk_dtor_rel_tac srel_def Irel_defs Isrel_defs dtor_Isrel)
|> Thm.close_derivation)
- goals srel_defs Isrel_simp_thms
+ goals srel_defs dtor_Isrel_thms
end;
val timer = time (timer "additional properties");
@@ -1783,11 +1783,11 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val Ibnf_notes =
- [(map_simpsN, map single folded_map_simp_thms),
- (rel_simpN, map single Irel_simp_thms),
+ [(dtor_relN, map single dtor_Irel_thms),
+ (dtor_srelN, map single dtor_Isrel_thms),
+ (map_simpsN, map single folded_map_simp_thms),
(set_inclN, set_incl_thmss),
- (set_set_inclN, map flat set_set_incl_thmsss),
- (srel_simpN, map single Isrel_simp_thms)] @
+ (set_set_inclN, map flat set_set_incl_thmsss)] @
map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Sep 21 18:25:17 2012 +0200
@@ -23,6 +23,8 @@
val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> 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_ex_copy_alg_tac: int -> thm -> thm -> tactic
val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm ->
@@ -69,8 +71,6 @@
val mk_set_natural_tac: thm -> tactic
val mk_set_simp_tac: thm -> thm -> thm list -> tactic
val mk_set_tac: thm -> tactic
- val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm ->
- thm -> thm list -> thm list -> thm list list -> tactic
val mk_wit_tac: int -> thm list -> thm list -> tactic
val mk_wpull_tac: thm -> tactic
end;
@@ -770,7 +770,7 @@
EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_srel_simp_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
+fun mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
ctor_dtor set_naturals set_incls set_set_inclss =
let
val m = length set_incls;
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Fri Sep 21 18:25:17 2012 +0200
@@ -27,7 +27,7 @@
val mk_Abs_inj_thm: thm -> thm
val simple_srel_O_Gr_tac: Proof.context -> tactic
- val mk_rel_simp_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
+ val mk_dtor_rel_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
tactic
val mk_map_comp_id_tac: thm -> tactic
@@ -101,10 +101,10 @@
fun simple_srel_O_Gr_tac ctxt =
unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
-fun mk_rel_simp_tac srel_def IJrel_defs IJsrel_defs srel_simp {context = ctxt, prems = _} =
+fun mk_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
unfold_thms_tac ctxt IJrel_defs THEN
subst_tac ctxt [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
- @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) srel_simp] 1 THEN
+ @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel] 1 THEN
unfold_thms_tac ctxt (srel_def ::
@{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
split_conv}) THEN