--- a/NEWS Wed Feb 17 21:08:11 2016 +0100
+++ b/NEWS Wed Feb 17 21:08:18 2016 +0100
@@ -13,6 +13,26 @@
typesetting. E.g. to produce proof holes in examples and documentation.
+*** HOL ***
+
+* (Co)datatype package:
+ - the predicator :: ('a => bool) => 'a F => bool is now a first-class
+ citizen in bounded natural functors
+ - "primrec" now allows nested calls through the predicator in addition
+ to the map function.
+ - "bnf" automatically discharges reflexive proof obligations
+ "bnf" outputs a slightly modified proof obligation expressing rel in
+ terms of map and set
+ (not giving a specification for rel makes this one reflexive)
+ "bnf" outputs a new proof obligation expressing pred in terms of set
+ (not giving a specification for pred makes this one reflexive)
+ INCOMPATIBILITY: manual "bnf" declarations may need adjustment
+ - Renamed lemmas:
+ rel_prod_apply ~> rel_prod_inject
+ pred_prod_apply ~> pred_prod_inject
+ INCOMPATIBILITY.
+
+
New in Isabelle2016 (February 2016)
-----------------------------------
--- a/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 21:08:18 2016 +0100
@@ -342,7 +342,7 @@
text \<open>
The @{command datatype} command introduces various constants in addition to
the constructors. With each datatype are associated set functions, a map
-function, a relator, discriminators, and selectors, all of which can be given
+function,, a predicator, a relator, discriminators, and selectors, all of which can be given
custom names. In the example below, the familiar names @{text null}, @{text hd},
@{text tl}, @{text set}, @{text map}, and @{text list_all2} override the
default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
@@ -359,7 +359,7 @@
Cons (infixr "#" 65)
hide_type list
- hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list pred_list
+ hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all
context early
begin
@@ -370,6 +370,7 @@
for
map: map
rel: list_all2
+ pred: list_all
where
"tl Nil = Nil"
@@ -439,6 +440,7 @@
for
map: map
rel: list_all2
+ pred: list_all
text \<open>
\noindent
@@ -652,7 +654,7 @@
\noindent
The discriminators and selectors are generated only if the @{text "discs_sels"}
option is enabled or if names are specified for discriminators or selectors.
-The set functions, map function, and relator are generated only if $m > 0$.
+The set functions, map function, predicator, and relator are generated only if $m > 0$.
In addition, some of the plugins introduce their own constants
(Section~\ref{sec:selecting-plugins}). The case combinator, discriminators,
@@ -856,7 +858,7 @@
one live type argument (e.g., @{typ "'a list"}). They are partitioned in two
subgroups. The first subgroup consists of properties involving the
constructors or the destructors and either a set function, the map function,
-or the relator:
+the predicator, or the relator:
\begin{indentblock}
\begin{description}
@@ -942,7 +944,7 @@
(Section~\ref{ssec:code-generator}).
The second subgroup consists of more abstract properties of the set functions,
-the map function, and the relator:
+the map function, the predicator, and the relator:
\begin{indentblock}
\begin{description}
@@ -953,13 +955,8 @@
\item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\
@{thm list.inj_map_strong[no_vars]}
-\item[@{text "t."}\hthm{set_map}\rm:] ~ \\
-@{thm list.set_map[no_vars]}
-
-\item[@{text "t."}\hthm{set_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
-@{thm list.set_transfer[no_vars]} \\
-The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
-(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
+\item[@{text "t."}\hthm{map_comp}\rm:] ~ \\
+@{thm list.map_comp[no_vars]}
\item[@{text "t."}\hthm{map_cong0}\rm:] ~ \\
@{thm list.map_cong0[no_vars]}
@@ -967,6 +964,9 @@
\item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\
@{thm list.map_cong[no_vars]}
+\item[@{text "t."}\hthm{map_cong_pred}\rm:] ~ \\
+@{thm list.map_cong_pred[no_vars]}
+
\item[@{text "t."}\hthm{map_cong_simp}\rm:] ~ \\
@{thm list.map_cong_simp[no_vars]}
@@ -984,6 +984,40 @@
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
+\item[@{text "t."}\hthm{pred_cong} @{text "[fundef_cong]"}\rm:] ~ \\
+@{thm list.pred_cong[no_vars]}
+
+\item[@{text "t."}\hthm{pred_cong_simp}\rm:] ~ \\
+@{thm list.pred_cong_simp[no_vars]}
+
+\item[@{text "t."}\hthm{pred_map}\rm:] ~ \\
+@{thm list.pred_map[no_vars]}
+
+\item[@{text "t."}\hthm{pred_mono_strong}\rm:] ~ \\
+@{thm list.pred_mono_strong[no_vars]}
+
+\item[@{text "t."}\hthm{pred_rel}\rm:] ~ \\
+@{thm list.pred_rel[no_vars]}
+
+\item[@{text "t."}\hthm{pred_set}\rm:] ~ \\
+@{thm list.pred_set[no_vars]}
+
+\item[@{text "t."}\hthm{pred_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
+@{thm list.pred_transfer[no_vars]} \\
+The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
+
+\item[@{text "t."}\hthm{pred_True}\rm:] ~ \\
+@{thm list.pred_True[no_vars]}
+
+\item[@{text "t."}\hthm{set_map}\rm:] ~ \\
+@{thm list.set_map[no_vars]}
+
+\item[@{text "t."}\hthm{set_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
+@{thm list.set_transfer[no_vars]} \\
+The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
+(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
+
\item[@{text "t."}\hthm{rel_compp} @{text "[relator_distr]"}\rm:] ~ \\
@{thm list.rel_compp[no_vars]} \\
The @{text "[relator_distr]"} attribute is set by the @{text lifting} plugin
@@ -995,6 +1029,9 @@
\item[@{text "t."}\hthm{rel_eq}\rm:] ~ \\
@{thm list.rel_eq[no_vars]}
+\item[@{text "t."}\hthm{rel_eq_onp}\rm:] ~ \\
+@{thm list.rel_eq_onp[no_vars]}
+
\item[@{text "t."}\hthm{rel_flip}\rm:] ~ \\
@{thm list.rel_flip[no_vars]}
@@ -1432,6 +1469,14 @@
primrec (nonexhaustive) subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
"subtree_ft2 x y (FTNode2 g) = g x y"
+text \<open>
+For any datatype featuring nesting, the predicator can be used instead of the
+map function, typically when defining predicates. For example:
+\<close>
+
+ primrec increasing_tree :: "int \<Rightarrow> int tree\<^sub>f\<^sub>f \<Rightarrow> bool" where
+ "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \<longleftrightarrow> n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
+
subsubsection \<open> Nested-as-Mutual Recursion
\label{sssec:primrec-nested-as-mutual-recursion} \<close>
@@ -1739,6 +1784,7 @@
for
map: lmap
rel: llist_all2
+ pred: llist_all
where
"ltl LNil = LNil"
@@ -2090,6 +2136,9 @@
text \<open>
\noindent
+For technical reasons, @{text "case"}--@{text "of"} is only supported for
+case distinctions on (co)datatypes that provide discriminators and selectors.
+
Pattern matching is not supported by @{command primcorec}. Fortunately, it is
easy to generate pattern-maching equations using the @{command simps_of_case}
command provided by the theory @{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
@@ -2697,7 +2746,12 @@
(functorial action), $n$ set functions (natural transformations),
and an infinite cardinal bound that satisfy certain properties.
For example, @{typ "'a llist"} is a unary BNF.
-Its relator @{text "llist_all2 ::
+Its predicator @{text "llist_all ::
+ ('a \<Rightarrow> bool) \<Rightarrow>
+ 'a llist \<Rightarrow> bool"}
+extends unary predicates over elements to unary predicates over
+lazy lists.
+Similarly, its relator @{text "llist_all2 ::
('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow>
'a llist \<Rightarrow> 'b llist \<Rightarrow> bool"}
extends binary predicates over elements to binary predicates over parallel
@@ -2724,7 +2778,7 @@
The type is simply a copy of the function space @{typ "'d \<Rightarrow> 'a"}, where @{typ 'a}
is live and @{typ 'd} is dead. We introduce it together with its map function,
-set function, and relator.
+set function, predicator, and relator.
\<close>
typedef ('d, 'a) fn = "UNIV :: ('d \<Rightarrow> 'a) set"
@@ -2742,6 +2796,11 @@
text \<open> \blankline \<close>
lift_definition
+ pred_fn :: "('a \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> bool"
+ is
+ "pred_fun (\<lambda>_. True)" .
+
+ lift_definition
rel_fn :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn \<Rightarrow> bool"
is
"rel_fun (op =)" .
@@ -2753,6 +2812,7 @@
sets: set_fn
bd: "natLeq +c |UNIV :: 'd set|"
rel: rel_fn
+ pred: pred_fn
proof -
show "map_fn id = id"
by transfer auto
@@ -2792,13 +2852,13 @@
by (rule, transfer) (auto simp add: rel_fun_def)
next
fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
- show "rel_fn R =
- (BNF_Def.Grp {x. set_fn x \<subseteq> {(x, y). R x y}} (map_fn fst))\<inverse>\<inverse> OO
- BNF_Def.Grp {x. set_fn x \<subseteq> {(x, y). R x y}} (map_fn snd)"
- unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
- apply transfer
- unfolding rel_fun_def subset_iff image_iff
- by auto (force, metis prod.collapse)
+ show "rel_fn R = (\<lambda>x y. \<exists>z. set_fn z \<subseteq> {(x, y). R x y} \<and> map_fn fst z = x \<and> map_fn snd z = y)"
+ unfolding fun_eq_iff relcompp.simps conversep.simps
+ by transfer (force simp: rel_fun_def subset_iff)
+ next
+ fix P :: "'a \<Rightarrow> bool"
+ show "pred_fn P = (\<lambda>x. Ball (set_fn x) P)"
+ unfolding fun_eq_iff by transfer simp
qed
text \<open> \blankline \<close>
@@ -2861,7 +2921,7 @@
yval :: 'a
text \<open> \blankline \<close>
-
+
copy_bnf ('a, 'z) point_ext
text \<open>
@@ -2881,7 +2941,7 @@
lift_bnf (*<*)(no_warn_wits) (*>*)'a nonempty_list
proof -
- fix f and xs :: "'a list"
+ fix f (*<*):: "'a \<Rightarrow> 'c"(*>*)and xs :: "'a list"
assume "xs \<in> {xs. xs \<noteq> []}"
then show "map f xs \<in> {xs. xs \<noteq> []}"
by (cases xs(*<*) rule: list.exhaust(*>*)) auto
@@ -2896,7 +2956,7 @@
The next example declares a BNF axiomatically. This can be convenient for
reasoning abstractly about an arbitrary BNF. The @{command bnf_axiomatization}
command below introduces a type @{text "('a, 'b, 'c) F"}, three set constants,
-a map function, a relator, and a nonemptiness witness that depends only on
+a map function, a predicator, a relator, and a nonemptiness witness that depends only on
@{typ 'a}. The type @{text "'a \<Rightarrow> ('a, 'b, 'c) F"} of the witness can be read
as an implication: Given a witness for @{typ 'a}, we can construct a witness for
@{text "('a, 'b, 'c) F"}. The BNF properties are postulated as axioms.
@@ -2934,7 +2994,7 @@
\noindent
The @{command bnf} command registers an existing type as a bounded natural
functor (BNF). The type must be equipped with an appropriate map function
-(functorial action). In addition, custom set functions, relators, and
+(functorial action). In addition, custom set functions, predicators, relators, and
nonemptiness witnesses can be specified; otherwise, default versions are used.
The syntactic entity \synt{target} can be used to specify a local context,
@@ -2973,7 +3033,7 @@
structure on the raw type to the abstract type following a @{term
type_definition} theorem. The theorem is usually inferred from the type, but can
also be explicitly supplied by means of the optional @{text via} clause. In
-addition, custom names for the set functions, the map function, and the relator,
+addition, custom names for the set functions, the map function, the predicator, and the relator,
as well as nonemptiness witnesses can be specified.
Nonemptiness witnesses are not lifted from the raw type's BNF, as this would be
@@ -3024,7 +3084,7 @@
\noindent
The @{command bnf_axiomatization} command declares a new type and associated constants
-(map, set, relator, and cardinal bound) and asserts the BNF properties for
+(map, set, predicator, relator, and cardinal bound) and asserts the BNF properties for
these constants as axioms.
The syntactic entity \synt{target} can be used to specify a local context,
@@ -3349,9 +3409,6 @@
@{thm list.pred_inject(2)[no_vars]} \\
This property is generated only for (co)datatypes.
-\item[@{text "t."}\hthm{rel_eq_onp}\rm:] ~ \\
-@{thm list.rel_eq_onp[no_vars]}
-
\item[@{text "t."}\hthm{left_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.left_total_rel[no_vars]}
@@ -3414,9 +3471,9 @@
\end{indentblock}
In addition, the plugin sets the @{text "[relator_eq]"} attribute on a
-variant of the @{text t.rel_eq_onp} property generated by the @{text lifting}
-plugin, the @{text "[relator_mono]"} attribute on @{text t.rel_mono}, and the
-@{text "[relator_distr]"} attribute on @{text t.rel_compp}.
+variant of the @{text t.rel_eq_onp} property, the @{text "[relator_mono]"}
+attribute on @{text t.rel_mono}, and the @{text "[relator_distr]"} attribute
+on @{text t.rel_compp}.
\<close>
@@ -3462,7 +3519,7 @@
\setlength{\itemsep}{0pt}
\item
-\emph{Defining mutually (co)recursive (co)datatypes is slow.} Fortunately,
+\emph{Defining mutually (co)recursive (co)datatypes can be slow.} Fortunately,
it is always possible to recast mutual specifications to nested ones, which are
processed more efficiently.
@@ -3477,6 +3534,11 @@
\keyw{lemmas} command, is available as an alternative.
\item
+\emph{The \emph{\keyw{primcorec}} command does not allow corecursion under
+@{text "case"}--@{text "of"} for datatypes that are defined without
+discriminators and selectors.}
+
+\item
\emph{There is no way to use an overloaded constant from a syntactic type
class, such as @{text 0}, as a constructor.}
--- a/src/HOL/BNF_Composition.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/BNF_Composition.thy Wed Feb 17 21:08:18 2016 +0100
@@ -78,9 +78,11 @@
lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
by (unfold comp_apply collect_def) simp
-lemma wpull_cong:
- "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
- by simp
+lemma Collect_inj: "Collect P = Collect Q \<Longrightarrow> P = Q"
+ by blast
+
+lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
+by auto
lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)^--1 OO Grp (Collect (case_prod R)) snd = R"
unfolding Grp_def fun_eq_iff relcompp.simps by auto
@@ -101,6 +103,12 @@
lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
by simp
+lemma Ball_comp_iff: "(\<lambda>x. Ball (A x) f) o g = (\<lambda>x. Ball ((A o g) x) f)"
+ unfolding o_def by auto
+
+lemma conj_comp_iff: "(\<lambda>x. P x \<and> Q x) o g = (\<lambda>x. (P o g) x \<and> (Q o g) x)"
+ unfolding o_def by auto
+
context
fixes Rep Abs
assumes type_copy: "type_definition Rep Abs UNIV"
@@ -150,7 +158,7 @@
map: "id :: 'a \<Rightarrow> 'a"
bd: natLeq
rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
- by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
+ by (auto simp add: natLeq_card_order natLeq_cinfinite)
definition id_bnf :: "'a \<Rightarrow> 'a" where
"id_bnf \<equiv> (\<lambda>x. x)"
@@ -163,6 +171,7 @@
sets: "\<lambda>x. {x}"
bd: natLeq
rel: "id_bnf :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+ pred: "id_bnf :: ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
unfolding id_bnf_def
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
--- a/src/HOL/BNF_Def.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/BNF_Def.thy Wed Feb 17 21:08:18 2016 +0100
@@ -235,6 +235,40 @@
lemma diag_imp_eq_le: "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> \<forall>x y. x \<in> A \<longrightarrow> y \<in> A \<longrightarrow> x = y \<longrightarrow> R x y"
by blast
+definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
+
+lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id"
+ unfolding eq_onp_def Grp_def by auto
+
+lemma eq_onp_to_eq: "eq_onp P x y \<Longrightarrow> x = y"
+ by (simp add: eq_onp_def)
+
+lemma eq_onp_top_eq_eq: "eq_onp top = op ="
+ by (simp add: eq_onp_def)
+
+lemma eq_onp_same_args: "eq_onp P x x = P x"
+ using assms by (auto simp add: eq_onp_def)
+
+lemma eq_onp_eqD: "eq_onp P = Q \<Longrightarrow> P x = Q x x"
+ unfolding eq_onp_def by blast
+
+lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
+ by auto
+
+lemma eq_onp_mono0: "\<forall>x\<in>A. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>x\<in>A. \<forall>y\<in>A. eq_onp P x y \<longrightarrow> eq_onp Q x y"
+ unfolding eq_onp_def by auto
+
+lemma eq_onp_True: "eq_onp (\<lambda>_. True) = (op =)"
+ unfolding eq_onp_def by simp
+
+lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g o f)"
+ by auto
+
+lemma rel_fun_Collect_case_prodD:
+ "rel_fun A B f g \<Longrightarrow> X \<subseteq> Collect (case_prod A) \<Longrightarrow> x \<in> X \<Longrightarrow> B ((f o fst) x) ((g o snd) x)"
+ unfolding rel_fun_def by auto
+
ML_file "Tools/BNF/bnf_util.ML"
ML_file "Tools/BNF/bnf_tactics.ML"
ML_file "Tools/BNF/bnf_def_tactics.ML"
--- a/src/HOL/BNF_Fixpoint_Base.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy Wed Feb 17 21:08:18 2016 +0100
@@ -73,12 +73,12 @@
"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
by simp
-lemma prod_set_simps:
+lemma prod_set_simps[simp]:
"fsts (x, y) = {x}"
"snds (x, y) = {y}"
unfolding prod_set_defs by simp+
-lemma sum_set_simps:
+lemma sum_set_simps[simp]:
"setl (Inl x) = {x}"
"setl (Inr x) = {}"
"setr (Inl x) = {}"
@@ -236,6 +236,12 @@
lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
unfolding rel_fun_def by simp
+lemma eq_onp_live_step: "x = y \<Longrightarrow> eq_onp P a a \<and> x \<longleftrightarrow> P a \<and> y"
+ by (simp only: eq_onp_same_args)
+
+lemma top_conj: "top x \<and> P \<longleftrightarrow> P" "P \<and> top x \<longleftrightarrow> P"
+ by blast+
+
ML_file "Tools/BNF/bnf_fp_util.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
--- a/src/HOL/Basic_BNF_LFPs.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Basic_BNF_LFPs.thy Wed Feb 17 21:08:18 2016 +0100
@@ -32,6 +32,9 @@
lemma xtor_rel_induct: "(\<And>x y. vimage2p id_bnf id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR"
unfolding xtor_def vimage2p_def id_bnf_def ..
+lemma xtor_iff_xtor: "u = xtor w \<longleftrightarrow> xtor u = w"
+ unfolding xtor_def ..
+
lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))"
unfolding xtor_def id_bnf_def by (rule reflexive)
@@ -94,7 +97,7 @@
ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
-lemma size_bool[code]: "size (b::bool) = 0"
+lemma size_bool[code]: "size (b :: bool) = 0"
by (cases b) auto
declare prod.size[no_atp]
--- a/src/HOL/Basic_BNFs.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Basic_BNFs.thy Wed Feb 17 21:08:18 2016 +0100
@@ -30,12 +30,24 @@
"rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
by (auto intro: rel_sum.intros elim: rel_sum.cases)
+inductive
+ pred_sum :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool" for P1 P2
+where
+ "P1 a \<Longrightarrow> pred_sum P1 P2 (Inl a)"
+| "P2 b \<Longrightarrow> pred_sum P1 P2 (Inr b)"
+
+lemma pred_sum_inject[code, simp]:
+ "pred_sum P1 P2 (Inl a) \<longleftrightarrow> P1 a"
+ "pred_sum P1 P2 (Inr b) \<longleftrightarrow> P2 b"
+ by (simp add: pred_sum.simps)+
+
bnf "'a + 'b"
map: map_sum
sets: setl setr
bd: natLeq
wits: Inl Inr
rel: rel_sum
+ pred: pred_sum
proof -
show "map_sum id id = id" by (rule map_sum.id)
next
@@ -82,12 +94,12 @@
by (force elim: rel_sum.cases)
next
fix R S
- show "rel_sum R S =
- (Grp {x. setl x \<subseteq> Collect (case_prod R) \<and> setr x \<subseteq> Collect (case_prod S)} (map_sum fst fst))\<inverse>\<inverse> OO
- Grp {x. setl x \<subseteq> Collect (case_prod R) \<and> setr x \<subseteq> Collect (case_prod S)} (map_sum snd snd)"
- unfolding sum_set_defs Grp_def relcompp.simps conversep.simps fun_eq_iff
+ show "rel_sum R S = (\<lambda>x y.
+ \<exists>z. (setl z \<subseteq> {(x, y). R x y} \<and> setr z \<subseteq> {(x, y). S x y}) \<and>
+ map_sum fst fst z = x \<and> map_sum snd snd z = y)"
+ unfolding sum_set_defs relcompp.simps conversep.simps fun_eq_iff
by (fastforce elim: rel_sum.cases split: sum.splits)
-qed (auto simp: sum_set_defs)
+qed (auto simp: sum_set_defs fun_eq_iff pred_sum.simps split: sum.splits)
inductive_set fsts :: "'a \<times> 'b \<Rightarrow> 'a set" for p :: "'a \<times> 'b" where
"fst p \<in> fsts p"
@@ -102,19 +114,37 @@
where
"\<lbrakk>R1 a b; R2 c d\<rbrakk> \<Longrightarrow> rel_prod R1 R2 (a, c) (b, d)"
-lemma rel_prod_apply [code, simp]:
+inductive
+ pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" for P1 P2
+where
+ "\<lbrakk>P1 a; P2 b\<rbrakk> \<Longrightarrow> pred_prod P1 P2 (a, b)"
+
+lemma rel_prod_inject [code, simp]:
"rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
by (auto intro: rel_prod.intros elim: rel_prod.cases)
+lemma pred_prod_inject [code, simp]:
+ "pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
+ by (auto intro: pred_prod.intros elim: pred_prod.cases)
+
lemma rel_prod_conv:
"rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
by (rule ext, rule ext) auto
+definition
+ pred_fun :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+where
+ "pred_fun A B = (\<lambda>f. \<forall>x. A x \<longrightarrow> B (f x))"
+
+lemma pred_funI: "(\<And>x. A x \<Longrightarrow> B (f x)) \<Longrightarrow> pred_fun A B f"
+ unfolding pred_fun_def by simp
+
bnf "'a \<times> 'b"
map: map_prod
sets: fsts snds
bd: natLeq
rel: rel_prod
+ pred: pred_prod
proof (unfold prod_set_defs)
show "map_prod id id = id" by (rule map_prod.id)
next
@@ -150,18 +180,19 @@
show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
next
fix R S
- show "rel_prod R S =
- (Grp {x. {fst x} \<subseteq> Collect (case_prod R) \<and> {snd x} \<subseteq> Collect (case_prod S)} (map_prod fst fst))\<inverse>\<inverse> OO
- Grp {x. {fst x} \<subseteq> Collect (case_prod R) \<and> {snd x} \<subseteq> Collect (case_prod S)} (map_prod snd snd)"
- unfolding prod_set_defs rel_prod_apply Grp_def relcompp.simps conversep.simps fun_eq_iff
+ show "rel_prod R S = (\<lambda>x y.
+ \<exists>z. ({fst z} \<subseteq> {(x, y). R x y} \<and> {snd z} \<subseteq> {(x, y). S x y}) \<and>
+ map_prod fst fst z = x \<and> map_prod snd snd z = y)"
+ unfolding prod_set_defs rel_prod_inject relcompp.simps conversep.simps fun_eq_iff
by auto
-qed
+qed auto
bnf "'a \<Rightarrow> 'b"
map: "op \<circ>"
sets: range
bd: "natLeq +c |UNIV :: 'a set|"
rel: "rel_fun op ="
+ pred: "pred_fun (\<lambda>_. True)"
proof
fix f show "id \<circ> f = id f" by simp
next
@@ -194,17 +225,9 @@
show "rel_fun op = R OO rel_fun op = S \<le> rel_fun op = (R OO S)" by (auto simp: rel_fun_def)
next
fix R
- show "rel_fun op = R =
- (Grp {x. range x \<subseteq> Collect (case_prod R)} (op \<circ> fst))\<inverse>\<inverse> OO
- Grp {x. range x \<subseteq> Collect (case_prod R)} (op \<circ> snd)"
- unfolding rel_fun_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
- comp_apply mem_Collect_eq split_beta bex_UNIV
- proof (safe, unfold fun_eq_iff[symmetric])
- fix x xa a b c xb y aa ba
- assume *: "x = a" "xa = c" "a = ba" "b = aa" "c = (\<lambda>x. snd (b x))" "ba = (\<lambda>x. fst (aa x))" and
- **: "\<forall>t. (\<exists>x. t = aa x) \<longrightarrow> R (fst t) (snd t)"
- show "R (x y) (xa y)" unfolding * by (rule mp[OF spec[OF **]]) blast
- qed force
-qed
+ show "rel_fun op = R = (\<lambda>x y.
+ \<exists>z. range z \<subseteq> {(x, y). R x y} \<and> fst \<circ> z = x \<and> snd \<circ> z = y)"
+ unfolding rel_fun_def subset_iff by (force simp: fun_eq_iff[symmetric])
+qed (auto simp: pred_fun_def)
end
--- a/src/HOL/Cardinals/Bounded_Set.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Cardinals/Bounded_Set.thy Wed Feb 17 21:08:18 2016 +0100
@@ -98,10 +98,10 @@
by (rule predicate2I, transfer) (auto simp: rel_set_OO[symmetric])
next
fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
- show "rel_bset R = ((BNF_Def.Grp {x. set_bset x \<subseteq> {(x, y). R x y}} (map_bset fst))\<inverse>\<inverse> OO
- BNF_Def.Grp {x. set_bset x \<subseteq> {(x, y). R x y}} (map_bset snd) ::
- 'a set['k] \<Rightarrow> 'b set['k] \<Rightarrow> bool)"
- by (simp add: rel_bset_def map_fun_def o_def rel_set_def rel_bset_aux_infinite)
+ show "rel_bset R = ((\<lambda>x y. \<exists>z. set_bset z \<subseteq> {(x, y). R x y} \<and>
+ map_bset fst z = x \<and> map_bset snd z = y) :: 'a set['k] \<Rightarrow> 'b set['k] \<Rightarrow> bool)"
+ by (simp add: rel_bset_def map_fun_def o_def rel_set_def
+ rel_bset_aux_infinite[unfolded OO_Grp_alt])
next
fix x
assume "x \<in> set_bset bempty"
--- a/src/HOL/Library/Countable_Set_Type.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Wed Feb 17 21:08:18 2016 +0100
@@ -606,10 +606,9 @@
unfolding rel_cset_alt_def[abs_def] by fast
next
fix R
- show "rel_cset R =
- (BNF_Def.Grp {x. rcset x \<subseteq> Collect (case_prod R)} (cimage fst))\<inverse>\<inverse> OO
- BNF_Def.Grp {x. rcset x \<subseteq> Collect (case_prod R)} (cimage snd)"
- unfolding rel_cset_alt_def[abs_def] rel_cset_aux by simp
+ show "rel_cset R = (\<lambda>x y. \<exists>z. rcset z \<subseteq> {(x, y). R x y} \<and>
+ cimage fst z = x \<and> cimage snd z = y)"
+ unfolding rel_cset_alt_def[abs_def] rel_cset_aux[unfolded OO_Grp_alt] by simp
qed(simp add: bot_cset.rep_eq)
end
--- a/src/HOL/Library/Dlist.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Library/Dlist.thy Wed Feb 17 21:08:18 2016 +0100
@@ -326,7 +326,6 @@
subgoal by(simp add: natLeq_cinfinite)
subgoal by(rule ordLess_imp_ordLeq)(simp add: finite_iff_ordLess_natLeq[symmetric] set_def)
subgoal by(rule predicate2I)(transfer; auto simp add: wpull)
-subgoal by(rule refl)
subgoal by(simp add: set_def)
done
--- a/src/HOL/Library/FSet.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Library/FSet.thy Wed Feb 17 21:08:18 2016 +0100
@@ -972,7 +972,8 @@
apply (rule natLeq_cinfinite)
apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
apply (fastforce simp: rel_fset_alt)
- apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt rel_fset_aux)
+ apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt
+ rel_fset_aux[unfolded OO_Grp_alt])
apply transfer apply simp
done
--- a/src/HOL/Library/Multiset.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Feb 17 21:08:18 2016 +0100
@@ -2302,12 +2302,18 @@
lemma ex_mset: "\<exists>xs. mset xs = X"
by (induct X) (simp, metis mset.simps(2))
+inductive pred_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> bool"
+where
+ "pred_mset P {#}"
+| "\<lbrakk>P a; pred_mset P M\<rbrakk> \<Longrightarrow> pred_mset P (M + {#a#})"
+
bnf "'a multiset"
map: image_mset
sets: set_mset
bd: natLeq
wits: "{#}"
rel: rel_mset
+ pred: pred_mset
proof -
show "image_mset id = id"
by (rule image_mset.id)
@@ -2334,16 +2340,13 @@
done
done
show "rel_mset R =
- (BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset fst))\<inverse>\<inverse> OO
- BNF_Def.Grp {x. set_mset x \<subseteq> {(x, y). R x y}} (image_mset snd)" for R
- unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def
+ (\<lambda>x y. \<exists>z. set_mset z \<subseteq> {(x, y). R x y} \<and>
+ image_mset fst z = x \<and> image_mset snd z = y)" for R
+ unfolding rel_mset_def[abs_def]
apply (rule ext)+
- apply auto
- apply (rule_tac x = "mset (zip xs ys)" in exI; auto)
- apply (metis list_all2_lengthD map_fst_zip mset_map)
- apply (auto simp: list_all2_iff)[1]
- apply (metis list_all2_lengthD map_snd_zip mset_map)
- apply (auto simp: list_all2_iff)[1]
+ apply safe
+ apply (rule_tac x = "mset (zip xs ys)" in exI;
+ auto simp: in_set_zip list_all2_iff mset_map[symmetric])
apply (rename_tac XY)
apply (cut_tac X = XY in ex_mset)
apply (erule exE)
@@ -2355,6 +2358,16 @@
done
show "z \<in> set_mset {#} \<Longrightarrow> False" for z
by auto
+ show "pred_mset P = (\<lambda>x. Ball (set_mset x) P)" for P
+ proof (intro ext iffI)
+ fix x
+ assume "pred_mset P x"
+ then show "Ball (set_mset x) P" by (induct pred: pred_mset; simp)
+ next
+ fix x
+ assume "Ball (set_mset x) P"
+ then show "pred_mset P x" by (induct x; auto intro: pred_mset.intros)
+ qed
qed
inductive rel_mset'
--- a/src/HOL/Library/bnf_axiomatization.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Library/bnf_axiomatization.ML Wed Feb 17 21:08:18 2016 +0100
@@ -8,7 +8,8 @@
signature BNF_AXIOMATIZATION =
sig
val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding ->
- mixfix -> binding -> binding -> typ list -> local_theory -> BNF_Def.bnf * local_theory
+ mixfix -> binding -> binding -> binding -> typ list -> local_theory ->
+ BNF_Def.bnf * local_theory
end
structure BNF_Axiomatization : BNF_AXIOMATIZATION =
@@ -18,7 +19,7 @@
open BNF_Def
fun prepare_decl prepare_plugins prepare_constraint prepare_typ
- raw_plugins raw_vars b mx user_mapb user_relb user_witTs lthy =
+ raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy =
let
val plugins = prepare_plugins lthy raw_plugins;
@@ -72,7 +73,8 @@
Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
- user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
+ user_mapb user_relb user_predb user_setbs
+ (((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE)
lthy;
fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
@@ -116,12 +118,12 @@
val parse_bnf_axiomatization =
parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
- parse_witTs -- Parse.opt_mixfix -- parse_map_rel_bindings;
+ parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings;
val _ =
Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
(parse_bnf_axiomatization >>
- (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb)) =>
- bnf_axiomatization_cmd plugins bsTs b mx mapb relb witTs #> snd));
+ (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) =>
+ bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd));
end;
--- a/src/HOL/List.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/List.thy Wed Feb 17 21:08:18 2016 +0100
@@ -14,6 +14,7 @@
for
map: map
rel: list_all2
+ pred: list_all
where
"tl [] = []"
@@ -6241,10 +6242,7 @@
"x \<in> set xs \<longleftrightarrow> member xs x"
by (simp add: member_def)
-abbreviation "list_all == pred_list"
-
-lemma list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
-unfolding pred_list_def ..
+lemmas list_all_iff [code_abbrev] = fun_cong[OF list.pred_set]
definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
@@ -6305,9 +6303,7 @@
"list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
by (auto simp add: list_ex_iff set_conv_nth)
-lemma list_all_cong [fundef_cong]:
- "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
- by (simp add: list_all_iff)
+lemmas list_all_cong [fundef_cong] = list.pred_cong
lemma list_ex_cong [fundef_cong]:
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
--- a/src/HOL/Nat.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Nat.thy Wed Feb 17 21:08:18 2016 +0100
@@ -167,7 +167,7 @@
setup \<open>
let
fun basic_lfp_sugars_of _ [@{typ nat}] _ _ ctxt =
- ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, ctxt)
+ ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt)
| basic_lfp_sugars_of bs arg_Ts callers callssss ctxt =
BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt;
in
--- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Feb 17 21:08:18 2016 +0100
@@ -1097,10 +1097,9 @@
finally show ?thesis .
qed
- show "\<And>R. rel_pmf R =
- (BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO
- BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)"
- by (auto simp add: fun_eq_iff BNF_Def.Grp_def OO_def rel_pmf.simps)
+ show "\<And>R. rel_pmf R = (\<lambda>x y. \<exists>z. set_pmf z \<subseteq> {(x, y). R x y} \<and>
+ map_pmf fst z = x \<and> map_pmf snd z = y)"
+ by (auto simp add: fun_eq_iff rel_pmf.simps)
show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
--- a/src/HOL/Tools/BNF/bnf_comp.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Wed Feb 17 21:08:18 2016 +0100
@@ -171,9 +171,10 @@
(Variable.invent_types (replicate ilive @{sort type}) lthy3);
val Bss_repl = replicate olive Bs;
- val ((((fs', Qs'), Asets), xs), _) = names_lthy
+ val (((((fs', Qs'), Ps'), Asets), xs), _) = names_lthy
|> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs)
||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
+ ||>> apfst snd o mk_Frees' "P" (map mk_pred1T As)
||>> mk_Frees "A" (map HOLogic.mk_setT As)
||>> mk_Frees "x" As;
@@ -196,6 +197,11 @@
(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));
+ (*%P1 ... Pn. outer.pred (inner_1.pred P1 ... Pn) ... (inner_m.pred P1 ... Pn)*)
+ val pred = fold_rev Term.abs Ps'
+ (Term.list_comb (mk_pred_of_bnf oDs CAs outer,
+ map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
+ mk_pred_of_bnf Ds As) 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}*)
@@ -327,18 +333,28 @@
let
val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
val thm =
- (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
+ trans OF [in_alt_thm RS @{thm OO_Grp_cong},
trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
[trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
trans OF [rel_OO_of_bnf outer RS sym, rel_cong0_of_bnf outer OF
- (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym);
+ (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym;
in
unfold_thms_tac ctxt set'_eq_sets THEN rtac ctxt thm 1
end;
+ fun pred_set_tac ctxt =
+ let
+ val pred_alt = unfold_thms ctxt @{thms Ball_Collect}
+ (trans OF [pred_cong0_of_bnf outer OF map pred_set_of_bnf inners, pred_set_of_bnf outer]);
+ val in_alt = in_alt_thm RS @{thm Collect_inj} RS sym;
+ in
+ unfold_thms_tac ctxt (@{thm Ball_Collect} :: set'_eq_sets) THEN
+ HEADGOAL (rtac ctxt (trans OF [pred_alt, in_alt]))
+ end
+
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -361,7 +377,8 @@
val (bnf', lthy') =
bnf_def const_policy (K Dont_Note) true qualify tacs wit_tac (SOME (oDs @ flat Dss))
- Binding.empty Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
+ Binding.empty Binding.empty Binding.empty []
+ (((((((b, CCA), mapx), sets'), bd'), wits), SOME rel), SOME pred) lthy;
val phi =
Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_def])
@@ -394,7 +411,7 @@
val ((Asets, lives), _(*names_lthy*)) = lthy
|> 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;
+ val xs = map (fn T => Const (@{const_name undefined}, T)) killedAs @ lives;
val T = mk_T_of_bnf Ds As bnf;
@@ -402,6 +419,9 @@
val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
(*bnf.rel (op =) ... (op =)*)
val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs);
+ (*bnf.pred (%_. True) ... (%_ True)*)
+ val pred = Term.list_comb (mk_pred_of_bnf Ds As bnf,
+ map (fn T => Term.absdummy T @{term True}) killedAs);
val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
val sets = drop n bnf_sets;
@@ -448,8 +468,10 @@
rtac ctxt thm 1
end;
+ fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm;
+
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -460,7 +482,8 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (Ds @ killedAs))
- Binding.empty Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
+ Binding.empty Binding.empty Binding.empty []
+ (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -501,6 +524,8 @@
fold_rev Term.absdummy (map2 (curry op -->) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
(*%Q1 ... Qn. bnf.rel*)
val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
+ (*%P1 ... Pn. bnf.pred*)
+ val pred = fold_rev Term.absdummy (map mk_pred1T newAs) (mk_pred_of_bnf Ds As 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;
@@ -542,8 +567,10 @@
fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm;
+ fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm;
+
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -551,7 +578,8 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
- Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
+ Binding.empty Binding.empty []
+ (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -594,6 +622,9 @@
(*%Q(1) ... Q(n). bnf.rel Q\<sigma>(1) ... Q\<sigma>(n)*)
val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
(Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0))));
+ (*%P(1) ... P(n). bnf.pred P\<sigma>(1) ... P\<sigma>(n)*)
+ val pred = fold_rev Term.absdummy (permute (map mk_pred1T As))
+ (Term.list_comb (mk_pred_of_bnf Ds As bnf, unpermute (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;
@@ -624,8 +655,10 @@
fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm;
+ fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm;
+
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -633,7 +666,8 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty
- Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
+ Binding.empty Binding.empty []
+ (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -788,9 +822,10 @@
(Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live @{sort type}) lthy1);
- val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
+ val ((((fs, fs'), (Rs, Rs')), (Ps, Ps')), _(*names_lthy*)) = lthy
|> mk_Frees' "f" (map2 (curry op -->) As Bs)
- ||>> mk_Frees' "R" (map2 mk_pred2T As Bs);
+ ||>> mk_Frees' "R" (map2 mk_pred2T As Bs)
+ ||>> mk_Frees' "P" (map mk_pred1T As);
val repTA = mk_T_of_bnf Ds As bnf;
val T_bind = qualify b;
@@ -821,6 +856,8 @@
val bnf_bd = mk_bd_of_bnf Ds As bnf;
val bnf_rel = fold_rev Term.absfree Rs' (mk_vimage2p RepA RepB $
(Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, Rs)));
+ val bnf_pred = fold_rev Term.absfree Ps' (HOLogic.mk_comp
+ (Term.list_comb (mk_pred_of_bnf Ds As bnf, Ps), RepA));
(*bd may depend only on dead type variables*)
val bd_repT = fst (dest_relT (fastype_of bnf_bd));
@@ -873,11 +910,15 @@
type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
type_definition RS @{thm vimage2p_relcompp_converse}]) THEN'
rtac ctxt refl) 1;
+ fun pred_set_tac ctxt =
+ HEADGOAL (EVERY'
+ [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\<lambda>f. f o _"]} RS trans),
+ SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), rtac ctxt refl]);
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac
(map set_map0_tac (set_map0_of_bnf bnf))
(fn ctxt => rtac ctxt bd_card_order 1) (fn ctxt => rtac ctxt bd_cinfinite 1)
- set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
+ set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac;
val bnf_wits = map (fn (I, t) =>
fold Term.absdummy (map (nth As) I)
@@ -890,8 +931,8 @@
val (bnf', lthy') =
bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads)
- Binding.empty Binding.empty []
- ((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
+ Binding.empty Binding.empty Binding.empty []
+ (((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel), SOME bnf_pred) lthy;
val unfolds = @{thm id_bnf_apply} ::
(#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Wed Feb 17 21:08:18 2016 +0100
@@ -30,6 +30,7 @@
val mk_le_rel_OO_tac: Proof.context -> thm -> thm -> thm list -> tactic
val mk_simple_rel_OO_Grp_tac: Proof.context -> thm -> thm -> tactic
+ val mk_simple_pred_set_tac: Proof.context -> thm -> thm -> tactic
val mk_simple_wit_tac: Proof.context -> thm list -> tactic
val mk_simplified_set_tac: Proof.context -> thm -> tactic
val bd_ordIso_natLeq_tac: Proof.context -> tactic
@@ -229,11 +230,16 @@
(* Miscellaneous *)
fun mk_le_rel_OO_tac ctxt outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
- EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono ::
- inner_le_rel_OOs)) 1;
+ HEADGOAL (EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono ::
+ inner_le_rel_OOs)));
fun mk_simple_rel_OO_Grp_tac ctxt rel_OO_Grp in_alt_thm =
- rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
+ HEADGOAL (rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]));
+
+fun mk_simple_pred_set_tac ctxt pred_set in_alt_thm =
+ HEADGOAL (rtac ctxt (pred_set RS trans)) THEN
+ unfold_thms_tac ctxt @{thms Ball_Collect UNIV_def} THEN
+ HEADGOAL (rtac ctxt (unfold_thms ctxt @{thms UNIV_def} in_alt_thm RS @{thm Collect_inj} RS sym));
fun mk_simple_wit_tac ctxt wit_thms =
ALLGOALS (assume_tac ctxt ORELSE' eresolve_tac ctxt (@{thm emptyE} :: wit_thms));
--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Feb 17 21:08:18 2016 +0100
@@ -32,18 +32,21 @@
val nwits_of_bnf: bnf -> int
val mapN: string
+ val predN: string
val relN: string
val setN: string
val mk_setN: int -> string
val mk_witN: int -> string
val map_of_bnf: bnf -> term
+ val pred_of_bnf: bnf -> term
+ val rel_of_bnf: bnf -> term
val sets_of_bnf: bnf -> term list
- val rel_of_bnf: bnf -> term
val mk_T_of_bnf: typ list -> typ list -> bnf -> typ
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 -> 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_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list
@@ -60,10 +63,12 @@
val in_rel_of_bnf: bnf -> thm
val inj_map_of_bnf: bnf -> thm
val inj_map_strong_of_bnf: bnf -> thm
+ val le_rel_OO_of_bnf: bnf -> thm
val map_comp0_of_bnf: bnf -> thm
val map_comp_of_bnf: bnf -> thm
val map_cong0_of_bnf: bnf -> thm
val map_cong_of_bnf: bnf -> thm
+ val map_cong_pred_of_bnf: bnf -> thm
val map_cong_simp_of_bnf: bnf -> thm
val map_def_of_bnf: bnf -> thm
val map_id0_of_bnf: bnf -> thm
@@ -71,27 +76,38 @@
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
- val rel_def_of_bnf: bnf -> thm
+ val pred_cong0_of_bnf: bnf -> thm
+ val pred_cong_of_bnf: bnf -> thm
+ val pred_cong_simp_of_bnf: bnf -> thm
+ val pred_def_of_bnf: bnf -> thm
+ val pred_map_of_bnf: bnf -> thm
+ val pred_mono_strong0_of_bnf: bnf -> thm
+ val pred_mono_strong_of_bnf: bnf -> thm
+ val pred_set_of_bnf: bnf -> thm
+ val pred_rel_of_bnf: bnf -> thm
+ val pred_transfer_of_bnf: bnf -> thm
+ val pred_True_of_bnf: bnf -> thm
val rel_Grp_of_bnf: bnf -> thm
+ val rel_OO_Grp_of_bnf: bnf -> thm
val rel_OO_of_bnf: bnf -> thm
- val rel_OO_Grp_of_bnf: bnf -> thm
val rel_cong0_of_bnf: bnf -> thm
val rel_cong_of_bnf: bnf -> thm
val rel_cong_simp_of_bnf: bnf -> thm
val rel_conversep_of_bnf: bnf -> thm
+ val rel_def_of_bnf: bnf -> thm
+ val rel_eq_of_bnf: bnf -> thm
+ val rel_flip_of_bnf: bnf -> thm
+ val rel_map_of_bnf: bnf -> thm list
val rel_mono_of_bnf: bnf -> thm
val rel_mono_strong0_of_bnf: bnf -> thm
val rel_mono_strong_of_bnf: bnf -> thm
+ val rel_eq_onp_of_bnf: bnf -> thm
val rel_refl_of_bnf: bnf -> thm
val rel_refl_strong_of_bnf: bnf -> thm
val rel_reflp_of_bnf: bnf -> thm
val rel_symp_of_bnf: bnf -> thm
+ val rel_transfer_of_bnf: bnf -> thm
val rel_transp_of_bnf: bnf -> thm
- val rel_map_of_bnf: bnf -> thm list
- val rel_transfer_of_bnf: bnf -> thm
- val rel_eq_of_bnf: bnf -> thm
- val rel_flip_of_bnf: bnf -> thm
val set_bd_of_bnf: bnf -> thm list
val set_defs_of_bnf: bnf -> thm list
val set_map0_of_bnf: bnf -> thm list
@@ -101,6 +117,7 @@
val wit_thmss_of_bnf: bnf -> thm list list
val mk_map: int -> typ list -> typ list -> term -> term
+ val mk_pred: typ list -> term -> term
val mk_rel: int -> typ list -> typ list -> term -> term
val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> (typ * typ -> term) ->
@@ -114,7 +131,7 @@
val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
val wits_of_bnf: bnf -> nonemptiness_witness list
- val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
+ val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
datatype fact_policy = Dont_Note | Note_Some | Note_All
@@ -128,30 +145,34 @@
val print_bnfs: Proof.context -> unit
val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool ->
(binding -> binding) -> (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) ->
- typ list option -> binding -> binding -> binding list ->
- (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
+ typ list option -> binding -> binding -> binding -> binding list ->
+ ((((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option) * 'b option ->
+ Proof.context ->
string * term list * ((Proof.context -> thm list -> tactic) option * term list list) *
((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
local_theory * thm list
val define_bnf_consts: inline_policy -> fact_policy -> bool -> typ list option ->
- binding -> binding -> binding list ->
- (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
+ binding -> binding -> binding -> binding list ->
+ ((((((binding * typ) * term) * term list) * term) * term list) * term option) * term option ->
+ local_theory ->
((typ list * typ list * typ list * typ) *
- (term * term list * term * (int list * term) list * term) *
- (thm * thm list * thm * thm list * thm) *
+ (term * term list * term * (int list * term) list * term * term) *
+ (thm * thm list * thm * thm list * thm * thm) *
((typ list -> typ list -> typ list -> term) *
(typ list -> typ list -> term -> term) *
(typ list -> typ list -> typ -> typ) *
(typ list -> typ list -> typ list -> term) *
- (typ list -> typ list -> typ list -> term))) * local_theory
+ (typ list -> typ list -> term) *
+ (typ list -> typ list -> typ list -> term) *
+ (typ list -> typ list -> term))) * local_theory
val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> (binding -> binding) ->
(Proof.context -> tactic) list -> (Proof.context -> tactic) -> typ list option -> binding ->
- binding -> binding list ->
- (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
- bnf * local_theory
- val bnf_cmd: ((((((binding * string) * string) * string list) * string) * string list)
- * string option) * (Proof.context -> Plugin_Name.filter) ->
+ binding -> binding -> binding list ->
+ ((((((binding * typ) * term) * term list) * term) * term list) * term option) * term option ->
+ local_theory -> bnf * local_theory
+ val bnf_cmd: (((((((binding * string) * string) * string list) * string) * string list)
+ * string option) * string option) * (Proof.context -> Plugin_Name.filter) ->
Proof.context -> Proof.state
end;
@@ -174,12 +195,13 @@
bd_cinfinite: thm,
set_bd: thm list,
le_rel_OO: thm,
- rel_OO_Grp: thm
+ rel_OO_Grp: thm,
+ pred_set: thm
};
-fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), le_rel_OO), rel) =
+fun mk_axioms' (((((((((id, comp), cong), map), c_o), cinf), set_bd), le_rel_OO), rel), pred) =
{map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o,
- bd_cinfinite = cinf, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel};
+ bd_cinfinite = cinf, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel, pred_set = pred};
fun dest_cons [] = raise List.Empty
| dest_cons (x :: xs) = (x, xs);
@@ -194,19 +216,15 @@
||>> dest_cons
||>> chop n
||>> dest_cons
+ ||>> dest_cons
||> the_single
|> mk_axioms';
-fun zip_axioms mid mcomp mcong smap bdco bdinf sbd le_rel_OO rel =
- [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel];
-
-fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
- le_rel_OO, rel_OO_Grp} =
- zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd le_rel_OO
- rel_OO_Grp;
+fun zip_axioms mid mcomp mcong smap bdco bdinf sbd le_rel_OO rel pred =
+ [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel, pred];
fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
- le_rel_OO, rel_OO_Grp} =
+ le_rel_OO, rel_OO_Grp,pred_set} =
{map_id0 = f map_id0,
map_comp0 = f map_comp0,
map_cong0 = f map_cong0,
@@ -215,20 +233,22 @@
bd_cinfinite = f bd_cinfinite,
set_bd = map f set_bd,
le_rel_OO = f le_rel_OO,
- rel_OO_Grp = f rel_OO_Grp};
+ rel_OO_Grp = f rel_OO_Grp,
+ pred_set = f pred_set};
val morph_axioms = map_axioms o Morphism.thm;
type defs = {
map_def: thm,
set_defs: thm list,
- rel_def: thm
+ rel_def: thm,
+ pred_def: thm
}
-fun mk_defs map sets rel = {map_def = map, set_defs = sets, rel_def = rel};
+fun mk_defs map sets rel pred = {map_def = map, set_defs = sets, rel_def = rel, pred_def = pred};
-fun map_defs f {map_def, set_defs, rel_def} =
- {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def};
+fun map_defs f {map_def, set_defs, rel_def, pred_def} =
+ {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def, pred_def = f pred_def};
val morph_defs = map_defs o Morphism.thm;
@@ -246,6 +266,7 @@
map_comp: thm lazy,
map_cong: thm lazy,
map_cong_simp: thm lazy,
+ map_cong_pred: thm lazy,
map_id: thm lazy,
map_ident0: thm lazy,
map_ident: thm lazy,
@@ -269,14 +290,25 @@
rel_reflp: thm lazy,
rel_symp: thm lazy,
rel_transp: thm lazy,
- rel_transfer: thm lazy
+ rel_transfer: thm lazy,
+ rel_eq_onp: thm lazy,
+ pred_transfer: thm lazy,
+ pred_True: thm lazy,
+ pred_map: thm lazy,
+ pred_rel: thm lazy,
+ pred_mono_strong0: thm lazy,
+ pred_mono_strong: thm lazy,
+ pred_cong0: thm lazy,
+ pred_cong: thm lazy,
+ pred_cong_simp: thm lazy
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
- inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident map_transfer
- rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono rel_mono_strong0
- rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp
- rel_symp rel_transp rel_transfer = {
+ inj_map inj_map_strong map_comp map_cong map_cong_simp map_cong_pred map_id map_ident0 map_ident
+ map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono
+ rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl
+ rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp pred_transfer pred_True
+ pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0 pred_cong pred_cong_simp = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
@@ -290,6 +322,7 @@
map_comp = map_comp,
map_cong = map_cong,
map_cong_simp = map_cong_simp,
+ map_cong_pred = map_cong_pred,
map_id = map_id,
map_ident0 = map_ident0,
map_ident = map_ident,
@@ -313,7 +346,17 @@
rel_reflp = rel_reflp,
rel_symp = rel_symp,
rel_transp = rel_transp,
- set_transfer = set_transfer};
+ set_transfer = set_transfer,
+ rel_eq_onp = rel_eq_onp,
+ pred_transfer = pred_transfer,
+ pred_True = pred_True,
+ pred_map = pred_map,
+ pred_rel = pred_rel,
+ pred_mono_strong0 = pred_mono_strong0,
+ pred_mono_strong = pred_mono_strong,
+ pred_cong0 = pred_cong0,
+ pred_cong = pred_cong,
+ pred_cong_simp = pred_cong_simp};
fun map_facts f {
bd_Card_order,
@@ -329,6 +372,7 @@
map_comp,
map_cong,
map_cong_simp,
+ map_cong_pred,
map_id,
map_ident0,
map_ident,
@@ -352,7 +396,17 @@
rel_reflp,
rel_symp,
rel_transp,
- set_transfer} =
+ set_transfer,
+ rel_eq_onp,
+ pred_transfer,
+ pred_True,
+ pred_map,
+ pred_rel,
+ pred_mono_strong0,
+ pred_mono_strong,
+ pred_cong0,
+ pred_cong,
+ pred_cong_simp} =
{bd_Card_order = f bd_Card_order,
bd_Cinfinite = f bd_Cinfinite,
bd_Cnotzero = f bd_Cnotzero,
@@ -366,6 +420,7 @@
map_comp = Lazy.map f map_comp,
map_cong = Lazy.map f map_cong,
map_cong_simp = Lazy.map f map_cong_simp,
+ map_cong_pred = Lazy.map f map_cong_pred,
map_id = Lazy.map f map_id,
map_ident0 = Lazy.map f map_ident0,
map_ident = Lazy.map f map_ident,
@@ -389,7 +444,17 @@
rel_reflp = Lazy.map f rel_reflp,
rel_symp = Lazy.map f rel_symp,
rel_transp = Lazy.map f rel_transp,
- set_transfer = Lazy.map (map f) set_transfer};
+ set_transfer = Lazy.map (map f) set_transfer,
+ rel_eq_onp = Lazy.map f rel_eq_onp,
+ pred_transfer = Lazy.map f pred_transfer,
+ pred_True = Lazy.map f pred_True,
+ pred_map = Lazy.map f pred_map,
+ pred_rel = Lazy.map f pred_rel,
+ pred_mono_strong0 = Lazy.map f pred_mono_strong0,
+ pred_mono_strong = Lazy.map f pred_mono_strong,
+ pred_cong0 = Lazy.map f pred_cong0,
+ pred_cong = Lazy.map f pred_cong,
+ pred_cong_simp = Lazy.map f pred_cong_simp};
val morph_facts = map_facts o Morphism.thm;
@@ -419,7 +484,8 @@
facts: facts,
nwits: int,
wits: nonemptiness_witness list,
- rel: term
+ rel: term,
+ pred: term
};
(* getters *)
@@ -482,13 +548,20 @@
Term.subst_atomic_types
((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#rel bnf_rep)
end;
+val pred_of_bnf = #pred o rep_bnf;
+fun mk_pred_of_bnf Ds Ts bnf =
+ let val bnf_rep = rep_bnf bnf;
+ in
+ Term.subst_atomic_types
+ ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)) (#pred bnf_rep)
+ end;
(*thms*)
-val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
-val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf;
val bd_Card_order_of_bnf = #bd_Card_order o #facts o rep_bnf;
val bd_Cinfinite_of_bnf = #bd_Cinfinite o #facts o rep_bnf;
val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf;
+val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
+val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf;
val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf;
val in_bd_of_bnf = Lazy.force o #in_bd o #facts o rep_bnf;
val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
@@ -496,29 +569,42 @@
val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
val inj_map_of_bnf = Lazy.force o #inj_map o #facts o rep_bnf;
val inj_map_strong_of_bnf = Lazy.force o #inj_map_strong o #facts o rep_bnf;
+val le_rel_OO_of_bnf = #le_rel_OO o #axioms 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;
+val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
+val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
+val map_cong_pred_of_bnf = Lazy.force o #map_cong_pred o #facts o rep_bnf;
+val map_cong_simp_of_bnf = Lazy.force o #map_cong_simp o #facts o rep_bnf;
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;
-val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
-val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
-val map_cong_simp_of_bnf = Lazy.force o #map_cong_simp o #facts o rep_bnf;
val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
-val le_rel_OO_of_bnf = #le_rel_OO o #axioms o rep_bnf;
+val rel_eq_onp_of_bnf = Lazy.force o #rel_eq_onp o #facts o rep_bnf;
+val pred_def_of_bnf = #pred_def o #defs o rep_bnf;
+val pred_map_of_bnf = Lazy.force o #pred_map o #facts o rep_bnf;
+val pred_mono_strong0_of_bnf = Lazy.force o #pred_mono_strong0 o #facts o rep_bnf;
+val pred_mono_strong_of_bnf = Lazy.force o #pred_mono_strong o #facts o rep_bnf;
+val pred_cong0_of_bnf = Lazy.force o #pred_cong0 o #facts o rep_bnf;
+val pred_cong_of_bnf = Lazy.force o #pred_cong o #facts o rep_bnf;
+val pred_cong_simp_of_bnf = Lazy.force o #pred_cong_simp o #facts o rep_bnf;
+val pred_rel_of_bnf = Lazy.force o #pred_rel o #facts o rep_bnf;
+val pred_set_of_bnf = #pred_set o #axioms o rep_bnf;
+val pred_transfer_of_bnf = Lazy.force o #pred_transfer o #facts o rep_bnf;
+val pred_True_of_bnf = Lazy.force o #pred_True o #facts o rep_bnf;
+val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
+val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf;
+val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
+val rel_cong0_of_bnf = Lazy.force o #rel_cong0 o #facts o rep_bnf;
+val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
+val rel_cong_simp_of_bnf = Lazy.force o #rel_cong_simp o #facts o rep_bnf;
+val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts 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_map0_of_bnf = #set_map0 o #axioms o rep_bnf;
-val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
-val set_transfer_of_bnf = Lazy.force o #set_transfer o #facts o rep_bnf;
-val rel_cong0_of_bnf = Lazy.force o #rel_cong0 o #facts o rep_bnf;
-val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
-val rel_cong_simp_of_bnf = Lazy.force o #rel_cong_simp o #facts o rep_bnf;
+val rel_map_of_bnf = Lazy.force o #rel_map o #facts o rep_bnf;
val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
@@ -526,33 +612,33 @@
val rel_refl_strong_of_bnf = Lazy.force o #rel_refl_strong o #facts o rep_bnf;
val rel_reflp_of_bnf = Lazy.force o #rel_reflp o #facts o rep_bnf;
val rel_symp_of_bnf = Lazy.force o #rel_symp o #facts o rep_bnf;
+val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf;
val rel_transp_of_bnf = Lazy.force o #rel_transp o #facts o rep_bnf;
-val rel_map_of_bnf = Lazy.force o #rel_map o #facts o rep_bnf;
-val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf;
-val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
-val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
-val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
-val rel_OO_Grp_of_bnf = #rel_OO_Grp 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_map0_of_bnf = #set_map0 o #axioms o rep_bnf;
+val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
+val set_transfer_of_bnf = Lazy.force o #set_transfer o #facts 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 rel =
+fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel pred =
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, rel = rel};
+ nwits = length wits, wits = wits, rel = rel, pred = pred};
-fun map_bnf f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16
+fun map_bnf f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17
(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, rel = rel}) =
+ nwits = nwits, wits = wits, rel = rel, pred = pred}) =
BNF {name = f1 name, T = f2 T,
live = f3 live, lives = f4 lives, lives' = f5 lives', dead = f6 dead, deads = f7 deads,
map = f8 map, sets = f9 sets, bd = f10 bd,
axioms = f11 axioms, defs = f12 defs, facts = f13 facts,
- nwits = f14 nwits, wits = f15 wits, rel = f16 rel};
+ nwits = f14 nwits, wits = f15 wits, rel = f16 rel, pred = f17 pred};
fun morph_bnf phi =
let
@@ -560,10 +646,10 @@
val tphi = Morphism.term phi;
in
map_bnf (Morphism.binding phi) Tphi I (map Tphi) (map Tphi) I (map Tphi) tphi (map tphi) tphi
- (morph_axioms phi) (morph_defs phi) (morph_facts phi) I (map (morph_witness phi)) tphi
+ (morph_axioms phi) (morph_defs phi) (morph_facts phi) I (map (morph_witness phi)) tphi tphi
end;
-fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I;
+fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I I;
val transfer_bnf = morph_bnf o Morphism.transfer_morphism;
@@ -600,6 +686,15 @@
in Envir.subst_term (tyenv, Vartab.empty) rel end
handle Type.TYPE_MATCH => error "Bad relator";
+fun normalize_pred ctxt instTs instA pred =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val tyenv =
+ Sign.typ_match thy (fastype_of pred, Library.foldr (op -->) (instTs, mk_pred1T instA))
+ Vartab.empty;
+ in Envir.subst_term (tyenv, Vartab.empty) pred end
+ handle Type.TYPE_MATCH => error "Bad predicator";
+
fun normalize_wit insts CA As wit =
let
fun strip_param (Ts, T as Type (@{type_name fun}, [T1, T2])) =
@@ -626,6 +721,11 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
+fun mk_pred Ts t =
+ let val Type (_, Ts0) = domain_type (body_fun_type (fastype_of t)) in
+ Term.subst_atomic_types (Ts0 ~~ Ts) t
+ end;
+
fun mk_rel live Ts Us t =
let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
@@ -677,49 +777,61 @@
val witN = "wit";
fun mk_witN i = witN ^ nonzero_string_of_int i;
val relN = "rel";
+val predN = "pred";
-val bd_card_orderN = "bd_card_order";
-val bd_cinfiniteN = "bd_cinfinite";
val bd_Card_orderN = "bd_Card_order";
val bd_CinfiniteN = "bd_Cinfinite";
val bd_CnotzeroN = "bd_Cnotzero";
+val bd_card_orderN = "bd_card_order";
+val bd_cinfiniteN = "bd_cinfinite";
val collect_set_mapN = "collect_set_map";
val in_bdN = "in_bd";
val in_monoN = "in_mono";
val in_relN = "in_rel";
val inj_mapN = "inj_map";
val inj_map_strongN = "inj_map_strong";
-val map_id0N = "map_id0";
-val map_idN = "map_id";
-val map_identN = "map_ident";
val map_comp0N = "map_comp0";
val map_compN = "map_comp";
val map_cong0N = "map_cong0";
val map_congN = "map_cong";
val map_cong_simpN = "map_cong_simp";
+val map_cong_predN = "map_cong_pred";
+val map_id0N = "map_id0";
+val map_idN = "map_id";
+val map_identN = "map_ident";
val map_transferN = "map_transfer";
+val pred_mono_strong0N = "pred_mono_strong0";
+val pred_mono_strongN = "pred_mono_strong";
+val pred_transferN = "pred_transfer";
+val pred_TrueN = "pred_True";
+val pred_mapN = "pred_map";
+val pred_relN = "pred_rel";
+val pred_setN = "pred_set";
+val pred_congN = "pred_cong";
+val pred_cong_simpN = "pred_cong_simp";
+val rel_GrpN = "rel_Grp";
+val rel_comppN = "rel_compp";
+val rel_compp_GrpN = "rel_compp_Grp";
+val rel_congN = "rel_cong";
+val rel_cong_simpN = "rel_cong_simp";
+val rel_conversepN = "rel_conversep";
val rel_eqN = "rel_eq";
+val rel_eq_onpN = "rel_eq_onp";
val rel_flipN = "rel_flip";
-val set_map0N = "set_map0";
-val set_mapN = "set_map";
-val set_bdN = "set_bd";
-val set_transferN = "set_transfer";
-val rel_GrpN = "rel_Grp";
-val rel_conversepN = "rel_conversep";
val rel_mapN = "rel_map";
val rel_monoN = "rel_mono";
val rel_mono_strong0N = "rel_mono_strong0";
val rel_mono_strongN = "rel_mono_strong";
-val rel_congN = "rel_cong";
-val rel_cong_simpN = "rel_cong_simp";
val rel_reflN = "rel_refl";
val rel_refl_strongN = "rel_refl_strong";
val rel_reflpN = "rel_reflp";
val rel_sympN = "rel_symp";
+val rel_transferN = "rel_transfer";
val rel_transpN = "rel_transp";
-val rel_transferN = "rel_transfer";
-val rel_comppN = "rel_compp";
-val rel_compp_GrpN = "rel_compp_Grp";
+val set_bdN = "set_bd";
+val set_map0N = "set_map0";
+val set_mapN = "set_map";
+val set_transferN = "set_transfer";
datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
@@ -755,6 +867,7 @@
(in_monoN, [Lazy.force (#in_mono facts)]),
(map_comp0N, [#map_comp0 axioms]),
(rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
+ (pred_mono_strong0N, [Lazy.force (#pred_mono_strong0 facts)]),
(set_map0N, #set_map0 axioms),
(set_bdN, #set_bd axioms)] @
(witNs ~~ wit_thmss_of_bnf bnf)
@@ -775,14 +888,24 @@
(map_cong0N, [#map_cong0 axioms], []),
(map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
(map_cong_simpN, [Lazy.force (#map_cong_simp facts)], []),
+ (map_cong_predN, [Lazy.force (#map_cong_pred facts)], []),
(map_idN, [Lazy.force (#map_id facts)], []),
(map_id0N, [#map_id0 axioms], []),
(map_transferN, [Lazy.force (#map_transfer facts)], []),
(map_identN, [Lazy.force (#map_ident facts)], []),
+ (pred_mono_strongN, [Lazy.force (#pred_mono_strong facts)], []),
+ (pred_congN, [Lazy.force (#pred_cong facts)], fundefcong_attrs),
+ (pred_cong_simpN, [Lazy.force (#pred_cong_simp facts)], []),
+ (pred_mapN, [Lazy.force (#pred_map facts)], []),
+ (pred_relN, [Lazy.force (#pred_rel facts)], []),
+ (pred_transferN, [Lazy.force (#pred_transfer facts)], []),
+ (pred_TrueN, [Lazy.force (#pred_True facts)], []),
+ (pred_setN, [#pred_set axioms], []),
(rel_comppN, [Lazy.force (#rel_OO facts)], []),
(rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
(rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
(rel_eqN, [Lazy.force (#rel_eq facts)], []),
+ (rel_eq_onpN, [Lazy.force (#rel_eq_onp facts)], []),
(rel_flipN, [Lazy.force (#rel_flip facts)], []),
(rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
(rel_mapN, Lazy.force (#rel_map facts), []),
@@ -831,8 +954,9 @@
(* Define new BNFs *)
-fun define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
- ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy =
+fun define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b pred_b set_bs
+ (((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt), pred_rhs_opt)
+ no_defs_lthy =
let
val live = length set_rhss;
@@ -947,7 +1071,7 @@
(*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
- val OO_Grp =
+ val rel_spec =
let
val map1 = Term.list_comb (mk_bnf_map Ds RTs As, map fst_const RTs);
val map2 = Term.list_comb (mk_bnf_map Ds RTs Bs, map snd_const RTs);
@@ -957,12 +1081,34 @@
|> fold_rev Term.absfree Rs'
end;
- val rel_rhs = the_default OO_Grp rel_rhs_opt;
+ val rel_rhs = the_default rel_spec rel_rhs_opt;
val rel_bind_def =
(fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b),
rel_rhs);
+ val pred_spec =
+ if live = 0 then Term.absdummy (mk_bnf_T Ds As Calpha) @{term True} else
+ let
+ val sets = map (mk_bnf_t Ds As) bnf_sets;
+ val argTs = map mk_pred1T As;
+ val T = mk_bnf_T Ds As Calpha;
+ val ((Ps, Ps'), x) = lthy
+ |> mk_Frees' "P" argTs
+ ||>> yield_singleton (mk_Frees "x") T
+ |> fst;
+ val conjs = map2 (fn set => fn P => mk_Ball (set $ x) P) sets Ps;
+ in
+ fold_rev Term.absfree Ps'
+ (Term.absfree (dest_Free x) (Library.foldr1 HOLogic.mk_conj conjs))
+ end;
+
+ val pred_rhs = the_default pred_spec pred_rhs_opt;
+
+ val pred_bind_def =
+ (fn () => def_qualify (if Binding.is_empty pred_b then mk_prefix_binding predN else pred_b),
+ pred_rhs);
+
val wit_rhss =
if null wit_rhss then
[fold_rev Term.absdummy As (Term.list_comb (mk_bnf_map Ds As As,
@@ -976,10 +1122,12 @@
else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits);
in bs ~~ wit_rhss end;
- val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
+ val ((((bnf_rel_term, raw_rel_def), (bnf_pred_term, raw_pred_def)),
+ (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
lthy
|> Local_Theory.open_target |> snd
|> maybe_define (is_some rel_rhs_opt) rel_bind_def
+ ||>> maybe_define (is_some pred_rhs_opt) pred_bind_def
||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs
||> `Local_Theory.close_target;
@@ -990,22 +1138,30 @@
normalize_rel lthy (map2 mk_pred2T As' Bs') (mk_bnf_T Ds As' Calpha) (mk_bnf_T Ds Bs' Calpha)
bnf_rel;
+ val bnf_pred_def = Morphism.thm phi raw_pred_def;
+ val bnf_pred = Morphism.term phi bnf_pred_term;
+ fun mk_bnf_pred Ds As' =
+ normalize_pred lthy (map mk_pred1T As') (mk_bnf_T Ds As' Calpha) bnf_pred;
+
val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs;
val bnf_wits =
map (normalize_wit Calpha_params Calpha alphas o Morphism.term phi) bnf_wit_terms;
- fun mk_OO_Grp Ds' As' Bs' =
- Term.subst_atomic_types ((Ds ~~ Ds') @ (As ~~ As') @ (Bs ~~ Bs')) OO_Grp;
+ fun mk_rel_spec Ds' As' Bs' =
+ Term.subst_atomic_types ((Ds ~~ Ds') @ (As ~~ As') @ (Bs ~~ Bs')) rel_spec;
+
+ fun mk_pred_spec Ds' As' =
+ Term.subst_atomic_types ((Ds ~~ Ds') @ (As ~~ As')) pred_spec;
in
(((alphas, betas, deads, Calpha),
- (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
- (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
- (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy)
+ (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel, bnf_pred),
+ (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def, bnf_pred_def),
+ (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_bnf_pred, mk_rel_spec, mk_pred_spec)), lthy)
end;
fun prepare_def const_policy mk_fact_policy internal qualify prep_typ prep_term Ds_opt map_b rel_b
- set_bs ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
- no_defs_lthy =
+ pred_b set_bs (((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt),
+ raw_pred_opt) no_defs_lthy =
let
val fact_policy = mk_fact_policy no_defs_lthy;
val bnf_b = qualify raw_bnf_b;
@@ -1017,6 +1173,7 @@
val bd_rhs = prep_term no_defs_lthy raw_bd;
val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
val rel_rhs_opt = Option.map (prep_term no_defs_lthy) raw_rel_opt;
+ val pred_rhs_opt = Option.map (prep_term no_defs_lthy) raw_pred_opt;
fun err T =
error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
@@ -1031,11 +1188,12 @@
else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
val (((alphas, betas, deads, Calpha),
- (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
- (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
- (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) =
- define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs
- ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy;
+ (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel, bnf_pred),
+ (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def, bnf_pred_def),
+ (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, _, mk_rel_spec, mk_pred_spec)), lthy) =
+ define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b pred_b set_bs
+ (((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt), pred_rhs_opt)
+ no_defs_lthy;
val dead = length deads;
@@ -1057,6 +1215,8 @@
val mk_bnf_t = mk_bnf_t_Ds Ds;
val mk_bnf_T = mk_bnf_T_Ds Ds;
+ val pred1PTs = map mk_pred1T As';
+ val pred1QTs = map mk_pred1T Bs';
val pred2RTs = map2 mk_pred2T As' Bs';
val pred2RTsAsCs = map2 mk_pred2T As' Cs;
val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
@@ -1083,11 +1243,11 @@
val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets;
val bnf_bd_As = mk_bnf_t As' bnf_bd;
fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
+ fun mk_bnf_pred PTs CA = normalize_pred lthy PTs CA bnf_pred;
- val pre_names_lthy = lthy;
- val (((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), y'), zs), zs'), ys), As),
- As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs), S_BsEs),
- transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
+ val ((((((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), y'), zs), zs'), ys), As),
+ As_copy), bs), (Ps, Ps')), Ps_copy), Qs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs), S_BsEs),
+ transfer_domRs), transfer_ranRs), _) = lthy
|> mk_Frees "f" (map2 (curry op -->) As' Bs')
||>> mk_Frees "f" (map2 (curry op -->) As' Bs')
||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs)
@@ -1103,6 +1263,9 @@
||>> mk_Frees "A" (map HOLogic.mk_setT As')
||>> mk_Frees "A" (map HOLogic.mk_setT As')
||>> mk_Frees "b" As'
+ ||>> mk_Frees' "P" pred1PTs
+ ||>> mk_Frees "P" pred1PTs
+ ||>> mk_Frees "Q" pred1QTs
||>> mk_Frees "R" pred2RTs
||>> mk_Frees "R" pred2RTs
||>> mk_Frees "S" pred2RTsBsCs
@@ -1117,6 +1280,8 @@
val y_copy = retype_const_or_free CB' x';
val rel = mk_bnf_rel pred2RTs CA' CB';
+ val pred = mk_bnf_pred pred1PTs CA';
+ val pred' = mk_bnf_pred pred1QTs CB';
val relCsEs = mk_bnf_rel pred2RTsCsEs CC' CE';
val relAsAs = mk_bnf_rel self_pred2RTs CA' CA';
val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
@@ -1181,10 +1346,13 @@
fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_rhs rel_OO_lhs));
val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs),
- Term.list_comb (mk_OO_Grp Ds As' Bs', Rs)));
+ Term.list_comb (mk_rel_spec Ds As' Bs', Rs)));
+
+ val pred_set_goal = fold_rev Logic.all Ps (mk_Trueprop_eq (Term.list_comb (pred, Ps),
+ Term.list_comb (mk_pred_spec Ds As', Ps)));
val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal
- card_order_bd_goal cinfinite_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal;
+ card_order_bd_goal cinfinite_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal pred_set_goal;
val mk_wit_goals = mk_wit_goals bs zs bnf_sets_As;
fun triv_wit_tac ctxt = mk_trivial_wit_tac ctxt bnf_wit_defs;
@@ -1210,7 +1378,7 @@
(*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
in
- Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
mk_collect_set_map_tac ctxt (#set_map0 axioms))
|> Thm.close_derivation
end;
@@ -1447,9 +1615,7 @@
val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
- fun mk_rel_mono_strong () = Object_Logic.rulify lthy (Lazy.force rel_mono_strong0)
-
- val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
+ val rel_mono_strong = Lazy.map (Object_Logic.rulify lthy) rel_mono_strong0;
fun mk_rel_cong_prem mk_implies x x' z z' set set' R R_copy =
Logic.all z (Logic.all z'
@@ -1475,6 +1641,99 @@
val rel_cong = Lazy.lazy (mk_rel_cong Logic.mk_implies);
val rel_cong_simp = Lazy.lazy (mk_rel_cong (fn (a, b) => @{term simp_implies} $ a $ b));
+ fun mk_pred_prems f = map2 (HOLogic.mk_Trueprop oo f) Ps Ps_copy;
+ fun mk_pred_concl f = HOLogic.mk_Trueprop
+ (f (Term.list_comb (pred, Ps), Term.list_comb (pred, Ps_copy)));
+
+ fun mk_pred_cong0 () =
+ let
+ val cong_prems = mk_pred_prems (curry HOLogic.mk_eq);
+ val cong_concl = mk_pred_concl HOLogic.mk_eq;
+ in
+ Goal.prove_sorry lthy [] []
+ (fold_rev Logic.all (Ps @ Ps_copy) (Logic.list_implies (cong_prems, cong_concl)))
+ (fn {context = ctxt, prems = _} => (TRY o hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
+ |> Thm.close_derivation
+ end;
+
+ val pred_cong0 = Lazy.lazy mk_pred_cong0;
+
+ fun mk_rel_eq_onp () =
+ let
+ val lhs = Term.list_comb (relAsAs, map mk_eq_onp Ps);
+ val rhs = mk_eq_onp (Term.list_comb (pred, Ps));
+ in
+ Goal.prove_sorry lthy (map fst Ps') [] (mk_Trueprop_eq (lhs, rhs))
+ (fn {context = ctxt, prems = _} =>
+ mk_rel_eq_onp_tac ctxt (#pred_set axioms) (#map_id0 axioms) (Lazy.force rel_Grp))
+ |> Thm.close_derivation
+ end;
+
+ val rel_eq_onp = Lazy.lazy mk_rel_eq_onp;
+ val pred_rel = Lazy.map (fn thm => thm RS sym RS @{thm eq_onp_eqD}) rel_eq_onp;
+
+ fun mk_pred_mono_strong0 () =
+ let
+ fun mk_prem setA P Q a =
+ HOLogic.mk_Trueprop
+ (mk_Ball (setA $ x) (Term.absfree (dest_Free a) (HOLogic.mk_imp (P $ a, Q $ a))));
+ val prems = HOLogic.mk_Trueprop (Term.list_comb (pred, Ps) $ x) ::
+ @{map 4} mk_prem bnf_sets_As Ps Ps_copy zs;
+ val concl = HOLogic.mk_Trueprop (Term.list_comb (pred, Ps_copy) $ x);
+ in
+ Goal.prove_sorry lthy [] []
+ (fold_rev Logic.all (x :: Ps @ Ps_copy) (Logic.list_implies (prems, concl)))
+ (fn {context = ctxt, prems = _} =>
+ mk_pred_mono_strong0_tac ctxt (Lazy.force pred_rel) (Lazy.force rel_mono_strong0))
+ |> Thm.close_derivation
+ end;
+
+ val pred_mono_strong0 = Lazy.lazy mk_pred_mono_strong0;
+
+ val pred_mono_strong = Lazy.map (Object_Logic.rulify lthy) pred_mono_strong0;
+
+ fun mk_pred_cong_prem mk_implies x z set P P_copy =
+ Logic.all z
+ (mk_implies (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (P $ z, P_copy $ z)));
+
+ fun mk_pred_cong mk_implies () =
+ let
+ val prem0 = mk_Trueprop_eq (x, x_copy);
+ val prems = @{map 4} (mk_pred_cong_prem mk_implies x_copy) zs bnf_sets_As Ps Ps_copy;
+ val eq = mk_Trueprop_eq (Term.list_comb (pred, Ps) $ x,
+ Term.list_comb (pred, Ps_copy) $ x_copy);
+ in
+ fold (Variable.add_free_names lthy) (eq :: prem0 :: prems) []
+ |> (fn vars => Goal.prove_sorry lthy vars (prem0 :: prems) eq
+ (fn {context = ctxt, prems} =>
+ mk_rel_cong_tac ctxt (chop 1 prems) (Lazy.force pred_mono_strong)))
+ |> Thm.close_derivation
+ end;
+
+ val pred_cong = Lazy.lazy (mk_pred_cong Logic.mk_implies);
+ val pred_cong_simp = Lazy.lazy (mk_pred_cong (fn (a, b) => @{term simp_implies} $ a $ b));
+
+ fun mk_map_cong_pred () =
+ let
+ val prem0 = mk_Trueprop_eq (x, x_copy);
+ fun mk_eq f g z = Term.absfree (dest_Free z) (HOLogic.mk_eq (f $ z, g $ z));
+ val prem = HOLogic.mk_Trueprop
+ (Term.list_comb (pred, @{map 3} mk_eq fs fs_copy zs) $ x_copy);
+ val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
+ Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy);
+ val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
+ (Logic.list_implies ([prem0, prem], eq));
+ in
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ unfold_thms_tac ctxt [#pred_set axioms] THEN
+ HEADGOAL (EVERY' [REPEAT_DETERM o etac ctxt conjE,
+ etac ctxt (Lazy.force map_cong) THEN_ALL_NEW
+ (etac ctxt bspec THEN' assume_tac ctxt)]))
+ |> Thm.close_derivation
+ end;
+
+ val map_cong_pred = Lazy.lazy mk_map_cong_pred;
+
fun mk_rel_map () =
let
fun mk_goal lhs rhs =
@@ -1525,7 +1784,7 @@
Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
(fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt [prop_conv_thm] THEN
- HEADGOAL (rtac ctxt (Lazy.force thm RS sym RS @{thm ord_eq_le_trans})
+ HEADGOAL (rtac ctxt (Lazy.force thm RS sym RS @{thm ord_eq_le_trans})
THEN' rtac ctxt (Lazy.force rel_mono) THEN_ALL_NEW assume_tac ctxt))
|> Thm.close_derivation
end;
@@ -1534,6 +1793,41 @@
val rel_symp = Lazy.lazy (mk_rel_preserves mk_symp @{thm symp_conversep} rel_conversep);
val rel_transp = Lazy.lazy (mk_rel_preserves mk_transp @{thm transp_relcompp} rel_OO);
+ fun mk_pred_True () =
+ let
+ val lhs = Term.list_comb (pred, map (fn T => absdummy T @{term True}) As');
+ val rhs = absdummy CA' @{term True};
+ val goal = mk_Trueprop_eq (lhs, rhs);
+ in
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} =>
+ HEADGOAL (EVERY' (map (rtac ctxt) [ext, Lazy.force pred_rel RS trans,
+ Lazy.force rel_cong0 RS fun_cong RS fun_cong RS trans OF
+ replicate live @{thm eq_onp_True},
+ Lazy.force rel_eq RS fun_cong RS fun_cong RS trans, @{thm eqTrueI[OF refl]}])))
+ |> Thm.close_derivation
+ end;
+
+ val pred_True = Lazy.lazy mk_pred_True;
+
+ fun mk_pred_map () =
+ let
+ val lhs = Term.list_comb (pred', Qs) $ (Term.list_comb (bnf_map_AsBs, fs) $ x);
+ val rhs = Term.list_comb (pred, @{map 2} (curry HOLogic.mk_comp) Qs fs) $ x;
+ val goal = mk_Trueprop_eq (lhs, rhs);
+ val vars = Variable.add_free_names lthy goal [];
+ val pred_set = #pred_set axioms RS fun_cong RS sym;
+ in
+ Goal.prove_sorry lthy vars [] goal
+ (fn {context = ctxt, prems = _} =>
+ HEADGOAL (rtac ctxt (pred_set RSN (2, pred_set RSN (2, box_equals)))) THEN
+ unfold_thms_tac ctxt (@{thm Ball_image_comp} :: map Lazy.force set_map) THEN
+ HEADGOAL (rtac ctxt refl))
+ |> Thm.close_derivation
+ end;
+
+ val pred_map = Lazy.lazy mk_pred_map;
+
fun mk_map_transfer () =
let
val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
@@ -1553,6 +1847,23 @@
val map_transfer = Lazy.lazy mk_map_transfer;
+ fun mk_pred_transfer () =
+ let
+ val iff = HOLogic.eq_const HOLogic.boolT;
+ val prem_rels = map (fn T => mk_rel_fun T iff) Rs;
+ val prem_elems = mk_rel_fun (Term.list_comb (rel, Rs)) iff;
+ val goal = HOLogic.mk_Trueprop
+ (fold_rev mk_rel_fun prem_rels prem_elems $ pred $ pred');
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
+ mk_pred_transfer_tac ctxt live (Lazy.force in_rel) (Lazy.force pred_map)
+ (Lazy.force pred_cong))
+ |> Thm.close_derivation
+ end;
+
+ val pred_transfer = Lazy.lazy mk_pred_transfer;
+
fun mk_rel_transfer () =
let
val iff = HOLogic.eq_const HOLogic.boolT;
@@ -1621,27 +1932,32 @@
val inj_map_strong = Lazy.lazy mk_inj_map_strong;
- val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
+ val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_pred_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 inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0
- map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map
- rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO
- rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer;
+ in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_cong_pred map_id
+ map_ident0 map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp
+ rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep
+ rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp
+ pred_transfer pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0
+ pred_cong pred_cong_simp;
val wits = map2 mk_witness bnf_wits wit_thms;
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)) pred;
+
val bnf = mk_bnf bnf_b Calpha live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms
- defs facts wits bnf_rel;
+ defs facts wits bnf_rel bnf_pred;
in
note_bnf_thms fact_policy qualify bnf_b bnf lthy
end;
val one_step_defs =
- no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
+ no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @
+ [bnf_rel_def, bnf_pred_def]);
in
(key, goals, wit_goalss, after_qed, lthy, one_step_defs)
end;
@@ -1661,7 +1977,8 @@
fun register_bnf plugins key bnf =
register_bnf_raw key bnf #> interpret_bnf plugins bnf;
-fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs raw_csts =
+fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b pred_b set_bs
+ raw_csts =
(fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
let
fun mk_wits_tac ctxt set_maps =
@@ -1682,8 +1999,8 @@
goals (map (fn tac => fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
|> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
- end) o prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs
- raw_csts;
+ end) o prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b pred_b
+ set_bs raw_csts;
fun bnf_cmd (raw_csts, raw_plugins) =
(fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
@@ -1702,13 +2019,14 @@
NONE => (fn _ => [], map (map (rpair [])) wit_goalss)
| SOME tac => (mk_triv_wit_thms tac, []));
in
- Proof.unfolding ([[(defs, [])]])
- (lthy
- |> Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms)
- (map (single o rpair []) goals @ nontriv_wit_goals)
- |> Proof.refine_singleton (Method.primitive_text (K I)))
+ lthy
+ |> Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms)
+ (map (single o rpair []) goals @ nontriv_wit_goals)
+ |> Proof.unfolding ([[(@{thm OO_Grp_alt} :: @{thm mem_Collect_eq} :: defs, [])]])
+ |> Proof.refine_singleton (Method.Basic (fn ctxt =>
+ Method.SIMPLE_METHOD (TRYALL (rtac ctxt refl))))
end) o prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
- NONE Binding.empty Binding.empty [] raw_csts;
+ NONE Binding.empty Binding.empty Binding.empty [] raw_csts;
fun print_bnfs ctxt =
let
@@ -1752,6 +2070,7 @@
Scan.repeat1 (Scan.unless (Parse.reserved "rel" ||
Parse.reserved "plugins") Parse.term)) [] --
Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
+ Scan.option ((Parse.reserved "pred" -- @{keyword ":"}) |-- Parse.term) --
Scan.optional Plugin_Name.parse_filter (K Plugin_Name.default_filter)
>> bnf_cmd);
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Feb 17 21:08:18 2016 +0100
@@ -2,7 +2,8 @@
Author: Dmitriy Traytel, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Author: Martin Desharnais, TU Muenchen
- Copyright 2012, 2013, 2014
+ Author: Ondrej Kuncar, TU Muenchen
+ Copyright 2012, 2013, 2014, 2015
Tactics for definition of bounded natural functors.
*)
@@ -18,7 +19,6 @@
val mk_map_comp: thm -> thm
val mk_map_cong_tac: Proof.context -> thm -> tactic
val mk_set_map: thm -> thm
- val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic
val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
val mk_rel_eq_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
@@ -29,9 +29,13 @@
val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic
val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic
- val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
+ val mk_rel_eq_onp_tac: Proof.context -> thm -> thm -> thm -> tactic
+ val mk_pred_mono_strong0_tac: Proof.context -> thm -> thm -> tactic
val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
+ val mk_pred_transfer_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
+ val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
+ val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic
val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list ->
thm -> thm -> thm -> thm -> tactic
@@ -363,7 +367,7 @@
fun mk_rel_cong_tac ctxt (eqs, prems) mono =
let
fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt;
- fun mk_tacs iffD = etac ctxt mono ::
+ fun mk_tacs iffD = etac ctxt mono ::
map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD)
|> Drule.rotate_prems ~1 |> mk_tac) prems;
in
@@ -371,4 +375,25 @@
HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2))
end;
+fun subst_conv ctxt thm =
+ Conv.arg_conv (Conv.arg_conv
+ (Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) ctxt));
+
+fun mk_rel_eq_onp_tac ctxt pred_def map_id0 rel_Grp =
+ HEADGOAL (EVERY'
+ [SELECT_GOAL (unfold_thms_tac ctxt (pred_def :: @{thms UNIV_def eq_onp_Grp Ball_Collect})),
+ CONVERSION (subst_conv ctxt (map_id0 RS sym)),
+ rtac ctxt (unfold_thms ctxt @{thms UNIV_def} rel_Grp)]);
+
+fun mk_pred_mono_strong0_tac ctxt pred_rel rel_mono_strong0 =
+ unfold_thms_tac ctxt [pred_rel] THEN
+ HEADGOAL (etac ctxt rel_mono_strong0 THEN_ALL_NEW etac ctxt @{thm eq_onp_mono0});
+
+fun mk_pred_transfer_tac ctxt n in_rel pred_map pred_cong =
+ HEADGOAL (EVERY' [REPEAT_DETERM_N (n + 1) o rtac ctxt rel_funI, dtac ctxt (in_rel RS iffD1),
+ REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt,
+ rtac ctxt (box_equals OF [@{thm _}, pred_map RS sym, pred_map RS sym]),
+ rtac ctxt (refl RS pred_cong), REPEAT_DETERM_N n o
+ (etac ctxt @{thm rel_fun_Collect_case_prodD[where B="op ="]} THEN_ALL_NEW assume_tac ctxt)]);
+
end;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 17 21:08:18 2016 +0100
@@ -10,6 +10,7 @@
sig
type fp_ctr_sugar =
{ctrXs_Tss: typ list list,
+ ctor_iff_dtor: thm,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
ctr_transfers: thm list,
@@ -26,6 +27,7 @@
rel_sels: thm list,
rel_intros: thm list,
rel_cases: thm list,
+ pred_injects: thm list,
set_thms: thm list,
set_selssss: thm list list list list,
set_introssss: thm list list list list,
@@ -146,26 +148,27 @@
thm list -> Proof.context -> gfp_sugar_thms
val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
- binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
- BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
+ binding list -> binding list list -> binding list -> (string * sort) list ->
+ typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
BNF_FP_Util.fp_result * local_theory) ->
Ctr_Sugar.ctr_options
* ((((((binding option * (typ * sort)) list * binding) * mixfix)
- * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * (binding * binding))
+ * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) *
+ (binding * binding * binding))
* term list) list ->
local_theory -> local_theory
val co_datatype_cmd: BNF_Util.fp_kind ->
- (mixfix list -> binding list -> binding list -> binding list list -> binding list ->
- (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+ (mixfix list -> binding list -> binding list -> binding list -> binding list list ->
+ binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * Proof.context) ->
((Proof.context -> Plugin_Name.filter) * bool)
* ((((((binding option * (string * string option)) list * binding) * mixfix)
* ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list)
- * (binding * binding)) * string list) list ->
+ * (binding * binding * binding)) * string list) list ->
Proof.context -> local_theory
val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
- binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
- BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
+ binding list -> binding list list -> binding list -> (string * sort) list ->
+ typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
BNF_FP_Util.fp_result * local_theory) ->
(local_theory -> local_theory) parser
end;
@@ -181,9 +184,10 @@
open BNF_FP_Util
open BNF_FP_Def_Sugar_Tactics
-val EqN = "Eq_";
+val Eq_prefix = "Eq_";
val case_transferN = "case_transfer";
+val ctor_iff_dtorN = "ctor_iff_dtor";
val ctr_transferN = "ctr_transfer";
val disc_transferN = "disc_transfer";
val sel_transferN = "sel_transfer";
@@ -192,6 +196,7 @@
val map_disc_iffN = "map_disc_iff";
val map_o_corecN = "map_o_corec";
val map_selN = "map_sel";
+val pred_injectN = "pred_inject";
val rec_o_mapN = "rec_o_map";
val rec_transferN = "rec_transfer";
val set_casesN = "set_cases";
@@ -201,6 +206,7 @@
type fp_ctr_sugar =
{ctrXs_Tss: typ list list,
+ ctor_iff_dtor: thm,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
ctr_transfers: thm list,
@@ -217,6 +223,7 @@
rel_sels: thm list,
rel_intros: thm list,
rel_cases: thm list,
+ pred_injects: thm list,
set_thms: thm list,
set_selssss: thm list list list list,
set_introssss: thm list list list list,
@@ -261,7 +268,7 @@
fun strong_co_induct_of [_, s] = s;
fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_selss, rel_injects, rel_distincts,
- rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_introssss,
+ rel_sels, rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss,
set_cases} : fp_bnf_sugar) =
{map_thms = map (Morphism.thm phi) map_thms,
map_disc_iffs = map (Morphism.thm phi) map_disc_iffs,
@@ -271,6 +278,7 @@
rel_sels = map (Morphism.thm phi) rel_sels,
rel_intros = map (Morphism.thm phi) rel_intros,
rel_cases = map (Morphism.thm phi) rel_cases,
+ pred_injects = map (Morphism.thm phi) pred_injects,
set_thms = map (Morphism.thm phi) set_thms,
set_selssss = map (map (map (map (Morphism.thm phi)))) set_selssss,
set_introssss = map (map (map (map (Morphism.thm phi)))) set_introssss,
@@ -295,9 +303,10 @@
common_set_inducts = map (Morphism.thm phi) common_set_inducts,
set_inducts = map (Morphism.thm phi) set_inducts};
-fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers, case_transfers,
- disc_transfers, sel_transfers} : fp_ctr_sugar) =
+fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctor_iff_dtor, ctr_defs, ctr_sugar, ctr_transfers,
+ case_transfers, disc_transfers, sel_transfers} : fp_ctr_sugar) =
{ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
+ ctor_iff_dtor = Morphism.thm phi ctor_iff_dtor,
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,
ctr_transfers = map (Morphism.thm phi) ctr_transfers,
@@ -348,28 +357,26 @@
structure FP_Sugar_Plugin = Plugin(type T = fp_sugar list);
fun fp_sugars_interpretation name f =
- FP_Sugar_Plugin.interpretation name
- (fn fp_sugars => fn lthy =>
- f (map (transfer_fp_sugar (Proof_Context.theory_of lthy)) fp_sugars) lthy);
+ FP_Sugar_Plugin.interpretation name (fn fp_sugars => fn lthy =>
+ f (map (transfer_fp_sugar (Proof_Context.theory_of lthy)) fp_sugars) lthy);
val interpret_fp_sugars = FP_Sugar_Plugin.data;
-fun register_fp_sugars_raw fp_sugars =
+val register_fp_sugars_raw =
fold (fn fp_sugar as {T = Type (s, _), ...} =>
- Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
- fp_sugars;
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))));
fun register_fp_sugars plugins fp_sugars =
register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars;
fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
- live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss
- common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
- rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess set_thmss set_selsssss
- set_introsssss set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
- co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts
- set_inductss sel_transferss co_rec_o_mapss noted =
+ live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars co_recs co_rec_defs
+ map_thmss common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
+ rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess pred_injectss
+ set_thmss set_selsssss set_introsssss set_casess ctr_transferss case_transferss disc_transferss
+ co_rec_disc_iffss co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss
+ common_set_inducts set_inductss sel_transferss co_rec_o_mapss noted =
let
val fp_sugars =
map_index (fn (kk, T) =>
@@ -379,6 +386,7 @@
fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
fp_ctr_sugar =
{ctrXs_Tss = nth ctrXs_Tsss kk,
+ ctor_iff_dtor = nth ctor_iff_dtors kk,
ctr_defs = nth ctr_defss kk,
ctr_sugar = nth ctr_sugars kk,
ctr_transfers = nth ctr_transferss kk,
@@ -394,6 +402,7 @@
rel_sels = nth rel_selss kk,
rel_intros = nth rel_intross kk,
rel_cases = nth rel_casess kk,
+ pred_injects = nth pred_injectss kk,
set_thms = nth set_thmss kk,
set_selssss = nth set_selsssss kk,
set_introssss = nth set_introsssss kk,
@@ -530,8 +539,9 @@
fun type_binding_of_spec (((((_, b), _), _), _), _) = b;
fun mixfix_of_spec ((((_, mx), _), _), _) = mx;
fun mixfixed_ctr_specs_of_spec (((_, mx_ctr_specs), _), _) = mx_ctr_specs;
-fun map_binding_of_spec ((_, (b, _)), _) = b;
-fun rel_binding_of_spec ((_, (_, b)), _) = b;
+fun map_binding_of_spec ((_, (b, _, _)), _) = b;
+fun rel_binding_of_spec ((_, (_, b, _)), _) = b;
+fun pred_binding_of_spec ((_, (_, _, b)), _) = b;
fun sel_default_eqs_of_spec (_, ts) = ts;
fun add_nesting_bnf_names Us =
@@ -561,10 +571,10 @@
b_names Ts thmss)
#> filter_out (null o fst o hd o snd);
-fun derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs' fp_nesting_set_maps
- live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs fp_b_name fp_bnf fpT ctor
- ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm
- ctr_Tss abs
+fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
+ fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
+ live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor
+ dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss,
injects, distincts, distinct_discsss, ...} : ctr_sugar)
lthy =
@@ -577,13 +587,15 @@
val fpBT = B_ify_T fpT;
val live_AsBs = filter (op <>) (As ~~ Bs);
+ val live_As = map fst live_AsBs;
val fTs = map (op -->) live_AsBs;
- val (((((((xss, yss), fs), Rs), ta), tb), thesis), names_lthy) = lthy
+ val ((((((((xss, yss), fs), Ps), Rs), ta), tb), thesis), names_lthy) = lthy
|> fold (fold Variable.declare_typ) [As, Bs]
|> mk_Freess "x" ctr_Tss
||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss)
||>> mk_Frees "f" fTs
+ ||>> mk_Frees "P" (map mk_pred1T live_As)
||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
||>> yield_singleton (mk_Frees "a") fpT
||>> yield_singleton (mk_Frees "b") fpBT
@@ -592,7 +604,7 @@
val ctrAs = map (mk_ctr As) ctrs;
val ctrBs = map (mk_ctr Bs) ctrs;
- fun derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms =
+ fun derive_rel_case relAsBs rel_inject_thms rel_distinct_thms =
let
val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb;
@@ -617,13 +629,13 @@
val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_rel_cases_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects
+ mk_rel_case_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects
rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
- fun derive_case_transfer rel_cases_thm =
+ fun derive_case_transfer rel_case_thm =
let
val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy;
val caseA = mk_case As C casex;
@@ -631,7 +643,7 @@
val goal = mk_parametricity_goal names_lthy (S :: Rs) caseA caseB;
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_case_transfer_tac ctxt rel_cases_thm case_thms)
+ mk_case_transfer_tac ctxt rel_case_thm case_thms)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -640,9 +652,9 @@
if plugins transfer_plugin then
let
val relAsBs = HOLogic.eq_const fpT;
- val rel_cases_thm = derive_rel_cases relAsBs [] [];
-
- val case_transfer_thm = derive_case_transfer rel_cases_thm;
+ val rel_case_thm = derive_rel_case relAsBs [] [];
+
+ val case_transfer_thm = derive_case_transfer rel_case_thm;
val notes =
[(case_transferN, [case_transfer_thm], K [])]
@@ -653,11 +665,11 @@
val subst = Morphism.thm (substitute_noted_thm noted);
in
- (([], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], []),
- lthy')
+ (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [],
+ []), lthy')
end
else
- (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
+ (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
else
let
val mapx = mk_map live As Bs (map_of_bnf fp_bnf);
@@ -886,7 +898,8 @@
(map (rapp ta) selAs) (map (rapp tb) selBs)))]);
val goals =
- if n = 0 then []
+ if n = 0 then
+ []
else
[mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb,
(case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of
@@ -904,9 +917,9 @@
map prove goals
end;
- val (rel_cases_thm, rel_cases_attrs) =
+ val (rel_case_thm, rel_case_attrs) =
let
- val thm = derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms;
+ val thm = derive_rel_case relAsBs rel_inject_thms rel_distinct_thms;
val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs);
val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names));
val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
@@ -915,16 +928,18 @@
(thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
end;
- val case_transfer_thm = derive_case_transfer rel_cases_thm;
+ val case_transfer_thm = derive_case_transfer rel_case_thm;
val sel_transfer_thms =
- if null selAss then []
+ if null selAss then
+ []
else
let
val shared_sels = foldl1 (uncurry (inter (op =))) (map (op ~~) (selAss ~~ selBss));
val goals = map (uncurry (mk_parametricity_goal names_lthy Rs)) shared_sels;
in
- if null goals then []
+ if null goals then
+ []
else
let
val goal = Logic.mk_conjunction_balanced goals;
@@ -1087,6 +1102,51 @@
end)
end;
+ val pred_injects =
+ let
+ fun top_sweep_rewr_conv rewrs =
+ Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) @{context};
+
+ val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
+ (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})));
+
+ val eq_onps = map (rel_eq_onp_with_tops_of)
+ (map rel_eq_onp_of_bnf fp_bnfs @ fp_nesting_rel_eq_onps @ live_nesting_rel_eq_onps);
+ val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) live_As);
+ val cts = map (SOME o Thm.cterm_of lthy) (map mk_eq_onp Ps);
+
+ val get_rhs = Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> snd;
+
+ val pred_eq_onp_conj =
+ List.foldr (fn (_, thm) => thm RS @{thm eq_onp_live_step}) @{thm refl[of True]};
+
+ fun predify_rel_inject rel_inject =
+ let
+ val conjuncts = try (get_rhs #> HOLogic.dest_conj) rel_inject |> the_default [];
+
+ fun postproc thm =
+ if conjuncts <> [] then
+ @{thm box_equals} OF [thm, @{thm eq_onp_same_args},
+ pred_eq_onp_conj conjuncts |> unfold_thms lthy @{thms simp_thms(21)}]
+ else
+ thm RS (@{thm eq_onp_same_args} RS iffD1);
+ in
+ rel_inject
+ |> Thm.instantiate' cTs cts
+ |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
+ (Raw_Simplifier.rewrite lthy false
+ @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
+ |> unfold_thms lthy eq_onps
+ |> postproc
+ |> unfold_thms lthy @{thms top_conj}
+ end;
+ in
+ rel_inject_thms
+ |> map (unfold_thms lthy [@{thm conj_assoc}])
+ |> map predify_rel_inject
+ |> Proof_Context.export names_lthy lthy
+ end;
+
val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
val anonymous_notes =
@@ -1101,7 +1161,8 @@
(mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
(map_disc_iffN, map_disc_iff_thms, K simp_attrs),
(map_selN, map_sel_thms, K []),
- (rel_casesN, [rel_cases_thm], K rel_cases_attrs),
+ (pred_injectN, pred_injects, K simp_attrs),
+ (rel_casesN, [rel_case_thm], K rel_case_attrs),
(rel_distinctN, rel_distinct_thms, K simp_attrs),
(rel_injectN, rel_inject_thms, K simp_attrs),
(rel_introsN, rel_intro_thms, K []),
@@ -1128,7 +1189,8 @@
map subst rel_distinct_thms,
map subst rel_sel_thms,
map subst rel_intro_thms,
- [subst rel_cases_thm],
+ [subst rel_case_thm],
+ map subst pred_injects,
map subst set_thms,
map (map (map (map subst))) set_sel_thmssss,
map (map (map (map subst))) set_intros_thmssss,
@@ -1542,7 +1604,7 @@
flat (map2 append disc_concls ctr_concls)
end;
- val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
+ val coinduct_cases = quasi_unambiguous_case_names (map (prefix Eq_prefix) fp_b_names);
val coinduct_conclss =
@{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
@@ -1961,6 +2023,7 @@
val fp_common_name = mk_common_name fp_b_names;
val map_bs = map map_binding_of_spec specs;
val rel_bs = map rel_binding_of_spec specs;
+ val pred_bs = map pred_binding_of_spec specs;
fun prepare_type_arg (_, (ty, c)) =
let val TFree (s, _) = prepare_typ no_defs_lthy ty in
@@ -2091,8 +2154,8 @@
xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
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_lthy
+ fp_bnf (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
+ (map dest_TFree unsorted_As) (map dest_TFree killed_As) fp_eqs no_defs_lthy
handle BAD_DEAD (X, X_backdrop) =>
(case X_backdrop of
Type (bad_tc, _) =>
@@ -2137,15 +2200,17 @@
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
+ val fp_nesting_rel_eq_onps = map rel_eq_onp_of_bnf fp_nesting_bnfs;
val live_nesting_map_id0s = map map_id0_of_bnf live_nesting_bnfs;
val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs;
val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
+ val live_nesting_rel_eq_onps = map rel_eq_onp_of_bnf live_nesting_bnfs;
val live = live_of_bnf any_fp_bnf;
val _ =
- if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs) then
- warning "Map function and relator names ignored"
+ if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs @ pred_bs) then
+ warning "Map function, relator, and predicator names ignored"
else
();
@@ -2190,6 +2255,19 @@
val u = Free (u', fpT);
+ val ctor_iff_dtor_thm =
+ let
+ val goal =
+ fold_rev Logic.all [w, u]
+ (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
+ mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctr_absT, fpT])
+ (Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor)
+ |> Thm.close_derivation
+ end;
+
val ctr_rhss =
map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs))
ks xss;
@@ -2213,26 +2291,11 @@
fun wrap_ctrs lthy =
let
+ val sumEN_thm' =
+ unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms);
+
fun exhaust_tac {context = ctxt, prems = _} =
- let
- val ctor_iff_dtor_thm =
- let
- val goal =
- fold_rev Logic.all [w, u]
- (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
- val vars = Variable.add_free_names lthy goal [];
- in
- Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
- mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctr_absT, fpT])
- (Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor)
- |> Thm.close_derivation
- end;
-
- val sumEN_thm' =
- unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms);
- in
- mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
- end;
+ mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm';
val inject_tacss =
map2 (fn ctr_def => fn 0 => [] | _ => [fn {context = ctxt, ...} =>
@@ -2264,21 +2327,30 @@
val anonymous_notes =
[([case_cong], fundefcong_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
+ val notes =
+ if Config.get lthy' bnf_internals then
+ [(ctor_iff_dtorN, [ctor_iff_dtor_thm], K [])]
+ |> massage_simple_notes fp_b_name
+ else
+ [];
in
- (ctr_sugar, lthy' |> Local_Theory.notes anonymous_notes |> snd)
+ (ctr_sugar, lthy' |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
end;
fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
fun massage_res (((ctr_sugar, maps_sets_rels), co_rec_res), lthy) =
- (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy);
+ (((maps_sets_rels, (ctrs, xss, ctor_iff_dtor_thm, ctr_defs, ctr_sugar)), co_rec_res),
+ lthy);
in
(wrap_ctrs
#> (fn (ctr_sugar, lthy) =>
- derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs'
- fp_nesting_set_maps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs
- fp_b_name fp_bnf fpT ctor ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def
- fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs ctr_sugar lthy
+ derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
+ fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
+ live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor
+ ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms
+ fp_rel_thm ctr_Tss abs ctr_sugar lthy
|>> pair ctr_sugar)
##>>
(if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
@@ -2286,9 +2358,9 @@
#> massage_res, lthy')
end;
- fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
+ fun wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
fold_map I wrap_one_etc lthy
- |>> apsnd split_list o apfst (apsnd @{split_list 4} o apfst @{split_list 16} o split_list)
+ |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 17} o split_list)
o split_list;
fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
@@ -2325,7 +2397,8 @@
end;
fun derive_rec_o_map_thmss lthy recs rec_defs =
- if live = 0 then replicate nn []
+ if live = 0 then
+ replicate nn []
else
let
fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy);
@@ -2392,9 +2465,9 @@
fun derive_note_induct_recs_thms_for_types
((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
- rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss,
+ rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss,
set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss),
- (ctrss, _, ctr_defss, ctr_sugars)),
+ (ctrss, _, ctor_iff_dtors, ctr_defss, ctr_sugars)),
(recs, rec_defs)), lthy) =
let
val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
@@ -2453,13 +2526,13 @@
|>> name_noted_thms
(fst (dest_Type (hd fpTs)) ^ implode (map (prefix "_") (tl fp_b_names))) inductN
|-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
- fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
- map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
+ fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars
+ recs rec_defs map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
(replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss
- rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
- case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss
- common_rel_induct_thms rel_induct_thmss [] (replicate nn []) sel_transferss
- rec_o_map_thmss
+ rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess
+ ctr_transferss case_transferss disc_transferss (replicate nn []) (replicate nn [])
+ rec_transfer_thmss common_rel_induct_thms rel_induct_thmss [] (replicate nn [])
+ sel_transferss rec_o_map_thmss
end;
fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2479,7 +2552,8 @@
end;
fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs =
- if live = 0 then replicate nn []
+ if live = 0 then
+ replicate nn []
else
let
fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0);
@@ -2539,9 +2613,9 @@
fun derive_note_coinduct_corecs_thms_for_types
((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
- rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss, set_casess,
- ctr_transferss, case_transferss, disc_transferss, sel_transferss),
- (_, _, ctr_defss, ctr_sugars)),
+ rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss,
+ set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss),
+ (_, _, ctor_iff_dtors, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
let
val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)],
@@ -2594,8 +2668,7 @@
val (set_induct_thms, set_induct_attrss) =
derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars)
(map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_inducts
- (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss)
- dtor_ctors abs_inverses
+ (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss) dtor_ctors abs_inverses
|> split_list;
val simp_thmss =
@@ -2632,14 +2705,15 @@
[flat corec_sel_thmss, flat corec_thmss]
|> Local_Theory.notes (common_notes @ notes)
|-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos
- fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs
- map_thmss [coinduct_thm, coinduct_strong_thm]
+ fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars
+ corecs corec_defs map_thmss [coinduct_thm, coinduct_strong_thm]
(transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss
- rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
- case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms)
- corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms
- (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss map_o_corec_thmss
+ rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess
+ ctr_transferss case_transferss disc_transferss corec_disc_iff_thmss
+ (map single corec_code_thms) corec_transfer_thmss common_rel_coinduct_thms
+ rel_coinduct_thmss set_induct_thms (replicate nn (if nn = 1 then set_induct_thms else []))
+ sel_transferss map_o_corec_thmss
end;
val lthy'' = lthy'
@@ -2648,14 +2722,14 @@
xtor_co_recs ctor_dtors dtor_ctors ctor_injects pre_map_defs pre_set_defss pre_rel_defs
xtor_maps xtor_setss xtor_rels ns kss mss abss abs_injects type_definitions ctr_bindingss
ctr_mixfixess ctr_Tsss disc_bindingss sel_bindingsss raw_sel_default_eqss
- |> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types
+ |> wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types
|> case_fp fp derive_note_induct_recs_thms_for_types
derive_note_coinduct_corecs_thms_for_types;
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
co_prefix fp ^ "datatype"));
in
- timer; lthy''
+ lthy''
end;
fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) (K I) x;
@@ -2673,7 +2747,7 @@
val parse_spec =
parse_type_args_named_constrained -- Parse.binding -- Parse.opt_mixfix --
- (@{keyword "="} |-- parse_ctr_specs) -- parse_map_rel_bindings -- parse_sel_default_eqs;
+ (@{keyword "="} |-- parse_ctr_specs) -- parse_map_rel_pred_bindings -- parse_sel_default_eqs;
val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Feb 17 21:08:18 2016 +0100
@@ -40,8 +40,8 @@
tactic
val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic
- val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
- thm list -> thm list -> thm list -> tactic
+ val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
+ thm list -> thm list -> 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 -> thm list -> tactic
@@ -79,7 +79,7 @@
@{thms UN_empty UN_insert UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib
o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set;
-val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc};
+val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc};
fun is_def_looping def =
(case Thm.prop_of def of
@@ -103,10 +103,10 @@
val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs;
-fun mk_case_transfer_tac ctxt rel_cases cases =
- let val n = length (tl (Thm.prems_of rel_cases)) in
+fun mk_case_transfer_tac ctxt rel_case cases =
+ let val n = length (tl (Thm.prems_of rel_case)) in
REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
- HEADGOAL (etac ctxt rel_cases) THEN
+ HEADGOAL (etac ctxt rel_case) THEN
ALLGOALS (hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt cases THEN
ALLGOALS (fn k => (select_prem_tac ctxt n (dtac ctxt asm_rl) k) k) THEN
@@ -408,7 +408,7 @@
unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN
ALLGOALS (rtac ctxt refl);
-fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs =
+fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs =
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW
rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW
hyp_subst_tac ctxt) THEN
@@ -436,7 +436,7 @@
unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @
- @{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False
+ @{thms id_bnf_def rel_sum_simps rel_prod_inject vimage2p_def Inl_Inr_False
iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN'
(REPEAT_DETERM o rtac ctxt conjI) THEN' (rtac ctxt refl ORELSE' assume_tac ctxt))))
@@ -454,7 +454,7 @@
unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
@{thms id_bnf_def vimage2p_def}) THEN
TRYALL (hyp_subst_tac ctxt) THEN
- unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
+ unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_inject Inl_Inr_False
Inr_Inl_False sum.inject prod.inject}) THEN
TRYALL (rtac ctxt refl ORELSE' etac ctxt FalseE ORELSE'
(REPEAT_DETERM o etac ctxt conjE) THEN' assume_tac ctxt))
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 17 21:08:18 2016 +0100
@@ -10,6 +10,7 @@
val unfold_lets_splits: term -> term
val unfold_splits_lets: term -> term
val dest_map: Proof.context -> string -> term -> term * term list
+ val dest_pred: Proof.context -> string -> term -> term * term list
val mutualize_fp_sugars: (string -> bool) -> BNF_Util.fp_kind -> int list -> binding list ->
typ list -> term list -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
@@ -78,27 +79,29 @@
| unfold_splits_lets (Abs (s, T, t)) = Abs (s, T, unfold_splits_lets t)
| unfold_splits_lets t = unfold_lets_splits t;
-fun mk_map_pattern ctxt s =
+fun dest_either_map_or_pred map_or_pred_of_bnf ctxt T_name call =
let
- val bnf = the (bnf_of ctxt s);
- val mapx = map_of_bnf bnf;
+ val bnf = the (bnf_of ctxt T_name);
+ val const0 = map_or_pred_of_bnf bnf;
val live = live_of_bnf bnf;
- val (f_Ts, _) = strip_typeN live (fastype_of mapx);
- val fs = map_index (fn (i, T) => Var (("?f", i), T)) f_Ts;
+ val (f_Ts, _) = strip_typeN live (fastype_of const0);
+ val fs = map_index (fn (i, T) => Var (("f", i), T)) f_Ts;
+ val pat = betapplys (const0, fs);
+ val (_, tenv) = fo_match ctxt call pat;
in
- (mapx, betapplys (mapx, fs))
+ (const0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
end;
-fun dest_map ctxt s call =
- let
- val (map0, pat) = mk_map_pattern ctxt s;
- val (_, tenv) = fo_match ctxt call pat;
- in
- (map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
- end;
+val dest_map = dest_either_map_or_pred map_of_bnf;
+val dest_pred = dest_either_map_or_pred pred_of_bnf;
-fun dest_abs_or_applied_map _ _ (Abs (_, _, t)) = (Term.dummy, [t])
- | dest_abs_or_applied_map ctxt s (t1 $ _) = dest_map ctxt s t1;
+fun dest_map_or_pred ctxt T_name call =
+ (case try (dest_map ctxt T_name) call of
+ SOME res => res
+ | NONE => dest_pred ctxt T_name call);
+
+fun dest_abs_or_applied_map_or_pred _ _ (Abs (_, _, t)) = (Term.dummy, [t])
+ | dest_abs_or_applied_map_or_pred ctxt s (t1 $ _) = dest_map_or_pred ctxt s t1;
fun map_partition f xs =
fold_rev (fn x => fn (ys, (good, bad)) =>
@@ -144,6 +147,7 @@
morph_ctr_sugar phi ctr_sugar
end;
+ val ctor_iff_dtors = map (#ctor_iff_dtor o #fp_ctr_sugar) fp_sugars0;
val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0;
val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0;
val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
@@ -198,7 +202,7 @@
and freeze_fpTs_call kk fpT calls (T as Type (s, _)) =
(case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
([], _) =>
- (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
+ (case map_partition (try (snd o dest_abs_or_applied_map_or_pred no_defs_lthy s)) calls of
([], _) => freeze_fpTs_mutual_call kk fpT calls T
| callsp => freeze_fpTs_map kk fpT callsp T)
| callsp => freeze_fpTs_map kk fpT callsp T)
@@ -291,11 +295,12 @@
val names_lthy = lthy |> fold Variable.declare_typ (As @ Cs @ Xs);
val phi = Proof_Context.export_morphism names_lthy lthy;
- fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
- co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
+ fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctor_iff_dtor ctr_defs ctr_sugar
+ co_rec co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...},
fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels,
- rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...},
+ rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss,
+ set_cases, ...},
fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
set_inducts, ...},
@@ -305,6 +310,7 @@
fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
fp_ctr_sugar =
{ctrXs_Tss = ctrXs_Tss,
+ ctor_iff_dtor = ctor_iff_dtor,
ctr_defs = ctr_defs,
ctr_sugar = ctr_sugar,
ctr_transfers = ctr_transfers,
@@ -320,6 +326,7 @@
rel_sels = rel_sels,
rel_intros = rel_intros,
rel_cases = rel_cases,
+ pred_injects = pred_injects,
set_thms = set_thms,
set_selssss = set_selssss,
set_introssss = set_introssss,
@@ -343,8 +350,8 @@
|> morph_fp_sugar phi;
val target_fp_sugars =
- @{map 16} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss
- ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss
+ @{map 17} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctor_iff_dtors
+ ctr_defss ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss
co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0;
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Feb 17 21:08:18 2016 +0100
@@ -661,7 +661,7 @@
val timer = time (timer "FP construction in total");
in
- timer; ((pre_bnfs, absT_infos), res)
+ ((pre_bnfs, absT_infos), res)
end;
fun fp_antiquote_setup binding =
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 17 21:08:18 2016 +0100
@@ -9,9 +9,10 @@
signature BNF_GFP =
sig
- val construct_gfp: mixfix list -> binding list -> binding list -> binding list list ->
- binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
- BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory
+ val construct_gfp: mixfix list -> binding list -> binding list -> binding list ->
+ binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
+ BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
+ BNF_FP_Util.fp_result * local_theory
end;
structure BNF_GFP : BNF_GFP =
@@ -55,7 +56,7 @@
((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
(*all BNFs have the same lives*)
-fun construct_gfp mixfixes map_bs rel_bs set_bss0 bs resBs (resDs, Dss) bnfs _ lthy =
+fun construct_gfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs _ lthy =
let
val time = time lthy;
val timer = time (Timer.startRealTimer ());
@@ -1860,26 +1861,30 @@
val setss = map (fn i => map2 (mk_set Ts i) ls passiveAs) ks;
val (Jbnf_consts, lthy) =
- @{fold_map 7} (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T =>
- fn lthy =>
+ @{fold_map 8} (fn b => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn mapx =>
+ fn sets => fn T => fn lthy =>
define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
- map_b rel_b set_bs
- ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd),
- [Const (@{const_name undefined}, T)]), NONE) lthy)
- bs map_bs rel_bs set_bss fs_maps setss Ts lthy;
+ map_b rel_b pred_b set_bs
+ (((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd),
+ [Const (@{const_name undefined}, T)]), NONE), NONE) lthy)
+ bs map_bs rel_bs pred_bs set_bss fs_maps setss Ts lthy;
val (_, Jconsts, Jconst_defs, mk_Jconsts) = @{split_list 4} Jbnf_consts;
- val (_, Jsetss, Jbds_Ds, _, _) = @{split_list 5} Jconsts;
- val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = @{split_list 5} Jconst_defs;
- val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = @{split_list 5} mk_Jconsts;
+ val (_, Jsetss, Jbds_Ds, _, _, _) = @{split_list 6} Jconsts;
+ val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs, Jpred_defs) =
+ @{split_list 6} Jconst_defs;
+ val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, mk_Jpreds_Ds, _, _) =
+ @{split_list 7} mk_Jconsts;
val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs;
+ val Jpred_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jpred_defs;
val Jset_defs = flat Jset_defss;
fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds;
fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss;
val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds;
fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds;
+ fun mk_Jpreds As = map (fn mk => mk deads As) mk_Jpreds_Ds;
val Jmaps = mk_Jmaps passiveAs passiveBs;
val (Jsetss_by_range, Jsetss_by_bnf) = `transpose (mk_Jsetss passiveAs);
@@ -2240,6 +2245,7 @@
Jrel_unabs_defs;
val Jrels = mk_Jrels passiveAs passiveBs;
+ val Jpreds = mk_Jpreds passiveAs;
val Jrelphis = map (fn rel => Term.list_comb (rel, Jphis)) Jrels;
val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels;
val Jrelpsi1s = map (fn rel => Term.list_comb (rel, Jpsi1s)) (mk_Jrels passiveAs passiveCs);
@@ -2574,20 +2580,22 @@
val rel_OO_Grp_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Jrel_unabs_defs;
- val tacss = @{map 9} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
+ val pred_set_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Jpred_unabs_defs;
+
+ val tacss = @{map 10} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
+ bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs pred_set_tacs;
fun wit_tac thms ctxt =
mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
val (Jbnfs, lthy) =
- @{fold_map 6} (fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
+ @{fold_map 7} (fn tacs => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn wit_thms =>
fn consts =>
bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
- (SOME deads) map_b rel_b set_bs consts)
- tacss map_bs rel_bs set_bss wit_thmss
- ((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~
- all_witss) ~~ map SOME Jrels)
+ (SOME deads) map_b rel_b pred_b set_bs consts)
+ tacss map_bs rel_bs pred_bs set_bss wit_thmss
+ (((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~
+ all_witss) ~~ map SOME Jrels) ~~ map SOME Jpreds)
lthy;
val timer = time (timer "registered new codatatypes as BNFs");
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Feb 17 21:08:18 2016 +0100
@@ -60,7 +60,7 @@
val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
term -> 'a -> 'a
val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
- (typ list -> term -> unit) -> typ list -> term -> term
+ (typ list -> term -> unit) -> (typ list -> term -> term) -> typ list -> term -> term
val massage_nested_corec_call: Proof.context -> (term -> bool) ->
(typ list -> typ -> typ -> term -> term) -> (typ list -> typ -> typ -> term -> term) ->
typ list -> typ -> typ -> term -> term
@@ -129,6 +129,11 @@
error_at ctxt eqns "Nonprimitive corecursive specification";
fun unexpected_corec_call ctxt eqns t =
error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
+fun unsupported_case_around_corec_call ctxt eqns t =
+ error_at ctxt eqns ("Unsupported corecursive call under case expression " ^
+ quote (Syntax.string_of_term ctxt t) ^ "\n(Define " ^
+ quote (Syntax.string_of_typ ctxt (domain_type (fastype_of t))) ^
+ " with discriminators and selectors to circumvent this limitation.)");
fun use_primcorecursive () =
error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^
quote (#1 @{command_keyword primcorec}) ^ ")");
@@ -272,10 +277,10 @@
fun case_of ctxt s =
(case ctr_sugar_of ctxt s of
- SOME {casex = Const (s', _), split_sels = _ :: _, ...} => SOME s'
+ SOME {casex = Const (s', _), split_sels, ...} => SOME (s', not (null split_sels))
| _ => NONE);
-fun massage_let_if_case ctxt has_call massage_leaf unexpected_call bound_Ts t0 =
+fun massage_let_if_case ctxt has_call massage_leaf unexpected_call unsupported_case bound_Ts t0 =
let
val thy = Proof_Context.theory_of ctxt;
@@ -311,19 +316,26 @@
if n < length args then
(case gen_body_fun_T of
Type (_, [Type (T_name, _), _]) =>
- if case_of ctxt T_name = SOME c then
- let
- val (branches, obj_leftovers) = chop n args;
- val branches' = map2 (massage_abs bound_Ts) gen_branch_ms branches;
- val branch_Ts' = map typof branches';
- val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts'));
- val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
- in
- Term.list_comb (casex',
- branches' @ tap (List.app (check_no_call bound_Ts)) obj_leftovers)
- end
- else
- massage_leaf bound_Ts t
+ (case case_of ctxt T_name of
+ SOME (c', has_split_sels) =>
+ if c' = c then
+ if has_split_sels then
+ let
+ val (branches, obj_leftovers) = chop n args;
+ val branches' = map2 (massage_abs bound_Ts) gen_branch_ms branches;
+ val branch_Ts' = map typof branches';
+ val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts'));
+ val casex' =
+ Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
+ in
+ Term.list_comb (casex',
+ branches' @ tap (List.app (check_no_call bound_Ts)) obj_leftovers)
+ end
+ else
+ unsupported_case bound_Ts t
+ else
+ massage_leaf bound_Ts t
+ | NONE => massage_leaf bound_Ts t)
| _ => massage_leaf bound_Ts t)
else
massage_leaf bound_Ts t
@@ -338,7 +350,8 @@
end;
fun massage_let_if_case_corec ctxt has_call massage_leaf bound_Ts t0 =
- massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call ctxt [t0])) bound_Ts t0;
+ massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call ctxt [t0]))
+ (K (unsupported_case_around_corec_call ctxt [t0])) bound_Ts t0;
fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 =
let
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Feb 17 21:08:18 2016 +0100
@@ -104,11 +104,11 @@
(take k (nth excludesss (k - 1))))
end;
-fun prelude_tac ctxt defs thm =
- unfold_thms_tac ctxt defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets;
+fun prelude_tac ctxt fun_defs thm =
+ unfold_thms_tac ctxt fun_defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets;
-fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss =
- prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss;
+fun mk_primcorec_disc_tac ctxt fun_defs corec_disc k m excludesss =
+ prelude_tac ctxt fun_defs corec_disc THEN cases_tac ctxt k m excludesss;
fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
distinct_discs =
@@ -129,9 +129,9 @@
resolve_tac ctxt
(map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt));
-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
+fun mk_primcorec_sel_tac ctxt fun_defs distincts splits split_asms mapsx map_ident0s map_comps
+ fun_sel k m excludesss =
+ prelude_tac ctxt fun_defs (fun_sel RS trans) THEN
cases_tac ctxt k m excludesss THEN
HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE'
eresolve_tac ctxt falseEs ORELSE'
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Feb 17 21:08:18 2016 +0100
@@ -8,9 +8,10 @@
signature BNF_LFP =
sig
- val construct_lfp: mixfix list -> binding list -> binding list -> binding list list ->
- binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
- BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory
+ val construct_lfp: mixfix list -> binding list -> binding list -> binding list ->
+ binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
+ BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
+ BNF_FP_Util.fp_result * local_theory
end;
structure BNF_LFP : BNF_LFP =
@@ -26,7 +27,7 @@
open BNF_LFP_Tactics
(*all BNFs have the same lives*)
-fun construct_lfp mixfixes map_bs rel_bs set_bss0 bs resBs (resDs, Dss) bnfs _ lthy =
+fun construct_lfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs _ lthy =
let
val time = time lthy;
val timer = time (Timer.startRealTimer ());
@@ -1526,12 +1527,12 @@
end;
val (Ibnf_consts, lthy) =
- @{fold_map 8} (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
- fn wits => fn T => fn lthy =>
+ @{fold_map 9} (fn b => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn mapx =>
+ fn sets => fn wits => fn T => fn lthy =>
define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
- map_b rel_b set_bs
- ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd0), wits), NONE) lthy)
- bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
+ map_b rel_b pred_b set_bs
+ (((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd0), wits), NONE), NONE) lthy)
+ bs map_bs rel_bs pred_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
val ((((((((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), xFs), yFs))), Iphis), Ipsi1s),
Ipsi2s), fs), fs_copy), us), (ys, ys')), _) =
@@ -1550,11 +1551,14 @@
||>> mk_Frees' "y" passiveAs;
val (_, Iconsts, Iconst_defs, mk_Iconsts) = @{split_list 4} Ibnf_consts;
- val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = @{split_list 5} Iconsts;
- val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = @{split_list 5} Iconst_defs;
- val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, _) = @{split_list 5} mk_Iconsts;
+ val (_, Isetss, Ibds_Ds, Iwitss_Ds, _, _) = @{split_list 6} Iconsts;
+ val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs, Ipred_defs) =
+ @{split_list 6} Iconst_defs;
+ val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, mk_Ipreds_Ds, _, _) =
+ @{split_list 7} mk_Iconsts;
val Irel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Irel_defs;
+ val Ipred_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Ipred_defs;
val Iset_defs = flat Iset_defss;
fun mk_Imaps As Bs = map (fn mk => mk deads As Bs) mk_Imaps_Ds;
@@ -1563,6 +1567,7 @@
val Iwitss =
map2 (fn mk => fn Iwits => map (mk deads passiveAs o snd) Iwits) mk_It_Ds Iwitss_Ds;
fun mk_Irels As Bs = map (fn mk => mk deads As Bs) mk_Irels_Ds;
+ fun mk_Ipreds As = map (fn mk => mk deads As) mk_Ipreds_Ds;
val Imaps = mk_Imaps passiveAs passiveBs;
val fs_Imaps = map (fn m => Term.list_comb (m, fs)) Imaps;
@@ -1762,6 +1767,7 @@
val ctor_Iset_thmss' = transpose ctor_Iset_thmss;
val Irels = mk_Irels passiveAs passiveBs;
+ val Ipreds = mk_Ipreds passiveAs;
val Irelphis = map (fn rel => Term.list_comb (rel, Iphis)) Irels;
val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels;
val Irelpsi1s = map (fn rel => Term.list_comb (rel, Ipsi1s)) (mk_Irels passiveAs passiveCs);
@@ -1832,19 +1838,21 @@
val rel_OO_Grp_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Irel_unabs_defs;
- val tacss = @{map 9} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
+ val pred_set_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Ipred_unabs_defs;
+
+ val tacss = @{map 10} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
+ bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs pred_set_tacs;
fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN
mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
val (Ibnfs, lthy) =
- @{fold_map 5} (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts =>
+ @{fold_map 6} (fn tacs => fn map_b => fn rel_b => fn pred_b => fn set_bs => fn consts =>
bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
- map_b rel_b set_bs consts)
- tacss map_bs rel_bs set_bss
- ((((((replicate n Binding.empty ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~
- Iwitss) ~~ map SOME Irels) lthy;
+ map_b rel_b pred_b set_bs consts)
+ tacss map_bs rel_bs pred_bs set_bss
+ (((((((replicate n Binding.empty ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~
+ Iwitss) ~~ map SOME Irels) ~~ map SOME Ipreds) lthy;
val timer = time (timer "registered new datatypes as BNFs");
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Wed Feb 17 21:08:18 2016 +0100
@@ -74,6 +74,7 @@
live_nesting_bnfs = [],
fp_ctr_sugar =
{ctrXs_Tss = ctr_Tss,
+ ctor_iff_dtor = @{thm xtor_iff_xtor},
ctr_defs = @{thms Inl_def_alt Inr_def_alt},
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
ctr_transfers = @{thms Inl_transfer Inr_transfer},
@@ -89,6 +90,7 @@
rel_sels = @{thms rel_sum_sel},
rel_intros = @{thms rel_sum.intros},
rel_cases = @{thms rel_sum.cases},
+ pred_injects = @{thms pred_sum_inject},
set_thms = @{thms sum_set_simps},
set_selssss = [[[@{thms set_sum_sel(1)}], [[]]], [[[]], [@{thms set_sum_sel(2)}]]],
set_introssss = [[[@{thms setl.intros[OF refl]}], [[]]],
@@ -142,6 +144,7 @@
live_nesting_bnfs = [],
fp_ctr_sugar =
{ctrXs_Tss = [ctr_Ts],
+ ctor_iff_dtor = @{thm xtor_iff_xtor},
ctr_defs = @{thms Pair_def_alt},
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
ctr_transfers = @{thms Pair_transfer},
@@ -152,11 +155,12 @@
{map_thms = @{thms map_prod_simp},
map_disc_iffs = [],
map_selss = [@{thms fst_map_prod snd_map_prod}],
- rel_injects = @{thms rel_prod_apply},
+ rel_injects = @{thms rel_prod_inject},
rel_distincts = [],
rel_sels = @{thms rel_prod_sel},
rel_intros = @{thms rel_prod.intros},
rel_cases = @{thms rel_prod.cases},
+ pred_injects = @{thms pred_prod_inject},
set_thms = @{thms prod_set_simps},
set_selssss = [[[@{thms fsts.intros}, []]], [[[], @{thms snds.intros}]]],
set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]],
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Feb 17 21:08:18 2016 +0100
@@ -521,7 +521,7 @@
fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) =
(((((map new_type_args_of old_tyargs, b), mx), map new_ctr_spec_of old_ctr_specs),
- (Binding.empty, Binding.empty)), []);
+ (Binding.empty, Binding.empty, Binding.empty)), []);
val new_specs = map new_spec_of old_specs;
in
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Feb 17 21:08:18 2016 +0100
@@ -28,6 +28,7 @@
{recx: term,
fp_nesting_map_ident0s: thm list,
fp_nesting_map_comps: thm list,
+ fp_nesting_pred_maps: thm list,
ctr_specs: rec_ctr_spec list}
type basic_lfp_sugar =
@@ -44,16 +45,16 @@
is_new_datatype: Proof.context -> string -> bool,
basic_lfp_sugars_of: binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
- typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * Token.src list
- * bool * local_theory,
+ typ list * int list * basic_lfp_sugar list * thm list * thm list * thm list * thm
+ * Token.src list * bool * local_theory,
rewrite_nested_rec_call: (Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
term -> term -> term -> term) option};
val register_lfp_rec_extension: lfp_rec_extension -> theory -> theory
val default_basic_lfp_sugars_of: binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
- typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * Token.src list * bool
- * local_theory
+ typ list * int list * basic_lfp_sugar list * thm list * thm list * thm list * thm
+ * Token.src list * bool * local_theory
val rec_specs_of: binding list -> typ list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
(bool * rec_spec list * typ list * thm * thm list * Token.src list * typ list) * local_theory
@@ -117,6 +118,7 @@
{recx: term,
fp_nesting_map_ident0s: thm list,
fp_nesting_map_comps: thm list,
+ fp_nesting_pred_maps: thm list,
ctr_specs: rec_ctr_spec list};
type basic_lfp_sugar =
@@ -133,8 +135,8 @@
is_new_datatype: Proof.context -> string -> bool,
basic_lfp_sugars_of: binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
- typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * Token.src list * bool
- * local_theory,
+ typ list * int list * basic_lfp_sugar list * thm list * thm list * thm list * thm
+ * Token.src list * bool * local_theory,
rewrite_nested_rec_call: (Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
term -> term -> term -> term) option};
@@ -172,7 +174,7 @@
{T = T, fp_res_index = 0, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
recx = casex, rec_thms = case_thms};
in
- ([], [0], [basic_lfp_sugar], [], [], TrueI, [], false, ctxt)
+ ([], [0], [basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt)
end
| default_basic_lfp_sugars_of _ _ _ _ _ = error "Unsupported mutual recursion at this stage";
@@ -199,7 +201,7 @@
val thy = Proof_Context.theory_of lthy0;
val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_ident0s, fp_nesting_map_comps,
- common_induct, induct_attrs, n2m, lthy) =
+ fp_nesting_pred_maps, common_induct, induct_attrs, n2m, lthy) =
basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0;
val perm_basic_lfp_sugars = sort (int_ord o apply2 #fp_res_index) basic_lfp_sugars;
@@ -259,6 +261,7 @@
({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
{recx = mk_co_rec thy Least_FP perm_Cs' (substAT T) recx,
fp_nesting_map_ident0s = fp_nesting_map_ident0s, fp_nesting_map_comps = fp_nesting_map_comps,
+ fp_nesting_pred_maps = fp_nesting_pred_maps,
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,
@@ -492,10 +495,12 @@
|> (fn [] => NONE | callss => SOME (ctr, callss))
end;
-fun mk_primrec_tac ctxt num_extra_args map_ident0s map_comps fun_defs recx =
+fun mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
+ fp_nesting_pred_maps fun_defs recx =
unfold_thms_tac ctxt fun_defs THEN
HEADGOAL (rtac ctxt (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
- unfold_thms_tac ctxt (nested_simps ctxt @ map_ident0s @ map_comps) THEN
+ unfold_thms_tac ctxt (nested_simps ctxt @ fp_nesting_map_ident0s @ fp_nesting_map_comps @
+ fp_nesting_pred_maps) THEN
HEADGOAL (rtac ctxt refl);
fun prepare_primrec plugins nonexhaustives transfers fixes specs lthy0 =
@@ -541,8 +546,8 @@
val defs = build_defs lthy nonexhaustives bs mxs funs_data rec_specs has_call;
- fun prove def_thms ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...} : rec_spec)
- (fun_data : eqn_data list) lthy' =
+ fun prove def_thms ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps,
+ fp_nesting_pred_maps, ...} : rec_spec) (fun_data : eqn_data list) lthy' =
let
val js =
find_indices (op = o apply2 (fn {fun_name, ctr, ...} => (fun_name, ctr)))
@@ -556,7 +561,7 @@
Goal.prove_sorry lthy' [] [] user_eqn
(fn {context = ctxt, prems = _} =>
mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
- def_thms rec_thm)
+ fp_nesting_pred_maps def_thms rec_thm)
|> Thm.close_derivation);
in
((js, simps), lthy')
@@ -607,8 +612,9 @@
lthy'
|> fold_map Local_Theory.define defs
|-> (fn defs => fn lthy =>
- let val ((jss, simpss), lthy) = prove lthy defs;
- in ((names, (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy) end)
+ let val ((jss, simpss), lthy) = prove lthy defs in
+ ((names, (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy)
+ end)
end;
fun primrec_simple fixes ts lthy =
@@ -649,7 +655,7 @@
|-> (fn (names, (ts, defs, (jss, simpss))) =>
Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
#> Local_Theory.notes (mk_notes jss names simpss)
- #>> (fn notes => (ts, defs, map snd notes)))
+ #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
end
handle OLD_PRIMREC () =>
old_primrec raw_fixes raw_specs lthy
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Feb 17 21:08:18 2016 +0100
@@ -36,7 +36,7 @@
recx = recx, rec_thms = rec_thms};
fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy =
- ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, lthy)
+ ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, lthy)
| basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 =
let
val ((missing_arg_Ts, perm0_kks,
@@ -63,10 +63,11 @@
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;
+ val fp_nesting_pred_maps = map pred_map_of_bnf fp_nesting_bnfs;
in
(missing_arg_Ts, perm0_kks, @{map 3} basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
- fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs,
- is_some lfp_sugar_thms, lthy)
+ fp_nesting_map_ident0s, fp_nesting_map_comps, fp_nesting_pred_maps, common_induct,
+ induct_attrs, is_some lfp_sugar_thms, lthy)
end;
exception NO_MAP of term;
@@ -108,7 +109,16 @@
in
Term.list_comb (map', fs')
end
- | NONE => raise NO_MAP t)
+ | NONE =>
+ (case try (dest_pred ctxt s) t of
+ SOME (pred0, fs) =>
+ let
+ val pred' = mk_pred Us pred0;
+ val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs;
+ in
+ Term.list_comb (pred', fs')
+ end
+ | NONE => raise NO_MAP t))
| massage_map _ _ t = raise NO_MAP t
and massage_map_or_map_arg U T t =
if T = U then
--- a/src/HOL/Tools/BNF/bnf_lift.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Wed Feb 17 21:08:18 2016 +0100
@@ -13,21 +13,21 @@
| No_Warn_Wits
val copy_bnf:
(((lift_bnf_option list * (binding option * (string * sort option)) list) *
- string) * thm option) * (binding * binding) ->
+ string) * thm option) * (binding * binding * binding) ->
local_theory -> local_theory
val copy_bnf_cmd:
(((lift_bnf_option list * (binding option * (string * string option)) list) *
- string) * (Facts.ref * Token.src list) option) * (binding * binding) ->
+ string) * (Facts.ref * Token.src list) option) * (binding * binding * binding) ->
local_theory -> local_theory
val lift_bnf:
(((lift_bnf_option list * (binding option * (string * sort option)) list) *
- string) * thm option) * (binding * binding) ->
+ string) * thm option) * (binding * binding * binding) ->
({context: Proof.context, prems: thm list} -> tactic) list ->
local_theory -> local_theory
val lift_bnf_cmd:
((((lift_bnf_option list * (binding option * (string * string option)) list) *
- string) * string list) * (Facts.ref * Token.src list) option) * (binding * binding) ->
- local_theory -> Proof.state
+ string) * string list) * (Facts.ref * Token.src list) option) *
+ (binding * binding * binding) -> local_theory -> Proof.state
end
structure BNF_Lift : BNF_LIFT =
@@ -45,7 +45,7 @@
Plugins_Option of Proof.context -> Plugin_Name.filter
| No_Warn_Wits;
-fun typedef_bnf thm wits specs map_b rel_b opts lthy =
+fun typedef_bnf thm wits specs map_b rel_b pred_b opts lthy =
let
val plugins =
get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
@@ -212,6 +212,14 @@
val rel_G = fold_rev absfree (map dest_Free var_Rs)
(mk_vimage2p Rep_G Rep_Gb $ list_comb (rel_F, var_Rs));
+ (* val pred_G = @{term "\<lambda>P. pred_F P o Rep_G"}; *)
+ val pred_F = mk_pred_of_bnf deads alphas bnf;
+ val (typ_Ps, _) = strip_typeN lives (fastype_of pred_F);
+
+ val (var_Ps, names_lthy) = mk_Frees "P" typ_Ps names_lthy;
+ val pred_G = fold_rev absfree (map dest_Free var_Ps)
+ (HOLogic.mk_comp (list_comb (pred_F, var_Ps), Rep_G));
+
(* val wits_G = [@{term "Abs_G o wit_F"}]; *)
val (var_as, _) = mk_Frees "a" alphas names_lthy;
val wits_G =
@@ -297,6 +305,12 @@
[rtac ctxt (iffD1 OF [Abs_inject_thm OF [map_closed_thm OF [Rep_thm], Rep_thm]]),
etac ctxt (Rep_inverse_thm RS sym RSN (2, trans))]]));
+ fun pred_set_tac ctxt =
+ HEADGOAL (EVERY'
+ [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\<lambda>f. f o _"]} RS trans),
+ SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})),
+ rtac ctxt refl]);
+
fun wit_tac ctxt =
HEADGOAL (EVERY'
(map (fn thm => (EVERY'
@@ -306,11 +320,12 @@
wit_thms));
val tactics = [map_id0_tac, map_comp0_tac, map_cong0_tac] @ set_map0s_tac @
- [card_order_bd_tac, cinfinite_bd_tac] @ set_bds_tac @ [le_rel_OO_tac, rel_OO_Grp_tac];
+ [card_order_bd_tac, cinfinite_bd_tac] @ set_bds_tac @
+ [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac];
val (bnf, lthy) = bnf_def Dont_Inline (user_policy Note_Some) false I
- tactics wit_tac NONE map_b rel_b set_bs
- ((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G)
+ tactics wit_tac NONE map_b rel_b pred_b set_bs
+ (((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G)
lthy;
val bnf = morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) bnf;
@@ -328,7 +343,7 @@
local
fun prepare_common prepare_name prepare_sort prepare_term prepare_thm
- (((((plugins, raw_specs), raw_Tname), raw_wits), xthm_opt), (map_b, rel_b)) lthy =
+ (((((plugins, raw_specs), raw_Tname), raw_wits), xthm_opt), (map_b, rel_b, pred_b)) lthy =
let
val Tname = prepare_name lthy raw_Tname;
val input_thm =
@@ -344,7 +359,7 @@
Const (@{const_name type_definition}, _) $ _ $ _ $ _ => ()
| _ => error "Unsupported type of a theorem: only type_definition is supported");
in
- typedef_bnf input_thm wits specs map_b rel_b plugins lthy
+ typedef_bnf input_thm wits specs map_b rel_b pred_b plugins lthy
end;
fun prepare_lift_bnf prepare_name prepare_sort prepare_term prepare_thm =
@@ -413,13 +428,13 @@
Outer_Syntax.local_theory_to_proof @{command_keyword lift_bnf}
"register a subtype of a bounded natural functor (BNF) as a BNF"
((parse_options -- parse_type_args_named_constrained -- Parse.type_const -- parse_wits --
- parse_typedef_thm -- parse_map_rel_bindings) >> lift_bnf_cmd);
+ parse_typedef_thm -- parse_map_rel_pred_bindings) >> lift_bnf_cmd);
val _ =
Outer_Syntax.local_theory @{command_keyword copy_bnf}
"register a type copy of a bounded natural functor (BNF) as a BNF"
((parse_plugins -- parse_type_args_named_constrained -- Parse.type_const --
- parse_typedef_thm -- parse_map_rel_bindings) >> copy_bnf_cmd);
+ parse_typedef_thm -- parse_map_rel_pred_bindings) >> copy_bnf_cmd);
end;
--- a/src/HOL/Tools/BNF/bnf_util.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Feb 17 21:08:18 2016 +0100
@@ -52,6 +52,7 @@
val mk_cprod: term -> term -> term
val mk_csum: term -> term -> term
val mk_dir_image: term -> term -> term
+ val mk_eq_onp: term -> term
val mk_rel_fun: term -> term -> term
val mk_image: term -> term
val mk_in: term list -> term list -> typ -> term
@@ -103,7 +104,7 @@
val fold_thms: Proof.context -> thm list -> thm -> thm
val parse_type_args_named_constrained: (binding option * (string * string option)) list parser
- val parse_map_rel_bindings: (binding * binding) parser
+ val parse_map_rel_pred_bindings: (binding * binding * binding) parser
val typedef: binding * (string * sort) list * mixfix -> term ->
(binding * binding) option -> (Proof.context -> tactic) ->
@@ -130,17 +131,18 @@
@{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
Scan.succeed [];
-val parse_map_rel_binding = Parse.name --| @{keyword ":"} -- Parse.binding;
+val parse_map_rel_pred_binding = Parse.name --| @{keyword ":"} -- Parse.binding;
-val no_map_rel = (Binding.empty, Binding.empty);
+val no_map_rel = (Binding.empty, Binding.empty, Binding.empty);
-fun extract_map_rel ("map", b) = apfst (K b)
- | extract_map_rel ("rel", b) = apsnd (K b)
- | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
+fun extract_map_rel_pred ("map", m) = (fn (_, r, p) => (m, r, p))
+ | extract_map_rel_pred ("rel", r) = (fn (m, _, p) => (m, r, p))
+ | extract_map_rel_pred ("pred", p) = (fn (m, r, _) => (m, r, p))
+ | extract_map_rel_pred (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
-val parse_map_rel_bindings =
- @{keyword "for"} |-- Scan.repeat parse_map_rel_binding
- >> (fn ps => fold extract_map_rel ps no_map_rel)
+val parse_map_rel_pred_bindings =
+ @{keyword "for"} |-- Scan.repeat parse_map_rel_pred_binding
+ >> (fn ps => fold extract_map_rel_pred ps no_map_rel)
|| Scan.succeed no_map_rel;
fun typedef (b, Ts, mx) set opt_morphs tac lthy =
@@ -352,6 +354,13 @@
(T1 --> T2) --> (U1 --> U2) --> mk_pred2T T2 U2 --> mk_pred2T T1 U1) $ f $ g
end;
+fun mk_eq_onp P =
+ let
+ val T = domain_type (fastype_of P);
+ in
+ Const (@{const_name eq_onp}, (T --> HOLogic.boolT) --> T --> T --> HOLogic.boolT) $ P
+ end;
+
fun mk_pred name R =
Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R;
val mk_reflp = mk_pred @{const_name reflp};
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Feb 17 21:08:18 2016 +0100
@@ -205,9 +205,8 @@
structure Ctr_Sugar_Plugin = Plugin(type T = ctr_sugar);
fun ctr_sugar_interpretation name f =
- Ctr_Sugar_Plugin.interpretation name
- (fn ctr_sugar => fn lthy =>
- f (transfer_ctr_sugar (Proof_Context.theory_of lthy) ctr_sugar) lthy);
+ Ctr_Sugar_Plugin.interpretation name (fn ctr_sugar => fn lthy =>
+ f (transfer_ctr_sugar (Proof_Context.theory_of lthy) ctr_sugar) lthy);
val interpret_ctr_sugar = Ctr_Sugar_Plugin.data;
@@ -228,12 +227,12 @@
|> Named_Target.theory_map (Ctr_Sugar_Plugin.data plugins ctr_sugar)
end;
-val isN = "is_";
-val unN = "un_";
-val notN = "not_";
+val is_prefix = "is_";
+val un_prefix = "un_";
+val not_prefix = "not_";
-fun mk_unN 1 1 suf = unN ^ suf
- | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
+fun mk_unN 1 1 suf = un_prefix ^ suf
+ | mk_unN _ l suf = un_prefix ^ suf ^ string_of_int l;
val caseN = "case";
val case_congN = "case_cong";
@@ -301,11 +300,11 @@
fun name_of_disc t =
(case head_of t of
Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
- Long_Name.map_base_name (prefix notN) (name_of_disc t')
+ Long_Name.map_base_name (prefix not_prefix) (name_of_disc t')
| Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
- Long_Name.map_base_name (prefix isN) (name_of_disc t')
+ Long_Name.map_base_name (prefix is_prefix) (name_of_disc t')
| Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
- Long_Name.map_base_name (prefix (notN ^ isN)) (name_of_disc t')
+ Long_Name.map_base_name (prefix (not_prefix ^ is_prefix)) (name_of_disc t')
| t' => name_of_const "discriminator" (perhaps (try domain_type)) t');
val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
@@ -437,7 +436,7 @@
fun is_disc_binding_valid b =
not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
- val standard_disc_binding = Binding.name o prefix isN o base_name_of_ctr;
+ val standard_disc_binding = Binding.name o prefix is_prefix o base_name_of_ctr;
val disc_bindings =
raw_disc_bindings
@@ -469,8 +468,7 @@
val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
- val ((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))) =
- no_defs_lthy
+ val (((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))), _) = no_defs_lthy
|> add_bindings
|> yield_singleton (mk_Frees fc_b_name) fcT
||>> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *)
@@ -479,8 +477,7 @@
||>> mk_Frees "f" case_Ts
||>> mk_Frees "g" case_Ts
||>> yield_singleton (mk_Frees "z") B
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT
- |> fst;
+ ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
val q = Free (fst p', mk_pred1T B);
@@ -679,8 +676,7 @@
fun after_qed ([exhaust_thm] :: thmss) lthy =
let
- val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) =
- lthy
+ val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) = lthy
|> add_bindings
|> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT
||>> mk_Freess' "x" ctr_Tss
@@ -901,11 +897,11 @@
val nontriv_disc_thmss =
map2 (fn b => if is_disc_binding_valid b then I else K []) disc_bindings disc_thmss;
- fun is_discI_boring b =
+ fun is_discI_triv b =
(n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding);
val nontriv_discI_thms =
- flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings
+ flat (map2 (fn b => if is_discI_triv b then K [] else single) disc_bindings
discI_thms);
val (distinct_disc_thms, (distinct_disc_thmsss', distinct_disc_thmsss)) =
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Feb 17 21:08:18 2016 +0100
@@ -85,14 +85,8 @@
(* relator_eq_onp *)
-fun relator_eq_onp bnf ctxt =
- let
- val relator_eq_onp_thm = lookup_defined_pred_data ctxt (type_name_of_bnf bnf)
- |> Transfer.rel_eq_onp
- in
- [((Binding.empty, []), [([relator_eq_onp_thm], @{attributes [relator_eq_onp]})])]
- end
- handle NO_PRED_DATA _ => [] (* the "lifting" plugin should work even if "quotient" is disabled *)
+fun relator_eq_onp bnf =
+ [((Binding.empty, []), [([rel_eq_onp_of_bnf bnf], @{attributes [relator_eq_onp]})])]
(* relator_mono *)
@@ -110,7 +104,7 @@
if dead_of_bnf bnf > 0 then lthy
else
let
- val notess = [relator_eq_onp bnf lthy, Quotient_map bnf lthy, relator_mono bnf,
+ val notess = [relator_eq_onp bnf, Quotient_map bnf lthy, relator_mono bnf,
relator_distr bnf]
in
lthy |> fold (perhaps o try o (snd oo Local_Theory.notes)) notess
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 21:08:18 2016 +0100
@@ -919,9 +919,8 @@
bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
finitizable_dataTs
val _ = if skipped > 0 then
- print_nt (fn () => "Too many scopes. Skipping " ^
- string_of_int skipped ^ " scope" ^
- plural_s skipped ^
+ print_nt (fn () => "Skipping " ^ string_of_int skipped ^
+ " scope" ^ plural_s skipped ^
". (Consider using \"mono\" or \
\\"merge_type_vars\" to prevent this.)")
else
--- a/src/HOL/Tools/Transfer/transfer.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed Feb 17 21:08:18 2016 +0100
@@ -10,7 +10,6 @@
type pred_data
val mk_pred_data: thm -> thm -> thm list -> pred_data
val rel_eq_onp: pred_data -> thm
- val rel_eq_onp_with_tops: pred_data -> thm
val pred_def: pred_data -> thm
val pred_simps: pred_data -> thm list
val update_pred_simps: thm list -> pred_data -> pred_data
@@ -76,9 +75,6 @@
fun rep_pred_data (PRED_DATA p) = p
val rel_eq_onp = #rel_eq_onp o rep_pred_data
-val rel_eq_onp_with_tops = (Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
- (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))))
- o #rel_eq_onp o rep_pred_data
val pred_def = #pred_def o rep_pred_data
val pred_simps = #pred_simps o rep_pred_data
fun update_pred_simps new_pred_data = map_pred_data' I I (K new_pred_data)
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Feb 17 21:08:18 2016 +0100
@@ -27,7 +27,6 @@
(* util functions *)
fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
-fun mk_Frees_free x Ts ctxt = Variable.variant_frees ctxt [] (mk_names (length Ts) x ~~ Ts) |> map Free
fun mk_Domainp P =
let
@@ -37,26 +36,6 @@
Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P
end
-fun mk_pred pred_def args T =
- let
- val pred_name = pred_def |> Thm.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 =
- let
- val argT = domain_type (fastype_of arg)
- in
- Const (@{const_name eq_onp}, (argT --> HOLogic.boolT) --> argT --> argT --> HOLogic.boolT)
- $ arg
- end
-
-fun subst_conv thm =
- Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) @{context}
-
fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
fun is_Type (Type _) = true
@@ -76,19 +55,19 @@
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 =
let
val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf,
rel_OO_of_bnf bnf]
in
- (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac ctxt (rel_mono_of_bnf bnf)
- THEN_ALL_NEW assume_tac ctxt) i
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac ctxt (rel_mono_of_bnf bnf)
+ THEN_ALL_NEW assume_tac ctxt
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 =
+ SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
CONJ_WRAP' (fn thm => rtac ctxt thm THEN_ALL_NEW
- (REPEAT_DETERM o etac ctxt conjE THEN' assume_tac ctxt)) sided_constr_intros) i
+ (REPEAT_DETERM o etac ctxt conjE THEN' assume_tac ctxt)) sided_constr_intros
fun generate_relation_constraint_goal ctxt bnf constraint_def =
let
@@ -162,41 +141,16 @@
fun bnf_transfer_rules bnf =
let
- val transfer_rules = map_transfer_of_bnf bnf :: rel_transfer_of_bnf bnf
- :: set_transfer_of_bnf bnf
+ val transfer_rules = map_transfer_of_bnf bnf :: pred_transfer_of_bnf bnf
+ :: rel_transfer_of_bnf bnf :: set_transfer_of_bnf bnf
val transfer_attr = @{attributes [transfer_rule]}
in
map (fn thm => ((Binding.empty,[]),[([thm],transfer_attr)])) transfer_rules
end
-(* predicator definition and Domainp and eq_onp theorem *)
+(* Domainp theorem for predicator *)
-fun define_pred bnf lthy =
- let
- fun mk_pred_name c = Binding.prefix_name "pred_" c
- val live = live_of_bnf bnf
- val Tname = base_name_of_bnf bnf
- val ((As, Ds), lthy) = lthy
- |> mk_TFrees live
- ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
- val T = mk_T_of_bnf Ds As bnf
- val sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf
- val argTs = map mk_pred1T As
- val args = mk_Frees_free "P" argTs lthy
- val conjs = map (fn (set, arg) => mk_Ball (set $ Bound 0) arg) (sets ~~ args)
- val rhs = Abs ("x", T, foldr1 HOLogic.mk_conj conjs)
- val pred_name = mk_pred_name Tname
- val headT = argTs ---> (T --> HOLogic.boolT)
- 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)),
- ((Binding.empty, []), def)) lthy
- in
- (pred_def, lthy)
- end
-
-fun Domainp_tac bnf pred_def ctxt i =
+fun Domainp_tac bnf pred_def ctxt =
let
val n = live_of_bnf bnf
val set_map's = set_map_of_bnf bnf
@@ -219,7 +173,7 @@
REPEAT_DETERM o resolve_tac ctxt [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
dtac ctxt (rotate_prems 1 bspec), assume_tac ctxt,
etac ctxt @{thm DomainpE}, etac ctxt @{thm someI}]) set_map's
- ] i
+ ]
end
fun prove_Domainp_rel ctxt bnf pred_def =
@@ -233,10 +187,9 @@
val relator = mk_rel_of_bnf Ds As Bs bnf
val relsT = map2 mk_pred2T As Bs
- val T = mk_T_of_bnf Ds As bnf
val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
val lhs = mk_Domainp (list_comb (relator, args))
- val rhs = mk_pred pred_def (map mk_Domainp args) T
+ val rhs = Term.list_comb (mk_pred_of_bnf Ds As bnf, map mk_Domainp args)
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
val thm = Goal.prove_sorry ctxt [] [] goal
(fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
@@ -245,46 +198,17 @@
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},
- @{thm Ball_Collect}, pred_def]) THEN' CONVERSION (subst_conv (map_id0_of_bnf bnf RS sym))
- THEN' rtac ctxt (rel_Grp_of_bnf bnf)) i
-
-fun prove_rel_eq_onp ctxt bnf pred_def =
- let
- val live = live_of_bnf bnf
- val old_ctxt = ctxt
- val ((As, Ds), ctxt) = ctxt
- |> mk_TFrees live
- ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
- val T = mk_T_of_bnf Ds As bnf
- val argTs = map mk_pred1T As
- val (args, ctxt) = mk_Frees "P" argTs ctxt
- val relator = mk_rel_of_bnf Ds As As bnf
- 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_sorry ctxt [] [] goal
- (fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1)
- |> Thm.close_derivation
- in
- Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
- end
-
fun predicator bnf lthy =
let
- val (pred_def, lthy) = define_pred bnf lthy
- val pred_def = Morphism.thm (Local_Theory.target_morphism lthy) pred_def
+ val pred_def = pred_set_of_bnf bnf
val Domainp_rel = prove_Domainp_rel lthy bnf pred_def
- val rel_eq_onp = prove_rel_eq_onp lthy bnf pred_def
+ val rel_eq_onp = rel_eq_onp_of_bnf bnf
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 pred_data = Transfer.mk_pred_data pred_def rel_eq_onp []
val type_name = type_name_of_bnf bnf
val relator_domain_attr = @{attributes [relator_domain]}
- val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
- ((rel_eq_onp_thm_name, []), [([rel_eq_onp], [])])]
+ val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)])]
in
lthy
|> Local_Theory.notes notes
@@ -320,61 +244,6 @@
SOME data => data
| NONE => raise NO_PRED_DATA ()
-fun lives_of_fp (fp_sugar: fp_sugar) =
- let
- val As = snd (dest_Type (#T fp_sugar))
- val liveness = liveness_of_fp_bnf (length As) (hd (#bnfs (#fp_res fp_sugar)));
- in
- map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ As)
- end
-
-fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
- let
- val involved_types = distinct op= (
- 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_with_tops o lookup_defined_pred_data lthy) involved_types
- val old_lthy = lthy
- val (As, lthy) = mk_TFrees' (map Type.sort_of_atyp (lives_of_fp fp_sugar)) lthy
- val predTs = map mk_pred1T As
- val (preds, lthy) = mk_Frees "P" predTs lthy
- val args = map mk_eq_onp preds
- val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) As)
- val cts = map (SOME o Thm.cterm_of lthy) args
- fun get_rhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
- fun is_eqn thm = can get_rhs thm
- fun rel2pred_massage thm =
- let
- val live_step = @{lemma "x = y \<Longrightarrow> (eq_onp P a a \<and> x) = (P a \<and> y)" by (simp only: eq_onp_same_args)}
- val kill_top1 = @{lemma "(top x \<and> P) = P" by blast}
- val kill_top2 = @{lemma "(P \<and> top x) = P" by blast}
- fun pred_eq_onp_conj conjs = List.foldr (fn (_, thm) => thm RS live_step)
- @{thm refl[of True]} conjs
- val conjuncts = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj else []
- val kill_top = Local_Defs.unfold lthy [kill_top2] #> Local_Defs.unfold lthy [kill_top1]
- val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}]
- in
- thm
- |> Thm.instantiate' cTs cts
- |> 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}
- 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
- end
- val rel_injects = #rel_injects (#fp_bnf_sugar fp_sugar)
- in
- rel_injects
- |> map (Local_Defs.unfold lthy [@{thm conj_assoc}])
- |> map rel2pred_massage
- |> Variable.export lthy old_lthy
- |> map Drule.zero_var_indexes
- end
- handle NO_PRED_DATA () => []
-
(* fp_sugar interpretation *)
@@ -389,28 +258,22 @@
map (fn thm => ((Binding.empty, []), [([thm], transfer_attr)])) transfer_rules
end
-fun pred_injects fp_sugar lthy =
+fun register_pred_injects fp_sugar lthy =
let
- val pred_injects = prove_pred_inject lthy fp_sugar
- fun qualify defname suffix = Binding.qualified true suffix defname
- val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject"
- val simp_attrs = @{attributes [simp]}
+ val pred_injects = #pred_injects (#fp_bnf_sugar fp_sugar)
val type_name = type_name_of_bnf (#fp_bnf fp_sugar)
val pred_data = lookup_defined_pred_data lthy type_name
|> Transfer.update_pred_simps pred_injects
in
lthy
- |> Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects)
- |> snd
|> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
+ (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
|> Local_Theory.restore
end
-
fun transfer_fp_sugars_interpretation fp_sugar lthy =
let
- val lthy = pred_injects fp_sugar lthy
+ val lthy = register_pred_injects fp_sugar lthy
val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar
in
lthy
--- a/src/HOL/Transfer.thy Wed Feb 17 21:08:11 2016 +0100
+++ b/src/HOL/Transfer.thy Wed Feb 17 21:08:18 2016 +0100
@@ -229,28 +229,7 @@
end
-subsection \<open>Equality restricted by a predicate\<close>
-definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
- where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
-
-lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id"
-unfolding eq_onp_def Grp_def by auto
-
-lemma eq_onp_to_eq:
- assumes "eq_onp P x y"
- shows "x = y"
-using assms by (simp add: eq_onp_def)
-
-lemma eq_onp_top_eq_eq: "eq_onp top = op="
-by (simp add: eq_onp_def)
-
-lemma eq_onp_same_args:
- shows "eq_onp P x x = P x"
-using assms by (auto simp add: eq_onp_def)
-
-lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
-by auto
ML_file "Tools/Transfer/transfer.ML"
declare refl [transfer_rule]
@@ -557,7 +536,7 @@
lemma prod_pred_parametric [transfer_rule]:
"((A ===> op =) ===> (B ===> op =) ===> rel_prod A B ===> op =) pred_prod pred_prod"
-unfolding pred_prod_def[abs_def] Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps
+unfolding prod.pred_set[abs_def] Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps
by simp transfer_prover
lemma apfst_parametric [transfer_rule]: