--- a/src/HOL/Codatatype/BNF_Comp.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Comp.thy Thu Sep 20 02:42:49 2012 +0200
@@ -82,6 +82,9 @@
lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)"
by auto
+lemma mem_Id_eq_eq: "(\<lambda>x y. (x, y) \<in> Id) = (op =)"
+by simp
+
ML_file "Tools/bnf_comp_tactics.ML"
ML_file "Tools/bnf_comp.ML"
--- a/src/HOL/Codatatype/BNF_Util.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Util.thy Thu Sep 20 02:42:49 2012 +0200
@@ -18,11 +18,8 @@
lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
by blast
-lemma mem_Collect_eq_split: "{(x, y). (x, y) \<in> X} = X"
-by simp
-
definition collect where
- "collect F x = (\<Union>f \<in> F. f x)"
+"collect F x = (\<Union>f \<in> F. f x)"
(* Weak pullbacks: *)
definition wpull where
@@ -50,6 +47,16 @@
lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
unfolding bij_def inj_on_def by auto blast
+lemma pair_mem_Collect_split:
+"(\<lambda>x y. (x, y) \<in> {(x, y). P x y}) = P"
+by simp
+
+lemma Collect_pair_mem_eq: "{(x, y). (x, y) \<in> R} = R"
+by simp
+
+lemma Collect_fst_snd_mem_eq: "{p. (fst p, snd p) \<in> A} = A"
+by simp
+
(* Operator: *)
definition "Gr A f = {(a, f a) | a. a \<in> A}"
--- a/src/HOL/Codatatype/Basic_BNFs.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Basic_BNFs.thy Thu Sep 20 02:42:49 2012 +0200
@@ -25,7 +25,7 @@
unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
- "id :: ('a \<times> 'b) set \<Rightarrow> ('a \<times> 'b) set"
+ "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
apply auto
apply (rule natLeq_card_order)
apply (rule natLeq_cinfinite)
@@ -51,10 +51,8 @@
apply (auto simp: Gr_def fun_eq_iff)
done
-definition DEADID_rel :: "('a \<times> 'a) set" where
-"DEADID_rel = {p. \<exists>x. p = (x, x)}"
-
-bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] DEADID_rel
+bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
+ "op =::'a \<Rightarrow> 'a \<Rightarrow> bool"
apply (auto simp add: wpull_id)
apply (rule card_order_csum)
apply (rule natLeq_card_order)
@@ -71,7 +69,7 @@
apply (rule card_of_Card_order)
apply (rule ctwo_Cnotzero)
apply (rule card_of_Card_order)
-apply (auto simp: DEADID_rel_def Id_def Gr_def fun_eq_iff)
+apply (auto simp: Id_def Gr_def fun_eq_iff)
done
definition setl :: "'a + 'b \<Rightarrow> 'a set" where
@@ -82,13 +80,12 @@
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
-definition sum_rel :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a + 'c) \<times> ('b + 'd)) set" where
-"sum_rel R S =
- {x. case x of (Inl a, Inl c) \<Rightarrow> (a, c) \<in> R
- | (Inr b, Inr d) \<Rightarrow> (b, d) \<in> S
- | _ \<Rightarrow> False}"
+definition sum_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool" where
+"sum_pred \<phi> \<psi> x y =
+ (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
+ | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
-bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
+bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_pred
proof -
show "sum_map id id = id" by (rule sum_map.id)
next
@@ -199,10 +196,10 @@
qed
next
fix R S
- show "sum_rel R S =
- (Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O
- Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)"
- unfolding setl_def setr_def sum_rel_def Gr_def relcomp_unfold converse_unfold
+ show "{p. sum_pred (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
+ (Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O
+ Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)"
+ unfolding setl_def setr_def sum_pred_def Gr_def relcomp_unfold converse_unfold
by (fastforce split: sum.splits)
qed (auto simp: sum_set_defs)
@@ -224,10 +221,10 @@
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
-definition prod_rel :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a \<times> 'c) \<times> 'b \<times> 'd) set" where
-"prod_rel R S = {((a, c), b, d) | a b c d. (a, b) \<in> R \<and> (c, d) \<in> S}"
+definition prod_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where
+"prod_pred \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)"
-bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel
+bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_pred
proof (unfold prod_set_defs)
show "map_pair id id = id" by (rule map_pair.id)
next
@@ -304,10 +301,10 @@
unfolding wpull_def by simp fast
next
fix R S
- show "prod_rel R S =
- (Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O
- Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)"
- unfolding prod_set_defs prod_rel_def Gr_def relcomp_unfold converse_unfold
+ show "{p. prod_pred (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
+ (Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O
+ Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)"
+ unfolding prod_set_defs prod_pred_def Gr_def relcomp_unfold converse_unfold
by auto
qed simp+
@@ -347,11 +344,11 @@
ultimately show ?thesis using card_of_ordLeq by fast
qed
-definition fun_rel :: "('a \<times> 'b) set \<Rightarrow> (('c \<Rightarrow> 'a) \<times> ('c \<Rightarrow> 'b)) set" where
-"fun_rel R = {(f, g) | f g. \<forall>x. (f x, g x) \<in> R}"
+definition fun_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b) \<Rightarrow> bool" where
+"fun_pred \<phi> f g = (\<forall>x. \<phi> (f x) (g x))"
bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
- fun_rel
+ fun_pred
proof
fix f show "id \<circ> f = id f" by simp
next
@@ -410,8 +407,10 @@
using wpull_cat[OF p c r] by simp metis
qed
next
- fix R show "fun_rel R = (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
- unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold
+ fix R
+ show "{p. fun_pred (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
+ (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
+ unfolding fun_pred_def Gr_def relcomp_unfold converse_unfold
by (auto intro!: exI dest!: in_mono)
qed auto
--- a/src/HOL/Codatatype/Examples/HFset.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/HFset.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Codatatype_Examples/HFset.thy
+(* Title: HOL/Codatatype/Examples/HFset.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Gram_Lang.thy
+(* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,3 +1,12 @@
+(* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy
+ Author: Andrei Popescu, TU Muenchen
+ Copyright 2012
+
+Parallel composition.
+*)
+
+header {* Parallel Composition *}
+
theory Parallel
imports Tree
begin
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,10 +1,11 @@
-(* Title: Gram_Tree.thy
+(* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
-Preliminaries
+Preliminaries.
*)
+header {* Preliminaries *}
theory Prelim
imports "../../Codatatype/Codatatype"
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,18 +1,18 @@
-(* Title: Gram_Tree.thy
+(* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
Trees with nonterminal internal nodes and terminal leafs.
*)
-
header {* Trees with nonterminal internal nodes and terminal leafs *}
-
theory Tree
imports Prelim
begin
+hide_fact (open) Quotient_Product.prod_pred_def
+
typedecl N typedecl T
codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset"
@@ -41,7 +41,7 @@
(\<forall> tr2. Inr tr2 \<in> fset as2 \<longrightarrow> (\<exists> tr1. Inr tr1 \<in> fset as1 \<and> \<phi> tr1 tr2))"
lemma pre_Tree_pred: "pre_Tree_pred \<phi> (n1,as1) (n2,as2) \<longleftrightarrow> n1 = n2 \<and> llift2 \<phi> as1 as2"
-unfolding llift2_def pre_Tree.pred_unfold
+unfolding llift2_def pre_Tree_pred_def sum_pred_def[abs_def] prod_pred_def fset_pred_def split_conv
apply (auto split: sum.splits)
apply (metis sumE)
apply (metis sumE)
--- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Codatatype_Examples/Lambda_Term.thy
+(* Title: HOL/Codatatype/Examples/Lambda_Term.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
--- a/src/HOL/Codatatype/Examples/ListF.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/ListF.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Codatatype_Examples/ListF.thy
+(* Title: HOL/Codatatype/Examples/ListF.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
--- a/src/HOL/Codatatype/Examples/Misc_Codata.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Codatatype_Examples/Misc_Data.thy
+(* Title: HOL/Codatatype/Examples/Misc_Data.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Codatatype_Examples/Misc_Data.thy
+(* Title: HOL/Codatatype/Examples/Misc_Data.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
@@ -9,13 +9,9 @@
header {* Miscellaneous Datatype Declarations *}
theory Misc_Data
-imports (* "../Codatatype" *) "../BNF_LFP"
+imports "../Codatatype"
begin
-bnf_def ID2: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
- "id :: ('a \<times> 'b) set \<Rightarrow> ('a \<times> 'b) set"
-sorry
-
data simple = X1 | X2 | X3 | X4
data simple' = X1' unit | X2' unit | X3' unit | X4' unit
--- a/src/HOL/Codatatype/Examples/Process.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Process.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Codatatype_Examples/Process.thy
+(* Title: HOL/Codatatype/Examples/Process.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
@@ -11,6 +11,8 @@
imports "../Codatatype"
begin
+hide_fact (open) Quotient_Product.prod_pred_def
+
codata 'a process =
isAction: Action (prefOf: 'a) (contOf: "'a process") |
isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process")
@@ -21,7 +23,10 @@
subsection {* Basic properties *}
-declare pre_process.pred_unfold[simp]
+declare
+ pre_process_pred_def[simp]
+ sum_pred_def[simp]
+ prod_pred_def[simp]
(* Constructors versus discriminators *)
theorem isAction_isChoice:
--- a/src/HOL/Codatatype/Examples/Stream.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Stream.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Codatatype_Examples/Stream.thy
+(* Title: HOL/Codatatype/Examples/Stream.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
@@ -12,6 +12,9 @@
imports TreeFI
begin
+hide_const (open) Quotient_Product.prod_pred
+hide_fact (open) Quotient_Product.prod_pred_def
+
codata_raw stream: 's = "'a \<times> 's"
(* selectors for streams *)
@@ -115,10 +118,10 @@
unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def]
map_pair_def o_def prod_case_beta by simp
-lemma pre_stream_pred[simp]: "pre_stream_pred \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))"
-by (auto simp: pre_stream.pred_unfold)
+lemma prod_pred[simp]: "prod_pred \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))"
+unfolding prod_pred_def by auto
-lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded pre_stream_pred[abs_def],
+lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded prod_pred[abs_def],
folded hdd_def tll_def]
definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
@@ -133,27 +136,22 @@
definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
lemma "ones \<oplus> ones = twos"
-by (intro stream_coind[where P="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"])
- auto
+by (intro stream_coind[where P="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
lemma "n \<cdot> twos = ns (2 * n)"
-by (intro stream_coind[where P="%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"])
- force+
+by (intro stream_coind[where P="%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
-by (intro stream_coind[where P="%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"])
- force+
+by (intro stream_coind[where P="%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
by (intro stream_coind[where P="%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
(force simp: add_mult_distrib2)+
lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
-by (intro stream_coind[where P="%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"])
- force+
+by (intro stream_coind[where P="%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
-by (intro stream_coind[where P="%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"])
- force+
+by (intro stream_coind[where P="%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
end
--- a/src/HOL/Codatatype/Examples/TreeFI.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFI.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Codatatype_Examples/TreeFI.thy
+(* Title: HOL/Codatatype/Examples/TreeFI.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: Codatatype_Examples/TreeFsetI.thy
+(* Title: HOL/Codatatype/Examples/TreeFsetI.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
@@ -13,6 +13,7 @@
begin
hide_const (open) Sublist.sub
+hide_fact (open) Quotient_Product.prod_pred_def
definition pair_fun (infixr "\<odot>" 50) where
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
@@ -46,7 +47,7 @@
(\<forall>t \<in> fset (snd b). (\<exists>u \<in> fset (snd a). R2 u t)))"
apply (cases a)
apply (cases b)
-apply (simp add: pre_treeFsetI.pred_unfold)
+apply (simp add: pre_treeFsetI_pred_def prod_pred_def fset_pred_def)
done
lemmas treeFsetI_coind = mp[OF treeFsetI.pred_coinduct]
--- a/src/HOL/Codatatype/More_BNFs.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/More_BNFs.thy Thu Sep 20 02:42:49 2012 +0200
@@ -22,10 +22,14 @@
lemma option_rec_conv_option_case: "option_rec = option_case"
by (simp add: fun_eq_iff split: option.split)
-definition option_rel :: "('a \<times> 'b) set \<Rightarrow> ('a option \<times> 'b option) set" where
-"option_rel R = {x. case x of (None, None) \<Rightarrow> True | (Some a, Some b) \<Rightarrow> (a, b) \<in> R | _ \<Rightarrow> False}"
+definition option_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool" where
+"option_pred R x_opt y_opt =
+ (case (x_opt, y_opt) of
+ (None, None) \<Rightarrow> True
+ | (Some x, Some y) \<Rightarrow> R x y
+ | _ \<Rightarrow> False)"
-bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_rel
+bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_pred
proof -
show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
next
@@ -86,9 +90,9 @@
thus False by simp
next
fix R
- show "option_rel R =
+ show "{p. option_pred (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
(Gr {x. Option.set x \<subseteq> R} (Option.map fst))\<inverse> O Gr {x. Option.set x \<subseteq> R} (Option.map snd)"
- unfolding option_rel_def Gr_def relcomp_unfold converse_unfold
+ unfolding option_pred_def Gr_def relcomp_unfold converse_unfold
by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
split: option.splits) blast
qed
@@ -356,35 +360,36 @@
lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
-lemma fset_pred:
-"(a, b) \<in> (Gr {a. fset a \<subseteq> {(a, b). R a b}} (map_fset fst))\<inverse> O
- Gr {a. fset a \<subseteq> {(a, b). R a b}} (map_fset snd) \<longleftrightarrow>
- ((\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u))" (is "?L = ?R")
+definition fset_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" where
+"fset_pred R a b \<longleftrightarrow>
+ (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and>
+ (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
+
+lemma fset_pred_aux:
+"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
+ (a, b) \<in> (Gr {a. fset a \<subseteq> {(a, b). R a b}} (map_fset fst))\<inverse> O
+ Gr {a. fset a \<subseteq> {(a, b). R a b}} (map_fset snd)" (is "?L = ?R")
proof
- assume ?L thus ?R unfolding Gr_def relcomp_unfold converse_unfold
+ assume ?L
+ def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
+ have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto
+ hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
+ show ?R unfolding Gr_def relcomp_unfold converse_unfold
+ proof (intro CollectI prod_caseI exI conjI)
+ from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?L`]
+ by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
+ from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?L`]
+ by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
+ qed (auto simp add: *)
+next
+ assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
apply (simp add: subset_eq Ball_def)
apply (rule conjI)
apply (clarsimp, metis snd_conv)
by (clarsimp, metis fst_conv)
-next
- assume ?R
- def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?R'")
- have "finite ?R'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto
- hence *: "fset R' = ?R'" unfolding R'_def by (intro fset_to_fset)
- show ?L unfolding Gr_def relcomp_unfold converse_unfold
- proof (intro CollectI prod_caseI exI conjI)
- from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?R`]
- by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
- from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?R`]
- by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
- qed (auto simp add: *)
qed
-definition fset_rel :: "('a \<times> 'b) set \<Rightarrow> ('a fset \<times> 'b fset) set" where
-"fset_rel R = {(a, b) | a b. (\<forall>t \<in> fset a. \<exists>u \<in> fset b. (t, u) \<in> R) \<and>
- (\<forall>u \<in> fset b. \<exists>t \<in> fset a. (t, u) \<in> R)}"
-
-bnf_def map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
+bnf_def map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_pred
proof -
show "map_fset id = id"
unfolding map_fset_def2 map_id o_id afset_rfset_id ..
@@ -460,11 +465,9 @@
qed
next
fix R
- let ?pred = "\<lambda>Q x y. (x, y) \<in> (Gr {x. fset x \<subseteq> {(x, y). Q x y}} (map_fset fst))\<inverse> O Gr {x. fset x \<subseteq> {(x, y). Q x y}} (map_fset snd)"
- have rel_as_pred: "fset_rel R = {(a, b) | a b. ?pred (\<lambda>t u. (t, u) \<in> R) a b}"
- unfolding fset_rel_def fset_pred by (rule refl)
- show "fset_rel R = (Gr {x. fset x \<subseteq> R} (map_fset fst))\<inverse> O Gr {x. fset x \<subseteq> R} (map_fset snd)"
- unfolding rel_as_pred by simp
+ show "{p. fset_pred (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
+ (Gr {x. fset x \<subseteq> R} (map_fset fst))\<inverse> O Gr {x. fset x \<subseteq> R} (map_fset snd)"
+ unfolding fset_pred_def fset_pred_aux by simp
qed auto
(* Countable sets *)
@@ -534,41 +537,42 @@
lemma rcset_natural': "rcset (cIm f x) = f ` rcset x"
unfolding cIm_def[abs_def] by simp
-lemma cset_pred:
-"(a, b) \<in> (Gr {x. rcset x \<subseteq> {(a, b). R a b}} (cIm fst))\<inverse> O
- Gr {x. rcset x \<subseteq> {(a, b). R a b}} (cIm snd) \<longleftrightarrow>
- ((\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t))" (is "?L = ?R")
+definition cset_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
+"cset_pred R a b \<longleftrightarrow>
+ (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
+ (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)"
+
+lemma cset_pred_aux:
+"(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t) \<longleftrightarrow>
+ (a, b) \<in> (Gr {x. rcset x \<subseteq> {(a, b). R a b}} (cIm fst))\<inverse> O
+ Gr {x. rcset x \<subseteq> {(a, b). R a b}} (cIm snd)" (is "?L = ?R")
proof
- assume ?L thus ?R unfolding Gr_def relcomp_unfold converse_unfold
+ assume ?L
+ def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
+ (is "the_inv rcset ?L'")
+ have "countable ?L'" by auto
+ hence *: "rcset R' = ?L'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset)
+ show ?R unfolding Gr_def relcomp_unfold converse_unfold
+ proof (intro CollectI prod_caseI exI conjI)
+ have "rcset a = fst ` ({(x, y). R x y} \<inter> rcset a \<times> rcset b)" (is "_ = ?A")
+ using conjunct1[OF `?L`] unfolding image_def by (auto simp add: Collect_Int_Times)
+ hence "a = acset ?A" by (metis acset_rcset)
+ thus "(R', a) = (R', cIm fst R')" unfolding cIm_def * by auto
+ have "rcset b = snd ` ({(x, y). R x y} \<inter> rcset a \<times> rcset b)" (is "_ = ?B")
+ using conjunct2[OF `?L`] unfolding image_def by (auto simp add: Collect_Int_Times)
+ hence "b = acset ?B" by (metis acset_rcset)
+ thus "(R', b) = (R', cIm snd R')" unfolding cIm_def * by auto
+ qed (auto simp add: *)
+next
+ assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
apply (simp add: subset_eq Ball_def)
apply (rule conjI)
apply (clarsimp, metis (lifting, no_types) rcset_natural' image_iff surjective_pairing)
apply (clarsimp)
by (metis Domain.intros Range.simps rcset_natural' fst_eq_Domain snd_eq_Range)
-next
- assume ?R
- def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
- (is "the_inv rcset ?R'")
- have "countable ?R'" by auto
- hence *: "rcset R' = ?R'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset)
- show ?L unfolding Gr_def relcomp_unfold converse_unfold
- proof (intro CollectI prod_caseI exI conjI)
- have "rcset a = fst ` ({(x, y). R x y} \<inter> rcset a \<times> rcset b)" (is "_ = ?A")
- using conjunct1[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times)
- hence "a = acset ?A" by (metis acset_rcset)
- thus "(R', a) = (R', cIm fst R')" unfolding cIm_def * by auto
- have "rcset b = snd ` ({(x, y). R x y} \<inter> rcset a \<times> rcset b)" (is "_ = ?B")
- using conjunct2[OF `?R`] unfolding image_def by (auto simp add: Collect_Int_Times)
- hence "b = acset ?B" by (metis acset_rcset)
- thus "(R', b) = (R', cIm snd R')" unfolding cIm_def * by auto
- qed (auto simp add: *)
qed
-definition cset_rel :: "('a \<times> 'b) set \<Rightarrow> ('a cset \<times> 'b cset) set" where
-"cset_rel R = {(a, b) | a b. (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. (t, u) \<in> R) \<and>
- (\<forall>u \<in> rcset b. \<exists>t \<in> rcset a. (t, u) \<in> R)}"
-
-bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_rel
+bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_pred
proof -
show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
next
@@ -632,11 +636,9 @@
qed
next
fix R
- let ?pred = "\<lambda>Q x y. (x, y) \<in> (Gr {x. rcset x \<subseteq> {(x, y). Q x y}} (cIm fst))\<inverse> O Gr {x. rcset x \<subseteq> {(x, y). Q x y}} (cIm snd)"
- have rel_as_pred: "cset_rel R = {(a, b) | a b. ?pred (\<lambda>t u. (t, u) \<in> R) a b}"
- unfolding cset_rel_def cset_pred by (rule refl)
- show "cset_rel R = (Gr {x. rcset x \<subseteq> R} (cIm fst))\<inverse> O Gr {x. rcset x \<subseteq> R} (cIm snd)"
- unfolding rel_as_pred by simp
+ show "{p. cset_pred (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
+ (Gr {x. rcset x \<subseteq> R} (cIm fst))\<inverse> O Gr {x. rcset x \<subseteq> R} (cIm snd)"
+ unfolding cset_pred_def cset_pred_aux by simp
qed (unfold cEmp_def, auto)
@@ -1302,27 +1304,27 @@
declare multiset.count_inverse[simp]
declare union_preserves_multiset[simp]
-lemma mmap_Plus[simp]:
+lemma mmap_Plus[simp]:
assumes "K \<in> multiset" and "L \<in> multiset"
shows "mmap f (\<lambda>a. K a + L a) a = mmap f K a + mmap f L a"
proof-
- have "{aa. f aa = a \<and> (0 < K aa \<or> 0 < L aa)} \<subseteq>
+ have "{aa. f aa = a \<and> (0 < K aa \<or> 0 < L aa)} \<subseteq>
{aa. 0 < K aa} \<union> {aa. 0 < L aa}" (is "?C \<subseteq> ?A \<union> ?B") by auto
- moreover have "finite (?A \<union> ?B)" apply(rule finite_UnI)
+ moreover have "finite (?A \<union> ?B)" apply(rule finite_UnI)
using assms unfolding multiset_def by auto
ultimately have C: "finite ?C" using finite_subset by blast
have "setsum K {aa. f aa = a \<and> 0 < K aa} = setsum K {aa. f aa = a \<and> 0 < K aa + L aa}"
apply(rule setsum_mono_zero_cong_left) using C by auto
- moreover
+ moreover
have "setsum L {aa. f aa = a \<and> 0 < L aa} = setsum L {aa. f aa = a \<and> 0 < K aa + L aa}"
apply(rule setsum_mono_zero_cong_left) using C by auto
ultimately show ?thesis
unfolding mmap_def unfolding comm_monoid_add_class.setsum.F_fun_f by auto
qed
-lemma multiset_map_Plus[simp]:
+lemma multiset_map_Plus[simp]:
"multiset_map f (M1 + M2) = multiset_map f M1 + multiset_map f M2"
-unfolding multiset_map_def
+unfolding multiset_map_def
apply(subst multiset.count_inject[symmetric])
unfolding plus_multiset.rep_eq comp_def by auto
@@ -1335,23 +1337,23 @@
by (simp, simp add: single_def)
qed
-lemma multiset_pred_Plus:
+lemma multiset_pred_Plus:
assumes ab: "R a b" and MN: "multiset_pred R M N"
shows "multiset_pred R (M + {#a#}) (N + {#b#})"
proof-
{fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
- hence "\<exists>ya. multiset_map fst y + {#a#} = multiset_map fst ya \<and>
- multiset_map snd y + {#b#} = multiset_map snd ya \<and>
+ hence "\<exists>ya. multiset_map fst y + {#a#} = multiset_map fst ya \<and>
+ multiset_map snd y + {#b#} = multiset_map snd ya \<and>
set_of ya \<subseteq> {(x, y). R x y}"
apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
}
thus ?thesis
- using assms
+ using assms
unfolding multiset_pred_def Gr_def relcomp_unfold by force
qed
-lemma multiset_pred'_imp_multiset_pred:
-"multiset_pred' R M N \<Longrightarrow> multiset_pred R M N"
+lemma multiset_pred'_imp_multiset_pred:
+"multiset_pred' R M N \<Longrightarrow> multiset_pred R M N"
apply(induct rule: multiset_pred'.induct)
using multiset_pred_Zero multiset_pred_Plus by auto
@@ -1364,14 +1366,14 @@
using finite_Collect_mem .
ultimately have fin: "finite {b. \<exists>a. f a = b \<and> a \<in># M}" by(rule finite_subset)
have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp
- by (metis (lifting, mono_tags) mem_Collect_eq rel_simps(54)
+ by (metis (lifting, mono_tags) mem_Collect_eq rel_simps(54)
setsum_gt_0_iff setsum_infinite)
have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
apply safe
apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff)
hence AB: "A ` ?B = {A b | b. \<exists> a \<in> A b. count M a > 0}" by auto
-
+
have "setsum (\<lambda> x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B"
unfolding comp_def ..
also have "... = (\<Sum>x\<in> A ` ?B. setsum (count M) x)"
@@ -1383,7 +1385,7 @@
also have "?J = {a. a \<in># M}" unfolding AB unfolding A_def by auto
finally have "setsum (\<lambda> x. setsum (count M) (A x)) ?B =
setsum (count M) {a. a \<in># M}" .
- thus ?thesis unfolding A_def mcard_def multiset_map_def by (simp add: mmap_def)
+ thus ?thesis unfolding A_def mcard_def multiset_map_def by (simp add: mmap_def)
qed
lemma multiset_pred_mcard:
@@ -1412,7 +1414,7 @@
case True hence "N = {#}" using less.prems by auto
thus ?thesis using True empty by auto
next
- case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
+ case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
have "N \<noteq> {#}" using False less.prems by auto
then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
have "mcard M1 = mcard N1" using less.prems unfolding M N by auto
@@ -1420,7 +1422,7 @@
qed
qed
-lemma msed_map_invL:
+lemma msed_map_invL:
assumes "multiset_map f (M + {#a#}) = N"
shows "\<exists> N1. N = N1 + {#f a#} \<and> multiset_map f M = N1"
proof-
@@ -1431,19 +1433,19 @@
thus ?thesis using N by blast
qed
-lemma msed_map_invR:
+lemma msed_map_invR:
assumes "multiset_map f M = N + {#b#}"
shows "\<exists> M1 a. M = M1 + {#a#} \<and> f a = b \<and> multiset_map f M1 = N"
proof-
obtain a where a: "a \<in># M" and fa: "f a = b"
using multiset.set_natural'[of f M] unfolding assms
- by (metis image_iff mem_set_of_iff union_single_eq_member)
+ by (metis image_iff mem_set_of_iff union_single_eq_member)
then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
have "multiset_map f M1 = N" using assms unfolding M fa[symmetric] by simp
thus ?thesis using M fa by blast
qed
-lemma msed_pred_invL:
+lemma msed_pred_invL:
assumes "multiset_pred R (M + {#a#}) N"
shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> multiset_pred R M N1"
proof-
@@ -1451,7 +1453,7 @@
and KN: "multiset_map snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
using assms
unfolding multiset_pred_def Gr_def relcomp_unfold by auto
- obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
+ obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
and K1M: "multiset_map fst K1 = M" using msed_map_invR[OF KM] by auto
obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "multiset_map snd K1 = N1"
using msed_map_invL[OF KN[unfolded K]] by auto
@@ -1461,29 +1463,29 @@
thus ?thesis using N Rab by auto
qed
-lemma msed_pred_invR:
+lemma msed_pred_invR:
assumes "multiset_pred R M (N + {#b#})"
shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> multiset_pred R M1 N"
proof-
obtain K where KN: "multiset_map snd K = N + {#b#}"
and KM: "multiset_map fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
using assms
- unfolding multiset_pred_def Gr_def relcomp_unfold by auto
- obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
+ unfolding multiset_pred_def Gr_def relcomp_unfold by auto
+ obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
and K1N: "multiset_map snd K1 = N" using msed_map_invR[OF KN] by auto
obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "multiset_map fst K1 = M1"
using msed_map_invL[OF KM[unfolded K]] by auto
have Rab: "R (fst ab) b" using sK b unfolding K by auto
- have "multiset_pred R M1 N" using sK K1N K1M1
+ have "multiset_pred R M1 N" using sK K1N K1M1
unfolding K multiset_pred_def Gr_def relcomp_unfold by auto
thus ?thesis using M Rab by auto
qed
-lemma multiset_pred_imp_multiset_pred':
+lemma multiset_pred_imp_multiset_pred':
assumes "multiset_pred R M N"
shows "multiset_pred' R M N"
using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
- case (less M)
+ case (less M)
have c: "mcard M = mcard N" using multiset_pred_mcard[OF less.prems] .
show ?case
proof(cases "M = {#}")
@@ -1498,12 +1500,12 @@
qed
qed
-lemma multiset_pred_multiset_pred':
+lemma multiset_pred_multiset_pred':
"multiset_pred R M N = multiset_pred' R M N"
using multiset_pred_imp_multiset_pred' multiset_pred'_imp_multiset_pred by auto
(* The main end product for multiset_pred: inductive characterization *)
-theorems multiset_pred_induct[case_names empty add, induct pred: multiset_pred] =
+theorems multiset_pred_induct[case_names empty add, induct pred: multiset_pred] =
multiset_pred'.induct[unfolded multiset_pred_multiset_pred'[symmetric]]
end
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Sep 20 02:42:49 2012 +0200
@@ -12,6 +12,7 @@
val empty_unfold: unfold_thms
val map_unfolds_of: unfold_thms -> thm list
val set_unfoldss_of: unfold_thms -> thm list list
+ val pred_unfolds_of: unfold_thms -> thm list
val rel_unfolds_of: unfold_thms -> thm list
val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
@@ -36,6 +37,7 @@
type unfold_thms = {
map_unfolds: thm list,
set_unfoldss: thm list list,
+ pred_unfolds: thm list,
rel_unfolds: thm list
};
@@ -44,17 +46,21 @@
fun adds_to_thms thms NONE = thms
| adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
-val empty_unfold = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
+val empty_unfold = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []};
-fun add_to_unfold_opt map_opt sets_opt rel_opt {map_unfolds, set_unfoldss, rel_unfolds} = {
- map_unfolds = add_to_thms map_unfolds map_opt,
- set_unfoldss = adds_to_thms set_unfoldss sets_opt,
- rel_unfolds = add_to_thms rel_unfolds rel_opt};
+fun add_to_unfold_opt map_opt sets_opt pred_opt rel_opt
+ {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} =
+ {map_unfolds = add_to_thms map_unfolds map_opt,
+ set_unfoldss = adds_to_thms set_unfoldss sets_opt,
+ pred_unfolds = add_to_thms pred_unfolds pred_opt,
+ rel_unfolds = add_to_thms rel_unfolds rel_opt};
-fun add_to_unfold map sets rel = add_to_unfold_opt (SOME map) (SOME sets) (SOME rel);
+fun add_to_unfold map sets pred rel =
+ add_to_unfold_opt (SOME map) (SOME sets) (SOME pred) (SOME rel);
val map_unfolds_of = #map_unfolds;
val set_unfoldss_of = #set_unfoldss;
+val pred_unfolds_of = #pred_unfolds;
val rel_unfolds_of = #rel_unfolds;
val bdTN = "bdT";
@@ -64,8 +70,6 @@
fun mk_permuteN src dest =
"_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
-val subst_rel_def = @{thm subst_rel_def};
-
(*copied from Envir.expand_term_free*)
fun expand_term_const defs =
let
@@ -99,9 +103,9 @@
(Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
val Bss_repl = replicate olive Bs;
- val ((((fs', Rs'), Asets), xs), _(*names_lthy*)) = lthy
+ val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy
|> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs)
- ||>> apfst snd o mk_Frees' "R" (map2 (curry mk_relT) As Bs)
+ ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
||>> mk_Frees "A" (map HOLogic.mk_setT As)
||>> mk_Frees "x" As;
@@ -116,13 +120,13 @@
(*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
val mapx = fold_rev Term.abs fs'
(Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
- map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
+ map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
mk_map_of_bnf Ds As Bs) Dss inners));
- (*%R1 ... Rn. outer.rel (inner_1.rel R1 ... Rn) ... (inner_m.rel R1 ... Rn)*)
- val rel = fold_rev Term.abs Rs'
- (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer,
- map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
- mk_rel_of_bnf Ds As Bs) Dss inners));
+ (*%Q1 ... Qn. outer.pred (inner_1.pred Q1 ... Qn) ... (inner_m.pred Q1 ... Qn)*)
+ val pred = fold_rev Term.abs Qs'
+ (Term.list_comb (mk_pred_of_bnf oDs CAs CBs outer,
+ map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
+ mk_pred_of_bnf Ds As Bs) Dss inners));
(*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
(*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
@@ -229,16 +233,20 @@
fun rel_O_Gr_tac _ =
let
+ val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
val outer_rel_cong = rel_cong_of_bnf outer;
+ val thm =
+ (trans OF [in_alt_thm RS @{thm subst_rel_def},
+ trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
+ [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
+ rel_converse_of_bnf outer RS sym], outer_rel_Gr],
+ trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
+ (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
+ |> unfold_defs lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
in
- rtac (trans OF [in_alt_thm RS subst_rel_def,
- trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
- [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
- rel_converse_of_bnf outer RS sym], outer_rel_Gr],
- trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
- (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym) 1
- end
+ unfold_defs_tac lthy basic_thms THEN rtac thm 1
+ end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
@@ -264,10 +272,10 @@
val (bnf', lthy') =
bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
- (((((b, mapx), sets), bd), wits), SOME rel) lthy;
+ (((((b, mapx), sets), bd), wits), SOME pred) lthy;
- val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
- unfold;
+ val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+ (rel_def_of_bnf bnf') unfold;
in
(bnf', (unfold', lthy'))
end;
@@ -299,8 +307,8 @@
(*bnf.map id ... id*)
val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
- (*bnf.rel Id ... Id*)
- val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map Id_const killedAs);
+ (*bnf.pred (op =) ... (op =)*)
+ val pred = Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs);
val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
val sets = drop n bnf_sets;
@@ -312,7 +320,7 @@
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
fun map_comp_tac {context, ...} =
- Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
fun map_cong_tac {context, ...} =
mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
@@ -340,14 +348,17 @@
fun rel_O_Gr_tac _ =
let
val rel_Gr = rel_Gr_of_bnf bnf RS sym
+ val thm =
+ (trans OF [in_alt_thm RS @{thm subst_rel_def},
+ trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
+ [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]},
+ rel_converse_of_bnf bnf RS sym], rel_Gr],
+ trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
+ (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
+ replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
+ |> unfold_defs lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
in
- rtac (trans OF [in_alt_thm RS subst_rel_def,
- trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
- [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]},
- rel_converse_of_bnf bnf RS sym], rel_Gr],
- trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
- (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
- replicate (live - n) @{thm Gr_fst_snd})]]] RS sym) 1
+ rtac thm 1
end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
@@ -362,10 +373,10 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
- (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+ (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
- val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
- unfold;
+ val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+ (rel_def_of_bnf bnf') unfold;
in
(bnf', (unfold', lthy'))
end;
@@ -396,9 +407,8 @@
(*%f1 ... fn. bnf.map*)
val mapx =
fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
- (*%R1 ... Rn. bnf.rel*)
- val rel =
- fold_rev Term.absdummy (map2 (curry mk_relT) newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
+ (*%Q1 ... Qn. bnf.pred*)
+ val pred = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_pred_of_bnf Ds As Bs bnf);
val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
@@ -407,7 +417,7 @@
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
fun map_comp_tac {context, ...} =
- Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
fun map_cong_tac {context, ...} =
rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
@@ -439,7 +449,7 @@
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
fun rel_O_Gr_tac _ =
- rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
+ mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
@@ -450,10 +460,10 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
- (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+ (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
- val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
- unfold;
+ val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+ (pred_def_of_bnf bnf') unfold;
in
(bnf', (unfold', lthy'))
end;
@@ -483,10 +493,10 @@
(*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
- (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0))));
- (*%R(1) ... R(n). bnf.rel R\<sigma>(1) ... R\<sigma>(n)*)
- val rel = fold_rev Term.absdummy (permute (map2 (curry mk_relT) As Bs))
- (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0))));
+ (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
+ (*%Q(1) ... Q(n). bnf.pred Q\<sigma>(1) ... Q\<sigma>(n)*)
+ val pred = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
+ (Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
val sets = permute bnf_sets;
@@ -517,7 +527,7 @@
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
fun rel_O_Gr_tac _ =
- rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
+ mk_simple_rel_O_Gr_tac lthy (rel_def_of_bnf bnf) (rel_O_Gr_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
@@ -528,10 +538,10 @@
val (bnf', lthy') =
bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
- (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+ (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
- val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
- unfold;
+ val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+ (pred_def_of_bnf bnf') unfold;
in
(bnf', (unfold', lthy'))
end;
@@ -607,22 +617,25 @@
val map_unfolds = map_unfolds_of unfold;
val set_unfoldss = set_unfoldss_of unfold;
+ val pred_unfolds = pred_unfolds_of unfold;
val rel_unfolds = rel_unfolds_of unfold;
val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
map_unfolds);
val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of))
set_unfoldss);
- val expand_rels = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
- rel_unfolds);
- val unfold_maps = fold (Local_Defs.unfold lthy o single) map_unfolds;
- val unfold_sets = fold (Local_Defs.unfold lthy) set_unfoldss;
- val unfold_defs = unfold_sets o unfold_maps;
+ val expand_preds = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
+ pred_unfolds);
+ val unfold_maps = fold (unfold_defs lthy o single) map_unfolds;
+ val unfold_sets = fold (unfold_defs lthy) set_unfoldss;
+ val unfold_preds = unfold_defs lthy pred_unfolds;
+ val unfold_rels = unfold_defs lthy rel_unfolds;
+ val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels;
val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
val bnf_sets = map (expand_maps o expand_sets)
(mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
val bnf_bd = mk_bd_of_bnf Ds As bnf;
- val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf);
+ val bnf_pred = expand_preds (mk_pred_of_bnf Ds As Bs bnf);
val T = mk_T_of_bnf Ds As bnf;
(*bd should only depend on dead type variables!*)
@@ -655,22 +668,24 @@
@{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2},
bd_Card_order_of_bnf bnf]];
- fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN'
+ fun mk_tac thm {context = ctxt, prems = _} =
+ (rtac (unfold_all thm) THEN'
SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
(mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
- (mk_tac (map_wpull_of_bnf bnf)) (mk_tac (rel_O_Gr_of_bnf bnf));
+ (mk_tac (map_wpull_of_bnf bnf))
+ (mk_tac (unfold_defs lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
- fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
+ fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
val policy = user_policy Derive_All_Facts;
val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
- (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
+ (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_pred) lthy;
in
((bnf', deads), lthy')
end;
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Thu Sep 20 02:42:49 2012 +0200
@@ -35,6 +35,7 @@
val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic
val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
+ val mk_simple_rel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic
val mk_simple_wit_tac: thm list -> tactic
end;
@@ -65,8 +66,8 @@
(* Composition *)
fun mk_comp_set_alt_tac ctxt collect_set_natural =
- Local_Defs.unfold_tac ctxt @{thms sym[OF o_assoc]} THEN
- Local_Defs.unfold_tac ctxt [collect_set_natural RS sym] THEN
+ unfold_defs_tac ctxt @{thms sym[OF o_assoc]} THEN
+ unfold_defs_tac ctxt [collect_set_natural RS sym] THEN
rtac refl 1;
fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
@@ -139,10 +140,9 @@
rtac bd;
fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
in
- Local_Defs.unfold_tac ctxt [comp_set_alt] THEN
+ unfold_defs_tac ctxt [comp_set_alt] THEN
rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
- Local_Defs.unfold_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib
- o_apply} THEN
+ unfold_defs_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
(rtac ctrans THEN'
WRAP' gen_before gen_after bds (rtac last_bd) THEN'
rtac @{thm ordIso_imp_ordLeq} THEN'
@@ -154,12 +154,12 @@
conj_assoc};
fun mk_comp_in_alt_tac ctxt comp_set_alts =
- Local_Defs.unfold_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
- Local_Defs.unfold_tac ctxt @{thms set_eq_subset} THEN
+ unfold_defs_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
+ unfold_defs_tac ctxt @{thms set_eq_subset} THEN
rtac conjI 1 THEN
REPEAT_DETERM (
rtac @{thm subsetI} 1 THEN
- Local_Defs.unfold_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
+ unfold_defs_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
(REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
REPEAT_DETERM (CHANGED ((
(rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE'
@@ -216,7 +216,7 @@
fun mk_comp_wit_tac ctxt Gwit_thms collect_set_natural Fwit_thms =
ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
- Local_Defs.unfold_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
+ unfold_defs_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
REPEAT_DETERM (
atac 1 ORELSE
REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
@@ -409,6 +409,10 @@
WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
+fun mk_simple_rel_O_Gr_tac ctxt rel_def rel_O_Gr in_alt_thm =
+ rtac (unfold_defs ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
+ 1;
+
fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
end;
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Sep 20 02:42:49 2012 +0200
@@ -98,6 +98,7 @@
struct
open BNF_Util
+open BNF_Tactics
open BNF_Def_Tactics
type axioms = {
@@ -140,22 +141,20 @@
fun dest_axioms {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
in_bd, map_wpull, rel_O_Gr} =
zip_axioms map_id map_comp map_cong set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
- rel_O_Gr;
+ rel_O_Gr;
-fun map_axioms f
- {map_id = map_id, map_comp = map_comp, map_cong = map_cong, set_natural = set_natural,
- bd_card_order = bd_card_order, bd_cinfinite = bd_cinfinite, set_bd = set_bd, in_bd = in_bd,
- map_wpull = map_wpull, rel_O_Gr} =
+fun map_axioms f {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
+ in_bd, map_wpull, rel_O_Gr} =
{map_id = f map_id,
- map_comp = f map_comp,
- map_cong = f map_cong,
- set_natural = map f set_natural,
- bd_card_order = f bd_card_order,
- bd_cinfinite = f bd_cinfinite,
- set_bd = map f set_bd,
- in_bd = f in_bd,
- map_wpull = f map_wpull,
- rel_O_Gr = f rel_O_Gr};
+ map_comp = f map_comp,
+ map_cong = f map_cong,
+ set_natural = map f set_natural,
+ bd_card_order = f bd_card_order,
+ bd_cinfinite = f bd_cinfinite,
+ set_bd = map f set_bd,
+ in_bd = f in_bd,
+ map_wpull = f map_wpull,
+ rel_O_Gr = f rel_O_Gr};
val morph_axioms = map_axioms o Morphism.thm;
@@ -168,8 +167,8 @@
fun mk_defs map sets pred rel = {map_def = map, set_defs = sets, pred_def = pred, rel_def = rel};
-fun map_defs f {map_def = map, set_defs = sets, pred_def = pred, rel_def = rel} =
- {map_def = f map, set_defs = List.map f sets, pred_def = f pred, rel_def = f rel};
+fun map_defs f {map_def, set_defs, pred_def, rel_def} =
+ {map_def = f map_def, set_defs = map f set_defs, pred_def = f pred_def, rel_def = f rel_def};
val morph_defs = map_defs o Morphism.thm;
@@ -429,8 +428,8 @@
let
val thy = Proof_Context.theory_of ctxt;
val tyenv =
- Sign.typ_match thy (fastype_of pred,
- Library.foldr (op -->) (instTs, instA --> instB --> HOLogic.boolT)) Vartab.empty;
+ Sign.typ_match thy (fastype_of pred, Library.foldr (op -->) (instTs, mk_pred2T instA instB))
+ Vartab.empty;
in Envir.subst_term (tyenv, Vartab.empty) pred end
handle Type.TYPE_MATCH => error "Bad predicator";
@@ -464,8 +463,6 @@
else minimize ((I, wit) :: done) todo;
in minimize [] wits end;
-fun unfold_defs_tac lthy defs mk_tac context = Local_Defs.unfold_tac lthy defs THEN mk_tac context;
-
(* Names *)
@@ -527,7 +524,7 @@
(* Define new BNFs *)
fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt
- (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
+ (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_pred_opt) no_defs_lthy =
let
val fact_policy = mk_fact_policy no_defs_lthy;
val b = qualify raw_b;
@@ -553,10 +550,10 @@
| T => err T)
else (b, Local_Theory.full_name no_defs_lthy b);
- fun maybe_define needed_for_extra_facts (b, rhs) lthy =
+ fun maybe_define user_specified (b, rhs) lthy =
let
val inline =
- (not needed_for_extra_facts orelse fact_policy = Derive_Few_Facts) andalso
+ (user_specified orelse fact_policy = Derive_Few_Facts) andalso
(case const_policy of
Dont_Inline => false
| Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
@@ -593,10 +590,10 @@
(bnf_bd_term, raw_bd_def)),
(bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
no_defs_lthy
- |> maybe_define false map_bind_def
- ||>> apfst split_list o fold_map (maybe_define false) set_binds_defs
- ||>> maybe_define false bd_bind_def
- ||>> apfst split_list o fold_map (maybe_define false) wit_binds_defs
+ |> maybe_define true map_bind_def
+ ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs
+ ||>> maybe_define true bd_bind_def
+ ||>> apfst split_list o fold_map (maybe_define true) wit_binds_defs
||> `(maybe_restore no_defs_lthy);
val phi = Proof_Context.export_morphism lthy_old lthy;
@@ -662,12 +659,13 @@
val setRTsBsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (Bs' ~~ Cs);
val setRT's = map (HOLogic.mk_setT o HOLogic.mk_prodT) (Bs' ~~ As');
val self_setRTs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ As');
- val QTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) As' Bs';
+ val QTs = map2 mk_pred2T As' Bs';
val CA' = mk_bnf_T As' CA;
val CB' = mk_bnf_T Bs' CA;
val CC' = mk_bnf_T Cs CA;
val CRs' = mk_bnf_T RTs CA;
+ val CA'CB' = HOLogic.mk_prodT (CA', CB');
val bnf_map_AsAs = mk_bnf_map As' As';
val bnf_map_AsBs = mk_bnf_map As' Bs';
@@ -678,13 +676,14 @@
val bnf_bd_As = mk_bnf_t As' bnf_bd;
val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
- val ((((((((((((((((((((((((fs, fs_copy), gs), hs), (x, x')), (y, y')), (z, z')), zs), As),
+ val (((((((((((((((((((((((((fs, fs_copy), gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As),
As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
(Qs, Qs')), _) = 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)
||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts)
+ ||>> yield_singleton (mk_Frees "p") CA'CB'
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "x") CA'
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "y") CB'
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs'
@@ -707,7 +706,7 @@
||>> mk_Frees' "Q" QTs;
(*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
- val rel_O_Gr_rhs =
+ val O_Gr =
let
val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
@@ -716,9 +715,39 @@
mk_rel_comp (mk_converse (mk_Gr bnf_in map1), mk_Gr bnf_in map2)
end;
- val rel_rhs = (case raw_rel_opt of
- NONE => fold_rev Term.absfree Rs' rel_O_Gr_rhs
- | SOME raw_rel => prep_term no_defs_lthy raw_rel);
+ fun mk_predicate_of_set x_name y_name t =
+ let
+ val (T, U) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of t));
+ val x = Free (x_name, T);
+ val y = Free (y_name, U);
+ in fold_rev Term.lambda [x, y] (HOLogic.mk_mem (HOLogic.mk_prod (x, y), t)) end;
+
+ val pred_rhs = (case raw_pred_opt of
+ NONE =>
+ fold_rev absfree Qs' (mk_predicate_of_set (fst x') (fst y')
+ (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, map3 (fn Q => fn T => fn U =>
+ HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs')))
+ | SOME raw_pred => prep_term no_defs_lthy raw_pred);
+
+ val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs);
+
+ val ((bnf_pred_term, raw_pred_def), (lthy, lthy_old)) =
+ lthy
+ |> maybe_define (is_some raw_pred_opt) pred_bind_def
+ ||> `(maybe_restore lthy);
+
+ val phi = Proof_Context.export_morphism lthy_old lthy;
+ val bnf_pred_def = Morphism.thm phi raw_pred_def;
+ val bnf_pred = Morphism.term phi bnf_pred_term;
+
+ fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy QTs CA' CB' bnf_pred;
+
+ val pred = mk_bnf_pred QTs CA' CB';
+
+ val rel_rhs =
+ fold_rev Term.absfree Rs' (HOLogic.Collect_const CA'CB' $
+ Term.lambda p (Term.list_comb (pred, map (mk_predicate_of_set (fst x') (fst y')) Rs) $
+ HOLogic.mk_fst p $ HOLogic.mk_snd p));
val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
@@ -735,25 +764,6 @@
val rel = mk_bnf_rel setRTs CA' CB';
- val pred_rhs = fold absfree (y' :: x' :: rev Qs') (HOLogic.mk_mem (HOLogic.mk_prod (x, y),
- Term.list_comb (rel, map3 (fn Q => fn T => fn U =>
- HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q)
- Qs As' Bs')));
- val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs);
-
- val ((bnf_pred_term, raw_pred_def), (lthy, lthy_old)) =
- lthy
- |> maybe_define true pred_bind_def
- ||> `(maybe_restore lthy);
-
- val phi = Proof_Context.export_morphism lthy_old lthy;
- val bnf_pred_def = Morphism.thm phi raw_pred_def;
- val bnf_pred = Morphism.term phi bnf_pred_term;
-
- fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy QTs CA' CB' bnf_pred;
-
- val pred = mk_bnf_pred QTs CA' CB';
-
val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @
raw_wit_defs @ [raw_pred_def, raw_rel_def]) of
[] => ()
@@ -852,8 +862,7 @@
(Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull))
end;
- val rel_O_Gr_goal =
- fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), rel_O_Gr_rhs));
+ val rel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), O_Gr));
val goals = zip_axioms map_id_goal map_comp_goal map_cong_goal set_naturals_goal
card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_O_Gr_goal;
@@ -1176,11 +1185,11 @@
| mk_conjunction_balanced' ts = Logic.mk_conjunction_balanced ts;
fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
- (fn (_, goals, wit_goalss, after_qed, lthy, defs) =>
+ (fn (_, goals, wit_goalss, after_qed, lthy, one_step_defs) =>
let
val wits_tac =
K (TRYALL Goal.conjunction_tac) THEN' K (TRYALL (rtac TrueI)) THEN'
- unfold_defs_tac lthy defs wit_tac;
+ mk_unfold_defs_then_tac lthy one_step_defs wit_tac;
val wit_goals = map mk_conjunction_balanced' wit_goalss;
val wit_thms =
Skip_Proof.prove lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac
@@ -1189,7 +1198,7 @@
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
in
map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
- goals (map (unfold_defs_tac lthy defs) tacs)
+ goals (map (mk_unfold_defs_then_tac lthy one_step_defs) tacs)
|> (fn thms => after_qed (map single thms @ wit_thms) lthy)
end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Thu Sep 20 02:42:49 2012 +0200
@@ -71,8 +71,8 @@
val n = length set_naturals;
in
if null set_naturals then
- Local_Defs.unfold_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
- else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+ unfold_defs_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+ else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac subsetI,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
@@ -105,7 +105,7 @@
end;
fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
+ unfold_defs_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
subst_tac ctxt [map_id] 1 THEN
(if n = 0 then rtac refl 1
else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
@@ -113,7 +113,7 @@
CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt rel_O_Grs THEN
+ unfold_defs_tac ctxt rel_O_Grs THEN
EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
@@ -124,8 +124,8 @@
val n = length set_naturals;
in
if null set_naturals then
- Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
- else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+ unfold_defs_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
+ else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
@@ -151,8 +151,8 @@
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
in
- if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
- else Local_Defs.unfold_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+ if null set_naturals then unfold_defs_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
+ else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
@@ -197,7 +197,7 @@
let
val ls' = replicate (Int.max (1, m)) ();
in
- Local_Defs.unfold_tac ctxt (rel_O_Grs @
+ unfold_defs_tac ctxt (rel_O_Grs @
@{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
--- a/src/HOL/Codatatype/Tools/bnf_fp.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Thu Sep 20 02:42:49 2012 +0200
@@ -97,8 +97,6 @@
val retype_free: typ -> term -> term
- val mk_predT: typ -> typ;
-
val mk_sumTN: typ list -> typ
val mk_sumTN_balanced: typ list -> typ
@@ -245,8 +243,6 @@
val mk_common_name = space_implode "_" o map Binding.name_of;
-fun mk_predT T = T --> HOLogic.boolT;
-
fun retype_free T (Free (s, _)) = Free (s, T);
fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 02:42:49 2012 +0200
@@ -261,7 +261,7 @@
(*avoid "'a itself" arguments in coiterators and corecursors*)
val mss' = map (fn [0] => [1] | ms => ms) mss;
- val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_predT) ns Cs;
+ val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
fun zip_predss_getterss qss fss = maps (op @) (qss ~~ fss);
@@ -277,7 +277,7 @@
map3 (fn C => map2 (map (map (curry (op -->) C) o maybe_dest_sumT) oo dest_tupleT))
Cs mss' f_prod_Tss;
val q_Tssss =
- map (map (map (fn [_] => [] | [_, C] => [mk_predT (domain_type C)]))) f_Tssss;
+ map (map (map (fn [_] => [] | [_, C] => [mk_pred1T (domain_type C)]))) f_Tssss;
val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end;
@@ -383,7 +383,7 @@
end;
val sumEN_thm' =
- Local_Defs.unfold lthy @{thms all_unit_eq}
+ unfold_defs lthy @{thms all_unit_eq}
(Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
(mk_sumEN_balanced n))
|> Morphism.thm phi;
@@ -521,7 +521,7 @@
val (((phis, phis'), vs'), names_lthy) =
lthy
- |> mk_Frees' "P" (map mk_predT fpTs)
+ |> mk_Frees' "P" (map mk_pred1T fpTs)
||>> Variable.variant_fixes (map Binding.name_of fp_bs);
val vs = map2 (curry Free) vs' fpTs;
@@ -756,7 +756,7 @@
coiterss_goal coiter_tacss,
map2 (map2 (fn goal => fn tac =>
Skip_Proof.prove lthy [] [] goal (tac o #context)
- |> Local_Defs.unfold lthy @{thms sum_case_if} |> Thm.close_derivation))
+ |> unfold_defs lthy @{thms sum_case_if} |> Thm.close_derivation))
corecss_goal corec_tacss)
end;
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Thu Sep 20 02:42:49 2012 +0200
@@ -43,14 +43,14 @@
val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
- Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
+ unfold_defs_tac ctxt [case_def, ctr_def, unf_fld] THEN
(rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
rtac refl) 1;
fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' =
- Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
- Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
+ unfold_defs_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
+ unfold_defs_tac ctxt @{thms all_prod_eq} THEN
EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec,
etac meta_mp, atac]) (1 upto n)) 1;
@@ -58,33 +58,33 @@
(rtac iffI THEN'
EVERY' (map3 (fn cTs => fn cx => fn th =>
dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
+ SELECT_GOAL (unfold_defs_tac ctxt [th]) THEN'
atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
fun mk_half_distinct_tac ctxt fld_inject ctr_defs =
- Local_Defs.unfold_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN
+ unfold_defs_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN
rtac @{thm sum.distinct(1)} 1;
fun mk_inject_tac ctxt ctr_def fld_inject =
- Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
- Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
+ unfold_defs_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
+ unfold_defs_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
val iter_like_thms =
@{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
split_conv};
fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt =
- Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
- iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
+ unfold_defs_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
+ iter_like_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1;
val coiter_like_ss = ss_only @{thms if_True if_False};
val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
- Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
+ unfold_defs_tac ctxt (ctr_def :: coiter_like_defs) THEN
subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
- Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
- Local_Defs.unfold_tac ctxt @{thms id_def} THEN
+ unfold_defs_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
+ unfold_defs_tac ctxt @{thms id_def} THEN
TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
val solve_prem_prem_tac =
@@ -99,7 +99,7 @@
fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
- SELECT_GOAL (Local_Defs.unfold_tac ctxt
+ SELECT_GOAL (unfold_defs_tac ctxt
(pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
solve_prem_prem_tac]) (rev kks)) 1;
@@ -118,7 +118,7 @@
val nn = length ns;
val n = Integer.sum ns;
in
- Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
+ unfold_defs_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
pre_set_defss mss (unflat mss (1 upto n)) kkss)
end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Sep 20 02:42:49 2012 +0200
@@ -220,9 +220,9 @@
val map_comp's = map map_comp'_of_bnf bnfs;
val map_congs = map map_cong_of_bnf bnfs;
val map_id's = map map_id'_of_bnf bnfs;
- val pred_defs = map pred_def_of_bnf bnfs;
val rel_congs = map rel_cong_of_bnf bnfs;
val rel_converses = map rel_converse_of_bnf bnfs;
+ val rel_defs = map rel_def_of_bnf bnfs;
val rel_Grs = map rel_Gr_of_bnf bnfs;
val rel_Ids = map rel_Id_of_bnf bnfs;
val rel_monos = map rel_mono_of_bnf bnfs;
@@ -1060,9 +1060,9 @@
val sum_card_order = mk_sum_card_order bd_card_orders;
- val sbd_ordIso = Local_Defs.fold lthy [sbd_def]
+ val sbd_ordIso = fold_defs lthy [sbd_def]
(@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order]);
- val sbd_card_order = Local_Defs.fold lthy [sbd_def]
+ val sbd_card_order = fold_defs lthy [sbd_def]
(@{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]);
val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero};
@@ -1873,7 +1873,7 @@
||>> mk_Frees "f" coiter_fTs
||>> mk_Frees "g" coiter_fTs
||>> mk_Frees "s" corec_sTs
- ||>> mk_Frees "P" (map (fn T => T --> mk_predT T) Ts);
+ ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1));
val unf_name = Binding.name_of o unf_bind;
@@ -2070,7 +2070,7 @@
val flds = mk_flds params';
val fld_defs = map (Morphism.thm phi) fld_def_frees;
- val fld_o_unf_thms = map2 (Local_Defs.fold lthy o single) fld_defs coiter_o_unf_thms;
+ val fld_o_unf_thms = map2 (fold_defs lthy o single) fld_defs coiter_o_unf_thms;
val unf_o_fld_thms =
let
@@ -2213,7 +2213,7 @@
val rel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
val coinduct_params = rev (Term.add_tfrees rel_coinduct_goal []);
- val rel_coinduct = Local_Defs.unfold lthy @{thms diag_UNIV}
+ val rel_coinduct = unfold_defs lthy @{thms diag_UNIV}
(Skip_Proof.prove lthy [] [] rel_coinduct_goal
(K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm))
|> Thm.close_derivation);
@@ -2266,12 +2266,12 @@
(tcoalg_thm RS bis_diag_thm))))
|> Thm.close_derivation;
- val pred_coinduct = rel_coinduct
- |> Local_Defs.unfold lthy @{thms Id_def'}
- |> Local_Defs.fold lthy pred_defs;
- val pred_coinduct_upto = rel_coinduct_upto
- |> Local_Defs.unfold lthy @{thms Id_def'}
- |> Local_Defs.fold lthy pred_defs;
+ (*### FIXME: get rid of mem_Id_eq_eq? or Id_def'? *)
+ val pred_of_rel_thms =
+ rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv mem_Id_eq_eq snd_conv split_conv};
+
+ val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct;
+ val pred_coinduct_upto = unfold_defs lthy pred_of_rel_thms rel_coinduct_upto;
in
(unf_coinduct, rev (Term.add_tfrees unf_coinduct_goal []), rel_coinduct, pred_coinduct,
unf_coinduct_upto, rel_coinduct_upto, pred_coinduct_upto)
@@ -2291,7 +2291,7 @@
val pTs = map2 (curry op -->) passiveXs passiveCs;
val uTs = map2 (curry op -->) Ts Ts';
val JRTs = map2 (curry mk_relT) passiveAs passiveBs;
- val JphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs;
+ val JphiTs = map2 mk_pred2T passiveAs passiveBs;
val prodTs = map2 (curry HOLogic.mk_prodT) Ts Ts';
val B1Ts = map HOLogic.mk_setT passiveAs;
val B2Ts = map HOLogic.mk_setT passiveBs;
@@ -2309,7 +2309,7 @@
||>> mk_Frees "u" uTs
||>> mk_Frees' "b" Ts'
||>> mk_Frees' "b" Ts'
- ||>> mk_Freess "P" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs)
+ ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs)
||>> mk_Frees "R" JRTs
||>> mk_Frees "P" JphiTs
||>> mk_Frees "B1" B1Ts
@@ -2669,10 +2669,10 @@
map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm
mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss;
- val rel_O_gr_tacs = replicate n (K (rtac refl 1));
+ val rel_O_Gr_tacs = replicate n (simple_rel_O_Gr_tac o #context);
val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_gr_tacs;
+ bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs;
val (hset_unf_incl_thmss, hset_hset_unf_incl_thmsss, hset_induct_thms) =
let
@@ -2714,7 +2714,7 @@
map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
((set_minimal
|> Drule.instantiate' [] (mk_induct_tinst phis jsets y y')
- |> Local_Defs.unfold lthy incls) OF
+ |> unfold_defs lthy incls) OF
(replicate n ballI @
maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
|> singleton (Proof_Context.export names_lthy lthy)
@@ -2865,10 +2865,10 @@
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
- val fold_maps = Local_Defs.fold lthy (map (fn bnf =>
+ val fold_maps = fold_defs lthy (map (fn bnf =>
mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Jbnfs);
- val fold_sets = Local_Defs.fold lthy (maps (fn bnf =>
+ val fold_sets = fold_defs lthy (maps (fn bnf =>
map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Jbnfs);
val timer = time (timer "registered new codatatypes as BNFs");
@@ -2889,6 +2889,7 @@
val in_rels = map in_rel_of_bnf bnfs;
val in_Jrels = map in_rel_of_bnf Jbnfs;
+ val Jrel_defs = map rel_def_of_bnf Jbnfs;
val Jpred_defs = map pred_def_of_bnf Jbnfs;
val folded_map_simp_thms = map fold_maps map_simp_thms;
@@ -2919,10 +2920,11 @@
(mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz')));
val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis;
in
- map3 (fn goal => fn pred_def => fn Jrel_simp =>
- Skip_Proof.prove lthy [] [] goal (mk_pred_simp_tac pred_def Jpred_defs Jrel_simp)
+ map3 (fn goal => fn rel_def => fn Jrel_simp =>
+ Skip_Proof.prove lthy [] [] goal
+ (mk_pred_simp_tac rel_def Jpred_defs Jrel_defs Jrel_simp)
|> Thm.close_derivation)
- goals pred_defs Jrel_simp_thms
+ goals rel_defs Jrel_simp_thms
end;
val timer = time (timer "additional properties");
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Sep 20 02:42:49 2012 +0200
@@ -350,7 +350,7 @@
fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins
{context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
+ unfold_defs_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
CONJ_WRAP' (fn (coalg_in, morE) =>
@@ -363,7 +363,7 @@
val n = length in_monos;
val ks = 1 upto n;
in
- Local_Defs.unfold_tac ctxt [bis_def] THEN
+ unfold_defs_tac ctxt [bis_def] THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn i =>
EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
@@ -426,7 +426,7 @@
rtac conjI, etac @{thm Shift_prefCl},
rtac conjI, rtac ballI,
rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
- SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Succ_Shift shift_def}),
+ SELECT_GOAL (unfold_defs_tac ctxt @{thms Succ_Shift shift_def}),
etac bspec, etac @{thm ShiftD},
CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),
@@ -450,7 +450,7 @@
rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
in
- Local_Defs.unfold_tac ctxt defs THEN
+ unfold_defs_tac ctxt defs THEN
CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1
end;
@@ -603,7 +603,7 @@
val m = length strT_hsets;
in
if m = 0 then atac 1
- else (Local_Defs.unfold_tac ctxt [isNode_def] THEN
+ else (unfold_defs_tac ctxt [isNode_def] THEN
EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
rtac exI, rtac conjI, atac,
CONJ_WRAP' (fn (thm, i) => if i > m then atac
@@ -992,7 +992,7 @@
(K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
if n = 1 then K all_tac
else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [from_to_sbd]), rtac refl,
+ SELECT_GOAL (unfold_defs_tac ctxt [from_to_sbd]), rtac refl,
rtac refl])
ks to_sbd_injs from_to_sbds)];
in
@@ -1049,7 +1049,7 @@
fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
{context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt defs THEN
+ unfold_defs_tac ctxt defs THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
@@ -1061,7 +1061,7 @@
(Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt defs THEN
+ unfold_defs_tac ctxt defs THEN
EVERY' [rtac conjI,
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
@@ -1116,14 +1116,14 @@
fun mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unfs
{context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt [fld_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
+ unfold_defs_tac ctxt [fld_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
rtac trans, rtac coiter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
EVERY' (map (fn thm =>
rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_unfs),
rtac sym, rtac @{thm id_apply}] 1;
fun mk_corec_tac m corec_defs coiter map_cong corec_Inls {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
+ unfold_defs_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
rtac trans, rtac coiter, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
REPEAT_DETERM_N m o rtac refl,
EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
@@ -1262,7 +1262,7 @@
fun mk_map_unique_tac coiter_unique map_comps {context = ctxt, prems = _} =
rtac coiter_unique 1 THEN
- Local_Defs.unfold_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
+ unfold_defs_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
ALLGOALS (etac sym);
fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
@@ -1271,11 +1271,11 @@
val n = length map_simps;
in
EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
- REPEAT_DETERM o rtac allI, SELECT_GOAL (Local_Defs.unfold_tac ctxt rec_0s),
+ REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_defs_tac ctxt rec_0s),
CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
REPEAT_DETERM o rtac allI,
CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
- [SELECT_GOAL (Local_Defs.unfold_tac ctxt
+ [SELECT_GOAL (unfold_defs_tac ctxt
(rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
rtac @{thm Un_cong}, rtac refl,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
@@ -1372,14 +1372,14 @@
fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs
{context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt [coalg_def] THEN
+ unfold_defs_tac ctxt [coalg_def] THEN
CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) =>
EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
pickWP_assms_tac,
- SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms o_apply prod.cases}), rtac impI,
+ SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI,
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}),
@@ -1394,16 +1394,16 @@
let
val n = length map_comps;
in
- Local_Defs.unfold_tac ctxt [mor_def] THEN
+ unfold_defs_tac ctxt [mor_def] THEN
EVERY' [rtac conjI,
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
hyp_subst_tac,
- SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms o_apply prod.cases}),
+ SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}),
rtac (map_comp RS trans),
- SELECT_GOAL (Local_Defs.unfold_tac ctxt (conv :: @{thms o_id id_o})),
+ SELECT_GOAL (unfold_defs_tac ctxt (conv :: @{thms o_id id_o})),
rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
pickWP_assms_tac])
(map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
@@ -1413,12 +1413,12 @@
val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
fun mk_mor_thePull_pick_tac mor_def coiters map_comps {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
+ unfold_defs_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) coiters 1 THEN
CONJ_WRAP' (fn (coiter, map_comp) =>
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
hyp_subst_tac,
- SELECT_GOAL (Local_Defs.unfold_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})),
+ SELECT_GOAL (unfold_defs_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})),
rtac refl])
(coiters ~~ map_comps) 1;
@@ -1442,12 +1442,12 @@
rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac ord_eq_le_trans, rtac rec_Suc,
rtac @{thm Un_least},
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, nth set_naturals (j - 1),
+ SELECT_GOAL (unfold_defs_tac ctxt [coiter, nth set_naturals (j - 1),
@{thm prod.cases}]),
etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
EVERY' [rtac @{thm UN_least},
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, set_natural, @{thm prod.cases}]),
+ SELECT_GOAL (unfold_defs_tac ctxt [coiter, set_natural, @{thm prod.cases}]),
etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
(ks ~~ rev (drop m set_naturals))])
@@ -1482,7 +1482,7 @@
ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
REPEAT_DETERM (atac 1 ORELSE
EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
- K (Local_Defs.unfold_tac ctxt unf_flds),
+ K (unfold_defs_tac ctxt unf_flds),
REPEAT_DETERM_N n o etac UnE,
REPEAT_DETERM o
(TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
@@ -1490,11 +1490,11 @@
(dresolve_tac wit THEN'
(etac FalseE ORELSE'
EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
- K (Local_Defs.unfold_tac ctxt unf_flds), REPEAT_DETERM_N n o etac UnE]))))] 1);
+ K (unfold_defs_tac ctxt unf_flds), REPEAT_DETERM_N n o etac UnE]))))] 1);
fun mk_coind_wit_tac induct coiters set_nats wits {context = ctxt, prems = _} =
rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
- Local_Defs.unfold_tac ctxt (coiters @ set_nats @ @{thms image_id id_apply}) THEN
+ unfold_defs_tac ctxt (coiters @ set_nats @ @{thms image_id id_apply}) THEN
ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Sep 20 02:42:49 2012 +0200
@@ -794,7 +794,7 @@
||>> mk_Frees' "x" init_FTs
||>> mk_Frees "f" init_fTs
||>> mk_Frees "f" init_fTs
- ||>> mk_Frees "P" (replicate n (mk_predT initT));
+ ||>> mk_Frees "P" (replicate n (mk_pred1T initT));
val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
(HOLogic.mk_conj (HOLogic.mk_eq (iidx,
@@ -991,8 +991,8 @@
||>> mk_Frees "s" rec_sTs;
val Izs = map2 retype_free Ts zs;
- val phis = map2 retype_free (map mk_predT Ts) init_phis;
- val phi2s = map2 retype_free (map2 (fn T => fn T' => T --> mk_predT T') Ts Ts') init_phis;
+ val phis = map2 retype_free (map mk_pred1T Ts) init_phis;
+ val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis;
fun fld_bind i = Binding.suffix_name ("_" ^ fldN) (nth bs (i - 1));
val fld_name = Binding.name_of o fld_bind;
@@ -1167,7 +1167,7 @@
val unfs = mk_unfs params';
val unf_defs = map (Morphism.thm phi) unf_def_frees;
- val fld_o_unf_thms = map2 (Local_Defs.fold lthy o single) unf_defs fld_o_iter_thms;
+ val fld_o_unf_thms = map2 (fold_defs lthy o single) unf_defs fld_o_iter_thms;
val unf_o_fld_thms =
let
@@ -1356,7 +1356,7 @@
val XTs = mk_Ts passiveXs;
val YTs = mk_Ts passiveYs;
val IRTs = map2 (curry mk_relT) passiveAs passiveBs;
- val IphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs;
+ val IphiTs = map2 mk_pred2T passiveAs passiveBs;
val (((((((((((((((fs, fs'), fs_copy), us),
B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), IRs), Iphis),
@@ -1670,10 +1670,10 @@
in_incl_min_alg_thms card_of_min_alg_thms;
val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
- val rel_O_gr_tacs = replicate n (K (rtac refl 1));
+ val rel_O_Gr_tacs = replicate n (simple_rel_O_Gr_tac o #context);
val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_gr_tacs;
+ bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_Gr_tacs;
val fld_witss =
let
@@ -1711,10 +1711,10 @@
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
- val fold_maps = Local_Defs.fold lthy (map (fn bnf =>
+ val fold_maps = fold_defs lthy (map (fn bnf =>
mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Ibnfs);
- val fold_sets = Local_Defs.fold lthy (maps (fn bnf =>
+ val fold_sets = fold_defs lthy (maps (fn bnf =>
map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
val timer = time (timer "registered new datatypes as BNFs");
@@ -1731,7 +1731,8 @@
val in_rels = map in_rel_of_bnf bnfs;
val in_Irels = map in_rel_of_bnf Ibnfs;
- val pred_defs = map pred_def_of_bnf bnfs;
+ val rel_defs = map rel_def_of_bnf bnfs;
+ val Irel_defs = map rel_def_of_bnf Ibnfs;
val Ipred_defs = map pred_def_of_bnf Ibnfs;
val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
@@ -1764,10 +1765,11 @@
(mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF));
val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
in
- map3 (fn goal => fn pred_def => fn Irel_simp =>
- Skip_Proof.prove lthy [] [] goal (mk_pred_simp_tac pred_def Ipred_defs Irel_simp)
+ map3 (fn goal => fn rel_def => fn Irel_simp =>
+ Skip_Proof.prove lthy [] [] goal
+ (mk_pred_simp_tac rel_def Ipred_defs Irel_defs Irel_simp)
|> Thm.close_derivation)
- goals pred_defs Irel_simp_thms
+ goals rel_defs Irel_simp_thms
end;
val timer = time (timer "additional properties");
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Thu Sep 20 02:42:49 2012 +0200
@@ -390,7 +390,7 @@
fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN
- Local_Defs.unfold_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
+ unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
alg_sets set_natural's str_init_defs =
@@ -435,7 +435,7 @@
rtac mor_select THEN' atac THEN' rtac CollectI THEN'
REPEAT_DETERM o rtac exI THEN'
rtac conjI THEN' rtac refl THEN' atac THEN'
- K (Local_Defs.unfold_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
+ K (unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
etac mor_comp THEN' etac mor_incl_min_alg) 1
end;
@@ -490,7 +490,7 @@
end;
fun mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} =
- (K (Local_Defs.unfold_tac ctxt fld_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
+ (K (unfold_defs_tac ctxt fld_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
EVERY' (map rtac inver_Abss) THEN'
EVERY' (map rtac inver_Reps)) 1;
@@ -526,7 +526,7 @@
rtac sym, rtac id_apply] 1;
fun mk_rec_tac rec_defs iter fst_recs {context = ctxt, prems = _}=
- Local_Defs.unfold_tac ctxt
+ unfold_defs_tac ctxt
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iter RS @{thm arg_cong[of _ _ snd]}),
rtac @{thm snd_convol'}] 1;
@@ -813,8 +813,7 @@
CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
- rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply,
- atac,
+ rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
(fn (active_set_natural, in_Irel) => EVERY' [rtac ord_eq_le_trans,
rtac @{thm UN_cong[OF _ refl]}, rtac active_set_natural, rtac @{thm UN_least},
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Thu Sep 20 02:42:49 2012 +0200
@@ -16,6 +16,8 @@
val subst_asm_tac: Proof.context -> thm list -> int -> tactic
val subst_tac: Proof.context -> thm list -> int -> tactic
val substs_tac: Proof.context -> thm list -> int -> tactic
+ val unfold_defs_tac: Proof.context -> thm list -> tactic
+ val mk_unfold_defs_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
@@ -24,7 +26,9 @@
val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
val mk_Abs_inj_thm: thm -> thm
- val mk_pred_simp_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val simple_rel_O_Gr_tac: Proof.context -> tactic
+ val mk_pred_simp_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
+ tactic
val mk_map_comp_id_tac: thm -> tactic
val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
@@ -53,13 +57,16 @@
rtac (Drule.instantiate_normalize insts thm) 1
end);
-(*unlike "unfold_tac", succeeds when the RHS contains schematic variables not in the LHS*)
+fun unfold_defs_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
+
+fun mk_unfold_defs_then_tac lthy defs tac x = unfold_defs_tac lthy defs THEN tac x;
+
+(*unlike "unfold_defs_tac", succeeds when the RHS contains schematic variables not in the LHS*)
fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
-
(* Theorems for open typedefs with UNIV as representing set *)
fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I);
@@ -91,9 +98,17 @@
gen_tac
end;
-fun mk_pred_simp_tac pred_def pred_defs rel_simp {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN
- rtac rel_simp 1;
+fun simple_rel_O_Gr_tac ctxt =
+ unfold_defs_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
+
+fun mk_pred_simp_tac rel_def IJpred_defs IJrel_defs rel_simp {context = ctxt, prems = _} =
+ unfold_defs_tac ctxt IJpred_defs THEN
+ subst_tac ctxt [unfold_defs ctxt (IJpred_defs @ IJrel_defs @
+ @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) rel_simp] 1 THEN
+ unfold_defs_tac ctxt (rel_def ::
+ @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
+ split_conv}) THEN
+ rtac refl 1;
fun mk_map_comp_id_tac map_comp =
(rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
--- a/src/HOL/Codatatype/Tools/bnf_util.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Thu Sep 20 02:42:49 2012 +0200
@@ -62,6 +62,9 @@
val strip_typeN: int -> typ -> typ list * typ
+ val mk_predT: typ list -> typ
+ val mk_pred1T: typ -> typ
+ val mk_pred2T: typ -> typ -> typ
val mk_optionT: typ -> typ
val mk_relT: typ * typ -> typ
val dest_relT: typ -> typ * typ
@@ -122,6 +125,9 @@
val mk_trans: thm -> thm -> thm
val mk_unabs_def: int -> thm -> thm
+ val fold_defs: Proof.context -> thm list -> thm -> thm
+ val unfold_defs: Proof.context -> thm list -> thm -> thm
+
val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
val find_indices: ''a list -> ''a list -> int list
@@ -316,8 +322,11 @@
fun strip_typeN 0 T = ([], T)
| strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T
- | strip_typeN n T = raise TYPE ("strip_typeN", [T], []);
+ | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []);
+fun mk_predT Ts = Ts ---> HOLogic.boolT;
+fun mk_pred1T T = mk_predT [T];
+fun mk_pred2T T U = mk_predT [T, U];
fun mk_optionT T = Type (@{type_name option}, [T]);
val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT;
val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT;
@@ -583,4 +592,7 @@
fun mk_unabs_def 0 thm = thm
| mk_unabs_def n thm = mk_unabs_def (n - 1) thm RS @{thm spec[OF iffD1[OF fun_eq_iff]]};
+fun fold_defs ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
+fun unfold_defs ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
+
end;
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Thu Sep 20 02:42:49 2012 +0200
@@ -166,7 +166,7 @@
||>> yield_singleton (mk_Frees "w") dataT
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
- val q = Free (fst p', B --> HOLogic.boolT);
+ val q = Free (fst p', mk_pred1T B);
fun ap_v t = t $ v;
fun mk_v_eq_v () = HOLogic.mk_eq (v, v);
@@ -200,7 +200,7 @@
(true, [], [], [], [], [], no_defs_lthy)
else
let
- fun disc_free b = Free (Binding.name_of b, dataT --> HOLogic.boolT);
+ fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT);
fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr);
@@ -417,7 +417,7 @@
disc_defs';
val not_discI_thms =
map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
- (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
+ (unfold_defs lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
ms disc_defs';
val (disc_thmss', disc_thmss) =
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Thu Sep 20 02:42:49 2012 +0200
@@ -38,7 +38,7 @@
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct exhaust' =
EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
- hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
+ hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
rtac distinct, rtac exhaust'] @
(([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
|> k = 1 ? swap |> op @)) 1;
@@ -64,13 +64,13 @@
else
REPEAT_DETERM_N m o etac exE THEN'
hyp_subst_tac THEN'
- SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
+ SELECT_GOAL (unfold_defs_tac ctxt sel_thms) THEN'
rtac refl)) 1;
fun mk_case_eq_tac ctxt n exhaust' case_thms disc_thmss' sel_thmss =
(rtac exhaust' THEN'
EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms =>
- EVERY' [hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)),
+ EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_disc_thms @ sel_thms)),
rtac case_thm])
case_thms (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) disc_thmss') sel_thmss)) 1;
@@ -90,6 +90,6 @@
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
fun mk_split_asm_tac ctxt split =
- rtac (split RS trans) 1 THEN Local_Defs.unfold_tac ctxt split_asm_thms THEN rtac refl 1;
+ rtac (split RS trans) 1 THEN unfold_defs_tac ctxt split_asm_thms THEN rtac refl 1;
end;