--- a/src/HOL/Datatype_Examples/Cyclic_List.thy Mon Feb 24 20:57:29 2020 +0100
+++ b/src/HOL/Datatype_Examples/Cyclic_List.thy Mon Feb 24 21:46:45 2020 +0100
@@ -34,10 +34,9 @@
by(unfold_locales)
(auto dest: retract_cyclic1 cyclic_set_eq simp add: list.in_rel list.rel_compp map_respect_cyclic[THEN rel_funD, OF refl] confluentp_cyclic1 intro: rtranclp_mono[THEN predicate2D, OF symclp_greater])
-lift_bnf 'a cyclic_list [wits: "[]"]
+lift_bnf 'a cyclic_list
subgoal by(rule confluent_quotient.subdistributivity[OF confluent_quotient_cyclic1])
subgoal by(force dest: cyclic_set_eq)
- subgoal by(auto elim: allE[where x="[]"])
done
end
--- a/src/HOL/Datatype_Examples/Dlist.thy Mon Feb 24 20:57:29 2020 +0100
+++ b/src/HOL/Datatype_Examples/Dlist.thy Mon Feb 24 21:46:45 2020 +0100
@@ -71,10 +71,9 @@
"confluent_quotient double dlist_eq dlist_eq dlist_eq dlist_eq dlist_eq (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set"
by(unfold_locales)(auto intro: strong_confluentp_imp_confluentp strong_confluentp_double dest: factor_double_map dlist_eq_into_doubles[THEN predicate2D] dlist_eq_set_eq simp add: list.in_rel list.rel_compp dlist_eq_map_respect equivp_dlist_eq equivp_imp_transp)
-lift_bnf 'a dlist [wits: "[]"]
+lift_bnf 'a dlist
subgoal for A B by(rule confluent_quotient.subdistributivity[OF confluent_quotient_dlist])
subgoal by(force dest: dlist_eq_set_eq intro: equivp_reflp[OF equivp_dlist_eq])
- subgoal by(auto simp add: dlist_eq_def vimage2p_def)
done
end
--- a/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy Mon Feb 24 20:57:29 2020 +0100
+++ b/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy Mon Feb 24 21:46:45 2020 +0100
@@ -256,10 +256,9 @@
"confluent_quotient cancel1\<inverse>\<inverse> eq eq eq eq eq (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set"
by(unfold_locales)(auto dest: retract_cancel1 eq_set_eq simp add: list.in_rel list.rel_compp map_respect_eq[THEN rel_funD, OF refl] semiconfluentp_imp_confluentp semiconfluentp_cancel1)+
-lift_bnf 'a fim [wits: "[]"]
+lift_bnf 'a fim
subgoal for A B by(rule confluent_quotient.subdistributivity[OF confluent_quotient_fim])
subgoal by(force dest: eq_set_eq)
- subgoal by(auto elim: allE[where x="[]"])
done
end
--- a/src/HOL/Datatype_Examples/LDL.thy Mon Feb 24 20:57:29 2020 +0100
+++ b/src/HOL/Datatype_Examples/LDL.thy Mon Feb 24 21:46:45 2020 +0100
@@ -328,7 +328,7 @@
quotient_type 'a ACI_rexp = "'a rexp" / "(\<approx>)"
unfolding ACIEQ_alt by (auto intro!: equivpI reflpI sympI transpI)
-lift_bnf (no_warn_wits) 'a ACI_rexp
+lift_bnf 'a ACI_rexp
unfolding ACIEQ_alt
subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACI])
subgoal for Ss by (intro eq_set_preserves_inter[rotated] ACIcl_set_eq; auto)
--- a/src/HOL/Datatype_Examples/Lift_BNF.thy Mon Feb 24 20:57:29 2020 +0100
+++ b/src/HOL/Datatype_Examples/Lift_BNF.thy Mon Feb 24 21:46:45 2020 +0100
@@ -186,7 +186,7 @@
quotient_type 'a cpy_list = "'a list" / "(=)"
by (rule identity_equivp)
-lift_bnf 'a cpy_list [wits: "[]"]
+lift_bnf 'a cpy_list
by (auto intro: list_all2_trans)
quotient_type ('a, 'b) funk = "('a \<Rightarrow> 'b)" / "\<lambda>f g. \<forall>a. f a = g a"
@@ -195,7 +195,7 @@
lemma funk_closure: "{(x, x'). \<forall>a. x a = x' a} `` {x. range x \<subseteq> A} = {x. range x \<subseteq> A}"
by auto
-lift_bnf (dead 'a, 'b) funk [wits: "\<lambda>b _.b :: 'b"]
+lift_bnf (dead 'a, 'b) funk
unfolding funk_closure rel_fun_def by (auto 0 10 split: if_splits)
lemma assumes "equivp REL"
--- a/src/HOL/Datatype_Examples/TLList.thy Mon Feb 24 20:57:29 2020 +0100
+++ b/src/HOL/Datatype_Examples/TLList.thy Mon Feb 24 21:46:45 2020 +0100
@@ -83,7 +83,7 @@
done
lift_bnf (tlset1: 'a, tlset2: 'b) tllist
- [wits: "\<lambda>b. (LNil :: 'a llist, b)" "\<lambda>a. (lconst a, undefined)" ]
+ [wits: "\<lambda>a. (lconst a, undefined)" ]
for map: tlmap rel: tlrel
subgoal for P Q P' Q'
by (force simp: eq_tllist_def relcompp_apply llist.rel_compp lfinite_lrel_eq split: if_splits)
@@ -93,10 +93,6 @@
apply (auto 0 0 simp: eq_tllist_def)
by metis
subgoal for x b
- by (auto simp: eq_tllist_def split: if_splits)
- subgoal for x b
- by (auto simp: eq_tllist_def split: if_splits)
- subgoal for x b
by (auto simp: eq_tllist_def llist.set_map dest: lset_lconst split: if_splits)
subgoal for x b
by (auto simp: eq_tllist_def sum_set_defs split: if_splits sum.splits)
--- a/src/HOL/Tools/BNF/bnf_lift.ML Mon Feb 24 20:57:29 2020 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Mon Feb 24 21:46:45 2020 +0100
@@ -140,9 +140,36 @@
val Iwits = the_default wits_F (Option.map (map (`(map (fn T =>
find_index (fn U => T = U) alphas) o binder_types_until_eq RepT o fastype_of))) wits);
+ val Iwits = if is_quotient then
+ let
+ val subsumed_Iwits =
+ filter (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) wits_F) Iwits;
+ val _ = if null subsumed_Iwits orelse exists (fn No_Warn_Wits => true | _ => false) opts
+ then ()
+ else
+ let
+ val (suffix1, suffix2, be) =
+ (if length subsumed_Iwits = 1 then ("", "", "is") else ("s", "es", "are"))
+ in
+ subsumed_Iwits
+ |> map (Syntax.pretty_typ lthy o fastype_of o snd)
+ |> Pretty.big_list
+ ("The following type" ^ suffix1 ^ " of nonemptiness witness" ^ suffix2 ^
+ " of the raw type's BNF " ^ be ^ " subsumed by the existing raw witnesses:")
+ |> (fn pt => Pretty.chunks [pt,
+ Pretty.para ("You do not need to lift these subsumed witnesses.")])
+ |> Pretty.string_of
+ |> warning
+ end;
+ in
+ filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) wits_F) Iwits
+ end
+ else Iwits;
+
val wit_goals = maps (BNF_Def.mk_wit_goals var_as var_as' sets) Iwits;
- val lost_wits = filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) Iwits) wits_F;
+ val lost_wits = if is_quotient then [] else
+ filter_out (fn (J, _) => exists (fn (I, _) => subset (op =) (I, J)) Iwits) wits_F;
val _ =
if null lost_wits orelse exists (fn No_Warn_Wits => true | _ => false) opts then ()
@@ -1023,9 +1050,6 @@
@{thm equivp_add_relconj} OF [equiv_thm', equiv_thm', rel_pos_distr_thm0];
val (rel_Inter_thms, wit_thmss) = apply2 (fn f => flat (f live thmss)) (take, drop);
- val wit_thms = (case wit_thmss of
- [] => wit_thms_of_bnf bnf_F
- | _ => wit_thmss);
(* construct map_G, sets_G, bd_G, rel_G and wits_G *)
@@ -1079,10 +1103,6 @@
val rel_raw = fold_rev lambda var_Ps rel_F'_tm
|> subst_atomic_types (betas ~~ gammas);
- (* val wits_G = [abs_G o wit_F] *)
- val wits_G = map (fn (I, wit) => let val vars = (map (fn n => nth var_as n) I)
- in fold_rev lambda vars (abs_G $ list_comb (wit, vars)) end) Iwits;
-
(* auxiliary lemmas *)
val bd_card_order = bd_card_order_of_bnf bnf_F;
val bd_cinfinite = bd_cinfinite_of_bnf bnf_F;
@@ -1844,6 +1864,22 @@
map2 mk_set_G_bd_tac set_F'_thmss set_bd_thms @
rel_compp_tac :: rel_compp_Grp_tac :: [pred_G_set_G_tac];
+ (* val wits_G = [abs_G o wit_F] *)
+ val (wits_G, wit_thms) =
+ let
+ val wit_F_thmss = map (map2 (fn set_F' => fn wit =>
+ (#set_F'_subset set_F' RS set_mp RS wit)
+ |> unfold_thms lthy [#set_F'_def set_F']) set_F'_thmss)
+ (wit_thmss_of_bnf bnf_F);
+ val (wits_F, wit_F_thmss) = split_list
+ (filter_out (fn ((J, _), _) => exists (fn (I, _) => subset (op =) (I, J)) Iwits)
+ (wits_F ~~ wit_F_thmss));
+ fun mk_wit (I, wit) = let val vars = (map (fn n => nth var_as n) I)
+ in fold_rev lambda vars (abs_G $ list_comb (wit, vars)) end;
+ in
+ (map mk_wit (Iwits @ wits_F), wit_thmss @ flat wit_F_thmss)
+ end;
+
fun mk_wit_tacs ({set_F'_def, set_F'_respect, ...} :: set_F'_thmss) (w :: ws) ctxt =
EVERY [unfold_thms_tac ctxt [@{thm o_def},
set_F'_respect RS @{thm rel_funD} OF [#rep_abs qthms OF [(#reflp qthms)]]],