--- a/src/HOL/BNF/BNF_Comp.thy Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/BNF_Comp.thy Tue May 07 14:22:54 2013 +0200
@@ -73,6 +73,12 @@
lemma O_Gr_cong: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
by simp
+lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
+unfolding Grp_def fun_eq_iff relcompp.simps by auto
+
+lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
+by simp
+
ML_file "Tools/bnf_comp_tactics.ML"
ML_file "Tools/bnf_comp.ML"
--- a/src/HOL/BNF/BNF_Def.thy Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy Tue May 07 14:22:54 2013 +0200
@@ -21,10 +21,18 @@
"R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
unfolding converse_def by auto
+lemma conversep_mono:
+"R1 ^--1 \<le> R2 ^--1 \<longleftrightarrow> R1 \<le> R2"
+unfolding conversep.simps by auto
+
lemma converse_shift:
"R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
unfolding converse_def by auto
+lemma conversep_shift:
+"R1 \<le> R2 ^--1 \<Longrightarrow> R1 ^--1 \<le> R2"
+unfolding conversep.simps by auto
+
definition convol ("<_ , _>") where
"<f , g> \<equiv> %a. (f a, g a)"
@@ -42,6 +50,10 @@
"\<lbrakk>f x = f' x; g x = g' x; P x\<rbrakk> \<Longrightarrow> <f , g> x \<in> {(f' a, g' a) |a. P a}"
unfolding convol_def by auto
+lemma convol_mem_GrpI:
+"\<lbrakk>g x = g' x; x \<in> A\<rbrakk> \<Longrightarrow> <id , g> x \<in> (Collect (split (Grp A g)))"
+unfolding convol_def Grp_def by auto
+
definition csquare where
"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
@@ -91,48 +103,111 @@
lemma Id_alt: "Id = Gr UNIV id"
unfolding Gr_def by auto
+lemma eq_alt: "op = = Grp UNIV id"
+unfolding Grp_def by auto
+
+lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1"
+ by auto
+
+lemma eq_OOI: "R = op = \<Longrightarrow> R = R OO R"
+ by auto
+
lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f"
unfolding Gr_def by auto
+lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f"
+unfolding Grp_def by auto
+
+lemma Grp_UNIV_idI: "x = y \<Longrightarrow> Grp UNIV id x y"
+unfolding Grp_def by auto
+
lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f"
unfolding Gr_def by auto
+lemma Grp_mono: "A \<le> B \<Longrightarrow> Grp A f \<le> Grp B f"
+unfolding Grp_def by auto
+
+lemma GrpI: "\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> Grp A f x y"
+unfolding Grp_def by auto
+
+lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
+unfolding Grp_def by auto
+
+lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
+unfolding Grp_def o_def by auto
+
+lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
+unfolding Grp_def o_def by auto
+
lemma wpull_Gr:
"wpull (Gr A f) A (f ` A) f id fst snd"
unfolding wpull_def Gr_def by auto
+lemma wpull_Grp:
+"wpull (Collect (split (Grp A f))) A (f ` A) f id fst snd"
+unfolding wpull_def Grp_def by auto
+
definition "pick_middle P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
+definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
+
lemma pick_middle:
"(a,c) \<in> P O Q \<Longrightarrow> (a, pick_middle P Q a c) \<in> P \<and> (pick_middle P Q a c, c) \<in> Q"
-unfolding pick_middle_def apply(rule someI_ex)
-using assms unfolding relcomp_def by auto
+unfolding pick_middle_def apply(rule someI_ex) by auto
+
+lemma pick_middlep:
+"(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c"
+unfolding pick_middlep_def apply(rule someI_ex) by auto
definition fstO where "fstO P Q ac = (fst ac, pick_middle P Q (fst ac) (snd ac))"
definition sndO where "sndO P Q ac = (pick_middle P Q (fst ac) (snd ac), snd ac)"
+definition fstOp where "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))"
+definition sndOp where "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))"
+
lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
-unfolding fstO_def
-by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct1])
+unfolding fstO_def by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct1])
+
+lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
+unfolding fstOp_def mem_Collect_eq
+by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct1])
lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
unfolding comp_def fstO_def by simp
+lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc"
+unfolding comp_def fstOp_def by simp
+
lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc"
unfolding comp_def sndO_def by simp
+lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc"
+unfolding comp_def sndOp_def by simp
+
lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
unfolding sndO_def
by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct2])
+lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
+unfolding sndOp_def mem_Collect_eq
+by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct2])
+
lemma csquare_fstO_sndO:
"csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
unfolding csquare_def fstO_def sndO_def using pick_middle by simp
+lemma csquare_fstOp_sndOp:
+"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
+unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
+
lemma wppull_fstO_sndO:
shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
using pick_middle unfolding wppull_def fstO_def sndO_def relcomp_def by auto
+lemma wppull_fstOp_sndOp:
+shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q)) snd fst fst snd (fstOp P Q) (sndOp P Q)"
+using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto
+
lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
by (simp split: prod.split)
@@ -142,11 +217,17 @@
lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R"
by auto
+lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
+by auto
+
lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
unfolding o_def fun_eq_iff by simp
-lemma eqset_imp_iff_pair: "A = B \<Longrightarrow> (a, b) \<in> A \<longleftrightarrow> (a, b) \<in> B"
-by (rule eqset_imp_iff)
+lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
+ by auto
+
+lemma predicate2_cong: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
+by metis
lemma fun_cong_pair: "f = g \<Longrightarrow> f {(a, b). R a b} = g {(a, b). R a b}"
by (rule fun_cong)
@@ -161,4 +242,5 @@
ML_file "Tools/bnf_def_tactics.ML"
ML_file "Tools/bnf_def.ML"
+
end
--- a/src/HOL/BNF/BNF_GFP.thy Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy Tue May 07 14:22:54 2013 +0200
@@ -79,6 +79,9 @@
lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}"
by auto
+lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
+by auto
+
lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
by auto
@@ -100,6 +103,36 @@
lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
unfolding Gr_def by auto
+lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
+unfolding fun_eq_iff by auto
+
+lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
+by auto
+
+lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
+by force
+
+lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
+by auto
+
+lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
+unfolding fun_eq_iff by auto
+
+lemmas conversep_in_rel_Id_on =
+ trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]
+
+lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
+unfolding fun_eq_iff by auto
+
+lemmas relcompp_in_rel_Id_on =
+ trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]
+
+lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
+unfolding Gr_def Grp_def fun_eq_iff by auto
+
+lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
+unfolding fun_eq_iff by auto
+
definition relImage where
"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
--- a/src/HOL/BNF/BNF_Util.thy Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/BNF_Util.thy Tue May 07 14:22:54 2013 +0200
@@ -60,6 +60,8 @@
(* Operator: *)
definition "Gr A f = {(a, f a) | a. a \<in> A}"
+definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
+
ML_file "Tools/bnf_util.ML"
ML_file "Tools/bnf_tactics.ML"
--- a/src/HOL/BNF/Basic_BNFs.thy Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Basic_BNFs.thy Tue May 07 14:22:54 2013 +0200
@@ -27,9 +27,12 @@
lemma wpull_Gr_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Gr B1 f1 O (Gr B2 f2)\<inverse> \<subseteq> (Gr A p1)\<inverse> O Gr A p2"
unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
+lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2"
+ unfolding wpull_def Grp_def by auto
+
bnf ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
- "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
-apply (auto simp: Gr_def fun_eq_iff natLeq_card_order natLeq_cinfinite)
+ "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
apply (rule ordLeq_transitive)
@@ -46,8 +49,8 @@
done
bnf 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_Gr_def Gr_def
+ "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
+apply (auto simp add: wpull_Grp_def Grp_def
card_order_csum natLeq_card_order card_of_card_order_on
cinfinite_csum natLeq_cinfinite)
apply (rule ordLess_imp_ordLeq)
@@ -185,10 +188,10 @@
qed
next
fix R S
- show "{p. sum_rel (\<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_rel_def Gr_def relcomp_unfold converse_unfold
+ show "sum_rel R S =
+ (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
+ Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
+ unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
by (fastforce split: sum.splits)
qed (auto simp: sum_set_defs)
@@ -284,10 +287,10 @@
unfolding wpull_def by simp fast
next
fix R S
- show "{p. prod_rel (\<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_rel_def Gr_def relcomp_unfold converse_unfold
+ show "prod_rel R S =
+ (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
+ Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
+ unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
by auto
qed simp+
@@ -385,10 +388,11 @@
qed
next
fix R
- show "{p. fun_rel op = (\<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_rel_def Gr_def relcomp_unfold converse_unfold
- by force
+ show "fun_rel op = R =
+ (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
+ Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
+ unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
+ by auto (force, metis pair_collapse)
qed auto
end
--- a/src/HOL/BNF/More_BNFs.thy Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Tue May 07 14:22:54 2013 +0200
@@ -83,11 +83,12 @@
thus False by simp
next
fix R
- show "{p. option_rel (\<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_unfold Gr_def relcomp_unfold converse_unfold
+ show "option_rel R =
+ (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
+ Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
+ unfolding option_rel_unfold Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
- split: option.splits) blast
+ split: option.splits)
qed
lemma card_of_list_in:
@@ -244,22 +245,22 @@
lemma fset_rel_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}} (fmap fst))\<inverse> O
- Gr {a. fset a \<subseteq> {(a, b). R a b}} (fmap snd)" (is "?L = ?R")
+ ((Grp {a. fset a \<subseteq> {(a, b). R a b}} (fmap fst))\<inverse>\<inverse> OO
+ Grp {a. fset a \<subseteq> {(a, b). R a b}} (fmap snd)) a b" (is "?L = ?R")
proof
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) (transfer, simp)+
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', fmap fst R')" using conjunct1[OF `?L`]
- by (clarify, transfer, auto simp add: image_def Int_def split: prod.splits)
- from * show "(R', b) = (R', fmap snd R')" using conjunct2[OF `?L`]
- by (clarify, transfer, auto simp add: image_def Int_def split: prod.splits)
+ show ?R unfolding Grp_def relcompp.simps conversep.simps
+ proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
+ from * show "a = fmap fst R'" using conjunct1[OF `?L`]
+ by (transfer, auto simp add: image_def Int_def split: prod.splits)
+ from * show "b = fmap snd R'" using conjunct2[OF `?L`]
+ by (transfer, auto simp add: image_def Int_def split: prod.splits)
qed (auto simp add: *)
next
- assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
+ assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
apply (simp add: subset_eq Ball_def)
apply (rule conjI)
apply (transfer, clarsimp, metis snd_conv)
@@ -339,7 +340,7 @@
apply (rule ordLeq_transitive[OF surj_imp_ordLeq[of _ abs_fset] list_in_bd])
apply (auto simp: fset_def intro!: image_eqI[of _ abs_fset]) []
apply (erule wpull_fmap)
- apply (simp add: Gr_def relcomp_unfold converse_unfold fset_rel_def fset_rel_aux)
+ apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_def fset_rel_aux)
apply transfer apply simp
done
@@ -419,27 +420,27 @@
lemma cset_rel_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")
+ ((Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cIm fst))\<inverse>\<inverse> OO
+ Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cIm snd)) a b" (is "?L = ?R")
proof
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)
+ show ?R unfolding Grp_def relcompp.simps conversep.simps
+ proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
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
+ thus "a = 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
+ thus "b = cIm snd R'" unfolding cIm_def * by auto
qed (auto simp add: *)
next
- assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
+ assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
apply (simp add: subset_eq Ball_def)
apply (rule conjI)
apply (clarsimp, metis (lifting, no_types) rcset_map' image_iff surjective_pairing)
@@ -511,9 +512,9 @@
qed
next
fix R
- show "{p. cset_rel (\<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_rel_def cset_rel_aux by simp
+ show "cset_rel R =
+ (Grp {x. rcset x \<subseteq> Collect (split R)} (cIm fst))\<inverse>\<inverse> OO Grp {x. rcset x \<subseteq> Collect (split R)} (cIm snd)"
+ unfolding cset_rel_def[abs_def] cset_rel_aux by simp
qed (unfold cEmp_def, auto)
@@ -1143,7 +1144,7 @@
lemma multiset_map_Zero[simp]: "multiset_map f {#} = {#}" by simp
lemma multiset_rel_Zero: "multiset_rel R {#} {#}"
-unfolding multiset_rel_def Gr_def relcomp_unfold by auto
+unfolding multiset_rel_def Grp_def by auto
declare multiset.count[simp]
declare mmap[simp]
@@ -1196,7 +1197,7 @@
}
thus ?thesis
using assms
- unfolding multiset_rel_def Gr_def relcomp_unfold by force
+ unfolding multiset_rel_def Grp_def by force
qed
lemma multiset_rel'_imp_multiset_rel:
@@ -1238,7 +1239,7 @@
lemma multiset_rel_mcard:
assumes "multiset_rel R M N"
shows "mcard M = mcard N"
-using assms unfolding multiset_rel_def relcomp_unfold Gr_def by auto
+using assms unfolding multiset_rel_def Grp_def by auto
lemma multiset_induct2[case_names empty addL addR]:
assumes empty: "P {#} {#}"
@@ -1299,14 +1300,14 @@
obtain K where KM: "multiset_map fst K = M + {#a#}"
and KN: "multiset_map snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
using assms
- unfolding multiset_rel_def Gr_def relcomp_unfold by auto
+ unfolding multiset_rel_def Grp_def by auto
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
have Rab: "R a (snd ab)" using sK a unfolding K by auto
have "multiset_rel R M N1" using sK K1M K1N1
- unfolding K multiset_rel_def Gr_def relcomp_unfold by auto
+ unfolding K multiset_rel_def Grp_def by auto
thus ?thesis using N Rab by auto
qed
@@ -1317,14 +1318,14 @@
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_rel_def Gr_def relcomp_unfold by auto
+ unfolding multiset_rel_def Grp_def 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_rel R M1 N" using sK K1N K1M1
- unfolding K multiset_rel_def Gr_def relcomp_unfold by auto
+ unfolding K multiset_rel_def Grp_def by auto
thus ?thesis using M Rab by auto
qed
--- a/src/HOL/BNF/Tools/bnf_comp.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Tue May 07 14:22:54 2013 +0200
@@ -40,25 +40,22 @@
type unfold_set = {
map_unfolds: thm list,
set_unfoldss: thm list list,
- rel_unfolds: thm list,
- srel_unfolds: thm list
+ rel_unfolds: thm list
};
-val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = [], srel_unfolds = []};
+val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
-fun add_to_unfolds map sets rel srel
- {map_unfolds, set_unfoldss, rel_unfolds, srel_unfolds} =
+fun add_to_unfolds map sets rel
+ {map_unfolds, set_unfoldss, rel_unfolds} =
{map_unfolds = add_to_thms map_unfolds map,
set_unfoldss = adds_to_thms set_unfoldss sets,
- rel_unfolds = add_to_thms rel_unfolds rel,
- srel_unfolds = add_to_thms srel_unfolds srel};
+ rel_unfolds = add_to_thms rel_unfolds rel};
fun add_bnf_to_unfolds bnf =
- add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf)
- (srel_def_of_bnf bnf);
+ add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf);
val bdTN = "bdT";
@@ -221,25 +218,24 @@
fun map_wpull_tac _ =
mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
- fun srel_O_Gr_tac _ =
+ fun rel_OO_Grp_tac _ =
let
- val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
- val outer_srel_Gr = srel_Gr_of_bnf outer RS sym;
- val outer_srel_cong = srel_cong_of_bnf outer;
+ val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
+ val outer_rel_cong = rel_cong_of_bnf outer;
val thm =
- (trans OF [in_alt_thm RS @{thm O_Gr_cong},
- trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
- [trans OF [outer_srel_Gr RS @{thm arg_cong[of _ _ converse]},
- srel_converse_of_bnf outer RS sym], outer_srel_Gr],
- trans OF [srel_O_of_bnf outer RS sym, outer_srel_cong OF
- (map (fn bnf => srel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
- |> unfold_thms lthy (basic_thms @ srel_def_of_bnf outer :: map srel_def_of_bnf inners);
+ (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
+ trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
+ [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
+ rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
+ trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF
+ (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym)
+ (*|> unfold_thms lthy (rel_def_of_bnf outer :: map rel_def_of_bnf inners)*);
in
- unfold_thms_tac lthy basic_thms THEN rtac thm 1
+ rtac thm 1
end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -332,24 +328,24 @@
(bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
- fun srel_O_Gr_tac _ =
+ fun rel_OO_Grp_tac _ =
let
- val srel_Gr = srel_Gr_of_bnf bnf RS sym
+ val rel_Grp = rel_Grp_of_bnf bnf RS sym
val thm =
- (trans OF [in_alt_thm RS @{thm O_Gr_cong},
- trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
- [trans OF [srel_Gr RS @{thm arg_cong[of _ _ converse]},
- srel_converse_of_bnf bnf RS sym], srel_Gr],
- trans OF [srel_O_of_bnf bnf RS sym, srel_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_thms lthy (srel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
+ (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
+ trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
+ [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]},
+ rel_conversep_of_bnf bnf RS sym], rel_Grp],
+ trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
+ (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
+ replicate (live - n) @{thm Grp_fst_snd})]]] RS sym)
+ (*|> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv})*);
in
rtac thm 1
end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -432,11 +428,10 @@
fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
- fun srel_O_Gr_tac _ =
- mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
+ fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -509,11 +504,10 @@
mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
- fun srel_O_Gr_tac _ =
- mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
+ fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
+ bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -598,7 +592,6 @@
val map_unfolds = #map_unfolds unfold_set;
val set_unfoldss = #set_unfoldss unfold_set;
val rel_unfolds = #rel_unfolds unfold_set;
- val srel_unfolds = #srel_unfolds unfold_set;
val expand_maps =
fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
@@ -609,8 +602,7 @@
val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
val unfold_rels = unfold_thms lthy rel_unfolds;
- val unfold_srels = unfold_thms lthy srel_unfolds;
- val unfold_all = unfold_sets o unfold_maps o unfold_rels o unfold_srels;
+ val unfold_all = unfold_sets o unfold_maps 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);
@@ -656,7 +648,7 @@
(mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_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 (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
+ (mk_tac (unfold_thms lthy [rel_def_of_bnf bnf] (rel_OO_Grp_of_bnf bnf)));
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Tue May 07 14:22:54 2013 +0200
@@ -36,7 +36,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_srel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic
+ val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
val mk_simple_wit_tac: thm list -> tactic
end;
@@ -52,8 +52,6 @@
val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
val card_of_Card_order = @{thm card_of_Card_order};
val csum_Cnotzero1 = @{thm csum_Cnotzero1};
-val csum_Cnotzero2 = @{thm csum_Cnotzero2};
-val ctwo_Cnotzero = @{thm ctwo_Cnotzero};
val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
val ordIso_transitive = @{thm ordIso_transitive};
val ordLeq_csum2 = @{thm ordLeq_csum2};
@@ -389,9 +387,8 @@
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_srel_O_Gr_tac ctxt srel_def srel_O_Gr in_alt_thm =
- rtac (unfold_thms ctxt [srel_def]
- (trans OF [srel_O_Gr, in_alt_thm RS @{thm O_Gr_cong} RS sym])) 1;
+fun mk_simple_rel_OO_Grp_tac rel_OO_Grp in_alt_thm =
+ rtac (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
--- a/src/HOL/BNF/Tools/bnf_def.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Tue May 07 14:22:54 2013 +0200
@@ -28,7 +28,6 @@
val relN: string
val setN: string
val mk_setN: int -> string
- val srelN: string
val map_of_bnf: bnf -> term
val sets_of_bnf: bnf -> term list
@@ -39,7 +38,6 @@
val mk_map_of_bnf: typ list -> typ list -> typ list -> bnf -> term
val mk_rel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
val mk_sets_of_bnf: typ list list -> typ list list -> bnf -> term list
- val mk_srel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
val mk_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list
val bd_Card_order_of_bnf: bnf -> thm
@@ -51,7 +49,7 @@
val in_bd_of_bnf: bnf -> thm
val in_cong_of_bnf: bnf -> thm
val in_mono_of_bnf: bnf -> thm
- val in_srel_of_bnf: bnf -> thm
+ val in_rel_of_bnf: bnf -> thm
val map_comp'_of_bnf: bnf -> thm
val map_comp_of_bnf: bnf -> thm
val map_cong0_of_bnf: bnf -> thm
@@ -62,21 +60,18 @@
val map_wppull_of_bnf: bnf -> thm
val map_wpull_of_bnf: bnf -> thm
val rel_def_of_bnf: bnf -> thm
+ val rel_Grp_of_bnf: bnf -> thm
+ val rel_OO_of_bnf: bnf -> thm
+ val rel_OO_Grp_of_bnf: bnf -> thm
+ val rel_cong_of_bnf: bnf -> thm
+ val rel_conversep_of_bnf: bnf -> thm
+ val rel_mono_of_bnf: bnf -> thm
val rel_eq_of_bnf: bnf -> thm
val rel_flip_of_bnf: bnf -> thm
- val rel_srel_of_bnf: bnf -> thm
val set_bd_of_bnf: bnf -> thm list
val set_defs_of_bnf: bnf -> thm list
val set_map'_of_bnf: bnf -> thm list
val set_map_of_bnf: bnf -> thm list
- val srel_def_of_bnf: bnf -> thm
- val srel_Gr_of_bnf: bnf -> thm
- val srel_Id_of_bnf: bnf -> thm
- val srel_O_of_bnf: bnf -> thm
- val srel_O_Gr_of_bnf: bnf -> thm
- val srel_cong_of_bnf: bnf -> thm
- val srel_converse_of_bnf: bnf -> thm
- val srel_mono_of_bnf: bnf -> thm
val wit_thms_of_bnf: bnf -> thm list
val wit_thmss_of_bnf: bnf -> thm list list
@@ -120,12 +115,12 @@
set_bd: thm list,
in_bd: thm,
map_wpull: thm,
- srel_O_Gr: thm
+ rel_OO_Grp: thm
};
-fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), srel) =
+fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), rel) =
{map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
- bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, srel_O_Gr = srel};
+ bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_OO_Grp = rel};
fun dest_cons [] = raise Empty
| dest_cons (x :: xs) = (x, xs);
@@ -144,16 +139,16 @@
||> the_single
|> mk_axioms';
-fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull srel =
- [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, srel];
+fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
+ [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, in_bd,
- map_wpull, srel_O_Gr} =
+ map_wpull, rel_OO_Grp} =
zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd in_bd map_wpull
- srel_O_Gr;
+ rel_OO_Grp;
fun map_axioms f {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
- in_bd, map_wpull, srel_O_Gr} =
+ in_bd, map_wpull, rel_OO_Grp} =
{map_id = f map_id,
map_comp = f map_comp,
map_cong0 = f map_cong0,
@@ -163,21 +158,20 @@
set_bd = map f set_bd,
in_bd = f in_bd,
map_wpull = f map_wpull,
- srel_O_Gr = f srel_O_Gr};
+ rel_OO_Grp = f rel_OO_Grp};
val morph_axioms = map_axioms o Morphism.thm;
type defs = {
map_def: thm,
set_defs: thm list,
- rel_def: thm,
- srel_def: thm
+ rel_def: thm
}
-fun mk_defs map sets rel srel = {map_def = map, set_defs = sets, rel_def = rel, srel_def = srel};
+fun mk_defs map sets rel = {map_def = map, set_defs = sets, rel_def = rel};
-fun map_defs f {map_def, set_defs, rel_def, srel_def} =
- {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def, srel_def = f srel_def};
+fun map_defs f {map_def, set_defs, rel_def} =
+ {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def};
val morph_defs = map_defs o Morphism.thm;
@@ -188,47 +182,43 @@
collect_set_map: thm lazy,
in_cong: thm lazy,
in_mono: thm lazy,
- in_srel: thm lazy,
+ in_rel: thm lazy,
map_comp': thm lazy,
map_cong: thm lazy,
map_id': thm lazy,
map_wppull: thm lazy,
rel_eq: thm lazy,
rel_flip: thm lazy,
- rel_srel: thm lazy,
set_map': thm lazy list,
- srel_cong: thm lazy,
- srel_mono: thm lazy,
- srel_Id: thm lazy,
- srel_Gr: thm lazy,
- srel_converse: thm lazy,
- srel_O: thm lazy
+ rel_cong: thm lazy,
+ rel_mono: thm lazy,
+ rel_Grp: thm lazy,
+ rel_conversep: thm lazy,
+ rel_OO: thm lazy
};
-fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono in_srel
- map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_map' srel_cong srel_mono
- srel_Id srel_Gr srel_converse srel_O = {
+fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono in_rel
+ map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map' rel_cong rel_mono
+ rel_Grp rel_conversep rel_OO = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
collect_set_map = collect_set_map,
in_cong = in_cong,
in_mono = in_mono,
- in_srel = in_srel,
+ in_rel = in_rel,
map_comp' = map_comp',
map_cong = map_cong,
map_id' = map_id',
map_wppull = map_wppull,
rel_eq = rel_eq,
rel_flip = rel_flip,
- rel_srel = rel_srel,
set_map' = set_map',
- srel_cong = srel_cong,
- srel_mono = srel_mono,
- srel_Id = srel_Id,
- srel_Gr = srel_Gr,
- srel_converse = srel_converse,
- srel_O = srel_O};
+ rel_cong = rel_cong,
+ rel_mono = rel_mono,
+ rel_Grp = rel_Grp,
+ rel_conversep = rel_conversep,
+ rel_OO = rel_OO};
fun map_facts f {
bd_Card_order,
@@ -237,42 +227,38 @@
collect_set_map,
in_cong,
in_mono,
- in_srel,
+ in_rel,
map_comp',
map_cong,
map_id',
map_wppull,
rel_eq,
rel_flip,
- rel_srel,
set_map',
- srel_cong,
- srel_mono,
- srel_Id,
- srel_Gr,
- srel_converse,
- srel_O} =
+ rel_cong,
+ rel_mono,
+ rel_Grp,
+ rel_conversep,
+ rel_OO} =
{bd_Card_order = f bd_Card_order,
bd_Cinfinite = f bd_Cinfinite,
bd_Cnotzero = f bd_Cnotzero,
collect_set_map = Lazy.map f collect_set_map,
in_cong = Lazy.map f in_cong,
in_mono = Lazy.map f in_mono,
- in_srel = Lazy.map f in_srel,
+ in_rel = Lazy.map f in_rel,
map_comp' = Lazy.map f map_comp',
map_cong = Lazy.map f map_cong,
map_id' = Lazy.map f map_id',
map_wppull = Lazy.map f map_wppull,
rel_eq = Lazy.map f rel_eq,
rel_flip = Lazy.map f rel_flip,
- rel_srel = Lazy.map f rel_srel,
set_map' = map (Lazy.map f) set_map',
- srel_cong = Lazy.map f srel_cong,
- srel_mono = Lazy.map f srel_mono,
- srel_Id = Lazy.map f srel_Id,
- srel_Gr = Lazy.map f srel_Gr,
- srel_converse = Lazy.map f srel_converse,
- srel_O = Lazy.map f srel_O};
+ rel_cong = Lazy.map f rel_cong,
+ rel_mono = Lazy.map f rel_mono,
+ rel_Grp = Lazy.map f rel_Grp,
+ rel_conversep = Lazy.map f rel_conversep,
+ rel_OO = Lazy.map f rel_OO};
val morph_facts = map_facts o Morphism.thm;
@@ -302,8 +288,7 @@
facts: facts,
nwits: int,
wits: nonemptiness_witness list,
- rel: term,
- srel: term
+ rel: term
};
(* getters *)
@@ -357,13 +342,6 @@
Term.subst_atomic_types
((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#rel bnf_rep)
end;
-val srel_of_bnf = #srel o rep_bnf;
-fun mk_srel_of_bnf Ds Ts Us bnf =
- let val bnf_rep = rep_bnf bnf;
- in
- Term.subst_atomic_types
- ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#srel bnf_rep)
- end;
(*thms*)
val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
@@ -375,7 +353,7 @@
val in_bd_of_bnf = #in_bd o #axioms o rep_bnf;
val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
-val in_srel_of_bnf = Lazy.force o #in_srel o #facts o rep_bnf;
+val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
val map_def_of_bnf = #map_def o #defs o rep_bnf;
val map_id_of_bnf = #map_id o #axioms o rep_bnf;
val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
@@ -388,33 +366,30 @@
val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
-val rel_srel_of_bnf = Lazy.force o #rel_srel o #facts o rep_bnf;
val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
val set_map_of_bnf = #set_map o #axioms o rep_bnf;
val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf;
-val srel_cong_of_bnf = Lazy.force o #srel_cong o #facts o rep_bnf;
-val srel_mono_of_bnf = Lazy.force o #srel_mono o #facts o rep_bnf;
-val srel_def_of_bnf = #srel_def o #defs o rep_bnf;
-val srel_Id_of_bnf = Lazy.force o #srel_Id o #facts o rep_bnf;
-val srel_Gr_of_bnf = Lazy.force o #srel_Gr o #facts o rep_bnf;
-val srel_converse_of_bnf = Lazy.force o #srel_converse o #facts o rep_bnf;
-val srel_O_of_bnf = Lazy.force o #srel_O o #facts o rep_bnf;
-val srel_O_Gr_of_bnf = #srel_O_Gr o #axioms o rep_bnf;
+val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
+val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
+val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
+val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
+val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
+val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf;
val wit_thms_of_bnf = maps #prop o wits_of_bnf;
val wit_thmss_of_bnf = map #prop o wits_of_bnf;
-fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel srel =
+fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel =
BNF {name = name, T = T,
live = live, lives = lives, lives' = lives', dead = dead, deads = deads,
map = map, sets = sets, bd = bd,
axioms = axioms, defs = defs, facts = facts,
- nwits = length wits, wits = wits, rel = rel, srel = srel};
+ nwits = length wits, wits = wits, rel = rel};
fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
dead = dead, deads = deads, map = map, sets = sets, bd = bd,
axioms = axioms, defs = defs, facts = facts,
- nwits = nwits, wits = wits, rel = rel, srel = srel}) =
+ nwits = nwits, wits = wits, rel = rel}) =
BNF {name = Morphism.binding phi name, T = Morphism.typ phi T,
live = live, lives = List.map (Morphism.typ phi) lives,
lives' = List.map (Morphism.typ phi) lives',
@@ -426,7 +401,7 @@
facts = morph_facts phi facts,
nwits = nwits,
wits = List.map (morph_witness phi) wits,
- rel = Morphism.term phi rel, srel = Morphism.term phi srel};
+ rel = Morphism.term phi rel};
fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...},
BNF {T = T2, live = live2, dead = dead2, ...}) =
@@ -460,15 +435,6 @@
Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_pred2T instA instB))
Vartab.empty;
in Envir.subst_term (tyenv, Vartab.empty) rel end
- handle Type.TYPE_MATCH => error "Bad predicator";
-
-fun normalize_srel ctxt instTs instA instB srel =
- let
- val thy = Proof_Context.theory_of ctxt;
- val tyenv =
- Sign.typ_match thy (fastype_of srel, Library.foldr (op -->) (instTs, mk_relT (instA, instB)))
- Vartab.empty;
- in Envir.subst_term (tyenv, Vartab.empty) srel end
handle Type.TYPE_MATCH => error "Bad relator";
fun normalize_wit insts CA As wit =
@@ -503,7 +469,6 @@
val witN = "wit";
fun mk_witN i = witN ^ nonzero_string_of_int i;
val relN = "rel";
-val srelN = "srel";
val bd_card_orderN = "bd_card_order";
val bd_cinfiniteN = "bd_cinfinite";
@@ -513,7 +478,7 @@
val collect_set_mapN = "collect_set_map";
val in_bdN = "in_bd";
val in_monoN = "in_mono";
-val in_srelN = "in_srel";
+val in_relN = "in_rel";
val map_idN = "map_id";
val map_id'N = "map_id'";
val map_compN = "map_comp";
@@ -523,16 +488,14 @@
val map_wpullN = "map_wpull";
val rel_eqN = "rel_eq";
val rel_flipN = "rel_flip";
-val rel_srelN = "rel_srel";
val set_mapN = "set_map";
val set_map'N = "set_map'";
val set_bdN = "set_bd";
-val srel_IdN = "srel_Id";
-val srel_GrN = "srel_Gr";
-val srel_converseN = "srel_converse";
-val srel_monoN = "srel_mono"
-val srel_ON = "srel_comp";
-val srel_O_GrN = "srel_comp_Gr";
+val rel_GrpN = "rel_Grp";
+val rel_conversepN = "rel_conversep";
+val rel_monoN = "rel_mono"
+val rel_OON = "rel_compp";
+val rel_OO_GrpN = "rel_compp_Grp";
datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
@@ -688,12 +651,12 @@
fun mk_bnf_t As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
fun mk_bnf_T As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
- val (setRTs, RTs) = map_split (`HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Bs');
- val setRTsAsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Cs);
- 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 mk_pred2T As' Bs';
+ val RTs = map HOLogic.mk_prodT (As' ~~ Bs');
+ val pred2RTs = map2 mk_pred2T As' Bs';
+ val pred2RTsAsCs = map2 mk_pred2T As' Cs;
+ val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
+ val pred2RT's = map2 mk_pred2T Bs' As';
+ val self_pred2RTs = map2 mk_pred2T As' As';
val CA' = mk_bnf_T As' CA;
val CB' = mk_bnf_T Bs' CA;
@@ -711,9 +674,9 @@
val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
val pre_names_lthy = lthy;
- val ((((((((((((((((((((((((fs, gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As),
+ val (((((((((((((((((((((((fs, 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')), names_lthy) = pre_names_lthy
+ names_lthy) = pre_names_lthy
|> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts)
@@ -734,39 +697,30 @@
||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts)
||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts)
||>> mk_Frees "b" As'
- ||>> mk_Frees' "r" setRTs
- ||>> mk_Frees "r" setRTs
- ||>> mk_Frees "s" setRTsBsCs
- ||>> mk_Frees' "P" QTs;
+ ||>> mk_Frees' "R" pred2RTs
+ ||>> mk_Frees "R" pred2RTs
+ ||>> mk_Frees "S" pred2RTsBsCs;
val fs_copy = map2 (retype_free o fastype_of) fs gs;
val x_copy = retype_free CA' y;
- (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
- val O_Gr =
+ val setRs =
+ map3 (fn R => fn T => fn U =>
+ HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As' Bs';
+
+ (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
+ Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
+ val OO_Grp =
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);
- val bnf_in = mk_in (map Free Rs') (map (mk_bnf_t RTs) bnf_sets) CRs';
+ val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
in
- mk_rel_comp (mk_converse (mk_Gr bnf_in map1), mk_Gr bnf_in map2)
+ mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2)
end;
- 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 sQs =
- map3 (fn Q => fn T => fn U =>
- HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs';
-
val rel_rhs = (case raw_rel_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, sQs)))
+ NONE => fold_rev Term.absfree Rs' OO_Grp
| SOME raw_rel => prep_term no_defs_lthy raw_rel);
val rel_bind_def =
@@ -782,32 +736,12 @@
val bnf_rel_def = Morphism.thm phi raw_rel_def;
val bnf_rel = Morphism.term phi bnf_rel_term;
- fun mk_bnf_rel QTs CA' CB' = normalize_rel lthy QTs CA' CB' bnf_rel;
-
- val rel = mk_bnf_rel QTs CA' CB';
-
- val srel_rhs =
- fold_rev Term.absfree Rs' (HOLogic.Collect_const CA'CB' $
- Term.lambda p (Term.list_comb (rel, map (mk_predicate_of_set (fst x') (fst y')) Rs) $
- HOLogic.mk_fst p $ HOLogic.mk_snd p));
-
- val srel_bind_def = (fn () => Binding.suffix_name ("_" ^ srelN) b, srel_rhs);
+ fun mk_bnf_rel RTs CA' CB' = normalize_rel lthy RTs CA' CB' bnf_rel;
- val ((bnf_srel_term, raw_srel_def), (lthy, lthy_old)) =
- lthy
- |> maybe_define false srel_bind_def
- ||> `(maybe_restore lthy);
-
- val phi = Proof_Context.export_morphism lthy_old lthy;
- val bnf_srel_def = Morphism.thm phi raw_srel_def;
- val bnf_srel = Morphism.term phi bnf_srel_term;
-
- fun mk_bnf_srel setRTs CA' CB' = normalize_srel lthy setRTs CA' CB' bnf_srel;
-
- val srel = mk_bnf_srel setRTs CA' CB';
+ val rel = mk_bnf_rel pred2RTs CA' CB';
val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @
- raw_wit_defs @ [raw_rel_def, raw_srel_def]) of
+ raw_wit_defs @ [raw_rel_def]) of
[] => ()
| defs => Proof_Display.print_consts true lthy_old (K false)
(map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
@@ -900,10 +834,10 @@
(Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull))
end;
- val srel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (srel, Rs), O_Gr));
+ val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_maps_goal card_order_bd_goal
- cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal;
+ cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_OO_Grp_goal;
fun mk_wit_goals (I, wit) =
let
@@ -953,11 +887,11 @@
fun mk_in_mono () =
let
- val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_subset) As As_copy;
+ val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_leq) As As_copy;
val in_mono_goal =
fold_rev Logic.all (As @ As_copy)
(Logic.list_implies (prems_mono, HOLogic.mk_Trueprop
- (mk_subset (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
+ (mk_leq (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
in
Goal.prove_sorry lthy [] [] in_mono_goal (K (mk_in_mono_tac live))
|> Thm.close_derivation
@@ -1038,41 +972,41 @@
val map_wppull = Lazy.lazy mk_map_wppull;
- val srel_O_Grs = no_refl [#srel_O_Gr axioms];
+ val rel_OO_Grps = no_refl [#rel_OO_Grp axioms];
- fun mk_srel_Gr () =
+ fun mk_rel_Grp () =
let
- val lhs = Term.list_comb (srel, map2 mk_Gr As fs);
- val rhs = mk_Gr (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
+ val lhs = Term.list_comb (rel, map2 mk_Grp As fs);
+ val rhs = mk_Grp (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
in
Goal.prove_sorry lthy [] [] goal
- (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
+ (mk_rel_Grp_tac rel_OO_Grps (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
(Lazy.force map_comp') (map Lazy.force set_map'))
|> Thm.close_derivation
end;
- val srel_Gr = Lazy.lazy mk_srel_Gr;
+ val rel_Grp = Lazy.lazy mk_rel_Grp;
- fun mk_srel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
- fun mk_srel_concl f = HOLogic.mk_Trueprop
- (f (Term.list_comb (srel, Rs), Term.list_comb (srel, Rs_copy)));
+ fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
+ fun mk_rel_concl f = HOLogic.mk_Trueprop
+ (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy)));
- fun mk_srel_mono () =
+ fun mk_rel_mono () =
let
- val mono_prems = mk_srel_prems mk_subset;
- val mono_concl = mk_srel_concl (uncurry mk_subset);
+ val mono_prems = mk_rel_prems mk_leq;
+ val mono_concl = mk_rel_concl (uncurry mk_leq);
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
- (mk_srel_mono_tac srel_O_Grs (Lazy.force in_mono))
+ (mk_rel_mono_tac rel_OO_Grps (Lazy.force in_mono))
|> Thm.close_derivation
end;
- fun mk_srel_cong () =
+ fun mk_rel_cong () =
let
- val cong_prems = mk_srel_prems (curry HOLogic.mk_eq);
- val cong_concl = mk_srel_concl HOLogic.mk_eq;
+ val cong_prems = mk_rel_prems (curry HOLogic.mk_eq);
+ val cong_concl = mk_rel_concl HOLogic.mk_eq;
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
@@ -1080,120 +1014,103 @@
|> Thm.close_derivation
end;
- val srel_mono = Lazy.lazy mk_srel_mono;
- val srel_cong = Lazy.lazy mk_srel_cong;
+ val rel_mono = Lazy.lazy mk_rel_mono;
+ val rel_cong = Lazy.lazy mk_rel_cong;
- fun mk_srel_Id () =
- let val srelAsAs = mk_bnf_srel self_setRTs CA' CA' in
+ fun mk_rel_eq () =
+ let val relAsAs = mk_bnf_rel self_pred2RTs CA' CA' in
Goal.prove_sorry lthy [] []
- (mk_Trueprop_eq (Term.list_comb (srelAsAs, map Id_const As'), Id_const CA'))
- (mk_srel_Id_tac live (Lazy.force srel_Gr) (#map_id axioms))
+ (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
+ HOLogic.eq_const CA'))
+ (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms))
|> Thm.close_derivation
end;
- val srel_Id = Lazy.lazy mk_srel_Id;
+ val rel_eq = Lazy.lazy mk_rel_eq;
- fun mk_srel_converse () =
+ fun mk_rel_conversep () =
let
- val srelBsAs = mk_bnf_srel setRT's CB' CA';
- val lhs = Term.list_comb (srelBsAs, map mk_converse Rs);
- val rhs = mk_converse (Term.list_comb (srel, Rs));
- val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
+ val relBsAs = mk_bnf_rel pred2RT's CB' CA';
+ val lhs = Term.list_comb (relBsAs, map mk_conversep Rs);
+ val rhs = mk_conversep (Term.list_comb (rel, Rs));
+ val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
val le_thm = Goal.prove_sorry lthy [] [] le_goal
- (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
+ (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
(Lazy.force map_comp') (map Lazy.force set_map'))
|> Thm.close_derivation
val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
in
- Goal.prove_sorry lthy [] [] goal (fn _ => mk_srel_converse_tac le_thm)
+ Goal.prove_sorry lthy [] [] goal
+ (K (mk_rel_conversep_tac le_thm (Lazy.force rel_mono)))
|> Thm.close_derivation
end;
- val srel_converse = Lazy.lazy mk_srel_converse;
+ val rel_conversep = Lazy.lazy mk_rel_conversep;
- fun mk_srel_O () =
+ fun mk_rel_OO () =
let
- val srelAsCs = mk_bnf_srel setRTsAsCs CA' CC';
- val srelBsCs = mk_bnf_srel setRTsBsCs CB' CC';
- val lhs = Term.list_comb (srelAsCs, map2 (curry mk_rel_comp) Rs Ss);
- val rhs = mk_rel_comp (Term.list_comb (srel, Rs), Term.list_comb (srelBsCs, Ss));
+ val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC';
+ val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC';
+ val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss);
+ val rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
in
Goal.prove_sorry lthy [] [] goal
- (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
+ (mk_rel_OO_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
(Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_map'))
|> Thm.close_derivation
end;
- val srel_O = Lazy.lazy mk_srel_O;
+ val rel_OO = Lazy.lazy mk_rel_OO;
- fun mk_in_srel () =
+ fun mk_in_rel () =
let
- val bnf_in = mk_in Rs (map (mk_bnf_t RTs) bnf_sets) CRs';
+ val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
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);
val map_fst_eq = HOLogic.mk_eq (map1 $ z, x);
val map_snd_eq = HOLogic.mk_eq (map2 $ z, y);
- val lhs = HOLogic.mk_mem (HOLogic.mk_prod (x, y), Term.list_comb (srel, Rs));
+ val lhs = Term.list_comb (rel, Rs) $ x $ y;
val rhs =
HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
val goal =
fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
in
- Goal.prove_sorry lthy [] [] goal (mk_in_srel_tac srel_O_Grs (length bnf_sets))
+ Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac rel_OO_Grps)
|> Thm.close_derivation
end;
- val in_srel = Lazy.lazy mk_in_srel;
-
- val eqset_imp_iff_pair = @{thm eqset_imp_iff_pair};
- val mem_Collect_etc = @{thms fst_conv mem_Collect_eq prod.cases snd_conv};
- val mem_Collect_etc' = @{thms fst_conv mem_Collect_eq pair_in_Id_conv snd_conv};
+ val in_rel = Lazy.lazy mk_in_rel;
- fun mk_rel_srel () =
- unfold_thms lthy mem_Collect_etc
- (funpow live (fn thm => thm RS @{thm fun_cong_pair}) (bnf_srel_def RS meta_eq_to_obj_eq)
- RS eqset_imp_iff_pair RS sym)
- |> Drule.zero_var_indexes;
-
- val rel_srel = Lazy.lazy mk_rel_srel;
-
- fun mk_rel_eq () =
- unfold_thms lthy (bnf_srel_def :: mem_Collect_etc')
- (Lazy.force srel_Id RS @{thm arg_cong[of _ _ "%A x y. (x, y) : A"]})
- |> Drule.eta_contraction_rule;
-
- val rel_eq = Lazy.lazy mk_rel_eq;
+ val predicate2_cong = @{thm predicate2_cong};
+ val mem_Collect_etc = @{thms fst_conv mem_Collect_eq prod.cases snd_conv};
fun mk_rel_flip () =
let
- val srel_converse_thm = Lazy.force srel_converse;
- val cts = map (SOME o certify lthy) sQs;
- val srel_converse_thm' = cterm_instantiate_pos cts srel_converse_thm;
+ val rel_conversep_thm = Lazy.force rel_conversep;
+ val cts = map (SOME o certify lthy) Rs;
+ val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
in
- unfold_thms lthy (bnf_srel_def :: @{thm converse_iff} :: mem_Collect_etc)
- (srel_converse_thm' RS eqset_imp_iff_pair)
+ unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS predicate2_cong)
|> singleton (Proof_Context.export names_lthy pre_names_lthy)
end;
val rel_flip = Lazy.lazy mk_rel_flip;
- val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def;
+ val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono
- in_srel map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_map'
- srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O;
+ in_rel map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map'
+ rel_cong rel_mono rel_Grp rel_conversep rel_OO;
val wits = map2 mk_witness bnf_wits wit_thms;
val bnf_rel =
Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;
- val bnf_srel =
- Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) srel;
val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts
- wits bnf_rel bnf_srel;
+ wits bnf_rel;
in
(bnf, lthy
|> (if fact_policy = Note_All then
@@ -1208,7 +1125,7 @@
(collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
(in_bdN, [#in_bd axioms]),
(in_monoN, [Lazy.force (#in_mono facts)]),
- (in_srelN, [Lazy.force (#in_srel facts)]),
+ (in_relN, [Lazy.force (#in_rel facts)]),
(map_compN, [#map_comp axioms]),
(map_idN, [#map_id axioms]),
(map_wpullN, [#map_wpull axioms]),
@@ -1232,14 +1149,12 @@
(map_id'N, [Lazy.force (#map_id' facts)], []),
(rel_eqN, [Lazy.force (#rel_eq facts)], []),
(rel_flipN, [Lazy.force (#rel_flip facts)], []),
- (rel_srelN, [Lazy.force (#rel_srel facts)], []),
(set_map'N, map Lazy.force (#set_map' facts), []),
- (srel_O_GrN, srel_O_Grs, []),
- (srel_IdN, [Lazy.force (#srel_Id facts)], []),
- (srel_GrN, [Lazy.force (#srel_Gr facts)], []),
- (srel_converseN, [Lazy.force (#srel_converse facts)], []),
- (srel_monoN, [Lazy.force (#srel_mono facts)], []),
- (srel_ON, [Lazy.force (#srel_O facts)], [])]
+ (rel_OO_GrpN, rel_OO_Grps, []),
+ (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
+ (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
+ (rel_monoN, [Lazy.force (#rel_mono facts)], []),
+ (rel_OON, [Lazy.force (#rel_OO facts)], [])]
|> filter_out (null o #2)
|> map (fn (thmN, thms, attrs) =>
((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)),
@@ -1252,8 +1167,7 @@
end;
val one_step_defs =
- no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def,
- bnf_srel_def]);
+ no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
in
(key, goals, wit_goalss, after_qed, lthy, one_step_defs)
end;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Tue May 07 14:22:54 2013 +0200
@@ -16,16 +16,16 @@
val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_set_map': thm -> thm
- val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_srel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
- val mk_srel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_rel_eq_tac: int -> thm -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_in_srel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
- val mk_srel_converse_tac: thm -> tactic
- val mk_srel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
+ val mk_in_rel_tac: thm list -> {prems: 'b, context: Proof.context} -> tactic
+ val mk_rel_conversep_tac: thm -> thm -> tactic
+ val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_srel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
end;
structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -71,86 +71,77 @@
rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
-fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_maps
+fun mk_rel_Grp_tac rel_OO_Grps map_id map_cong0 map_id' map_comp set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
in
if null set_maps then
- unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
- else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
- EVERY' [rtac equalityI, rtac subsetI,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
- rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
- REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
- rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
- rtac (@{thm snd_conv} RS sym)],
+ unfold_thms_tac ctxt ((map_id RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
+ rtac @{thm Grp_UNIV_idI[OF refl]} 1
+ else unfold_thms_tac ctxt rel_OO_Grps THEN
+ EVERY' [rtac @{thm antisym}, rtac @{thm predicate2I},
+ REPEAT_DETERM o
+ eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+ hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
+ REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac],
rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
- rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
- stac @{thm fst_conv}, atac]) set_maps,
- rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
- REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
- rtac @{thm relcompI}, rtac @{thm converseI},
+ rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac])
+ set_maps,
+ rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE],
+ hyp_subst_tac ctxt,
+ rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map2 (fn convol => fn map_id =>
- EVERY' [rtac CollectI, rtac exI, rtac conjI,
- rtac Pair_eqI, rtac conjI, rtac refl, rtac sym,
- rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
+ EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
REPEAT_DETERM_N n o rtac (convol RS fun_cong),
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
CONJ_WRAP' (fn thm =>
EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
- rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac])
+ rtac @{thm convol_mem_GrpI[OF refl]}, etac set_mp, atac])
set_maps])
@{thms fst_convol snd_convol} [map_id', refl])] 1
end;
-fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
- unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
- (if n = 0 then rtac refl 1
- else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
- rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
- CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id] 1);
+fun mk_rel_eq_tac n rel_Grp rel_cong map_id {context = ctxt, prems = _} =
+ (EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN'
+ rtac (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
+ (if n = 0 then rtac refl
+ else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ "Grp"]},
+ rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI,
+ CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id])) 1;
-fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} =
- unfold_thms_tac ctxt srel_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;
+fun mk_rel_mono_tac rel_OO_Grps in_mono {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt rel_OO_Grps THEN
+ EVERY' [rtac @{thm relcompp_mono}, rtac @{thm iffD2[OF conversep_mono]},
+ rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono},
+ rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1;
-fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_maps
+fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
in
- if null set_maps then
- unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
- else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
- EVERY' [rtac @{thm subrelI},
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt, rtac @{thm converseI},
- rtac @{thm relcompI}, rtac @{thm converseI},
- EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
- rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
+ if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1
+ else unfold_thms_tac ctxt (rel_OO_Grps) THEN
+ EVERY' [rtac @{thm predicate2I},
+ REPEAT_DETERM o
+ eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+ hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI},
+ EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans,
rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
rtac (map_comp RS sym), rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
- etac @{thm flip_rel}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
+ etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
end;
-fun mk_srel_converse_tac le_converse =
- EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
- rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
+fun mk_rel_conversep_tac le_conversep rel_mono =
+ EVERY' [rtac @{thm antisym}, rtac le_conversep, rtac @{thm xt1(6)}, rtac @{thm conversep_shift},
+ rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
+ REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
-fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_maps
+fun mk_rel_OO_tac rel_OO_Grs rel_eq map_cong0 map_wppull map_comp set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
@@ -158,59 +149,48 @@
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_maps;
in
- if null set_maps then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
- else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_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 Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
- rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
- rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
- REPEAT_DETERM_N n o rtac @{thm fst_fstO},
- in_tac @{thm fstO_in},
- rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
- REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
- rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
+ if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1
+ else unfold_thms_tac ctxt rel_OO_Grs THEN
+ EVERY' [rtac @{thm antisym}, rtac @{thm predicate2I},
+ REPEAT_DETERM o
+ eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+ hyp_subst_tac ctxt,
+ rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
+ rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
+ REPEAT_DETERM_N n o rtac @{thm fst_fstOp},
+ in_tac @{thm fstOp_in},
+ rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
+ REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply,
+ rtac ballE, rtac subst,
+ rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE,
etac set_mp, atac],
- in_tac @{thm fstO_in},
- rtac @{thm relcompI}, rtac @{thm converseI},
- rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
+ in_tac @{thm fstOp_in},
+ rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
+ rtac trans, rtac map_comp, rtac map_cong0,
REPEAT_DETERM_N n o rtac o_apply,
- in_tac @{thm sndO_in},
- rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
- REPEAT_DETERM_N n o rtac @{thm snd_sndO},
- in_tac @{thm sndO_in},
- rtac @{thm subrelI},
- REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o eresolve_tac [exE, conjE],
- REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
+ in_tac @{thm sndOp_in},
+ rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
+ REPEAT_DETERM_N n o rtac @{thm snd_sndOp},
+ in_tac @{thm sndOp_in},
+ rtac @{thm predicate2I},
+ REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}],
+ hyp_subst_tac ctxt,
rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
- CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_maps,
- etac allE, etac impE, etac conjI, etac conjI, atac,
+ CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps,
+ etac allE, etac impE, etac conjI, etac conjI, etac sym,
REPEAT_DETERM o eresolve_tac [bexE, conjE],
- rtac @{thm relcompI}, rtac @{thm converseI},
- EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
- rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
+ rtac @{thm relcomppI}, rtac @{thm conversepI},
+ EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans,
rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
- rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
+ rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
end;
-fun mk_in_srel_tac srel_O_Grs m {context = ctxt, prems = _} =
- let
- val ls' = replicate (Int.max (1, m)) ();
- in
- unfold_thms_tac ctxt (srel_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 ctxt, rtac exI,
- rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
- REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
- REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
- CONJ_WRAP' (K atac) ls']] 1
- end;
+fun mk_in_rel_tac rel_OO_Grs {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt rel_OO_Grs THEN
+ EVERY' [rtac iffI,
+ REPEAT_DETERM o eresolve_tac [@{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
+ hyp_subst_tac ctxt, rtac exI, rtac conjI, atac, rtac conjI, rtac refl, rtac refl,
+ REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},
+ etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1;
end;
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Tue May 07 14:22:54 2013 +0200
@@ -44,7 +44,7 @@
Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
-val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps};
+val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps id_apply};
val ss_if_True_False = simpset_of (ss_only @{thms if_True if_False} @{context});
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Tue May 07 14:22:54 2013 +0200
@@ -58,7 +58,6 @@
val ctor_relN: string
val ctor_set_inclN: string
val ctor_set_set_inclN: string
- val ctor_srelN: string
val disc_unfoldN: string
val disc_unfold_iffN: string
val disc_corecN: string
@@ -77,9 +76,6 @@
val dtor_relN: string
val dtor_set_inclN: string
val dtor_set_set_inclN: string
- val dtor_srelN: string
- val dtor_srel_coinductN: string
- val dtor_srel_strong_coinductN: string
val dtor_strong_coinductN: string
val dtor_unfoldN: string
val dtor_unfold_uniqueN: string
@@ -285,19 +281,15 @@
val dtor_exhaustN = dtorN ^ "_" ^ exhaustN
val ctor_relN = ctorN ^ "_" ^ relN
val dtor_relN = dtorN ^ "_" ^ relN
-val ctor_srelN = ctorN ^ "_" ^ srelN
-val dtor_srelN = dtorN ^ "_" ^ srelN
val inductN = "induct"
val coinductN = coN ^ inductN
val ctor_inductN = ctorN ^ "_" ^ inductN
val ctor_induct2N = ctor_inductN ^ "2"
val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
val dtor_coinductN = dtorN ^ "_" ^ coinductN
-val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN
val strong_coinductN = "strong_" ^ coinductN
val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN
val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN
-val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strong_coinductN
val hsetN = "Hset"
val hset_recN = hsetN ^ "_rec"
val set_inclN = "set_incl"
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 07 14:22:54 2013 +0200
@@ -145,7 +145,7 @@
val setssAs = mk_setss allAs;
val setssAs' = transpose setssAs;
val bis_setss = mk_setss (passiveAs @ RTs);
- val relsAsBs = map4 mk_srel_of_bnf Dss Ass Bss bnfs;
+ val relsAsBs = map4 mk_rel_of_bnf Dss Ass Bss bnfs;
val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
val sum_bdT = fst (dest_relT (fastype_of sum_bd));
@@ -226,14 +226,14 @@
val map_wpulls = map map_wpull_of_bnf bnfs;
val set_bdss = map set_bd_of_bnf bnfs;
val set_map'ss = map set_map'_of_bnf bnfs;
- val srel_congs = map srel_cong_of_bnf bnfs;
- val srel_converses = map srel_converse_of_bnf bnfs;
- val srel_defs = map srel_def_of_bnf bnfs;
- val srel_Grs = map srel_Gr_of_bnf bnfs;
- val srel_Ids = map srel_Id_of_bnf bnfs;
- val srel_monos = map srel_mono_of_bnf bnfs;
- val srel_Os = map srel_O_of_bnf bnfs;
- val srel_O_Grs = map srel_O_Gr_of_bnf bnfs;
+ val rel_congs = map rel_cong_of_bnf bnfs;
+ val rel_converseps = map rel_conversep_of_bnf bnfs;
+ val rel_defs = map rel_def_of_bnf bnfs;
+ val rel_Grps = map rel_Grp_of_bnf bnfs;
+ val rel_eqs = map rel_eq_of_bnf bnfs;
+ val rel_monos = map rel_mono_of_bnf bnfs;
+ val rel_OOs = map rel_OO_of_bnf bnfs;
+ val rel_OO_Grps = map rel_OO_Grp_of_bnf bnfs;
val timer = time (timer "Extracted terms & thms");
@@ -341,7 +341,7 @@
let
val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
- fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_subset (set $ (s $ x)) B);
+ fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
val prems = map2 mk_prem zs Bs;
val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) (As @ Bs) sets)
ss zs setssAs;
@@ -421,7 +421,7 @@
let
val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
- (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_subset (mk_image f $ B1) B2)));
+ (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
val image_goals = map3 mk_image_goal fs Bs B's;
fun mk_elim_goal B mapAsBs f s s' x =
fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
@@ -439,7 +439,7 @@
val mor_incl_thm =
let
- val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy;
+ val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
in
Goal.prove_sorry lthy [] []
@@ -621,12 +621,12 @@
val (set_incl_hset_thmss, set_hset_incl_hset_thmsss) =
let
fun mk_set_incl_hset s x set hset = fold_rev Logic.all (x :: ss)
- (HOLogic.mk_Trueprop (mk_subset (set $ (s $ x)) (hset $ x)));
+ (HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (hset $ x)));
fun mk_set_hset_incl_hset s x y set hset1 hset2 =
fold_rev Logic.all (x :: y :: ss)
(Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (s $ y))),
- HOLogic.mk_Trueprop (mk_subset (hset1 $ x) (hset2 $ y))));
+ HOLogic.mk_Trueprop (mk_leq (hset1 $ x) (hset2 $ y))));
val set_incl_hset_goalss =
map4 (fn s => fn x => fn sets => fn hsets =>
@@ -672,8 +672,8 @@
fun mk_set_incl_hin s x hsets1 set hsets2 T =
fold_rev Logic.all (x :: ss @ As)
(Logic.list_implies
- (map2 (fn hset => fn A => HOLogic.mk_Trueprop (mk_subset (hset $ x) A)) hsets1 As,
- HOLogic.mk_Trueprop (mk_subset (set $ (s $ x)) (mk_in As hsets2 T))));
+ (map2 (fn hset => fn A => HOLogic.mk_Trueprop (mk_leq (hset $ x) A)) hsets1 As,
+ HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (mk_in As hsets2 T))));
val set_incl_hin_goalss =
map4 (fn s => fn x => fn sets => fn hsets =>
@@ -689,12 +689,12 @@
val hset_minimal_thms =
let
fun mk_passive_prem set s x K =
- Logic.all x (HOLogic.mk_Trueprop (mk_subset (set $ (s $ x)) (K $ x)));
+ Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (K $ x)));
fun mk_active_prem s x1 K1 set x2 K2 =
fold_rev Logic.all [x1, x2]
(Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (s $ x1))),
- HOLogic.mk_Trueprop (mk_subset (K2 $ x2) (K1 $ x1))));
+ HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
val premss = map2 (fn j => fn Ks =>
map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) setssAs) ss zs Ks @
@@ -704,7 +704,7 @@
val hset_rec_minimal_thms =
let
- fun mk_conjunct j T i K x = mk_subset (mk_hset_rec ss nat i j T $ x) (K $ x);
+ fun mk_conjunct j T i K x = mk_leq (mk_hset_rec ss nat i j T $ x) (K $ x);
fun mk_concl j T Ks = list_all_free zs
(Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks zs));
val concls = map3 mk_concl ls passiveAs Kss;
@@ -723,7 +723,7 @@
goals ctss hset_rec_0ss' hset_rec_Sucss'
end;
- fun mk_conjunct j T i K x = mk_subset (mk_hset ss i j T $ x) (K $ x);
+ fun mk_conjunct j T i K x = mk_leq (mk_hset ss i j T $ x) (K $ x);
fun mk_concl j T Ks = Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks zs);
val concls = map3 mk_concl ls passiveAs Kss;
@@ -793,7 +793,7 @@
val bis_name = Binding.name_of bis_bind;
val bis_def_bind = (Thm.def_binding bis_bind, []);
- fun mk_bis_le_conjunct R B1 B2 = mk_subset R (mk_Times (B1, B2));
+ fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2));
val bis_le = Library.foldr1 HOLogic.mk_conj (map3 mk_bis_le_conjunct Rs Bs B's)
val bis_spec =
@@ -849,13 +849,12 @@
|> Thm.close_derivation
end;
- val bis_srel_thm =
+ val bis_rel_thm =
let
- fun mk_conjunct R s s' b1 b2 srel =
+ fun mk_conjunct R s s' b1 b2 rel =
list_all_free [b1, b2] (HOLogic.mk_imp
(HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
- HOLogic.mk_mem (HOLogic.mk_prod (s $ b1, s' $ b2),
- Term.list_comb (srel, passive_Id_ons @ Rs))));
+ Term.list_comb (rel, map mk_in_rel (passive_Id_ons @ Rs)) $ (s $ b1) $ (s' $ b2)));
val rhs = HOLogic.mk_conj
(bis_le, Library.foldr1 HOLogic.mk_conj
@@ -864,7 +863,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
(mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
- (K (mk_bis_srel_tac lthy m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss))
+ (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comp's map_cong0s set_map'ss))
|> Thm.close_derivation
end;
@@ -874,7 +873,7 @@
(Logic.mk_implies
(HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
- (K (mk_bis_converse_tac m bis_srel_thm srel_congs srel_converses))
+ (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converseps))
|> Thm.close_derivation;
val bis_O_thm =
@@ -888,7 +887,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
(Logic.list_implies (prems, concl)))
- (K (mk_bis_O_tac lthy m bis_srel_thm srel_congs srel_Os))
+ (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs))
|> Thm.close_derivation
end;
@@ -900,7 +899,7 @@
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
(Logic.list_implies ([coalg_prem, mor_prem], concl)))
- (mk_bis_Gr_tac bis_srel_thm srel_Grs mor_image_thms morE_thms coalg_in_thms)
+ (mk_bis_Gr_tac bis_rel_thm rel_Grps mor_image_thms morE_thms coalg_in_thms)
|> Thm.close_derivation
end;
@@ -988,7 +987,7 @@
val incl_lsbis_thms =
let
- fun mk_concl i R = HOLogic.mk_Trueprop (mk_subset R (mk_lsbis As Bs ss i));
+ fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis As Bs ss i));
val goals = map2 (fn i => fn R => fold_rev Logic.all (As @ Bs @ ss @ sRs)
(Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
in
@@ -1160,7 +1159,7 @@
val lhs = Term.list_comb (Free (isNode_name i, isNodeT), As @ [Kl, lab, kl]);
val rhs = list_exists_free [x]
(Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
- map2 mk_subset passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
+ map2 mk_leq passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
in
mk_Trueprop_eq (lhs, rhs)
end;
@@ -1184,7 +1183,7 @@
val isTree =
let
val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl);
- val Field = mk_subset Kl (mk_Field (mk_clists sum_sbd));
+ val Field = mk_leq Kl (mk_Field (mk_clists sum_sbd));
val prefCl = mk_prefCl Kl;
val tree = mk_Ball Kl (Term.absfree kl'
@@ -1345,7 +1344,7 @@
fun mk_inner_conjunct j T i x set i' carT =
HOLogic.mk_imp (HOLogic.mk_conj (mk_Kl_lab carT, mk_lab_kl i x),
- mk_subset (set $ x) (mk_hset strTAs i' j T $ Kl_lab));
+ mk_leq (set $ x) (mk_hset strTAs i' j T $ Kl_lab));
fun mk_conjunct j T i x set =
Library.foldr1 HOLogic.mk_conj (map2 (mk_inner_conjunct j T i x set) ks carTAs);
@@ -1562,7 +1561,7 @@
val Lev_sbd_thms =
let
- fun mk_conjunct i z = mk_subset (mk_Lev ss nat i $ z) (mk_Field (mk_clists sum_sbd));
+ fun mk_conjunct i z = mk_leq (mk_Lev ss nat i $ z) (mk_Field (mk_clists sum_sbd));
val goal = list_all_free zs
(Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
@@ -1654,7 +1653,7 @@
val set_rv_Lev_thmsss = if m = 0 then replicate n (replicate n []) else
let
fun mk_case s sets z z_free = Term.absfree z_free (Library.foldr1 HOLogic.mk_conj
- (map2 (fn set => fn A => mk_subset (set $ (s $ z)) A) (take m sets) As));
+ (map2 (fn set => fn A => mk_leq (set $ (s $ z)) A) (take m sets) As));
fun mk_conjunct i z B = HOLogic.mk_imp
(HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), HOLogic.mk_mem (z, B)),
@@ -1980,7 +1979,7 @@
let
val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs dtors TRs);
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map2 (fn R => fn T => mk_subset R (Id_const T)) TRs Ts));
+ (map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl));
in
`split_conj_thm (Goal.prove_sorry lthy [] [] goal
@@ -2205,49 +2204,46 @@
val timer = time (timer "corec definitions & thms");
(* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
- val (dtor_map_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_coinduct_thm,
- dtor_map_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, dtor_strong_coinduct_thm) =
+ val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm,
+ dtor_map_strong_coinduct_thm, dtor_strong_coinduct_thm) =
let
val zs = Jzs1 @ Jzs2;
val frees = phis @ zs;
- fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_Id_on passive_UNIVs;
-
fun mk_phi strong_eq phi z1 z2 = if strong_eq
then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2)
(HOLogic.mk_disj (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2))))
else phi;
- fun phi_srels strong_eq = map4 (fn phi => fn T => fn z1 => fn z2 =>
- HOLogic.Collect_const (HOLogic.mk_prodT (T, T)) $
- HOLogic.mk_split (mk_phi strong_eq phi z1 z2)) phis Ts Jzs1 Jzs2;
-
- val srels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
+ fun phi_rels strong_eq =
+ map3 (fn phi => fn z1 => fn z2 => mk_phi strong_eq phi z1 z2) phis Jzs1 Jzs2;
+
+ val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map3 mk_concl phis Jzs1 Jzs2));
- fun mk_srel_prem strong_eq phi dtor srel Jz Jz_copy =
+ fun mk_rel_prem strong_eq phi dtor rel Jz Jz_copy =
let
- val concl = HOLogic.mk_mem (HOLogic.mk_tuple [dtor $ Jz, dtor $ Jz_copy],
- Term.list_comb (srel, mk_Ids strong_eq @ phi_srels strong_eq));
+ val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phi_rels strong_eq) $
+ (dtor $ Jz) $ (dtor $ Jz_copy);
in
HOLogic.mk_Trueprop
(list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
end;
- val srel_prems = map5 (mk_srel_prem false) phis dtors srels Jzs Jzs_copy;
- val srel_strong_prems = map5 (mk_srel_prem true) phis dtors srels Jzs Jzs_copy;
-
- val dtor_srel_coinduct_goal =
- fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl));
- val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []);
-
- val dtor_srel_coinduct = unfold_thms lthy @{thms Id_on_UNIV}
- (Goal.prove_sorry lthy [] [] dtor_srel_coinduct_goal
- (K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
- |> Thm.close_derivation);
+ val rel_prems = map5 (mk_rel_prem false) phis dtors rels Jzs Jzs_copy;
+ val rel_strong_prems = map5 (mk_rel_prem true) phis dtors rels Jzs Jzs_copy;
+
+ val dtor_coinduct_goal =
+ fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
+ val coinduct_params = rev (Term.add_tfrees dtor_coinduct_goal []);
+
+ val dtor_coinduct =
+ Goal.prove_sorry lthy [] [] dtor_coinduct_goal
+ (K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs))
+ |> Thm.close_derivation;
fun mk_prem strong_eq phi dtor map_nth sets Jz Jz_copy FJz =
let
@@ -2277,19 +2273,18 @@
val strong_prems = mk_prems true;
val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl));
- val dtor_map_coinduct = Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal
- (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
+ val dtor_map_coinduct =
+ Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal
+ (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
|> Thm.close_derivation;
val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
- val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
+ val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
(Goal.prove_sorry lthy [] []
- (fold_rev Logic.all zs (Logic.list_implies (srel_strong_prems, concl)))
- (fn _ =>
- mk_dtor_srel_strong_coinduct_tac lthy
- m cTs cts dtor_srel_coinduct srel_monos srel_Ids))
+ (fold_rev Logic.all zs (Logic.list_implies (rel_strong_prems, concl)))
+ (K (mk_dtor_strong_coinduct_tac lthy m cTs cts dtor_coinduct rel_monos rel_eqs)))
|> Thm.close_derivation;
val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
@@ -2298,15 +2293,9 @@
(K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def
(tcoalg_thm RS bis_Id_on_thm))))
|> Thm.close_derivation;
-
- val rel_of_srel_thms =
- srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
-
- val dtor_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_coinduct;
- val dtor_strong_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_strong_coinduct;
in
- (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_srel_coinduct,
- dtor_coinduct, dtor_map_strong_coinduct, dtor_srel_strong_coinduct, dtor_strong_coinduct)
+ (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []),
+ dtor_coinduct, dtor_map_strong_coinduct, dtor_strong_coinduct)
end;
val timer = time (timer "coinduction");
@@ -2471,7 +2460,7 @@
val le_goals = map
(fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
- (mk_goals (uncurry mk_subset));
+ (mk_goals (uncurry mk_leq));
val set_le_thmss = map split_conj_thm
(map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss =>
Goal.prove_sorry lthy [] [] goal
@@ -2654,7 +2643,7 @@
val pick_col_thmss =
let
fun mk_conjunct AX Jpair pick thePull col =
- HOLogic.mk_imp (HOLogic.mk_mem (Jpair, thePull), mk_subset (col $ (pick $ Jpair)) AX);
+ HOLogic.mk_imp (HOLogic.mk_mem (Jpair, thePull), mk_leq (col $ (pick $ Jpair)) AX);
fun mk_concl AX cols =
list_all_free Jpairs (Library.foldr1 HOLogic.mk_conj
@@ -2707,10 +2696,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 srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
+ val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
+ bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_OO_Grp_tacs;
val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
let
@@ -2915,57 +2904,38 @@
val dtor_set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms;
- val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
- val Jsrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Jbnfs;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
val Jrels = map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
- val JsrelRs = map (fn Jsrel => Term.list_comb (Jsrel, JRs)) Jsrels;
- val srelRs = map (fn srel => Term.list_comb (srel, JRs @ JsrelRs)) srels;
- val Jrelphis = map (fn Jsrel => Term.list_comb (Jsrel, Jphis)) Jrels;
- val relphis = map (fn srel => Term.list_comb (srel, Jphis @ Jrelphis)) rels;
-
- val in_srels = map in_srel_of_bnf bnfs;
- val in_Jsrels = map in_srel_of_bnf Jbnfs;
- val Jsrel_defs = map srel_def_of_bnf Jbnfs;
+ val Jrelphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jrels;
+ val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels;
+
+ 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 folded_dtor_map_thms = map fold_maps dtor_map_thms;
val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss;
val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss;
- val dtor_Jsrel_thms =
+ val dtor_Jrel_thms =
let
- fun mk_goal Jz Jz' dtor dtor' JsrelR srelR = fold_rev Logic.all (Jz :: Jz' :: JRs)
- (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JsrelR),
- HOLogic.mk_mem (HOLogic.mk_prod (dtor $ Jz, dtor' $ Jz'), srelR)));
- val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs;
+ fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
+ (mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')));
+ val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
in
- map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
+ map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_dtor_srel_tac lthy in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
+ (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets
dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
+ ks goals in_rels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss
dtor_set_set_incl_thmsss
end;
- val dtor_Jrel_thms =
- let
- fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
- (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz')));
- val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
- in
- map3 (fn goal => fn srel_def => fn dtor_Jsrel =>
- Goal.prove_sorry lthy [] [] goal
- (mk_ctor_or_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel)
- |> Thm.close_derivation)
- goals srel_defs dtor_Jsrel_thms
- end;
-
val timer = time (timer "additional properties");
val ls' = if m = 1 then [0] else ls;
@@ -2981,10 +2951,6 @@
(dtor_relN, map single dtor_Jrel_thms),
(dtor_set_inclN, dtor_set_incl_thmss),
(dtor_set_set_inclN, map flat dtor_set_set_incl_thmsss)] @
- (if note_all then
- [(dtor_srelN, map single dtor_Jsrel_thms)]
- else
- []) @
map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' folded_dtor_set_thmss
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
@@ -2999,12 +2965,7 @@
[(dtor_coinductN, [dtor_coinduct_thm]),
(dtor_map_coinductN, [dtor_map_coinduct_thm]),
(dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
- (dtor_strong_coinductN, [dtor_strong_coinduct_thm])] @
- (if note_all then
- [(dtor_srel_coinductN, [dtor_srel_coinduct_thm]),
- (dtor_srel_strong_coinductN, [dtor_srel_strong_coinduct_thm])]
- else
- [])
+ (dtor_strong_coinductN, [dtor_strong_coinduct_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue May 07 14:22:54 2013 +0200
@@ -18,7 +18,7 @@
val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
- val mk_bis_srel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
+ val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
thm list list -> tactic
val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
{prems: 'a, context: Proof.context} -> tactic
@@ -46,10 +46,10 @@
val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
thm -> thm -> tactic
val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
- val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
- val mk_dtor_srel_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
+ val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
+ val mk_dtor_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
cterm option list -> thm -> thm list -> thm list -> tactic
- val mk_dtor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
@@ -259,50 +259,48 @@
EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
atac, atac, rtac (hset_def RS sym)] 1
-fun mk_bis_srel_tac ctxt m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
+fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comps map_cong0s set_mapss =
let
- val n = length srel_O_Grs;
- val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ srel_O_Grs);
+ val n = length rel_OO_Grps;
+ val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
- fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) =
+ fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
- rtac (srel_O_Gr RS equalityD2 RS set_mp),
- rtac @{thm relcompI}, rtac @{thm converseI},
+ rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
+ rtac @{thm relcomppI}, rtac @{thm conversepI},
EVERY' (map (fn thm =>
- EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
- rtac CollectI,
+ EVERY' [rtac @{thm GrpI},
+ rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
+ REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac,
+ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
CONJ_WRAP' (fn (i, thm) =>
if i <= m
then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
- etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}]
+ etac @{thm image_mono}, rtac @{thm image_subsetI},
+ etac @{thm Collect_split_in_relI[OF Id_onI]}]
else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
- rtac trans_fun_cong_image_id_id_apply, atac])
- (1 upto (m + n) ~~ set_maps),
- rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
- REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
+ rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
+ (1 upto (m + n) ~~ set_maps)])
@{thms fst_diag_id snd_diag_id})];
- fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) =
+ fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
etac allE, etac allE, etac impE, atac,
- dtac (srel_O_Gr RS equalityD1 RS set_mp),
- REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
- REPEAT_DETERM o dtac Pair_eqD,
- REPEAT_DETERM o etac conjE,
+ dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}),
+ REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
+ @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
hyp_subst_tac ctxt,
- REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
- etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+ atac, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
REPEAT_DETERM_N n o rtac refl,
- etac sym, rtac CollectI,
+ atac, rtac CollectI,
CONJ_WRAP' (fn (i, thm) =>
if i <= m
then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
@@ -316,45 +314,45 @@
etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
end;
-fun mk_bis_converse_tac m bis_srel srel_congs srel_converses =
- EVERY' [stac bis_srel, dtac (bis_srel RS iffD1),
+fun mk_bis_converse_tac m bis_rel rel_congs rel_converseps =
+ EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
- rtac equalityD2, rtac @{thm converse_Times}])) srel_congs,
- CONJ_WRAP' (fn (srel_cong, srel_converse) =>
- EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
- rtac (srel_cong RS trans),
- REPEAT_DETERM_N m o rtac (@{thm converse_Id_on} RS sym),
- REPEAT_DETERM_N (length srel_congs) o rtac refl,
- rtac srel_converse,
+ rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
+ CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
+ EVERY' [rtac allI, rtac allI, rtac impI,
+ rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
+ REPEAT_DETERM_N m o rtac @{thm conversep_in_rel_Id_on},
+ REPEAT_DETERM_N (length rel_congs) o rtac @{thm conversep_in_rel},
+ rtac (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
REPEAT_DETERM o etac allE,
- rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
+ rtac @{thm conversepI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1;
-fun mk_bis_O_tac ctxt m bis_srel srel_congs srel_Os =
- EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),
+fun mk_bis_O_tac ctxt m bis_rel rel_congs rel_OOs =
+ EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
- CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
- CONJ_WRAP' (fn (srel_cong, srel_O) =>
- EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
- rtac (srel_cong RS trans),
- REPEAT_DETERM_N m o rtac @{thm Id_on_Comp},
- REPEAT_DETERM_N (length srel_congs) o rtac refl,
- rtac srel_O,
+ CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
+ CONJ_WRAP' (fn (rel_cong, rel_OO) =>
+ EVERY' [rtac allI, rtac allI, rtac impI,
+ rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
+ REPEAT_DETERM_N m o rtac @{thm relcompp_in_rel_Id_on},
+ REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
+ rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
etac @{thm relcompE},
REPEAT_DETERM o dtac Pair_eqD,
etac conjE, hyp_subst_tac ctxt,
- REPEAT_DETERM o etac allE, rtac @{thm relcompI},
- etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
+ REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
+ etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
-fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins
+fun mk_bis_Gr_tac bis_rel rel_Grps mor_images morEs coalg_ins
{context = ctxt, prems = _} =
- unfold_thms_tac ctxt (bis_srel :: @{thm Id_on_Gr} :: srel_Grs) THEN
+ unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) 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) =>
- EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrI}, etac coalg_in,
- etac @{thm GrD1}, etac (morE RS trans), etac @{thm GrD1},
- etac (@{thm GrD2} RS arg_cong)]) (coalg_ins ~~ morEs)] 1;
+ EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrpI}, etac (morE RS trans),
+ etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}])
+ (coalg_ins ~~ morEs)] 1;
fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =
let
@@ -1130,26 +1128,31 @@
(corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
etac unfold_unique_mor 1;
-fun mk_dtor_srel_coinduct_tac ks raw_coind bis_srel =
- EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI,
- CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
- CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI,
- REPEAT_DETERM o etac allE, etac mp, etac CollectE, etac @{thm splitD}])) ks,
+fun mk_dtor_coinduct_tac m raw_coind bis_rel rel_congs =
+ EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI,
+ CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]}))
+ rel_congs,
+ CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI,
+ REPEAT_DETERM o etac allE, rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
+ REPEAT_DETERM_N m o rtac @{thm in_rel_Id_on_UNIV[symmetric]},
+ REPEAT_DETERM_N (length rel_congs) o rtac @{thm in_rel_Collect_split_eq[symmetric]},
+ etac mp, etac CollectE, etac @{thm splitD}])
+ rel_congs,
rtac impI, REPEAT_DETERM o etac conjE,
CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
- rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
+ rtac CollectI, etac @{thm prod_caseI}])) rel_congs] 1;
-fun mk_dtor_srel_strong_coinduct_tac ctxt m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
- EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_srel_coinduct),
- EVERY' (map2 (fn srel_mono => fn srel_Id =>
+fun mk_dtor_strong_coinduct_tac ctxt m cTs cts dtor_coinduct rel_monos rel_eqs =
+ EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct),
+ EVERY' (map2 (fn rel_mono => fn rel_eq =>
EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
- etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (srel_mono RS set_mp),
- REPEAT_DETERM_N m o rtac @{thm subset_refl},
- REPEAT_DETERM_N (length srel_monos) o rtac @{thm Id_subset},
- rtac (srel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
- srel_monos srel_Ids),
+ etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (rel_mono RS @{thm predicate2D}),
+ REPEAT_DETERM_N m o rtac @{thm order_refl},
+ REPEAT_DETERM_N (length rel_monos) o rtac @{thm eq_subset},
+ rtac (rel_eq RS sym RS @{thm eq_refl} RS @{thm predicate2D}), rtac refl])
+ rel_monos rel_eqs),
rtac impI, REPEAT_DETERM o etac conjE,
- CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) srel_Ids] 1;
+ CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_eqs] 1;
fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
let
@@ -1501,27 +1504,27 @@
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
-fun mk_dtor_srel_tac ctxt in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject
+fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets dtor_inject
dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
let
val m = length dtor_set_incls;
val n = length dtor_set_set_inclss;
val (passive_set_maps, active_set_maps) = chop m set_maps;
- val in_Jsrel = nth in_Jsrels (i - 1);
+ val in_Jrel = nth in_Jrels (i - 1);
val if_tac =
- EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
- rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+ rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
EVERY' (map2 (fn set_map => fn set_incl =>
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
etac (set_incl RS @{thm subset_trans})])
passive_set_maps dtor_set_incls),
- CONJ_WRAP' (fn (in_Jsrel, (set_map, dtor_set_set_incls)) =>
- EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI},
- rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ CONJ_WRAP' (fn (in_Jrel, (set_map, dtor_set_set_incls)) =>
+ EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI,
+ rtac @{thm prod_caseI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
rtac conjI, rtac refl, rtac refl])
- (in_Jsrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
+ (in_Jrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
@@ -1529,30 +1532,38 @@
rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
@{thms fst_conv snd_conv}];
val only_if_tac =
- EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
- rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+ rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn (dtor_set, passive_set_map) =>
EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map,
rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
- (fn (active_set_map, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
+ (fn (active_set_map, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
rtac active_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
- dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
+ dtac @{thm ssubst_mem[OF pair_collapse]},
+ REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
+ @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
+ hyp_subst_tac ctxt,
+ dtac (in_Jrel RS iffD1),
dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
- dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
- hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
- (rev (active_set_maps ~~ in_Jsrels))])
+ TRY o
+ EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
+ REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
+ (rev (active_set_maps ~~ in_Jrels))])
(dtor_sets ~~ passive_set_maps),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
- EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
- dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
- dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jsrels),
+ EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
+ dtac @{thm ssubst_mem[OF pair_collapse]},
+ REPEAT_DETERM o
+ eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
+ hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
+ dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
atac]]
in
EVERY' [rtac iffI, if_tac, only_if_tac] 1
--- a/src/HOL/BNF/Tools/bnf_gfp_util.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_util.ML Tue May 07 14:22:54 2013 +0200
@@ -19,6 +19,7 @@
val mk_congruent: term -> term -> term
val mk_clists: term -> term
val mk_Id_on: term -> term
+ val mk_in_rel: term -> term
val mk_equiv: term -> term -> term
val mk_fromCard: term -> term -> term
val mk_list_rec: term -> term -> term
@@ -65,6 +66,11 @@
val AAT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT AT);
in Const (@{const_name Id_on}, AT --> AAT) $ A end;
+fun mk_in_rel R =
+ let
+ val ((A, B), RT) = `dest_relT (fastype_of R);
+ in Const (@{const_name in_rel}, RT --> mk_pred2T A B) $ R end;
+
fun mk_Times (A, B) =
let val AT = HOLogic.dest_setT (fastype_of A);
in mk_Sigma (A, Term.absdummy AT B) end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 07 14:22:54 2013 +0200
@@ -254,7 +254,7 @@
val alg_set_thms =
let
val alg_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
- fun mk_prem x set B = HOLogic.mk_Trueprop (mk_subset (set $ x) B);
+ fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
val premss = map2 ((fn x => fn sets => map2 (mk_prem x) sets (As @ Bs))) xFs setssAs;
val concls = map3 mk_concl ss xFs Bs;
@@ -349,7 +349,7 @@
let
val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
- (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_subset (mk_image f $ B1) B2)));
+ (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
val image_goals = map3 mk_image_goal fs Bs B's;
fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
(HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
@@ -366,7 +366,7 @@
val mor_incl_thm =
let
- val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy;
+ val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
in
Goal.prove_sorry lthy [] []
@@ -392,7 +392,7 @@
val mor_inv_thm =
let
- fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_subset (mk_image inv_f $ B') B,
+ fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_leq (mk_image inv_f $ B') B,
HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
val prems = map HOLogic.mk_Trueprop
([mk_mor Bs ss B's s's fs,
@@ -672,7 +672,7 @@
|> Thm.close_derivation;
val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
- val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_subset min_algss Bs);
+ val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
val least_cT = certifyT lthy suc_bdT;
val least_ct = certify lthy (Term.absfree idx' least_conjunction);
@@ -748,7 +748,7 @@
val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (As @ Bs @ ss)
- (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_subset min_alg B))))
+ (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B))))
(K (mk_least_min_alg_tac def least_min_algs_thm))
|> Thm.close_derivation;
@@ -1695,10 +1695,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 srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
+ val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
+ bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_OO_Grp_tacs;
val ctor_witss =
let
@@ -1745,20 +1745,15 @@
val timer = time (timer "registered new datatypes as BNFs");
- val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
- val Isrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Ibnfs;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
- val IsrelRs = map (fn Isrel => Term.list_comb (Isrel, IRs)) Isrels;
- val srelRs = map (fn srel => Term.list_comb (srel, IRs @ IsrelRs)) srels;
- val Irelphis = map (fn Isrel => Term.list_comb (Isrel, Iphis)) Irels;
- val relphis = map (fn srel => Term.list_comb (srel, Iphis @ Irelphis)) rels;
+ val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels;
+ val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels;
- val in_srels = map in_srel_of_bnf bnfs;
- val in_Isrels = map in_srel_of_bnf Ibnfs;
- val srel_defs = map srel_def_of_bnf bnfs;
- val Isrel_defs = map srel_def_of_bnf Ibnfs;
+ val in_rels = map in_rel_of_bnf bnfs;
+ val in_Irels = map in_rel_of_bnf Ibnfs;
+ val rel_defs = map rel_def_of_bnf bnfs;
val Irel_defs = map rel_def_of_bnf Ibnfs;
val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
@@ -1767,38 +1762,24 @@
val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss;
val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss;
- val ctor_Isrel_thms =
+ val ctor_Irel_thms =
let
- fun mk_goal xF yF ctor ctor' IsrelR srelR = fold_rev Logic.all (xF :: yF :: IRs)
- (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IsrelR),
- HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), srelR)));
- val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs;
+ fun mk_goal xF yF ctor ctor' Irelphi relphi = fold_rev Logic.all (xF :: yF :: Iphis)
+ (mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF));
+ val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
in
- map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
+ map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_ctor_srel_tac lthy in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
+ (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets
ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
+ ks goals in_rels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss
ctor_set_set_incl_thmsss
end;
- val ctor_Irel_thms =
- let
- fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
- (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF));
- val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
- in
- map3 (fn goal => fn srel_def => fn ctor_Isrel =>
- Goal.prove_sorry lthy [] [] goal
- (mk_ctor_or_dtor_rel_tac srel_def Irel_defs Isrel_defs ctor_Isrel)
- |> Thm.close_derivation)
- goals srel_defs ctor_Isrel_thms
- end;
-
val timer = time (timer "additional properties");
val ls' = if m = 1 then [0] else ls
@@ -1813,10 +1794,6 @@
(ctor_relN, map single ctor_Irel_thms),
(ctor_set_inclN, ctor_set_incl_thmss),
(ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @
- (if note_all then
- [(ctor_srelN, map single ctor_Isrel_thms)]
- else
- []) @
map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_ctor_set_thmss
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Tue May 07 14:22:54 2013 +0200
@@ -23,7 +23,7 @@
val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
- val mk_ctor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
@@ -774,32 +774,32 @@
EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_ctor_srel_tac ctxt in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
+fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets ctor_inject
ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
let
val m = length ctor_set_incls;
val n = length ctor_set_set_inclss;
val (passive_set_maps, active_set_maps) = chop m set_maps;
- val in_Isrel = nth in_Isrels (i - 1);
+ val in_Irel = nth in_Irels (i - 1);
val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
val if_tac =
- EVERY' [dtac (in_Isrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
- rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+ rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
EVERY' (map2 (fn set_map => fn ctor_set_incl =>
EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
passive_set_maps ctor_set_incls),
- CONJ_WRAP' (fn (in_Isrel, (set_map, ctor_set_set_incls)) =>
- EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI},
- rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ CONJ_WRAP' (fn (in_Irel, (set_map, ctor_set_set_incls)) =>
+ EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI,
+ rtac @{thm prod_caseI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn thm =>
EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
ctor_set_set_incls,
rtac conjI, rtac refl, rtac refl])
- (in_Isrels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
+ (in_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
@@ -808,29 +808,37 @@
etac eq_arg_cong_ctor_dtor])
fst_snd_convs];
val only_if_tac =
- EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
- rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
+ rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn (ctor_set, passive_set_map) =>
EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least},
rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
rtac passive_set_map, rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
- (fn (active_set_map, in_Isrel) => EVERY' [rtac ord_eq_le_trans,
+ (fn (active_set_map, in_Irel) => EVERY' [rtac ord_eq_le_trans,
rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map, rtac @{thm UN_least},
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
- dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
- dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
- dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
- hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
- (rev (active_set_maps ~~ in_Isrels))])
+ dtac @{thm ssubst_mem[OF pair_collapse]},
+ REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
+ @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
+ hyp_subst_tac ctxt,
+ dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
+ TRY o
+ EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
+ REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
+ (rev (active_set_maps ~~ in_Irels))])
(ctor_sets ~~ passive_set_maps),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
- EVERY' (map (fn in_Isrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
- dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
- dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Isrels),
+ EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
+ dtac @{thm ssubst_mem[OF pair_collapse]},
+ REPEAT_DETERM o
+ eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
+ hyp_subst_tac ctxt,
+ dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac])
+ in_Irels),
atac]]
in
EVERY' [rtac iffI, if_tac, only_if_tac] 1
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Tue May 07 14:22:54 2013 +0200
@@ -22,7 +22,6 @@
val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
val mk_Abs_inj_thm: thm -> thm
- val simple_srel_O_Gr_tac: Proof.context -> tactic
val mk_ctor_or_dtor_rel_tac:
thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
@@ -86,9 +85,6 @@
gen_tac
end;
-fun simple_srel_O_Gr_tac ctxt =
- unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
-
fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
unfold_thms_tac ctxt IJrel_defs THEN
rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
--- a/src/HOL/BNF/Tools/bnf_util.ML Tue May 07 11:27:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Tue May 07 14:22:54 2013 +0200
@@ -77,6 +77,7 @@
val mk_optionT: typ -> typ
val mk_relT: typ * typ -> typ
val dest_relT: typ -> typ * typ
+ val dest_pred2T: typ -> typ * typ
val mk_sumT: typ * typ -> typ
val ctwo: term
@@ -89,6 +90,7 @@
val mk_Card_order: term -> term
val mk_Field: term -> term
val mk_Gr: term -> term -> term
+ val mk_Grp: term -> term -> term
val mk_IfN: typ -> term list -> term list -> term
val mk_Trueprop_eq: term * term -> term
val mk_UNION: term -> term -> term
@@ -101,14 +103,16 @@
val mk_cinfinite: term -> term
val mk_collect: term list -> typ -> term
val mk_converse: term -> term
+ val mk_conversep: term -> term
val mk_cprod: term -> term -> term
val mk_csum: term -> term -> term
val mk_dir_image: term -> term -> term
val mk_image: term -> term
val mk_in: term list -> term list -> typ -> term
+ val mk_leq: term -> term -> term
val mk_ordLeq: term -> term -> term
val mk_rel_comp: term * term -> term
- val mk_subset: term -> term -> term
+ val mk_rel_compp: term * term -> term
val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
val rapp: term -> term -> term
@@ -386,6 +390,7 @@
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;
+val dest_pred2T = apsnd Term.domain_type o Term.dest_funT;
fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]);
fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT;
@@ -422,6 +427,23 @@
let val ((AT, BT), FT) = `dest_funT (fastype_of f);
in Const (@{const_name Gr}, HOLogic.mk_setT AT --> FT --> mk_relT (AT, BT)) $ A $ f end;
+fun mk_conversep R =
+ let
+ val RT = dest_pred2T (fastype_of R);
+ val RST = mk_pred2T (snd RT) (fst RT);
+ in Const (@{const_name conversep}, fastype_of R --> RST) $ R end;
+
+fun mk_rel_compp (R, S) =
+ let
+ val RT = fastype_of R;
+ val ST = fastype_of S;
+ val RST = mk_pred2T (fst (dest_pred2T RT)) (snd (dest_pred2T ST));
+ in Const (@{const_name relcompp}, RT --> ST --> RST) $ R $ S end;
+
+fun mk_Grp A f =
+ let val ((AT, BT), FT) = `dest_funT (fastype_of f);
+ in Const (@{const_name Grp}, HOLogic.mk_setT AT --> FT --> mk_pred2T AT BT) $ A $ f end;
+
fun mk_image f =
let val (T, U) = dest_funT (fastype_of f);
in Const (@{const_name image},
@@ -528,7 +550,7 @@
A $ B1 $ B2 $ f1 $ f2 $ e1 $ e2 $ p1 $ p2)
end;
-fun mk_subset t1 t2 =
+fun mk_leq t1 t2 =
Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;
fun mk_card_binop binop typop t1 t2 =