--- a/src/HOL/BNF/Tools/bnf_comp.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Tue May 07 14:22:54 2013 +0200
@@ -40,25 +40,22 @@
type unfold_set = {
map_unfolds: thm list,
set_unfoldss: thm list list,
- rel_unfolds: thm list,
- srel_unfolds: thm list
+ rel_unfolds: thm list
};
-val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = [], srel_unfolds = []};
+val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
-fun add_to_unfolds map sets rel srel
- {map_unfolds, set_unfoldss, rel_unfolds, srel_unfolds} =
+fun add_to_unfolds map sets rel
+ {map_unfolds, set_unfoldss, rel_unfolds} =
{map_unfolds = add_to_thms map_unfolds map,
set_unfoldss = adds_to_thms set_unfoldss sets,
- rel_unfolds = add_to_thms rel_unfolds rel,
- srel_unfolds = add_to_thms srel_unfolds srel};
+ rel_unfolds = add_to_thms rel_unfolds rel};
fun add_bnf_to_unfolds bnf =
- add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf)
- (srel_def_of_bnf bnf);
+ add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf);
val bdTN = "bdT";
@@ -221,25 +218,24 @@
fun map_wpull_tac _ =
mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
- fun srel_O_Gr_tac _ =
+ fun rel_OO_Grp_tac _ =
let
- val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
- val outer_srel_Gr = srel_Gr_of_bnf outer RS sym;
- val outer_srel_cong = srel_cong_of_bnf outer;
+ val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
+ val outer_rel_cong = rel_cong_of_bnf outer;
val thm =
- (trans OF [in_alt_thm RS @{thm O_Gr_cong},
- trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
- [trans OF [outer_srel_Gr RS @{thm arg_cong[of _ _ converse]},
- srel_converse_of_bnf outer RS sym], outer_srel_Gr],
- trans OF [srel_O_of_bnf outer RS sym, outer_srel_cong OF
- (map (fn bnf => srel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
- |> unfold_thms lthy (basic_thms @ srel_def_of_bnf outer :: map srel_def_of_bnf inners);
+ (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
+ trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
+ [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
+ rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
+ trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF
+ (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym)
+ (*|> unfold_thms lthy (rel_def_of_bnf outer :: map rel_def_of_bnf inners)*);
in
- unfold_thms_tac lthy basic_thms THEN rtac thm 1
+ rtac thm 1
end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -332,24 +328,24 @@
(bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
- fun srel_O_Gr_tac _ =
+ fun rel_OO_Grp_tac _ =
let
- val srel_Gr = srel_Gr_of_bnf bnf RS sym
+ val rel_Grp = rel_Grp_of_bnf bnf RS sym
val thm =
- (trans OF [in_alt_thm RS @{thm O_Gr_cong},
- trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
- [trans OF [srel_Gr RS @{thm arg_cong[of _ _ converse]},
- srel_converse_of_bnf bnf RS sym], srel_Gr],
- trans OF [srel_O_of_bnf bnf RS sym, srel_cong_of_bnf bnf OF
- (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
- replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
- |> unfold_thms lthy (srel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
+ (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
+ trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
+ [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]},
+ rel_conversep_of_bnf bnf RS sym], rel_Grp],
+ trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
+ (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
+ replicate (live - n) @{thm Grp_fst_snd})]]] RS sym)
+ (*|> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv})*);
in
rtac thm 1
end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -432,11 +428,10 @@
fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
- fun srel_O_Gr_tac _ =
- mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
+ fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -509,11 +504,10 @@
mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
- fun srel_O_Gr_tac _ =
- mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
+ fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -598,7 +592,6 @@
val map_unfolds = #map_unfolds unfold_set;
val set_unfoldss = #set_unfoldss unfold_set;
val rel_unfolds = #rel_unfolds unfold_set;
- val srel_unfolds = #srel_unfolds unfold_set;
val expand_maps =
fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
@@ -609,8 +602,7 @@
val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
val unfold_rels = unfold_thms lthy rel_unfolds;
- val unfold_srels = unfold_thms lthy srel_unfolds;
- val unfold_all = unfold_sets o unfold_maps o unfold_rels o unfold_srels;
+ val unfold_all = unfold_sets o unfold_maps o unfold_rels;
val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
val bnf_sets = map (expand_maps o expand_sets)
(mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
@@ -656,7 +648,7 @@
(mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
(mk_tac (map_wpull_of_bnf bnf))
- (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
+ (mk_tac (unfold_thms lthy [rel_def_of_bnf bnf] (rel_OO_Grp_of_bnf bnf)));
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);