--- a/src/HOL/BNF_FP_Base.thy Tue Jun 24 12:36:45 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy Tue Jun 24 13:48:14 2014 +0200
@@ -83,6 +83,9 @@
"setr (Inr x) = {x}"
unfolding sum_set_defs by simp+
+lemma Inl_Inr_False: "(Inl x = Inr y) = False"
+ by simp
+
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
by blast
--- a/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 24 12:36:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Jun 24 13:48:14 2014 +0200
@@ -85,6 +85,7 @@
val mk_rel: int -> typ list -> typ list -> term -> term
val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term
val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term
+ val build_rel': Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list ->
'a list
@@ -533,10 +534,12 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
-fun build_map_or_rel mk const of_bnf dest ctxt build_simple =
+fun build_map_or_rel mk const of_bnf dest blacklist ctxt build_simple =
let
fun build (TU as (T, U)) =
- if T = U then
+ if exists (curry (op =) T) blacklist then
+ build_simple TU
+ else if T = U andalso not (exists_subtype_in blacklist T) then
const T
else
(case TU of
@@ -553,8 +556,9 @@
| _ => build_simple TU);
in build end;
-val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT;
-val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
+val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT [];
+val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T [];
+fun build_rel' ctxt blacklist = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T blacklist ctxt;
fun map_flattened_map_args ctxt s map_args fs =
let
@@ -1284,7 +1288,7 @@
(mk_Ball (setA $ x) (Term.absfree (dest_Free a)
(mk_Ball (setB $ y) (Term.absfree (dest_Free b)
(HOLogic.mk_imp (R $ a $ b, S $ a $ b))))));
- val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) ::
+ val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) ::
map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y);
in
@@ -1399,7 +1403,7 @@
|> 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));
- val (mk_wit_thms, nontriv_wit_goals) =
+ val (mk_wit_thms, nontriv_wit_goals) =
(case triv_tac_opt of
NONE => (fn _ => [], map (map (rpair [])) wit_goalss)
| SOME tac => (mk_triv_wit_thms tac, []));
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 24 12:36:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 24 13:48:14 2014 +0200
@@ -597,6 +597,92 @@
(rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
end;
+fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs ctr_sugars abs_inverses abs_injects
+ ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct =
+ let
+ val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts
+
+ val (Rs, IRs, fpAs, fpBs, names_lthy) =
+ let
+ val fp_names = map base_name_of_typ fpA_Ts;
+ val ((((Rs, IRs), fpAs_names), fpBs_names), names_lthy) = lthy
+ |> mk_Frees "R" (map2 mk_pred2T As Bs)
+ ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts)
+ ||>> Variable.variant_fixes fp_names
+ ||>> Variable.variant_fixes (map (suffix "'") fp_names);
+ in
+ (Rs, IRs,
+ map2 (curry Free) fpAs_names fpA_Ts,
+ map2 (curry Free) fpBs_names fpB_Ts, names_lthy)
+ end;
+
+ val ((discA_tss, selA_tsss), (discB_tss, selB_tsss)) =
+ let
+ val discss = map #discs ctr_sugars;
+ val selsss = map #selss ctr_sugars;
+ fun mk_discss ts Ts = map2 (map o rapp) ts (map (map (mk_disc_or_sel Ts)) discss);
+ fun mk_selsss ts Ts = map2 (map o map o rapp) ts (map (map (map (mk_disc_or_sel Ts)))
+ selsss);
+ in
+ ((mk_discss fpAs As, mk_selsss fpAs As)
+ ,(mk_discss fpBs Bs, mk_selsss fpBs Bs))
+ end;
+
+ fun choose_relator (A, B) = the (find_first (fn t =>
+ let
+ val T = fastype_of t
+ val arg1T = domain_type T;
+ val arg2T = domain_type (range_type T);
+ in
+ A = arg1T andalso B = arg2T
+ end) (Rs @ IRs));
+
+ val premises =
+ let
+ fun build_the_rel A B = build_rel' lthy fpA_Ts choose_relator (A, B);
+
+ fun build_rel_app selA_t selB_t =
+ (build_the_rel (fastype_of selA_t) (fastype_of selB_t )) $ selA_t $ selB_t
+
+ fun mk_prem_ctr_concls n k discA_t selA_ts discB_t selB_ts =
+ (if k = n then [] else [HOLogic.mk_eq (discA_t, discB_t)]) @
+ (case (selA_ts, selB_ts) of
+ ([],[]) => []
+ | (_ :: _, _ :: _) =>
+ [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [discA_t, discB_t],
+ Library.foldr1 HOLogic.mk_conj (map2 build_rel_app selA_ts selB_ts))]);
+
+ fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss =
+ Library.foldr1 HOLogic.mk_conj (flat (map5 (mk_prem_ctr_concls n)
+ (1 upto n) discA_ts selA_tss discB_ts selB_tss))
+ handle List.Empty => @{term True};
+
+ fun mk_prem IR tA tB n discA_ts selA_tss discB_ts selB_tss =
+ fold_rev Logic.all [tA, tB] (Logic.mk_implies (HOLogic.mk_Trueprop (IR $ tA $ tB),
+ HOLogic.mk_Trueprop (mk_prem_concl n discA_ts selA_tss discB_ts selB_tss)));
+ in
+ map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
+ end;
+
+ val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map2 mk_leq IRs (map (build_rel lthy choose_relator) (fpA_Ts ~~ fpB_Ts))));
+
+ fun string_of_list f Ts = "[" ^ (fold_rev (curry op ^) (separate ", " (map f Ts)) "") ^ "]"
+
+ (*
+ val _ = writeln ("Premises: " ^ string_of_list (Syntax.string_of_term names_lthy) premises)
+ val _ = writeln ("Goal: " ^ Syntax.string_of_term names_lthy goal)
+ val _ = writeln ("derive_rel_coinduct0_thm_for_types " ^ string_of_list (Syntax.string_of_typ names_lthy) fpA_Ts)
+ *)
+ in
+ Goal.prove_sorry lthy [] premises goal
+ (fn {context = ctxt, prems = prems} =>
+ mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
+ (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) (map (flat o #sel_thmss)
+ ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses)
+ |> singleton (Proof_Context.export names_lthy lthy)
+ end;
+
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
@@ -666,10 +752,12 @@
(1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss))
handle List.Empty => @{term True};
+ (* Probably the good premise *)
fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss =
fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss)));
+ (* Make a new conclusion (e.g. rel_concl) *)
val concl =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
@@ -946,7 +1034,7 @@
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_rec_thms, ...},
+ xtor_co_rec_thms, rel_xtor_co_induct_thm, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
(map dest_TFree killed_As) fp_eqs no_defs_lthy0
@@ -1481,6 +1569,10 @@
abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
(Proof_Context.export lthy' no_defs_lthy) lthy;
+ val rel_coinduct0_thm = derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs ctr_sugars
+ abs_inverses abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss
+ rel_xtor_co_induct_thm;
+
val sel_corec_thmss = map flat sel_corec_thmsss;
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
@@ -1493,7 +1585,7 @@
mapss rel_injectss rel_distinctss setss;
val common_notes =
- (if nn > 1 then
+ (rel_coinductN ^ "0", [rel_coinduct0_thm], []) :: (if nn > 1 then
[(coinductN, [coinduct_thm], common_coinduct_attrs),
(strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
else
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jun 24 12:36:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jun 24 13:48:14 2014 +0200
@@ -26,6 +26,9 @@
val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
+ val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
+ thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
+ thm list -> thm list -> tactic
val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
@@ -205,6 +208,27 @@
(1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
selsss));
+fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
+ dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses =
+ rtac dtor_rel_coinduct 1 THEN
+ EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
+ fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
+ (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
+ (dtac (rotate_prems (~1) ((cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct] @{thm
+ arg_cong2}) RS iffD1)) THEN'
+ atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'
+ REPEAT_DETERM o etac conjE))) 1 THEN
+ Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
+ sels @ @{thms simp_thms(6,7,8,11,12,15,16,22,24)}) THEN
+ Local_Defs.unfold_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
+ abs_inject :: ctor_defs @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps rel_prod_apply
+ vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject
+ simp_thms(6,7,8,11,12,15,16,22,24)}) THEN
+ REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
+ (rtac refl ORELSE' atac))))
+ cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
+ abs_inverses);
+
fun mk_sel_map_tac ctxt ct exhaust discs maps sels =
TRYALL Goal.conjunction_tac THEN
ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW