--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Jun 27 10:11:44 2014 +0200
@@ -61,6 +61,7 @@
val map_def_of_bnf: bnf -> thm
val map_id0_of_bnf: bnf -> thm
val map_id_of_bnf: bnf -> thm
+ val map_ident0_of_bnf: bnf -> thm
val map_ident_of_bnf: bnf -> thm
val map_transfer_of_bnf: bnf -> thm
val le_rel_OO_of_bnf: bnf -> thm
@@ -223,6 +224,7 @@
map_comp: thm lazy,
map_cong: thm lazy,
map_id: thm lazy,
+ map_ident0: thm lazy,
map_ident: thm lazy,
map_transfer: thm lazy,
rel_eq: thm lazy,
@@ -237,8 +239,8 @@
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
- inj_map map_comp map_cong map_id map_ident map_transfer rel_eq rel_flip set_map rel_cong
- rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
+ inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
+ rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
@@ -251,6 +253,7 @@
map_comp = map_comp,
map_cong = map_cong,
map_id = map_id,
+ map_ident0 = map_ident0,
map_ident = map_ident,
map_transfer = map_transfer,
rel_eq = rel_eq,
@@ -276,6 +279,7 @@
map_comp,
map_cong,
map_id,
+ map_ident0,
map_ident,
map_transfer,
rel_eq,
@@ -299,6 +303,7 @@
map_comp = Lazy.map f map_comp,
map_cong = Lazy.map f map_cong,
map_id = Lazy.map f map_id,
+ map_ident0 = Lazy.map f map_ident0,
map_ident = Lazy.map f map_ident,
map_transfer = Lazy.map f map_transfer,
rel_eq = Lazy.map f rel_eq,
@@ -418,6 +423,7 @@
val map_def_of_bnf = #map_def o #defs o rep_bnf;
val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
+val map_ident0_of_bnf = Lazy.force o #map_ident0 o #facts o rep_bnf;
val map_ident_of_bnf = Lazy.force o #map_ident o #facts o rep_bnf;
val map_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf;
val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf;
@@ -1104,6 +1110,7 @@
val in_cong = Lazy.lazy mk_in_cong;
val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
+ val map_ident0 = Lazy.lazy (fn () => mk_map_ident lthy (#map_id0 axioms));
val map_ident = Lazy.lazy (fn () => mk_map_ident lthy (Lazy.force map_id));
val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms));
@@ -1321,8 +1328,8 @@
val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
- in_mono in_rel inj_map map_comp map_cong map_id map_ident map_transfer rel_eq rel_flip
- set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
+ in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
+ rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
val wits = map2 mk_witness bnf_wits wit_thms;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jun 27 10:11:44 2014 +0200
@@ -456,9 +456,8 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
- val live_nesting_map_idents =
- map (unfold_thms lthy [id_def] o map_id0_of_bnf) live_nesting_bnfs;
- val fp_nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) fp_nesting_bnfs;
+ val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
+ val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -583,7 +582,7 @@
val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
val tacss = map4 (map ooo
- mk_rec_tac pre_map_defs (fp_nesting_map_idents @ live_nesting_map_idents) rec_defs)
+ mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs)
ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
fun prove goal tac =
@@ -736,8 +735,7 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
- val live_nesting_map_idents =
- map (unfold_thms lthy [id_def] o map_id0_of_bnf) live_nesting_bnfs;
+ val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -855,7 +853,7 @@
val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
val tacss =
- map4 (map ooo mk_corec_tac corec_defs live_nesting_map_idents)
+ map4 (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s)
ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss;
fun prove goal tac =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Jun 27 10:11:44 2014 +0200
@@ -98,15 +98,15 @@
@{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
case_unit_Unity} @ sumprod_thms_map;
-fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
+fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
- pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
+ pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map;
-fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
+fun mk_corec_tac corec_defs map_ident0s ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
let
- val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ corec_unfold_thms @
+ val ss = ss_only (pre_map_def :: abs_inverse :: map_ident0s @ corec_unfold_thms @
@{thms o_apply vimage2p_def if_True if_False}) ctxt;
in
unfold_thms_tac ctxt (ctr_def :: corec_defs) THEN
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200
@@ -80,7 +80,7 @@
disc_exhausts: thm list,
sel_defs: thm list,
fp_nesting_maps: thm list,
- fp_nesting_map_idents: thm list,
+ fp_nesting_map_ident0s: thm list,
fp_nesting_map_comps: thm list,
ctr_specs: corec_ctr_spec list};
@@ -466,8 +466,7 @@
{corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts,
sel_defs = sel_defs,
fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
- fp_nesting_map_idents =
- map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) fp_nesting_bnfs,
+ fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
sel_corecss};
@@ -1175,7 +1174,7 @@
|> single
end;
- fun prove_sel ({sel_defs, fp_nesting_maps, fp_nesting_map_idents, fp_nesting_map_comps,
+ fun prove_sel ({sel_defs, fp_nesting_maps, fp_nesting_map_ident0s, fp_nesting_map_comps,
ctr_specs, ...} : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
({fun_name, fun_T, fun_args, ctr, sel, rhs_term, code_rhs_opt, eqn_pos, ...}
: coeqn_data_sel) =
@@ -1198,7 +1197,7 @@
val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy rhs_term;
in
mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms fp_nesting_maps
- fp_nesting_map_idents fp_nesting_map_comps sel_corec k m excludesss
+ fp_nesting_map_ident0s fp_nesting_map_comps sel_corec k m excludesss
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
|> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Jun 27 10:11:44 2014 +0200
@@ -126,7 +126,7 @@
(etac FalseE ORELSE'
resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
-fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k
+fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k
m excludesss =
prelude_tac ctxt defs (fun_sel RS trans) THEN
cases_tac ctxt k m excludesss THEN
@@ -139,7 +139,7 @@
etac notE THEN' atac ORELSE'
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
- mapsx @ map_comps @ map_idents))) ORELSE'
+ mapsx @ map_ident0s @ map_comps))) ORELSE'
fo_rtac @{thm cong} ctxt ORELSE'
rtac @{thm ext}));
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Jun 27 10:11:44 2014 +0200
@@ -79,7 +79,7 @@
type rec_spec =
{recx: term,
- fp_nesting_map_idents: thm list,
+ fp_nesting_map_ident0s: thm list,
fp_nesting_map_comps: thm list,
ctr_specs: rec_ctr_spec list};
@@ -135,7 +135,7 @@
let
val thy = Proof_Context.theory_of lthy0;
- val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_idents, fp_nesting_map_comps,
+ val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_ident0s, fp_nesting_map_comps,
common_induct, n2m, lthy) =
get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
@@ -195,7 +195,7 @@
fun mk_spec ctr_offset
({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
{recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
- fp_nesting_map_idents = fp_nesting_map_idents, fp_nesting_map_comps = fp_nesting_map_comps,
+ fp_nesting_map_ident0s = fp_nesting_map_ident0s, fp_nesting_map_comps = fp_nesting_map_comps,
ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
in
((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts), lthy)
@@ -415,10 +415,10 @@
|> (fn [] => NONE | callss => SOME (ctr, callss))
end;
-fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
+fun mk_primrec_tac ctxt num_extra_args map_ident0s map_comps fun_defs recx =
unfold_thms_tac ctxt fun_defs THEN
HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
- unfold_thms_tac ctxt (nested_simps ctxt @ map_comps @ map_idents) THEN
+ unfold_thms_tac ctxt (nested_simps ctxt @ map_ident0s @ map_comps) THEN
HEADGOAL (rtac refl);
fun prepare_primrec nonexhaustive fixes specs lthy0 =
@@ -464,7 +464,7 @@
val defs = build_defs lthy nonexhaustive bs mxs funs_data rec_specs has_call;
- fun prove lthy' def_thms' ({ctr_specs, fp_nesting_map_idents, fp_nesting_map_comps, ...}
+ fun prove lthy' def_thms' ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...}
: rec_spec) (fun_data : eqn_data list) =
let
val js =
@@ -477,7 +477,7 @@
|> map_filter (try (fn (x, [y]) =>
(#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
|> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) =>
- mk_primrec_tac lthy' num_extra_args fp_nesting_map_idents fp_nesting_map_comps
+ mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
def_thms rec_thm
|> K |> Goal.prove_sorry lthy' [] [] user_eqn
(* for code extraction from proof terms: *)
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Jun 27 10:11:44 2014 +0200
@@ -47,12 +47,11 @@
val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss;
- val fp_nesting_map_idents =
- map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) fp_nesting_bnfs;
+ val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
in
(missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
- fp_nesting_map_idents, fp_nesting_map_comps, common_induct, is_some lfp_sugar_thms, lthy)
+ fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, is_some lfp_sugar_thms, lthy)
end;
exception NOT_A_MAP of term;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 10:11:44 2014 +0200
@@ -66,12 +66,13 @@
val rec_o_map_simp_thms =
@{thms o_def id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
-fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_idents abs_inverses ctor_rec_o_map =
+fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
+ ctor_rec_o_map =
unfold_thms_tac ctxt [rec_def] THEN
HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN
PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN
HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @
- distinct Thm.eq_thm_prop (live_nesting_map_idents @ abs_inverses) @ rec_o_map_simp_thms) ctxt));
+ distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simp_thms) ctxt));
val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
@@ -258,7 +259,7 @@
let
val pre_bnfs = map #pre_bnf fp_sugars;
val pre_map_defs = map map_def_of_bnf pre_bnfs;
- val live_nesting_map_idents = map map_ident_of_bnf live_nesting_bnfs;
+ val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
val rec_defs = map #co_rec_def fp_sugars;
@@ -303,7 +304,7 @@
val rec_o_map_thms =
map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
- mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_idents abs_inverses
+ mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
ctor_rec_o_map)
|> Thm.close_derivation)
rec_o_map_goals rec_defs ctor_rec_o_maps;
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Jun 27 10:11:44 2014 +0200
@@ -36,14 +36,14 @@
fun mk_pred pred_def args T =
let
- val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
+ val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
|> head_of |> fst o dest_Const
val argsT = map fastype_of args
in
list_comb (Const (pred_name, argsT ---> (T --> HOLogic.boolT)), args)
end
-fun mk_eq_onp arg =
+fun mk_eq_onp arg =
let
val argT = domain_type (fastype_of arg)
in
@@ -75,17 +75,17 @@
fun mk_relation_constraint name arg =
(Const (name, fastype_of arg --> HOLogic.boolT)) $ arg
-fun side_constraint_tac bnf constr_defs ctxt i =
+fun side_constraint_tac bnf constr_defs ctxt i =
let
val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf,
rel_OO_of_bnf bnf]
- in
+ in
(SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf)
THEN_ALL_NEW atac) i
end
-fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
- (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
+fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
+ (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i
fun generate_relation_constraint_goal ctxt bnf constraint_def =
@@ -97,7 +97,7 @@
|> mk_TFrees live
||>> mk_TFrees live
||>> mk_TFrees (dead_of_bnf bnf)
-
+
val relator = mk_rel_of_bnf Ds As Bs bnf
val relsT = map2 mk_pred2T As Bs
val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
@@ -112,7 +112,7 @@
let
val old_ctxt = ctxt
val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove ctxt [] [] goal
(fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1)
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
@@ -122,7 +122,7 @@
let
val old_ctxt = ctxt
val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove ctxt [] [] goal
(fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1)
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
@@ -136,11 +136,11 @@
val transfer_attr = @{attributes [transfer_rule]}
val Tname = base_name_of_bnf bnf
fun qualify suffix = Binding.qualified true suffix Tname
-
+
val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs
- val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
+ val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
[snd (nth defs 0), snd (nth defs 1)]
- val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
+ val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
[snd (nth defs 2), snd (nth defs 3)]
val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs
val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs
@@ -174,7 +174,7 @@
val head = Free (Binding.name_of pred_name, headT)
val lhs = list_comb (head, args)
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
- val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)),
+ val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)),
((Binding.empty, []), def)) lthy
in
(pred_def, lthy)
@@ -185,19 +185,19 @@
val n = live_of_bnf bnf
val set_map's = set_map_of_bnf bnf
in
- EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
+ EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
in_rel_of_bnf bnf, pred_def]), rtac iffI,
REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
- etac @{thm DomainPI}]) set_map's,
- REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
+ etac @{thm DomainPI}]) set_map's,
+ REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
map_id_of_bnf bnf]),
REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
rtac @{thm fst_conv}]), rtac CollectI,
- CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
+ CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's
] i
@@ -219,14 +219,14 @@
val lhs = mk_Domainp (list_comb (relator, args))
val rhs = mk_pred pred_def (map mk_Domainp args) T
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove ctxt [] [] goal
(fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
end
fun pred_eq_onp_tac bnf pred_def ctxt i =
- (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp},
+ (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp},
@{thm Ball_Collect}, pred_def]) THEN' CONVERSION (subst_conv (map_id0_of_bnf bnf RS sym))
THEN' rtac (rel_Grp_of_bnf bnf)) i
@@ -244,7 +244,7 @@
val lhs = list_comb (relator, map mk_eq_onp args)
val rhs = mk_eq_onp (mk_pred pred_def args T)
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove ctxt [] [] goal
(fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1)
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
@@ -259,7 +259,7 @@
fun qualify defname suffix = Binding.qualified true suffix defname
val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
- val rel_eq_onp_internal = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
+ val rel_eq_onp_internal = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
(Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
rel_eq_onp
val pred_data = {rel_eq_onp = rel_eq_onp_internal}
@@ -279,7 +279,7 @@
let
val constr_notes = if dead_of_bnf bnf > 0 then []
else prove_relation_constraints bnf lthy
- val relator_eq_notes = if dead_of_bnf bnf > 0 then []
+ val relator_eq_notes = if dead_of_bnf bnf > 0 then []
else relator_eq bnf
val (pred_notes, lthy) = predicator bnf lthy
in
@@ -299,8 +299,8 @@
fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
let
val involved_types = distinct op= (
- map type_name_of_bnf (#nested_bnfs fp_sugar)
- @ map type_name_of_bnf (#nesting_bnfs fp_sugar)
+ map type_name_of_bnf (#fp_nesting_bnfs fp_sugar)
+ @ map type_name_of_bnf (#live_nesting_bnfs fp_sugar)
@ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
val live = live_of_bnf (bnf_of_fp_sugar fp_sugar)
@@ -326,10 +326,10 @@
in
thm
|> Drule.instantiate' cTs cts
- |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
+ |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
(Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
|> Local_Defs.unfold lthy eq_onps
- |> (fn thm => if conjuncts <> [] then @{thm box_equals}
+ |> (fn thm => if conjuncts <> [] then @{thm box_equals}
OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj conjuncts |> kill_True]
else thm RS (@{thm eq_onp_same_args} RS iffD1))
|> kill_top