--- a/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 20 02:42:48 2012 +0200
@@ -9,11 +9,28 @@
header {* Miscellaneous Datatype Declarations *}
theory Misc_Data
-imports "../Codatatype"
+imports (* "../Codatatype" *) "../BNF_LFP"
begin
+declare [[bnf_note_all = false]]
+
+local_setup {* fn lthy =>
+snd (snd (BNF_Comp.bnf_of_typ BNF_Def.Dont_Inline (Binding.qualify true "xxx")
+ BNF_Comp.default_comp_sort
+ @{typ "('a \<Rightarrow> 'a) + ('a + 'b) + 'c"} (BNF_Comp.empty_unfold, lthy)))
+*}
+
+data 'a lst = Nl | Cns 'a "'a lst"
+
+thm pre_lst.rel_unfold
+ pre_lst.pred_unfold
+ lst.rel_unfold
+ lst.pred_unfold
+
data simple = X1 | X2 | X3 | X4
+thm simple.rel_unfold
+
data simple' = X1' unit | X2' unit | X3' unit | X4' unit
data 'a mylist = MyNil | MyCons 'a "'a mylist"
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:48 2012 +0200
@@ -13,7 +13,6 @@
val map_unfolds_of: unfold_thms -> thm list
val set_unfoldss_of: unfold_thms -> thm list list
val rel_unfolds_of: unfold_thms -> thm list
- val pred_unfolds_of: unfold_thms -> thm list
val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
@@ -37,34 +36,29 @@
type unfold_thms = {
map_unfolds: thm list,
set_unfoldss: thm list list,
- rel_unfolds: thm list,
- pred_unfolds: thm list
+ rel_unfolds: thm list
};
fun add_to_thms thms NONE = thms
| add_to_thms thms (SOME new) = if Thm.is_reflexive new then thms else insert Thm.eq_thm new thms;
fun adds_to_thms thms NONE = thms
- | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (filter_refl news) thms;
+ | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (filter_out_refl news) thms;
-fun mk_unfold_thms maps setss rels preds =
- {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds};
+fun mk_unfold_thms maps setss rels = {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels};
-val empty_unfold = mk_unfold_thms [] [] [] [];
+val empty_unfold = mk_unfold_thms [] [] [];
-fun add_to_unfold_opt map_opt sets_opt rel_opt pred_opt
- {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds} = {
+fun add_to_unfold_opt map_opt sets_opt rel_opt
+ {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels} = {
map_unfolds = add_to_thms maps map_opt,
set_unfoldss = adds_to_thms setss sets_opt,
- rel_unfolds = add_to_thms rels rel_opt,
- pred_unfolds = add_to_thms preds pred_opt};
+ rel_unfolds = add_to_thms rels rel_opt};
-fun add_to_unfold map sets rel pred =
- add_to_unfold_opt (SOME map) (SOME sets) (SOME rel) (SOME pred);
+fun add_to_unfold map sets rel = add_to_unfold_opt (SOME map) (SOME sets) (SOME rel);
val map_unfolds_of = #map_unfolds;
val set_unfoldss_of = #set_unfoldss;
val rel_unfolds_of = #rel_unfolds;
-val pred_unfolds_of = #pred_unfolds;
val bdTN = "bdT";
@@ -73,10 +67,7 @@
fun mk_permuteN src dest =
"_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
-val no_thm = refl;
-val Collect_split_box_equals = box_equals RS @{thm Collect_split_cong};
-val abs_pred_sym = sym RS @{thm abs_pred_def};
-val abs_pred_sym_pred_abs = abs_pred_sym RS @{thm pred_def_abs};
+val subst_rel_def = @{thm subst_rel_def};
(*copied from Envir.expand_term_free*)
fun expand_term_const defs =
@@ -111,9 +102,10 @@
(Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
val Bss_repl = replicate olive Bs;
- val (((fs', Asets), xs), _(*names_lthy*)) = lthy
+ val ((((fs', Rs'), Asets), xs), _(*names_lthy*)) = lthy
|> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs)
- ||>> mk_Frees "A" (map (HOLogic.mk_setT) As)
+ ||>> apfst snd o mk_Frees' "R" (map2 (curry mk_relT) As Bs)
+ ||>> mk_Frees "A" (map HOLogic.mk_setT As)
||>> mk_Frees "x" As;
val CAs = map3 mk_T_of_bnf Dss Ass_repl inners;
@@ -129,6 +121,11 @@
(Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
mk_map_of_bnf Ds As Bs) Dss inners));
+ (*%R1 ... Rn. outer.rel (inner_1.rel R1 ... Rn) ... (inner_m.rel R1 ... Rn)*)
+ val rel = fold_rev Term.abs Rs'
+ (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer,
+ map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
+ mk_rel_of_bnf Ds As Bs) Dss inners));
(*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
(*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
@@ -185,7 +182,7 @@
val set_alt_thms =
if ! quick_and_dirty then
- replicate ilive no_thm
+ []
else
map (fn goal =>
Skip_Proof.prove lthy [] [] goal
@@ -233,8 +230,21 @@
fun map_wpull_tac _ =
mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
- val tacs = [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];
+ fun rel_O_Gr_tac _ =
+ let
+ val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
+ val outer_rel_cong = rel_cong_of_bnf outer;
+ in
+ rtac (trans OF [in_alt_thm RS 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) 1
+ end
+
+ val tacs = zip_goals 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;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -259,25 +269,8 @@
bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
(((((b, mapx), sets), bd), wits), rel) lthy;
- val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
- val outer_rel_cong = rel_cong_of_bnf outer;
-
- val rel_unfold_thm =
- trans OF [rel_O_Gr_of_bnf bnf',
- 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)]]]];
-
- val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
- pred_def_of_bnf bnf' RS abs_pred_sym,
- trans OF [outer_rel_cong OF (map (fn bnf => pred_def_of_bnf bnf RS abs_pred_sym) inners),
- pred_def_of_bnf outer RS abs_pred_sym]];
-
- val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
- pred_unfold_thm unfold;
+ val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
+ unfold;
in
(bnf', (unfold', lthy'))
end;
@@ -301,7 +294,7 @@
(Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
val ((Asets, lives), _(*names_lthy*)) = lthy
- |> mk_Frees "A" (map (HOLogic.mk_setT) (drop n As))
+ |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
||>> mk_Frees "x" (drop n As);
val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
@@ -309,6 +302,8 @@
(*bnf.map id ... id*)
val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
+ (*bnf.rel Id ... Id*)
+ val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map Id_const killedAs);
val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
val sets = drop n bnf_sets;
@@ -345,8 +340,21 @@
(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);
- val tacs = [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];
+ fun rel_O_Gr_tac _ =
+ let
+ val rel_Gr = rel_Gr_of_bnf bnf RS sym
+ in
+ rtac (trans OF [in_alt_thm RS 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
+ (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
+ replicate (live - n) @{thm Gr_fst_snd})]]] RS sym) 1
+ end;
+
+ val tacs = zip_goals 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;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -357,26 +365,10 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
- ((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
-
- val rel_Gr = rel_Gr_of_bnf bnf RS sym;
+ (((((b, mapx), sets), Term.absdummy T bd), wits), rel) lthy;
- val rel_unfold_thm =
- trans OF [rel_O_Gr_of_bnf bnf',
- 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
- (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
- replicate (live - n) @{thm Gr_fst_snd})]]]];
-
- val pred_unfold_thm = Collect_split_box_equals OF
- [Local_Defs.unfold lthy' @{thms Id_def'} rel_unfold_thm, pred_def_of_bnf bnf' RS abs_pred_sym,
- pred_def_of_bnf bnf RS abs_pred_sym];
-
- val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
- pred_unfold_thm unfold;
+ val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
+ unfold;
in
(bnf', (unfold', lthy'))
end;
@@ -400,13 +392,16 @@
(Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
val (Asets, _(*names_lthy*)) = lthy
- |> mk_Frees "A" (map (HOLogic.mk_setT) (newAs @ As));
+ |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
val T = mk_T_of_bnf Ds As bnf;
(*%f1 ... fn. bnf.map*)
val mapx =
fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
+ (*%R1 ... Rn. bnf.rel*)
+ val rel =
+ fold_rev Term.absdummy (map2 (curry mk_relT) newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
@@ -446,8 +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);
- val tacs = [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];
+ fun rel_O_Gr_tac _ =
+ rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
+
+ val tacs = zip_goals 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;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -455,17 +453,10 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
- ((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
-
- val rel_unfold_thm =
- trans OF [rel_O_Gr_of_bnf bnf',
- trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_O_Gr_of_bnf bnf RS sym]];
+ (((((b, mapx), sets), Term.absdummy T bd), wits), rel) lthy;
- val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
- pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
-
- val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
- pred_unfold_thm unfold;
+ val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
+ unfold;
in
(bnf', (unfold', lthy'))
end;
@@ -489,14 +480,16 @@
(Variable.invent_types (replicate live HOLogic.typeS) lthy2);
val (Asets, _(*names_lthy*)) = lthy
- |> mk_Frees "A" (map (HOLogic.mk_setT) (permute As));
+ |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
val T = mk_T_of_bnf Ds As bnf;
(*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
- (Term.list_comb (mk_map_of_bnf Ds As Bs bnf,
- permute_rev (map Bound ((live - 1) downto 0))));
+ (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0))));
+ (*%R(1) ... R(n). bnf.rel R\<sigma>(1) ... R\<sigma>(n)*)
+ val rel = fold_rev Term.absdummy (permute (map2 (curry mk_relT) As Bs))
+ (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0))));
val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
val sets = permute bnf_sets;
@@ -526,8 +519,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);
- val tacs = [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];
+ fun rel_O_Gr_tac _ =
+ rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
+
+ val tacs = zip_goals 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;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -535,17 +531,10 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
- ((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
-
- val rel_unfold_thm =
- trans OF [rel_O_Gr_of_bnf bnf',
- trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_O_Gr_of_bnf bnf RS sym]];
+ (((((b, mapx), sets), Term.absdummy T bd), wits), rel) lthy;
- val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
- pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
-
- val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
- pred_unfold_thm unfold;
+ val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
+ unfold;
in
(bnf', (unfold', lthy'))
end;
@@ -619,13 +608,16 @@
val (Bs, _) = apfst (map TFree)
(Variable.invent_types (replicate live HOLogic.typeS) lthy1);
- val map_unfolds = filter_refl (map_unfolds_of unfold);
- val set_unfoldss = map filter_refl (set_unfoldss_of unfold);
+ val map_unfolds = filter_out_refl (map_unfolds_of unfold);
+ val set_unfoldss = map filter_out_refl (set_unfoldss_of unfold);
+ val rel_unfolds = filter_out_refl (rel_unfolds_of unfold);
val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
map_unfolds);
val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of))
set_unfoldss);
+ val expand_rels = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
+ rel_unfolds);
val unfold_maps = fold (Local_Defs.unfold lthy o single) map_unfolds;
val unfold_sets = fold (Local_Defs.unfold lthy) set_unfoldss;
val unfold_defs = unfold_sets o unfold_maps;
@@ -633,6 +625,7 @@
val bnf_sets = map (expand_maps o expand_sets)
(mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
val bnf_bd = mk_bd_of_bnf Ds As bnf;
+ val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf);
val T = mk_T_of_bnf Ds As bnf;
(*bd should only depend on dead type variables!*)
@@ -667,11 +660,11 @@
fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN'
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
- val tacs =
- map mk_tac ([map_id_of_bnf bnf, map_comp_of_bnf bnf, map_cong_of_bnf bnf] @
- set_natural_of_bnf bnf) @
- map K [rtac bd_card_order 1, rtac bd_cinfinite 1] @
- map mk_tac (set_bds @ [in_bd, map_wpull_of_bnf bnf]);
+
+ val tacs = zip_goals (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
+ (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 (rel_O_Gr_of_bnf bnf));
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -680,40 +673,15 @@
val policy = user_policy Derive_All_Facts;
val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
- ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
-
- val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
- val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs';
-
- val rel_O_Gr = unfold_defs' (rel_O_Gr_of_bnf bnf');
- val rel_unfold = Local_Defs.unfold lthy'
- (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_O_Gr;
-
- val unfold_defs'' = unfold_defs' o Local_Defs.unfold lthy' (filter_refl [rel_O_Gr_of_bnf bnf']);
-
- val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs);
- val pred_unfold = Local_Defs.unfold lthy'
- (map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def;
-
- val notes =
- [(rel_unfoldN, [rel_unfold]),
- (pred_unfoldN, [pred_unfold])]
- |> map (fn (thmN, thms) =>
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+ (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), bnf_rel) lthy;
in
- ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
+ ((bnf', deads), lthy')
end;
val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
-val ID_rel_O_Gr = rel_O_Gr_of_bnf ID_bnf;
-val ID_rel_O_Gr' = ID_rel_O_Gr RS sym;
-val ID_pred_def' = Local_Defs.unfold @{context} [ID_rel_O_Gr] (pred_def_of_bnf ID_bnf) RS sym;
-
-fun bnf_of_typ _ _ _ (T as TFree _) (unfold, lthy) =
- ((ID_bnf, ([], [T])),
- (add_to_unfold_opt NONE NONE (SOME ID_rel_O_Gr') (SOME ID_pred_def') unfold, lthy))
+fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
| bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
| bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
let
@@ -732,10 +700,7 @@
val deads_lives =
pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
(deads, lives);
- val rel_O_Gr = rel_O_Gr_of_bnf bnf;
- val unfold' = add_to_unfold_opt NONE NONE (SOME (rel_O_Gr RS sym))
- (SOME (Local_Defs.unfold lthy [rel_O_Gr] (pred_def_of_bnf bnf) RS sym)) unfold;
- in ((bnf, deads_lives), (unfold', lthy)) end
+ in ((bnf, deads_lives), (unfold, lthy)) end
else
let
val name = Long_Name.base_name C;
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:48 2012 +0200
@@ -27,8 +27,6 @@
val relN: string
val predN: string
val mk_setN: int -> string
- val rel_unfoldN: string
- val pred_unfoldN: string
val map_of_bnf: BNF -> term
@@ -79,6 +77,9 @@
val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
val wits_of_bnf: BNF -> nonemptiness_witness list
+ val filter_out_refl: thm list -> thm list
+ val zip_goals: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
+
datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
datatype fact_policy =
Derive_Some_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms
@@ -91,10 +92,6 @@
({prems: thm list, context: Proof.context} -> tactic) -> typ list option ->
((((binding * term) * term list) * term) * term list) * term -> local_theory ->
BNF * local_theory
-
- val filter_refl: thm list -> thm list
- val bnf_def_cmd: ((((binding * string) * string list) * string) * string list) * string ->
- local_theory -> Proof.state
end;
structure BNF_Def : BNF_DEF =
@@ -478,8 +475,6 @@
fun mk_witN i = witN ^ nonzero_string_of_int i;
val relN = "rel";
val predN = "pred";
-val rel_unfoldN = relN ^ "_unfold";
-val pred_unfoldN = predN ^ "_unfold";
val bd_card_orderN = "bd_card_order";
val bd_cinfiniteN = "bd_cinfinite";
@@ -529,8 +524,10 @@
handle TERM _ => false
end;
-val filter_refl = filter_out is_reflexive;
+val filter_out_refl = filter_out is_reflexive;
+fun zip_goals mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
+ [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
(* Define new BNFs *)
@@ -577,10 +574,9 @@
in map2 pair bs wit_rhss end;
val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
- fun maybe_define needed_for_extra_facts (b, rhs) lthy =
+ fun maybe_define (b, rhs) lthy =
let
val inline =
- (not needed_for_extra_facts orelse fact_policy = Derive_Some_Facts) andalso
(case const_policy of
Dont_Inline => false
| Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
@@ -601,17 +597,16 @@
(bnf_set_terms, raw_set_defs)),
(bnf_bd_term, raw_bd_def)),
(bnf_wit_terms, raw_wit_defs)),
- (bnf_rel_term, raw_rel_def)), (lthy', lthy)) =
+ (bnf_rel_term, raw_rel_def)), (lthy1, lthy0)) =
no_defs_lthy
- |> maybe_define false map_bind_def
- ||>> apfst split_list o fold_map (maybe_define false) set_binds_defs
- ||>> maybe_define false bd_bind_def
- ||>> apfst split_list o fold_map (maybe_define false) wit_binds_defs
- ||>> maybe_define false rel_bind_def
+ |> maybe_define map_bind_def
+ ||>> apfst split_list o fold_map maybe_define set_binds_defs
+ ||>> maybe_define bd_bind_def
+ ||>> apfst split_list o fold_map maybe_define wit_binds_defs
+ ||>> maybe_define rel_bind_def
||> `(maybe_restore no_defs_lthy);
- (*transforms defined frees into consts (and more)*)
- val phi = Proof_Context.export_morphism lthy lthy';
+ val phi = Proof_Context.export_morphism lthy0 lthy1;
val bnf_map_def = Morphism.thm phi raw_map_def;
val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;
@@ -620,12 +615,7 @@
val bnf_rel_def = Morphism.thm phi raw_rel_def;
val one_step_defs =
- filter_refl (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
-
- val _ = case map_filter (try dest_Free)
- (bnf_map_term :: bnf_set_terms @ [bnf_bd_term] @ bnf_wit_terms) of
- [] => ()
- | frees => Proof_Display.print_consts true lthy (K false) frees;
+ filter_out_refl (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
val bnf_map = Morphism.term phi bnf_map_term;
@@ -659,7 +649,7 @@
(*TODO: check type of bnf_rel*)
val ((((((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), domTs), ranTs), ranTs'), ranTs''),
- (Ts, T)) = lthy'
+ (Ts, T)) = lthy1
|> mk_TFrees live
||>> mk_TFrees live
||>> mk_TFrees live
@@ -679,7 +669,7 @@
fun mk_bnf_t As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
fun mk_bnf_T As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
- fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy setRTs CA' CB' bnf_rel;
+ fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy1 setRTs CA' CB' bnf_rel;
val (setRTs, RTs) = map_split (`HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Bs');
val setRTsAsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Cs);
@@ -705,7 +695,7 @@
val ((((((((((((((((((((((((fs, fs_copy), gs), hs), (x, x')), (y, y')), (z, z')), zs), As),
As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), Rs), Rs_copy), Ss),
- (Qs, Qs')), _) = lthy'
+ (Qs, Qs')), _) = lthy1
|> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
||>> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
@@ -737,23 +727,31 @@
Qs As' Bs')));
val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs);
- val ((bnf_pred_term, raw_pred_def), (lthy''', lthy'')) =
- lthy
- |> maybe_define true pred_bind_def
- ||> `(maybe_restore lthy');
+ val ((bnf_pred_term, raw_pred_def), (lthy3, lthy2)) =
+ lthy1
+ |> maybe_define pred_bind_def
+ ||> `(maybe_restore lthy1);
- val phi = Proof_Context.export_morphism lthy'' lthy''';
- val bnf_pred = Morphism.term phi bnf_pred_term;
+ val _ = case filter_out_refl (raw_map_def :: raw_set_defs @ [raw_bd_def] @
+ raw_wit_defs @ [raw_rel_def, raw_pred_def]) of
+ [] => ()
+ | defs => Proof_Display.print_consts true lthy2 (K false)
+ (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
- fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy''' QTs CA' CB' bnf_pred;
+ val phi = Proof_Context.export_morphism lthy2 lthy3;
- val pred = mk_bnf_pred QTs CA' CB';
val bnf_pred_def =
if fact_policy <> Derive_Some_Facts then
mk_unabs_def (live + 2) (Morphism.thm phi raw_pred_def RS meta_eq_to_obj_eq)
else
no_fact;
+ val bnf_pred = Morphism.term phi bnf_pred_term;
+
+ fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy3 QTs CA' CB' bnf_pred;
+
+ val pred = mk_bnf_pred QTs CA' CB';
+
val goal_map_id =
let
val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As');
@@ -857,10 +855,8 @@
fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (relAsBs, Rs), rhs))
end;
- val goals =
- [goal_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];
+ val goals = zip_goals goal_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;
fun mk_wit_goals (I, wit) =
let
@@ -1162,24 +1158,30 @@
I))
end;
in
- (key, goals, wit_goalss, after_qed, lthy''', one_step_defs)
+ (key, goals, wit_goalss, after_qed, lthy3, one_step_defs)
end;
fun register_bnf key (bnf, lthy) =
(bnf, Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) lthy);
+(* TODO: Once the invariant "nwits > 0" holds, remove "mk_conjunction_balanced'" and "rtac TrueI"
+ below *)
+fun mk_conjunction_balanced' [] = @{prop True}
+ | mk_conjunction_balanced' ts = Logic.mk_conjunction_balanced ts;
+
fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
(fn (_, goals, wit_goalss, after_qed, lthy, defs) =>
let
- val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac;
- val wit_goals = wit_goalss |> map Logic.mk_conjunction_balanced;
- val wit_goal = Logic.mk_conjunction_balanced wit_goals;
+ val wits_tac =
+ K (TRYALL Goal.conjunction_tac) THEN' K (TRYALL (rtac TrueI)) THEN'
+ unfold_defs_tac lthy defs wit_tac;
+ val wit_goals = map mk_conjunction_balanced' wit_goalss;
val wit_thms =
- Skip_Proof.prove lthy [] [] wit_goal wits_tac
+ Skip_Proof.prove lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
- |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0))
+ |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
in
map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
goals (map (unfold_defs_tac lthy defs) tacs)
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Sep 20 02:42:48 2012 +0200
@@ -53,10 +53,12 @@
val nchotomyN: string
val pred_coinductN: string
val pred_coinduct_uptoN: string
+ val pred_simpN: string
val recN: string
val recsN: string
val rel_coinductN: string
val rel_coinduct_uptoN: string
+ val rel_simpN: string
val rvN: string
val sel_coitersN: string
val sel_corecsN: string
@@ -129,8 +131,6 @@
val mk_sum_casesN: int -> int -> thm
val mk_sum_casesN_balanced: int -> int -> thm
- val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
-
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
@@ -223,6 +223,9 @@
val unf_coinductN = unfN ^ "_" ^ coinductN
val rel_coinductN = relN ^ "_" ^ coinductN
val pred_coinductN = predN ^ "_" ^ coinductN
+val simpN = "_simp";
+val rel_simpN = relN ^ simpN;
+val pred_simpN = predN ^ simpN;
val uptoN = "upto"
val unf_coinduct_uptoN = unf_coinductN ^ "_" ^ uptoN
val rel_coinduct_uptoN = rel_coinductN ^ "_" ^ uptoN
@@ -364,9 +367,6 @@
Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)},
right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k;
-fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull =
- [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull];
-
(* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:48 2012 +0200
@@ -2669,8 +2669,13 @@
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 tacss = map9 mk_tactics 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;
+ (* ### *)
+ fun rel_O_Gr_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
+
+ val rel_O_gr_tacs = replicate n rel_O_Gr_tac;
+
+ val tacss = map10 zip_goals 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;
val (hset_unf_incl_thmss, hset_hset_unf_incl_thmsss, hset_induct_thms) =
let
@@ -2859,7 +2864,7 @@
val (Jbnfs, lthy) =
fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => fn lthy =>
bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads)
- ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
+ (((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits), @{term True}(*###*)) lthy
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
@@ -2894,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 Jrel_unfold_thms =
+ val Jrel_simp_thms =
let
fun mk_goal Jz Jz' unf unf' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs)
(mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
@@ -2905,23 +2910,23 @@
fn map_simp => fn set_simps => fn unf_inject => fn unf_fld =>
fn set_naturals => fn set_incls => fn set_set_inclss =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
+ (K (mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
unf_inject unf_fld 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'
unf_inject_thms unf_fld_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
end;
- val Jpred_unfold_thms =
+ val Jpred_simp_thms =
let
fun mk_goal Jz Jz' unf unf' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
(mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz')));
val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis;
in
- map3 (fn goal => fn pred_def => fn Jrel_unfold =>
- Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Jpred_defs Jrel_unfold)
+ map3 (fn goal => fn pred_def => fn Jrel_simp =>
+ Skip_Proof.prove lthy [] [] goal (mk_pred_simp_tac pred_def Jpred_defs Jrel_simp)
|> Thm.close_derivation)
- goals pred_defs Jrel_unfold_thms
+ goals pred_defs Jrel_simp_thms
end;
val timer = time (timer "additional properties");
@@ -2938,8 +2943,8 @@
[(map_simpsN, map single folded_map_simp_thms),
(set_inclN, set_incl_thmss),
(set_set_inclN, map flat set_set_incl_thmsss),
- (rel_unfoldN, map single Jrel_unfold_thms),
- (pred_unfoldN, map single Jpred_unfold_thms)] @
+ (rel_simpN, map single Jrel_simp_thms),
+ (pred_simpN, map single Jpred_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 =>
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Sep 20 02:42:48 2012 +0200
@@ -90,7 +90,7 @@
val mk_rel_coinduct_tac: 'a list -> thm -> thm -> tactic
val mk_rel_coinduct_upto_tac: int -> ctyp option list -> cterm option list -> thm -> thm list ->
thm list -> tactic
- val mk_rel_unfold_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
+ 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
@@ -1499,7 +1499,7 @@
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
-fun mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps unf_inject unf_fld
+fun mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps unf_inject unf_fld
set_naturals set_incls set_set_inclss =
let
val m = length set_incls;
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:48 2012 +0200
@@ -1670,8 +1670,13 @@
in_incl_min_alg_thms card_of_min_alg_thms;
val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
- val tacss = map9 mk_tactics 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;
+ (* ### *)
+ fun rel_O_Gr_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
+
+ val rel_O_gr_tacs = replicate n rel_O_Gr_tac;
+
+ val tacss = map10 zip_goals 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;
val fld_witss =
let
@@ -1705,7 +1710,7 @@
val (Ibnfs, lthy) =
fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => fn lthy =>
bnf_def Dont_Inline policy I tacs wit_tac (SOME deads)
- ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
+ (((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits), @{term True}(*###*)) lthy
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
@@ -1739,7 +1744,7 @@
val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
- val Irel_unfold_thms =
+ val Irel_simp_thms =
let
fun mk_goal xF yF fld fld' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs)
(mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
@@ -1750,23 +1755,23 @@
fn map_simp => fn set_simps => fn fld_inject => fn fld_unf =>
fn set_naturals => fn set_incls => fn set_set_inclss =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_rel_unfold_tac in_Irels i in_rel map_comp map_cong map_simp set_simps
+ (K (mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps
fld_inject fld_unf 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'
fld_inject_thms fld_unf_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
end;
- val Ipred_unfold_thms =
+ val Ipred_simp_thms =
let
fun mk_goal xF yF fld fld' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
(mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF));
val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
in
- map3 (fn goal => fn pred_def => fn Irel_unfold =>
- Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Ipred_defs Irel_unfold)
+ map3 (fn goal => fn pred_def => fn Irel_simp =>
+ Skip_Proof.prove lthy [] [] goal (mk_pred_simp_tac pred_def Ipred_defs Irel_simp)
|> Thm.close_derivation)
- goals pred_defs Irel_unfold_thms
+ goals pred_defs Irel_simp_thms
end;
val timer = time (timer "additional properties");
@@ -1782,8 +1787,8 @@
[(map_simpsN, map single folded_map_simp_thms),
(set_inclN, set_incl_thmss),
(set_set_inclN, map flat set_set_incl_thmsss),
- (rel_unfoldN, map single Irel_unfold_thms),
- (pred_unfoldN, map single Ipred_unfold_thms)] @
+ (rel_simpN, map single Irel_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) =>
map2 (fn b => fn thms =>
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Thu Sep 20 02:42:48 2012 +0200
@@ -61,7 +61,7 @@
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_unfold_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm ->
+ 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
@@ -774,7 +774,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_rel_unfold_tac in_Irels i in_rel map_comp map_cong map_simp set_simps fld_inject
+fun mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps fld_inject
fld_unf set_naturals set_incls set_set_inclss =
let
val m = length set_incls;
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Thu Sep 20 02:42:48 2012 +0200
@@ -24,7 +24,7 @@
val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
val mk_Abs_inj_thm: thm -> thm
- val mk_pred_unfold_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_pred_simp_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
val mk_map_comp_id_tac: thm -> tactic
val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
@@ -91,14 +91,12 @@
gen_tac
end;
-fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} =
+fun mk_pred_simp_tac pred_def pred_defs rel_simp {context = ctxt, prems = _} =
Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN
- rtac rel_unfold 1;
+ rtac rel_simp 1;
fun mk_map_comp_id_tac map_comp =
- (rtac trans THEN' rtac map_comp) 1 THEN
- REPEAT_DETERM (stac @{thm o_id} 1) THEN
- rtac refl 1;
+ (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} =
EVERY' [rtac mp, rtac map_cong,