--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -13,7 +13,7 @@
val map_unfolds_of: unfold_set -> thm list
val set_unfoldss_of: unfold_set -> thm list list
val pred_unfolds_of: unfold_set -> thm list
- val rel_unfolds_of: unfold_set -> thm list
+ val srel_unfolds_of: unfold_set -> thm list
val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
@@ -38,29 +38,29 @@
map_unfolds: thm list,
set_unfoldss: thm list list,
pred_unfolds: thm list,
- rel_unfolds: thm list
+ srel_unfolds: thm list
};
-val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []};
+val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], srel_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 pred rel
- {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} =
+fun add_to_unfolds map sets pred srel
+ {map_unfolds, set_unfoldss, pred_unfolds, srel_unfolds} =
{map_unfolds = add_to_thms map_unfolds map,
set_unfoldss = adds_to_thms set_unfoldss sets,
pred_unfolds = add_to_thms pred_unfolds pred,
- rel_unfolds = add_to_thms rel_unfolds rel};
+ srel_unfolds = add_to_thms srel_unfolds srel};
fun add_bnf_to_unfolds bnf =
add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (pred_def_of_bnf bnf)
- (rel_def_of_bnf bnf);
+ (srel_def_of_bnf bnf);
val map_unfolds_of = #map_unfolds;
val set_unfoldss_of = #set_unfoldss;
val pred_unfolds_of = #pred_unfolds;
-val rel_unfolds_of = #rel_unfolds;
+val srel_unfolds_of = #srel_unfolds;
val bdTN = "bdT";
@@ -230,25 +230,25 @@
fun map_wpull_tac _ =
mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
- fun rel_O_Gr_tac _ =
+ fun srel_O_Gr_tac _ =
let
val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
- val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
- val outer_rel_cong = rel_cong_of_bnf outer;
+ val outer_srel_Gr = srel_Gr_of_bnf outer RS sym;
+ val outer_srel_cong = srel_cong_of_bnf outer;
val thm =
(trans OF [in_alt_thm RS @{thm subst_rel_def},
trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
- [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
- rel_converse_of_bnf outer RS sym], outer_rel_Gr],
- trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
- (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
- |> unfold_thms lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
+ [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);
in
unfold_thms_tac lthy basic_thms THEN rtac thm 1
end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -341,24 +341,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 rel_O_Gr_tac _ =
+ fun srel_O_Gr_tac _ =
let
- val rel_Gr = rel_Gr_of_bnf bnf RS sym
+ val srel_Gr = srel_Gr_of_bnf bnf RS sym
val thm =
(trans OF [in_alt_thm RS @{thm subst_rel_def},
trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
- [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]},
- rel_converse_of_bnf bnf RS sym], rel_Gr],
- trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf 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 (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
+ |> unfold_thms lthy (srel_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_cong_tac set_natural_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -441,11 +441,11 @@
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 rel_O_Gr_tac _ =
- mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
+ 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;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -518,11 +518,11 @@
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 rel_O_Gr_tac _ =
- mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
+ 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;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -607,7 +607,7 @@
val map_unfolds = map_unfolds_of unfold_set;
val set_unfoldss = set_unfoldss_of unfold_set;
val pred_unfolds = pred_unfolds_of unfold_set;
- val rel_unfolds = rel_unfolds_of unfold_set;
+ val srel_unfolds = srel_unfolds_of unfold_set;
val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
map_unfolds);
@@ -618,8 +618,8 @@
val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
val unfold_preds = unfold_thms lthy pred_unfolds;
- val unfold_rels = unfold_thms lthy rel_unfolds;
- val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels;
+ val unfold_srels = unfold_thms lthy srel_unfolds;
+ val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_srels;
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);
@@ -665,7 +665,7 @@
(mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_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 [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
+ (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -35,7 +35,7 @@
val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic
val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
- val mk_simple_rel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic
+ val mk_simple_srel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic
val mk_simple_wit_tac: thm list -> tactic
end;
@@ -407,9 +407,9 @@
WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
-fun mk_simple_rel_O_Gr_tac ctxt rel_def rel_O_Gr in_alt_thm =
- rtac (unfold_thms ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
- 1;
+fun mk_simple_srel_O_Gr_tac ctxt srel_def srel_O_Gr in_alt_thm =
+ rtac (unfold_thms ctxt [srel_def]
+ (trans OF [srel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym])) 1;
fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 15:53:29 2012 +0200
@@ -25,8 +25,8 @@
val mapN: string
val setN: string
val predN: string
- val relN: string
val mk_setN: int -> string
+ val srelN: string
val map_of_bnf: BNF -> term
@@ -34,8 +34,8 @@
val mk_bd_of_bnf: typ list -> typ list -> BNF -> term
val mk_map_of_bnf: typ list -> typ list -> typ list -> BNF -> term
val mk_pred_of_bnf: typ list -> typ list -> typ list -> BNF -> term
- val mk_rel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
val mk_sets_of_bnf: typ list list -> typ list list -> BNF -> term list
+ val mk_srel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
val mk_wits_of_bnf: typ list list -> typ list list -> BNF -> (int list * term) list
val bd_Card_order_of_bnf: BNF -> thm
@@ -47,7 +47,7 @@
val in_bd_of_bnf: BNF -> thm
val in_cong_of_bnf: BNF -> thm
val in_mono_of_bnf: BNF -> thm
- val in_rel_of_bnf: BNF -> thm
+ val in_srel_of_bnf: BNF -> thm
val map_comp'_of_bnf: BNF -> thm
val map_comp_of_bnf: BNF -> thm
val map_cong_of_bnf: BNF -> thm
@@ -57,19 +57,19 @@
val map_wppull_of_bnf: BNF -> thm
val map_wpull_of_bnf: BNF -> thm
val pred_def_of_bnf: BNF -> thm
- val rel_def_of_bnf: BNF -> thm
- val rel_Gr_of_bnf: BNF -> thm
- val rel_Id_of_bnf: BNF -> thm
- val rel_O_of_bnf: BNF -> thm
- val rel_O_Gr_of_bnf: BNF -> thm
- val rel_cong_of_bnf: BNF -> thm
- val rel_converse_of_bnf: BNF -> thm
- val rel_mono_of_bnf: BNF -> thm
val set_bd_of_bnf: BNF -> thm list
val set_defs_of_bnf: BNF -> thm list
val set_natural'_of_bnf: BNF -> thm list
val set_natural_of_bnf: BNF -> thm list
val sets_of_bnf: BNF -> term list
+ val srel_def_of_bnf: BNF -> thm
+ val srel_Gr_of_bnf: BNF -> thm
+ val srel_Id_of_bnf: BNF -> thm
+ val srel_O_of_bnf: BNF -> thm
+ val srel_O_Gr_of_bnf: BNF -> thm
+ val srel_cong_of_bnf: BNF -> thm
+ val srel_converse_of_bnf: BNF -> thm
+ val srel_mono_of_bnf: BNF -> thm
val wit_thms_of_bnf: BNF -> thm list
val wit_thmss_of_bnf: BNF -> thm list list
@@ -110,12 +110,12 @@
set_bd: thm list,
in_bd: thm,
map_wpull: thm,
- rel_O_Gr: thm
+ srel_O_Gr: thm
};
-fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), rel) =
+fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), srel) =
{map_id = id, map_comp = comp, map_cong = cong, set_natural = nat, bd_card_order = c_o,
- bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_O_Gr = rel};
+ bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, srel_O_Gr = srel};
fun dest_cons [] = raise Empty
| dest_cons (x :: xs) = (x, xs);
@@ -134,16 +134,16 @@
||> the_single
|> mk_axioms';
-fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
- [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
+fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull srel =
+ [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, srel];
fun dest_axioms {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
- in_bd, map_wpull, rel_O_Gr} =
+ in_bd, map_wpull, srel_O_Gr} =
zip_axioms map_id map_comp map_cong set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
- rel_O_Gr;
+ srel_O_Gr;
fun map_axioms f {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
- in_bd, map_wpull, rel_O_Gr} =
+ in_bd, map_wpull, srel_O_Gr} =
{map_id = f map_id,
map_comp = f map_comp,
map_cong = f map_cong,
@@ -153,7 +153,7 @@
set_bd = map f set_bd,
in_bd = f in_bd,
map_wpull = f map_wpull,
- rel_O_Gr = f rel_O_Gr};
+ srel_O_Gr = f srel_O_Gr};
val morph_axioms = map_axioms o Morphism.thm;
@@ -161,13 +161,13 @@
map_def: thm,
set_defs: thm list,
pred_def: thm,
- rel_def: thm
+ srel_def: thm
}
-fun mk_defs map sets pred rel = {map_def = map, set_defs = sets, pred_def = pred, rel_def = rel};
+fun mk_defs map sets pred srel = {map_def = map, set_defs = sets, pred_def = pred, srel_def = srel};
-fun map_defs f {map_def, set_defs, pred_def, rel_def} =
- {map_def = f map_def, set_defs = map f set_defs, pred_def = f pred_def, rel_def = f rel_def};
+fun map_defs f {map_def, set_defs, pred_def, srel_def} =
+ {map_def = f map_def, set_defs = map f set_defs, pred_def = f pred_def, srel_def = f srel_def};
val morph_defs = map_defs o Morphism.thm;
@@ -178,39 +178,39 @@
collect_set_natural: thm lazy,
in_cong: thm lazy,
in_mono: thm lazy,
- in_rel: thm lazy,
+ in_srel: thm lazy,
map_comp': thm lazy,
map_id': thm lazy,
map_wppull: thm lazy,
- rel_cong: thm lazy,
- rel_mono: thm lazy,
- rel_Id: thm lazy,
- rel_Gr: thm lazy,
- rel_converse: thm lazy,
- rel_O: thm lazy,
- set_natural': thm lazy list
+ set_natural': thm lazy list,
+ srel_cong: thm lazy,
+ srel_mono: thm lazy,
+ srel_Id: thm lazy,
+ srel_Gr: thm lazy,
+ srel_converse: thm lazy,
+ srel_O: thm lazy
};
-fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero
- collect_set_natural in_cong in_mono in_rel map_comp' map_id' map_wppull
- rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O set_natural' = {
+fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel
+ map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id srel_Gr srel_converse
+ srel_O = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
collect_set_natural = collect_set_natural,
in_cong = in_cong,
in_mono = in_mono,
- in_rel = in_rel,
+ in_srel = in_srel,
map_comp' = map_comp',
map_id' = map_id',
map_wppull = map_wppull,
- rel_cong = rel_cong,
- rel_mono = rel_mono,
- rel_Id = rel_Id,
- rel_Gr = rel_Gr,
- rel_converse = rel_converse,
- rel_O = rel_O,
- set_natural' = set_natural'};
+ set_natural' = set_natural',
+ srel_cong = srel_cong,
+ srel_mono = srel_mono,
+ srel_Id = srel_Id,
+ srel_Gr = srel_Gr,
+ srel_converse = srel_converse,
+ srel_O = srel_O};
fun map_facts f {
bd_Card_order,
@@ -219,34 +219,34 @@
collect_set_natural,
in_cong,
in_mono,
- in_rel,
+ in_srel,
map_comp',
map_id',
map_wppull,
- rel_cong,
- rel_mono,
- rel_Id,
- rel_Gr,
- rel_converse,
- rel_O,
- set_natural'} =
+ set_natural',
+ srel_cong,
+ srel_mono,
+ srel_Id,
+ srel_Gr,
+ srel_converse,
+ srel_O} =
{bd_Card_order = f bd_Card_order,
bd_Cinfinite = f bd_Cinfinite,
bd_Cnotzero = f bd_Cnotzero,
collect_set_natural = Lazy.map f collect_set_natural,
in_cong = Lazy.map f in_cong,
in_mono = Lazy.map f in_mono,
- in_rel = Lazy.map f in_rel,
+ in_srel = Lazy.map f in_srel,
map_comp' = Lazy.map f map_comp',
map_id' = Lazy.map f map_id',
map_wppull = Lazy.map f map_wppull,
- rel_cong = Lazy.map f rel_cong,
- rel_mono = Lazy.map f rel_mono,
- rel_Id = Lazy.map f rel_Id,
- rel_Gr = Lazy.map f rel_Gr,
- rel_converse = Lazy.map f rel_converse,
- rel_O = Lazy.map f rel_O,
- set_natural' = map (Lazy.map f) set_natural'};
+ set_natural' = map (Lazy.map f) set_natural',
+ srel_cong = Lazy.map f srel_cong,
+ srel_mono = Lazy.map f srel_mono,
+ srel_Id = Lazy.map f srel_Id,
+ srel_Gr = Lazy.map f srel_Gr,
+ srel_converse = Lazy.map f srel_converse,
+ srel_O = Lazy.map f srel_O};
val morph_facts = map_facts o Morphism.thm;
@@ -277,7 +277,7 @@
nwits: int,
wits: nonemptiness_witness list,
pred: term,
- rel: term
+ srel: term
};
(* getters *)
@@ -331,12 +331,12 @@
Term.subst_atomic_types
((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#pred bnf_rep)
end;
-val rel_of_bnf = #rel o rep_bnf;
-fun mk_rel_of_bnf Ds Ts Us bnf =
+val srel_of_bnf = #srel o rep_bnf;
+fun mk_srel_of_bnf Ds Ts Us bnf =
let val bnf_rep = rep_bnf bnf;
in
Term.subst_atomic_types
- ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#rel bnf_rep)
+ ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#srel bnf_rep)
end;
(*thms*)
@@ -349,7 +349,7 @@
val in_bd_of_bnf = #in_bd o #axioms o rep_bnf;
val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
-val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
+val in_srel_of_bnf = Lazy.force o #in_srel o #facts o rep_bnf;
val map_def_of_bnf = #map_def o #defs o rep_bnf;
val map_id_of_bnf = #map_id o #axioms o rep_bnf;
val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
@@ -359,32 +359,32 @@
val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
val pred_def_of_bnf = #pred_def o #defs 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_def_of_bnf = #rel_def o #defs o rep_bnf;
-val rel_Id_of_bnf = Lazy.force o #rel_Id o #facts o rep_bnf;
-val rel_Gr_of_bnf = Lazy.force o #rel_Gr o #facts o rep_bnf;
-val rel_converse_of_bnf = Lazy.force o #rel_converse o #facts o rep_bnf;
-val rel_O_of_bnf = Lazy.force o #rel_O o #facts o rep_bnf;
-val rel_O_Gr_of_bnf = #rel_O_Gr o #axioms o rep_bnf;
val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
val set_natural_of_bnf = #set_natural o #axioms o rep_bnf;
val set_natural'_of_bnf = map Lazy.force o #set_natural' o #facts o rep_bnf;
+val srel_cong_of_bnf = Lazy.force o #srel_cong o #facts o rep_bnf;
+val srel_mono_of_bnf = Lazy.force o #srel_mono o #facts o rep_bnf;
+val srel_def_of_bnf = #srel_def o #defs o rep_bnf;
+val srel_Id_of_bnf = Lazy.force o #srel_Id o #facts o rep_bnf;
+val srel_Gr_of_bnf = Lazy.force o #srel_Gr o #facts o rep_bnf;
+val srel_converse_of_bnf = Lazy.force o #srel_converse o #facts o rep_bnf;
+val srel_O_of_bnf = Lazy.force o #srel_O o #facts o rep_bnf;
+val srel_O_Gr_of_bnf = #srel_O_Gr o #axioms o rep_bnf;
val wit_thms_of_bnf = maps #prop o wits_of_bnf;
val wit_thmss_of_bnf = map #prop o wits_of_bnf;
-fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits pred rel =
+fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits pred srel =
BNF {name = name, T = T,
live = live, lives = lives, lives' = lives', dead = dead, deads = deads,
map = map, sets = sets, bd = bd,
axioms = axioms, defs = defs, facts = facts,
- nwits = length wits, wits = wits, pred = pred, rel = rel};
+ nwits = length wits, wits = wits, pred = pred, srel = srel};
fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
dead = dead, deads = deads, map = map, sets = sets, bd = bd,
axioms = axioms, defs = defs, facts = facts,
- nwits = nwits, wits = wits, pred = pred, rel = rel}) =
+ nwits = nwits, wits = wits, pred = pred, srel = srel}) =
BNF {name = Morphism.binding phi name, T = Morphism.typ phi T,
live = live, lives = List.map (Morphism.typ phi) lives,
lives' = List.map (Morphism.typ phi) lives',
@@ -396,7 +396,7 @@
facts = morph_facts phi facts,
nwits = nwits,
wits = List.map (morph_witness phi) wits,
- pred = Morphism.term phi pred, rel = Morphism.term phi rel};
+ pred = Morphism.term phi pred, srel = Morphism.term phi srel};
fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...},
BNF {T = T2, live = live2, dead = dead2, ...}) =
@@ -432,13 +432,13 @@
in Envir.subst_term (tyenv, Vartab.empty) pred end
handle Type.TYPE_MATCH => error "Bad predicator";
-fun normalize_rel ctxt instTs instA instB rel =
+fun normalize_srel ctxt instTs instA instB srel =
let
val thy = Proof_Context.theory_of ctxt;
val tyenv =
- Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_relT (instA, instB)))
+ Sign.typ_match thy (fastype_of srel, Library.foldr (op -->) (instTs, mk_relT (instA, instB)))
Vartab.empty;
- in Envir.subst_term (tyenv, Vartab.empty) rel end
+ in Envir.subst_term (tyenv, Vartab.empty) srel end
handle Type.TYPE_MATCH => error "Bad relator";
fun normalize_wit insts CA As wit =
@@ -473,7 +473,7 @@
val witN = "wit";
fun mk_witN i = witN ^ nonzero_string_of_int i;
val predN = "pred";
-val relN = "rel";
+val srelN = "srel";
val bd_card_orderN = "bd_card_order";
val bd_cinfiniteN = "bd_cinfinite";
@@ -483,19 +483,19 @@
val collect_set_naturalN = "collect_set_natural";
val in_bdN = "in_bd";
val in_monoN = "in_mono";
-val in_relN = "in_rel";
+val in_srelN = "in_srel";
val map_idN = "map_id";
val map_id'N = "map_id'";
val map_compN = "map_comp";
val map_comp'N = "map_comp'";
val map_congN = "map_cong";
val map_wpullN = "map_wpull";
-val rel_IdN = "rel_Id";
-val rel_GrN = "rel_Gr";
-val rel_converseN = "rel_converse";
-val rel_monoN = "rel_mono"
-val rel_ON = "rel_comp";
-val rel_O_GrN = "rel_comp_Gr";
+val srel_IdN = "srel_Id";
+val srel_GrN = "srel_Gr";
+val srel_converseN = "srel_converse";
+val srel_monoN = "srel_mono"
+val srel_ON = "srel_comp";
+val srel_O_GrN = "srel_comp_Gr";
val set_naturalN = "set_natural";
val set_natural'N = "set_natural'";
val set_bdN = "set_bd";
@@ -736,28 +736,28 @@
val pred = mk_bnf_pred QTs CA' CB';
- val rel_rhs =
+ val srel_rhs =
fold_rev Term.absfree Rs' (HOLogic.Collect_const CA'CB' $
Term.lambda p (Term.list_comb (pred, map (mk_predicate_of_set (fst x') (fst y')) Rs) $
HOLogic.mk_fst p $ HOLogic.mk_snd p));
- val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
+ val srel_bind_def = (fn () => Binding.suffix_name ("_" ^ srelN) b, srel_rhs);
- val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) =
+ val ((bnf_srel_term, raw_srel_def), (lthy, lthy_old)) =
lthy
- |> maybe_define false rel_bind_def
+ |> maybe_define false srel_bind_def
||> `(maybe_restore lthy);
val phi = Proof_Context.export_morphism lthy_old lthy;
- val bnf_rel_def = Morphism.thm phi raw_rel_def;
- val bnf_rel = Morphism.term phi bnf_rel_term;
+ val bnf_srel_def = Morphism.thm phi raw_srel_def;
+ val bnf_srel = Morphism.term phi bnf_srel_term;
- fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy setRTs CA' CB' bnf_rel;
+ fun mk_bnf_srel setRTs CA' CB' = normalize_srel lthy setRTs CA' CB' bnf_srel;
- val rel = mk_bnf_rel setRTs CA' CB';
+ val srel = mk_bnf_srel setRTs CA' CB';
val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @
- raw_wit_defs @ [raw_pred_def, raw_rel_def]) of
+ raw_wit_defs @ [raw_pred_def, raw_srel_def]) of
[] => ()
| defs => Proof_Display.print_consts true lthy_old (K false)
(map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
@@ -854,10 +854,10 @@
(Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull))
end;
- val rel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), O_Gr));
+ val srel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (srel, Rs), O_Gr));
val goals = zip_axioms map_id_goal map_comp_goal map_cong_goal set_naturals_goal
- card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_O_Gr_goal;
+ card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal;
fun mk_wit_goals (I, wit) =
let
@@ -978,43 +978,43 @@
|> Thm.close_derivation
end;
- val rel_O_Grs = no_refl [#rel_O_Gr axioms];
+ val srel_O_Grs = no_refl [#srel_O_Gr axioms];
val map_wppull = mk_lazy mk_map_wppull;
- fun mk_rel_Gr () =
+ fun mk_srel_Gr () =
let
- val lhs = Term.list_comb (rel, map2 mk_Gr As fs);
+ val lhs = Term.list_comb (srel, map2 mk_Gr As fs);
val rhs = mk_Gr (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal
- (mk_rel_Gr_tac rel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
+ (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
end;
- val rel_Gr = mk_lazy mk_rel_Gr;
+ val srel_Gr = mk_lazy mk_srel_Gr;
- fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
- fun mk_rel_concl f = HOLogic.mk_Trueprop
- (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy)));
+ fun mk_srel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
+ fun mk_srel_concl f = HOLogic.mk_Trueprop
+ (f (Term.list_comb (srel, Rs), Term.list_comb (srel, Rs_copy)));
- fun mk_rel_mono () =
+ fun mk_srel_mono () =
let
- val mono_prems = mk_rel_prems mk_subset;
- val mono_concl = mk_rel_concl (uncurry mk_subset);
+ val mono_prems = mk_srel_prems mk_subset;
+ val mono_concl = mk_srel_concl (uncurry mk_subset);
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
- (mk_rel_mono_tac rel_O_Grs (Lazy.force in_mono))
+ (mk_srel_mono_tac srel_O_Grs (Lazy.force in_mono))
|> Thm.close_derivation
end;
- fun mk_rel_cong () =
+ fun mk_srel_cong () =
let
- val cong_prems = mk_rel_prems (curry HOLogic.mk_eq);
- val cong_concl = mk_rel_concl HOLogic.mk_eq;
+ val cong_prems = mk_srel_prems (curry HOLogic.mk_eq);
+ val cong_concl = mk_srel_concl HOLogic.mk_eq;
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
@@ -1022,89 +1022,89 @@
|> Thm.close_derivation
end;
- val rel_mono = mk_lazy mk_rel_mono;
- val rel_cong = mk_lazy mk_rel_cong;
+ val srel_mono = mk_lazy mk_srel_mono;
+ val srel_cong = mk_lazy mk_srel_cong;
- fun mk_rel_Id () =
- let val relAsAs = mk_bnf_rel self_setRTs CA' CA' in
+ fun mk_srel_Id () =
+ let val relAsAs = mk_bnf_srel self_setRTs CA' CA' in
Skip_Proof.prove lthy [] []
(HOLogic.mk_Trueprop
(HOLogic.mk_eq (Term.list_comb (relAsAs, map Id_const As'), Id_const CA')))
- (mk_rel_Id_tac live (Lazy.force rel_Gr) (#map_id axioms))
+ (mk_srel_Id_tac live (Lazy.force srel_Gr) (#map_id axioms))
|> Thm.close_derivation
end;
- val rel_Id = mk_lazy mk_rel_Id;
+ val srel_Id = mk_lazy mk_srel_Id;
- fun mk_rel_converse () =
+ fun mk_srel_converse () =
let
- val relBsAs = mk_bnf_rel setRT's CB' CA';
+ val relBsAs = mk_bnf_srel setRT's CB' CA';
val lhs = Term.list_comb (relBsAs, map mk_converse Rs);
- val rhs = mk_converse (Term.list_comb (rel, Rs));
+ val rhs = mk_converse (Term.list_comb (srel, Rs));
val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
val le_thm = Skip_Proof.prove lthy [] [] le_goal
- (mk_rel_converse_le_tac rel_O_Grs (Lazy.force rel_Id) (#map_cong axioms)
+ (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
(Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
in
- Skip_Proof.prove lthy [] [] goal (fn _ => mk_rel_converse_tac le_thm)
+ Skip_Proof.prove lthy [] [] goal (fn _ => mk_srel_converse_tac le_thm)
|> Thm.close_derivation
end;
- val rel_converse = mk_lazy mk_rel_converse;
+ val srel_converse = mk_lazy mk_srel_converse;
- fun mk_rel_O () =
+ fun mk_srel_O () =
let
- val relAsCs = mk_bnf_rel setRTsAsCs CA' CC';
- val relBsCs = mk_bnf_rel setRTsBsCs CB' CC';
+ val relAsCs = mk_bnf_srel setRTsAsCs CA' CC';
+ val relBsCs = mk_bnf_srel setRTsBsCs CB' CC';
val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_comp) Rs Ss);
- val rhs = mk_rel_comp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
+ val rhs = mk_rel_comp (Term.list_comb (srel, Rs), Term.list_comb (relBsCs, Ss));
val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
in
Skip_Proof.prove lthy [] [] goal
- (mk_rel_O_tac rel_O_Grs (Lazy.force rel_Id) (#map_cong axioms)
+ (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
(Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
|> Thm.close_derivation
end;
- val rel_O = mk_lazy mk_rel_O;
+ val srel_O = mk_lazy mk_srel_O;
- fun mk_in_rel () =
+ fun mk_in_srel () =
let
val bnf_in = mk_in Rs (map (mk_bnf_t RTs) bnf_sets) CRs';
val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
val map_fst_eq = HOLogic.mk_eq (map1 $ z, x);
val map_snd_eq = HOLogic.mk_eq (map2 $ z, y);
- val lhs = HOLogic.mk_mem (HOLogic.mk_prod (x, y), Term.list_comb (rel, Rs));
+ val lhs = HOLogic.mk_mem (HOLogic.mk_prod (x, y), Term.list_comb (srel, Rs));
val rhs =
HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
val goal =
fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
in
- Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac rel_O_Grs (length bnf_sets))
+ Skip_Proof.prove lthy [] [] goal (mk_in_srel_tac srel_O_Grs (length bnf_sets))
|> Thm.close_derivation
end;
- val in_rel = mk_lazy mk_in_rel;
+ val in_srel = mk_lazy mk_in_srel;
- val defs = mk_defs bnf_map_def bnf_set_defs bnf_pred_def bnf_rel_def;
+ val defs = mk_defs bnf_map_def bnf_set_defs bnf_pred_def bnf_srel_def;
- val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural
- in_cong in_mono in_rel map_comp' map_id' map_wppull
- rel_cong rel_mono rel_Id rel_Gr rel_converse rel_O set_natural';
+ val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong
+ in_mono in_srel map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id
+ srel_Gr srel_converse srel_O;
val wits = map2 mk_witness bnf_wits wit_thms;
- val bnf_pred = Term.subst_atomic_types
- ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) pred;
- val bnf_rel = Term.subst_atomic_types
- ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;
+ val bnf_pred =
+ Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) pred;
+ val bnf_srel =
+ Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) srel;
val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts
- wits bnf_pred bnf_rel;
+ wits bnf_pred bnf_srel;
in
(bnf, lthy
|> (if fact_policy = Note_All_Facts_and_Axioms then
@@ -1119,7 +1119,7 @@
(collect_set_naturalN, [Lazy.force (#collect_set_natural facts)]),
(in_bdN, [#in_bd axioms]),
(in_monoN, [Lazy.force (#in_mono facts)]),
- (in_relN, [Lazy.force (#in_rel facts)]),
+ (in_srelN, [Lazy.force (#in_srel facts)]),
(map_compN, [#map_comp axioms]),
(map_idN, [#map_id axioms]),
(map_wpullN, [#map_wpull axioms]),
@@ -1138,16 +1138,16 @@
fact_policy = Derive_All_Facts_Note_Most then
let
val notes =
- [(map_congN, [#map_cong axioms]),
- (rel_O_GrN, rel_O_Grs),
- (rel_IdN, [Lazy.force (#rel_Id facts)]),
- (rel_GrN, [Lazy.force (#rel_Gr facts)]),
- (rel_converseN, [Lazy.force (#rel_converse facts)]),
- (rel_monoN, [Lazy.force (#rel_mono facts)]),
- (rel_ON, [Lazy.force (#rel_O facts)]),
+ [(map_comp'N, [Lazy.force (#map_comp' facts)]),
+ (map_congN, [#map_cong axioms]),
(map_id'N, [Lazy.force (#map_id' facts)]),
- (map_comp'N, [Lazy.force (#map_comp' facts)]),
- (set_natural'N, map Lazy.force (#set_natural' facts))]
+ (set_natural'N, map Lazy.force (#set_natural' facts)),
+ (srel_O_GrN, srel_O_Grs),
+ (srel_IdN, [Lazy.force (#srel_Id facts)]),
+ (srel_GrN, [Lazy.force (#srel_Gr facts)]),
+ (srel_converseN, [Lazy.force (#srel_converse facts)]),
+ (srel_monoN, [Lazy.force (#srel_mono facts)]),
+ (srel_ON, [Lazy.force (#srel_O facts)])]
|> filter_out (null o #2)
|> map (fn (thmN, thms) =>
((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
@@ -1161,7 +1161,7 @@
val one_step_defs =
no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_pred_def,
- bnf_rel_def]);
+ bnf_srel_def]);
in
(key, goals, wit_goalss, after_qed, lthy, one_step_defs)
end;
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -15,16 +15,16 @@
val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_set_natural': thm -> thm
- val mk_rel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
- val mk_rel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_srel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_srel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_in_rel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
- val mk_rel_converse_tac: thm -> tactic
- val mk_rel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
+ val mk_in_srel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
+ val mk_srel_converse_tac: thm -> tactic
+ val mk_srel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_srel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
end;
structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -63,14 +63,14 @@
rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
-fun mk_rel_Gr_tac rel_O_Grs map_id map_cong map_id' map_comp set_naturals
+fun mk_srel_Gr_tac srel_O_Grs map_id map_cong map_id' map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
in
if null set_naturals then
- unfold_thms_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
- else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+ unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+ else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
EVERY' [rtac equalityI, rtac subsetI,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac Pair_eqD,
@@ -104,28 +104,28 @@
@{thms fst_convol snd_convol} [map_id', refl])] 1
end;
-fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
- unfold_thms_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
+fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
subst_tac ctxt [map_id] 1 THEN
(if n = 0 then rtac refl 1
else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
-fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
- unfold_thms_tac ctxt rel_O_Grs THEN
+fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt srel_O_Grs THEN
EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
-fun mk_rel_converse_le_tac rel_O_Grs rel_Id map_cong map_comp set_naturals
+fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
in
if null set_naturals then
- unfold_thms_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
- else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+ unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
+ else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
EVERY' [rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac Pair_eqD,
@@ -139,11 +139,11 @@
etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
end;
-fun mk_rel_converse_tac le_converse =
+fun mk_srel_converse_tac le_converse =
EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
-fun mk_rel_O_tac rel_O_Grs rel_Id map_cong map_wppull map_comp set_naturals
+fun mk_srel_O_tac srel_O_Grs srel_Id map_cong map_wppull map_comp set_naturals
{context = ctxt, prems = _} =
let
val n = length set_naturals;
@@ -151,8 +151,8 @@
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
in
- if null set_naturals then unfold_thms_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
- else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+ if null set_naturals then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
+ else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
EVERY' [rtac equalityI, rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac Pair_eqD,
@@ -193,11 +193,11 @@
rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
end;
-fun mk_in_rel_tac rel_O_Grs m {context = ctxt, prems = _} =
+fun mk_in_srel_tac srel_O_Grs m {context = ctxt, prems = _} =
let
val ls' = replicate (Int.max (1, m)) ();
in
- unfold_thms_tac ctxt (rel_O_Grs @
+ unfold_thms_tac ctxt (srel_O_Grs @
@{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
--- 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
@@ -67,15 +67,15 @@
val pred_strong_coinductN: string
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
val sel_corecsN: string
val set_inclN: string
val set_set_inclN: string
val simpsN: string
+ val srel_coinductN: string
+ val srel_simpN: string
+ val srel_strong_coinductN: string
val strTN: string
val str_initN: string
val strongN: string
@@ -222,15 +222,15 @@
val ctor_inductN = ctorN ^ "_" ^ inductN
val ctor_induct2N = ctor_inductN ^ "2"
val dtor_coinductN = dtorN ^ "_" ^ coinductN
-val rel_coinductN = relN ^ "_" ^ coinductN
val pred_coinductN = predN ^ "_" ^ coinductN
+val srel_coinductN = srelN ^ "_" ^ coinductN
val simpN = "_simp";
-val rel_simpN = relN ^ simpN;
+val srel_simpN = srelN ^ simpN;
val pred_simpN = predN ^ simpN;
val strongN = "strong_"
val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN
-val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN
val pred_strong_coinductN = predN ^ "_" ^ strongN ^ coinductN
+val srel_strong_coinductN = srelN ^ "_" ^ 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
@@ -144,7 +144,7 @@
val setssAs = mk_setss allAs;
val setssAs' = transpose setssAs;
val bis_setss = mk_setss (passiveAs @ RTs);
- val relsAsBs = map4 mk_rel_of_bnf Dss Ass Bss bnfs;
+ val relsAsBs = map4 mk_srel_of_bnf Dss Ass Bss bnfs;
val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
val sum_bdT = fst (dest_relT (fastype_of sum_bd));
@@ -220,17 +220,17 @@
val map_comp's = map map_comp'_of_bnf bnfs;
val map_congs = map map_cong_of_bnf bnfs;
val map_id's = map map_id'_of_bnf bnfs;
- val rel_congs = map rel_cong_of_bnf bnfs;
- val rel_converses = map rel_converse_of_bnf bnfs;
- val rel_defs = map rel_def_of_bnf bnfs;
- val rel_Grs = map rel_Gr_of_bnf bnfs;
- val rel_Ids = map rel_Id_of_bnf bnfs;
- val rel_monos = map rel_mono_of_bnf bnfs;
- val rel_Os = map rel_O_of_bnf bnfs;
- val rel_O_Grs = map rel_O_Gr_of_bnf bnfs;
val map_wpulls = map map_wpull_of_bnf bnfs;
val set_bdss = map set_bd_of_bnf bnfs;
val set_natural'ss = map set_natural'_of_bnf bnfs;
+ val srel_congs = map srel_cong_of_bnf bnfs;
+ val srel_converses = map srel_converse_of_bnf bnfs;
+ val srel_defs = map srel_def_of_bnf bnfs;
+ val srel_Grs = map srel_Gr_of_bnf bnfs;
+ val srel_Ids = map srel_Id_of_bnf bnfs;
+ val srel_monos = map srel_mono_of_bnf bnfs;
+ val srel_Os = map srel_O_of_bnf bnfs;
+ val srel_O_Grs = map srel_O_Gr_of_bnf bnfs;
val timer = time (timer "Extracted terms & thms");
@@ -846,13 +846,13 @@
|> Thm.close_derivation
end;
- val bis_rel_thm =
+ val bis_srel_thm =
let
- fun mk_conjunct R s s' b1 b2 rel =
+ fun mk_conjunct R s s' b1 b2 srel =
list_all_free [b1, b2] (HOLogic.mk_imp
(HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
HOLogic.mk_mem (HOLogic.mk_prod (s $ b1, s' $ b2),
- Term.list_comb (rel, passive_diags @ Rs))));
+ Term.list_comb (srel, passive_diags @ Rs))));
val rhs = HOLogic.mk_conj
(bis_le, Library.foldr1 HOLogic.mk_conj
@@ -861,7 +861,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
(mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
- (K (mk_bis_rel_tac m bis_def rel_O_Grs map_comp's map_congs set_natural'ss))
+ (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_congs set_natural'ss))
|> Thm.close_derivation
end;
@@ -871,7 +871,7 @@
(Logic.mk_implies
(HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
- (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converses))
+ (K (mk_bis_converse_tac m bis_srel_thm srel_congs srel_converses))
|> Thm.close_derivation;
val bis_O_thm =
@@ -885,7 +885,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
(Logic.list_implies (prems, concl)))
- (K (mk_bis_O_tac m bis_rel_thm rel_congs rel_Os))
+ (K (mk_bis_O_tac m bis_srel_thm srel_congs srel_Os))
|> Thm.close_derivation
end;
@@ -897,7 +897,7 @@
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
(Logic.list_implies ([coalg_prem, mor_prem], concl)))
- (mk_bis_Gr_tac bis_rel_thm rel_Grs mor_image_thms morE_thms coalg_in_thms)
+ (mk_bis_Gr_tac bis_srel_thm srel_Grs mor_image_thms morE_thms coalg_in_thms)
|> Thm.close_derivation
end;
@@ -2178,8 +2178,8 @@
val timer = time (timer "corec definitions & thms");
- val (dtor_coinduct_thm, coinduct_params, rel_coinduct_thm, pred_coinduct_thm,
- dtor_strong_coinduct_thm, rel_strong_coinduct_thm, pred_strong_coinduct_thm) =
+ val (dtor_coinduct_thm, coinduct_params, srel_coinduct_thm, pred_coinduct_thm,
+ dtor_strong_coinduct_thm, srel_strong_coinduct_thm, pred_strong_coinduct_thm) =
let
val zs = Jzs1 @ Jzs2;
val frees = phis @ zs;
@@ -2191,34 +2191,34 @@
(HOLogic.mk_disj (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2))))
else phi;
- fun phi_rels upto_eq = map4 (fn phi => fn T => fn z1 => fn z2 =>
+ fun phi_srels upto_eq = map4 (fn phi => fn T => fn z1 => fn z2 =>
HOLogic.Collect_const (HOLogic.mk_prodT (T, T)) $
HOLogic.mk_split (mk_phi upto_eq phi z1 z2)) phis Ts Jzs1 Jzs2;
- val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
+ val srels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map3 mk_concl phis Jzs1 Jzs2));
- fun mk_rel_prem upto_eq phi dtor rel Jz Jz_copy =
+ fun mk_srel_prem upto_eq phi dtor srel Jz Jz_copy =
let
val concl = HOLogic.mk_mem (HOLogic.mk_tuple [dtor $ Jz, dtor $ Jz_copy],
- Term.list_comb (rel, mk_Ids upto_eq @ phi_rels upto_eq));
+ Term.list_comb (srel, mk_Ids upto_eq @ phi_srels upto_eq));
in
HOLogic.mk_Trueprop
(list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
end;
- val rel_prems = map5 (mk_rel_prem false) phis dtors rels Jzs Jzs_copy;
- val rel_upto_prems = map5 (mk_rel_prem true) phis dtors rels Jzs Jzs_copy;
-
- val rel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
- val coinduct_params = rev (Term.add_tfrees rel_coinduct_goal []);
-
- val rel_coinduct = unfold_thms lthy @{thms diag_UNIV}
- (Skip_Proof.prove lthy [] [] rel_coinduct_goal
- (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm))
+ 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))
|> Thm.close_derivation);
fun mk_dtor_prem upto_eq phi dtor map_nth sets Jz Jz_copy FJz =
@@ -2256,10 +2256,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 rel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
+ val srel_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_strong_coinduct_tac m cTs cts rel_coinduct rel_monos rel_Ids)))
+ (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)))
|> Thm.close_derivation;
val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
@@ -2269,14 +2269,14 @@
(tcoalg_thm RS bis_diag_thm))))
|> Thm.close_derivation;
- val pred_of_rel_thms =
- rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
-
- val pred_coinduct = unfold_thms lthy pred_of_rel_thms rel_coinduct;
- val pred_strong_coinduct = unfold_thms lthy pred_of_rel_thms rel_strong_coinduct;
+ val pred_of_srel_thms =
+ srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
+
+ val pred_coinduct = unfold_thms lthy pred_of_srel_thms srel_coinduct;
+ val pred_strong_coinduct = unfold_thms lthy pred_of_srel_thms srel_strong_coinduct;
in
- (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), rel_coinduct, pred_coinduct,
- dtor_strong_coinduct, rel_strong_coinduct, pred_strong_coinduct)
+ (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), srel_coinduct, pred_coinduct,
+ dtor_strong_coinduct, srel_strong_coinduct, pred_strong_coinduct)
end;
val timer = time (timer "coinduction");
@@ -2672,10 +2672,10 @@
map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm
mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss;
- val rel_O_Gr_tacs = replicate n (simple_rel_O_Gr_tac o #context);
+ val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs;
+ bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, hset_induct_thms) =
let
@@ -2880,40 +2880,40 @@
val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
val set_induct_thms = map fold_sets hset_induct_thms;
- val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
- val Jrels = map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
+ val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
+ val Jsrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Jbnfs;
val preds = map2 (fn Ds => mk_pred_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
val Jpreds = map (mk_pred_of_bnf deads passiveAs passiveBs) Jbnfs;
- val JrelRs = map (fn Jrel => Term.list_comb (Jrel, JRs)) Jrels;
- val relRs = map (fn rel => Term.list_comb (rel, JRs @ JrelRs)) rels;
- val Jpredphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jpreds;
- val predphis = map (fn rel => Term.list_comb (rel, Jphis @ Jpredphis)) preds;
-
- val in_rels = map in_rel_of_bnf bnfs;
- val in_Jrels = map in_rel_of_bnf Jbnfs;
- val Jrel_defs = map rel_def_of_bnf Jbnfs;
+ val JrelRs = map (fn Jsrel => Term.list_comb (Jsrel, JRs)) Jsrels;
+ val relRs = map (fn srel => Term.list_comb (srel, JRs @ JrelRs)) srels;
+ val Jpredphis = map (fn Jsrel => Term.list_comb (Jsrel, Jphis)) Jpreds;
+ val predphis = map (fn srel => Term.list_comb (srel, Jphis @ Jpredphis)) preds;
+
+ val in_srels = map in_srel_of_bnf bnfs;
+ val in_Jsrels = map in_srel_of_bnf Jbnfs;
+ val Jsrel_defs = map srel_def_of_bnf Jbnfs;
val Jpred_defs = map pred_def_of_bnf Jbnfs;
val folded_map_simp_thms = map fold_maps map_simp_thms;
val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
- val Jrel_simp_thms =
+ val Jsrel_simp_thms =
let
fun mk_goal Jz Jz' dtor dtor' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs)
(mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
HOLogic.mk_mem (HOLogic.mk_prod (dtor $ Jz, dtor' $ Jz'), relR)));
val goals = map6 mk_goal Jzs Jz's dtors dtor's JrelRs relRs;
in
- map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
+ map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
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_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
+ (K (mk_srel_simp_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_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
+ 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;
@@ -2923,11 +2923,11 @@
(mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz')));
val goals = map6 mk_goal Jzs Jz's dtors dtor's Jpredphis predphis;
in
- map3 (fn goal => fn rel_def => fn Jrel_simp =>
+ map3 (fn goal => fn srel_def => fn Jsrel_simp =>
Skip_Proof.prove lthy [] [] goal
- (mk_pred_simp_tac rel_def Jpred_defs Jrel_defs Jrel_simp)
+ (mk_pred_simp_tac srel_def Jpred_defs Jsrel_defs Jsrel_simp)
|> Thm.close_derivation)
- goals rel_defs Jrel_simp_thms
+ goals srel_defs Jsrel_simp_thms
end;
val timer = time (timer "additional properties");
@@ -2942,10 +2942,10 @@
val Jbnf_notes =
[(map_simpsN, map single folded_map_simp_thms),
+ (pred_simpN, map single Jpred_simp_thms),
(set_inclN, set_incl_thmss),
(set_set_inclN, map flat set_set_incl_thmsss),
- (rel_simpN, map single Jrel_simp_thms),
- (pred_simpN, map single Jpred_simp_thms)] @
+ (srel_simpN, map single Jsrel_simp_thms)] @
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 =>
@@ -2957,11 +2957,11 @@
val common_notes =
[(dtor_coinductN, [dtor_coinduct_thm]),
- (rel_coinductN, [rel_coinduct_thm]),
+ (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
(pred_coinductN, [pred_coinduct_thm]),
- (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
- (rel_strong_coinductN, [rel_strong_coinduct_thm]),
- (pred_strong_coinductN, [pred_strong_coinduct_thm])]
+ (pred_strong_coinductN, [pred_strong_coinduct_thm]),
+ (srel_coinductN, [srel_coinduct_thm]),
+ (srel_strong_coinductN, [srel_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
@@ -17,7 +17,7 @@
val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic
val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
- val mk_bis_rel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
+ val mk_bis_srel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
{prems: 'a, context: Proof.context} -> tactic
val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic
@@ -38,8 +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_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> thm ->
- thm -> 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 ->
{prems: 'a, context: Proof.context} -> tactic
val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
@@ -91,11 +91,6 @@
tactic
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_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
val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic
val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
@@ -111,6 +106,11 @@
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_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
@@ -256,15 +256,15 @@
EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
atac, atac, rtac (hset_def RS sym)] 1
-fun mk_bis_rel_tac m bis_def rel_O_Grs map_comps map_congs set_naturalss =
+fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_congs set_naturalss =
let
- val n = length rel_O_Grs;
- val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ rel_O_Grs);
+ val n = length srel_O_Grs;
+ val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ srel_O_Grs);
- fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), rel_O_Gr) =
+ fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
- rtac (rel_O_Gr RS equalityD2 RS set_mp),
+ rtac (srel_O_Gr RS equalityD2 RS set_mp),
rtac @{thm relcompI}, rtac @{thm converseI},
EVERY' (map (fn thm =>
EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
@@ -280,10 +280,10 @@
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
@{thms fst_diag_id snd_diag_id})];
- fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), rel_O_Gr) =
+ fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
etac allE, etac allE, etac impE, atac,
- dtac (rel_O_Gr RS equalityD1 RS set_mp),
+ dtac (srel_O_Gr RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
REPEAT_DETERM o dtac Pair_eqD,
@@ -313,39 +313,39 @@
etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
end;
-fun mk_bis_converse_tac m bis_rel rel_congs rel_converses =
- EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
+fun mk_bis_converse_tac m bis_srel srel_congs srel_converses =
+ EVERY' [stac bis_srel, dtac (bis_srel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
- rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
- CONJ_WRAP' (fn (rel_cong, rel_converse) =>
+ rtac equalityD2, rtac @{thm converse_Times}])) srel_congs,
+ CONJ_WRAP' (fn (srel_cong, srel_converse) =>
EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
- rtac (rel_cong RS trans),
+ rtac (srel_cong RS trans),
REPEAT_DETERM_N m o rtac @{thm diag_converse},
- REPEAT_DETERM_N (length rel_congs) o rtac refl,
- rtac rel_converse,
+ REPEAT_DETERM_N (length srel_congs) o rtac refl,
+ rtac srel_converse,
REPEAT_DETERM o etac allE,
- rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1;
+ rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
-fun mk_bis_O_tac m bis_rel rel_congs rel_Os =
- EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
+fun mk_bis_O_tac m bis_srel srel_congs srel_Os =
+ EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
- CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
- CONJ_WRAP' (fn (rel_cong, rel_O) =>
+ CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
+ CONJ_WRAP' (fn (srel_cong, srel_O) =>
EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
- rtac (rel_cong RS trans),
+ rtac (srel_cong RS trans),
REPEAT_DETERM_N m o rtac @{thm diag_Comp},
- REPEAT_DETERM_N (length rel_congs) o rtac refl,
- rtac rel_O,
+ REPEAT_DETERM_N (length srel_congs) o rtac refl,
+ rtac srel_O,
etac @{thm relcompE},
REPEAT_DETERM o dtac Pair_eqD,
etac conjE, hyp_subst_tac,
REPEAT_DETERM o etac allE, rtac @{thm relcompI},
- etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1;
+ etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
-fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins
+fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins
{context = ctxt, prems = _} =
- unfold_thms_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
+ unfold_thms_tac ctxt (bis_srel :: @{thm diag_Gr} :: srel_Grs) THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
CONJ_WRAP' (fn (coalg_in, morE) =>
@@ -1123,8 +1123,8 @@
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_rel_coinduct_tac ks raw_coind bis_rel =
- EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI,
+fun mk_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,
REPEAT_DETERM o etac allE, etac mp, etac CollectE, etac @{thm splitD}])) ks,
@@ -1132,17 +1132,17 @@
CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
-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 =>
+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),
+ 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 (rel_mono RS set_mp),
+ etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp),
REPEAT_DETERM_N m o rtac @{thm subset_refl},
- REPEAT_DETERM_N (length rel_monos) o rtac @{thm Id_subset},
- rtac (rel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
- rel_monos rel_Ids),
+ REPEAT_DETERM_N (length srel_monos) o rtac @{thm Id_subset},
+ rtac (srel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
+ srel_monos srel_Ids),
rtac impI, REPEAT_DETERM o etac conjE,
- CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_Ids] 1;
+ CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) srel_Ids] 1;
fun mk_dtor_coinduct_tac m ks raw_coind bis_def =
let
@@ -1494,27 +1494,27 @@
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
-fun mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
+fun mk_srel_simp_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;
val n = length set_set_inclss;
val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
- val in_Jrel = nth in_Jrels (i - 1);
+ val in_Jsrel = nth in_Jsrels (i - 1);
val if_tac =
- EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
- rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+ rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
EVERY' (map2 (fn set_natural => fn set_incl =>
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
etac (set_incl RS @{thm subset_trans})])
passive_set_naturals set_incls),
- CONJ_WRAP' (fn (in_Jrel, (set_natural, set_set_incls)) =>
+ CONJ_WRAP' (fn (in_Jsrel, (set_natural, set_set_incls)) =>
EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
- rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls,
rtac conjI, rtac refl, rtac refl])
- (in_Jrels ~~ (active_set_naturals ~~ set_set_inclss)),
+ (in_Jsrels ~~ (active_set_naturals ~~ set_set_inclss)),
CONJ_WRAP' (fn conv =>
EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
@@ -1522,30 +1522,30 @@
rtac trans, rtac sym, rtac map_simp, rtac (dtor_inject RS iffD2), atac])
@{thms fst_conv snd_conv}];
val only_if_tac =
- EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
- rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+ rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural,
rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
- (fn (active_set_natural, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
+ (fn (active_set_natural, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
rtac active_set_natural, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
- dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1),
+ dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
- (rev (active_set_naturals ~~ in_Jrels))])
+ (rev (active_set_naturals ~~ in_Jsrels))])
(set_simps ~~ passive_set_naturals),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac map_simp,
rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
- EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
- dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1), dtac @{thm someI_ex},
- REPEAT_DETERM o etac conjE, atac]) in_Jrels),
+ EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
+ dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
+ dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jsrels),
atac]]
in
EVERY' [rtac iffI, if_tac, only_if_tac] 1
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -1671,10 +1671,10 @@
in_incl_min_alg_thms card_of_min_alg_thms;
val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
- val rel_O_Gr_tacs = replicate n (simple_rel_O_Gr_tac o #context);
+ val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs;
+ bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
val ctor_witss =
let
@@ -1720,20 +1720,20 @@
val timer = time (timer "registered new datatypes as BNFs");
- val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
- val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
+ val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
+ val Isrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Ibnfs;
val preds = map2 (fn Ds => mk_pred_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
val Ipreds = map (mk_pred_of_bnf deads passiveAs passiveBs) Ibnfs;
- val IrelRs = map (fn Irel => Term.list_comb (Irel, IRs)) Irels;
- val relRs = map (fn rel => Term.list_comb (rel, IRs @ IrelRs)) rels;
- val Ipredphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Ipreds;
- val predphis = map (fn rel => Term.list_comb (rel, Iphis @ Ipredphis)) preds;
+ val IrelRs = map (fn Isrel => Term.list_comb (Isrel, IRs)) Isrels;
+ val relRs = map (fn srel => Term.list_comb (srel, IRs @ IrelRs)) srels;
+ val Ipredphis = map (fn Isrel => Term.list_comb (Isrel, Iphis)) Ipreds;
+ val predphis = map (fn srel => Term.list_comb (srel, Iphis @ Ipredphis)) preds;
- val in_rels = map in_rel_of_bnf bnfs;
- val in_Irels = map in_rel_of_bnf Ibnfs;
- val rel_defs = map rel_def_of_bnf bnfs;
- val Irel_defs = map rel_def_of_bnf Ibnfs;
+ val in_srels = map in_srel_of_bnf bnfs;
+ val in_Isrels = map in_srel_of_bnf Ibnfs;
+ val srel_defs = map srel_def_of_bnf bnfs;
+ val Isrel_defs = map srel_def_of_bnf Ibnfs;
val Ipred_defs = map pred_def_of_bnf Ibnfs;
val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
@@ -1742,21 +1742,21 @@
val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
- val Irel_simp_thms =
+ val Isrel_simp_thms =
let
fun mk_goal xF yF ctor ctor' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs)
(mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IrelR),
HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR)));
val goals = map6 mk_goal xFs yFs ctors ctor's IrelRs relRs;
in
- map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
+ map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
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_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps
+ (K (mk_srel_simp_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_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
+ 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;
@@ -1766,11 +1766,11 @@
(mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF));
val goals = map6 mk_goal xFs yFs ctors ctor's Ipredphis predphis;
in
- map3 (fn goal => fn rel_def => fn Irel_simp =>
+ map3 (fn goal => fn srel_def => fn Isrel_simp =>
Skip_Proof.prove lthy [] [] goal
- (mk_pred_simp_tac rel_def Ipred_defs Irel_defs Irel_simp)
+ (mk_pred_simp_tac srel_def Ipred_defs Isrel_defs Isrel_simp)
|> Thm.close_derivation)
- goals rel_defs Irel_simp_thms
+ goals srel_defs Isrel_simp_thms
end;
val timer = time (timer "additional properties");
@@ -1786,7 +1786,7 @@
[(map_simpsN, map single folded_map_simp_thms),
(set_inclN, set_incl_thmss),
(set_set_inclN, map flat set_set_incl_thmsss),
- (rel_simpN, map single Irel_simp_thms),
+ (srel_simpN, map single Isrel_simp_thms),
(pred_simpN, map single Ipred_simp_thms)] @
map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
|> maps (fn (thmN, thmss) =>
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -22,6 +22,7 @@
thm list -> tactic
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_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 ->
@@ -61,8 +62,6 @@
thm list -> tactic
val mk_mor_str_tac: 'a list -> thm -> tactic
val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> 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
val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int ->
{prems: 'a, context: Proof.context} -> tactic
val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
@@ -70,7 +69,8 @@
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_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> 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_wit_tac: int -> thm list -> thm list -> tactic
val mk_wpull_tac: thm -> tactic
end;
@@ -770,32 +770,32 @@
EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps ctor_inject
+fun mk_srel_simp_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;
val n = length set_set_inclss;
val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
- val in_Irel = nth in_Irels (i - 1);
+ val in_Isrel = nth in_Isrels (i - 1);
val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
val if_tac =
- EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
- rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ EVERY' [dtac (in_Isrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+ rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
EVERY' (map2 (fn set_natural => fn set_incl =>
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
rtac (set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
passive_set_naturals set_incls),
- CONJ_WRAP' (fn (in_Irel, (set_natural, set_set_incls)) =>
+ CONJ_WRAP' (fn (in_Isrel, (set_natural, set_set_incls)) =>
EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
- rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn thm =>
EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
set_set_incls,
rtac conjI, rtac refl, rtac refl])
- (in_Irels ~~ (active_set_naturals ~~ set_set_inclss)),
+ (in_Isrels ~~ (active_set_naturals ~~ set_set_inclss)),
CONJ_WRAP' (fn conv =>
EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
@@ -804,29 +804,29 @@
etac eq_arg_cong_ctor_dtor])
fst_snd_convs];
val only_if_tac =
- EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
- rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+ rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
- (fn (active_set_natural, in_Irel) => EVERY' [rtac ord_eq_le_trans,
+ (fn (active_set_natural, in_Isrel) => EVERY' [rtac ord_eq_le_trans,
rtac @{thm UN_cong[OF _ refl]}, rtac active_set_natural, rtac @{thm UN_least},
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
- dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Irel RS iffD1),
+ dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
- (rev (active_set_naturals ~~ in_Irels))])
+ (rev (active_set_naturals ~~ in_Isrels))])
(set_simps ~~ passive_set_naturals),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac map_simp, rtac (ctor_inject RS iffD2),
rtac trans, rtac map_comp, rtac trans, rtac map_cong,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
- EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
- dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Irel RS iffD1), dtac @{thm someI_ex},
- REPEAT_DETERM o etac conjE, atac]) in_Irels),
+ EVERY' (map (fn in_Isrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
+ dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
+ dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Isrels),
atac]]
in
EVERY' [rtac iffI, if_tac, only_if_tac] 1
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -26,7 +26,7 @@
val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
val mk_Abs_inj_thm: thm -> thm
- val simple_rel_O_Gr_tac: Proof.context -> tactic
+ val simple_srel_O_Gr_tac: Proof.context -> tactic
val mk_pred_simp_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
tactic
@@ -98,14 +98,14 @@
gen_tac
end;
-fun simple_rel_O_Gr_tac ctxt =
+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_pred_simp_tac rel_def IJpred_defs IJrel_defs rel_simp {context = ctxt, prems = _} =
+fun mk_pred_simp_tac srel_def IJpred_defs IJsrel_defs srel_simp {context = ctxt, prems = _} =
unfold_thms_tac ctxt IJpred_defs THEN
- subst_tac ctxt [unfold_thms ctxt (IJpred_defs @ IJrel_defs @
- @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) rel_simp] 1 THEN
- unfold_thms_tac ctxt (rel_def ::
+ subst_tac ctxt [unfold_thms ctxt (IJpred_defs @ IJsrel_defs @
+ @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) srel_simp] 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
rtac refl 1;