got rid of the set based relator---use (binary) predicate based relator instead
authortraytel
Tue May 07 14:22:54 2013 +0200 (2013-05-07)
changeset 51893596baae88a88
parent 51892 e5432ec161ff
child 51894 7c43b8df0f5d
child 51896 1cf1fe22145d
got rid of the set based relator---use (binary) predicate based relator instead
src/HOL/BNF/BNF_Comp.thy
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/BNF_Util.thy
src/HOL/BNF/Basic_BNFs.thy
src/HOL/BNF/More_BNFs.thy
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_comp_tactics.ML
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_def_tactics.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_fp_util.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_gfp_util.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
src/HOL/BNF/Tools/bnf_tactics.ML
src/HOL/BNF/Tools/bnf_util.ML
     1.1 --- a/src/HOL/BNF/BNF_Comp.thy	Tue May 07 11:27:29 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Comp.thy	Tue May 07 14:22:54 2013 +0200
     1.3 @@ -73,6 +73,12 @@
     1.4  lemma O_Gr_cong: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
     1.5  by simp
     1.6  
     1.7 +lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
     1.8 +unfolding Grp_def fun_eq_iff relcompp.simps by auto
     1.9 +
    1.10 +lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
    1.11 +by simp
    1.12 +
    1.13  ML_file "Tools/bnf_comp_tactics.ML"
    1.14  ML_file "Tools/bnf_comp.ML"
    1.15  
     2.1 --- a/src/HOL/BNF/BNF_Def.thy	Tue May 07 11:27:29 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_Def.thy	Tue May 07 14:22:54 2013 +0200
     2.3 @@ -21,10 +21,18 @@
     2.4  "R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
     2.5  unfolding converse_def by auto
     2.6  
     2.7 +lemma conversep_mono:
     2.8 +"R1 ^--1 \<le> R2 ^--1 \<longleftrightarrow> R1 \<le> R2"
     2.9 +unfolding conversep.simps by auto
    2.10 +
    2.11  lemma converse_shift:
    2.12  "R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
    2.13  unfolding converse_def by auto
    2.14  
    2.15 +lemma conversep_shift:
    2.16 +"R1 \<le> R2 ^--1 \<Longrightarrow> R1 ^--1 \<le> R2"
    2.17 +unfolding conversep.simps by auto
    2.18 +
    2.19  definition convol ("<_ , _>") where
    2.20  "<f , g> \<equiv> %a. (f a, g a)"
    2.21  
    2.22 @@ -42,6 +50,10 @@
    2.23  "\<lbrakk>f x = f' x; g x = g' x; P x\<rbrakk> \<Longrightarrow> <f , g> x \<in> {(f' a, g' a) |a. P a}"
    2.24  unfolding convol_def by auto
    2.25  
    2.26 +lemma convol_mem_GrpI:
    2.27 +"\<lbrakk>g x = g' x; x \<in> A\<rbrakk> \<Longrightarrow> <id , g> x \<in> (Collect (split (Grp A g)))"
    2.28 +unfolding convol_def Grp_def by auto
    2.29 +
    2.30  definition csquare where
    2.31  "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
    2.32  
    2.33 @@ -91,48 +103,111 @@
    2.34  lemma Id_alt: "Id = Gr UNIV id"
    2.35  unfolding Gr_def by auto
    2.36  
    2.37 +lemma eq_alt: "op = = Grp UNIV id"
    2.38 +unfolding Grp_def by auto
    2.39 +
    2.40 +lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1"
    2.41 +  by auto
    2.42 +
    2.43 +lemma eq_OOI: "R = op = \<Longrightarrow> R = R OO R"
    2.44 +  by auto
    2.45 +
    2.46  lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f"
    2.47  unfolding Gr_def by auto
    2.48  
    2.49 +lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f"
    2.50 +unfolding Grp_def by auto
    2.51 +
    2.52 +lemma Grp_UNIV_idI: "x = y \<Longrightarrow> Grp UNIV id x y"
    2.53 +unfolding Grp_def by auto
    2.54 +
    2.55  lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f"
    2.56  unfolding Gr_def by auto
    2.57  
    2.58 +lemma Grp_mono: "A \<le> B \<Longrightarrow> Grp A f \<le> Grp B f"
    2.59 +unfolding Grp_def by auto
    2.60 +
    2.61 +lemma GrpI: "\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> Grp A f x y"
    2.62 +unfolding Grp_def by auto
    2.63 +
    2.64 +lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
    2.65 +unfolding Grp_def by auto
    2.66 +
    2.67 +lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
    2.68 +unfolding Grp_def o_def by auto
    2.69 +
    2.70 +lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
    2.71 +unfolding Grp_def o_def by auto
    2.72 +
    2.73  lemma wpull_Gr:
    2.74  "wpull (Gr A f) A (f ` A) f id fst snd"
    2.75  unfolding wpull_def Gr_def by auto
    2.76  
    2.77 +lemma wpull_Grp:
    2.78 +"wpull (Collect (split (Grp A f))) A (f ` A) f id fst snd"
    2.79 +unfolding wpull_def Grp_def by auto
    2.80 +
    2.81  definition "pick_middle P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
    2.82  
    2.83 +definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
    2.84 +
    2.85  lemma pick_middle:
    2.86  "(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"
    2.87 -unfolding pick_middle_def apply(rule someI_ex)
    2.88 -using assms unfolding relcomp_def by auto
    2.89 +unfolding pick_middle_def apply(rule someI_ex) by auto
    2.90 +
    2.91 +lemma pick_middlep:
    2.92 +"(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c"
    2.93 +unfolding pick_middlep_def apply(rule someI_ex) by auto
    2.94  
    2.95  definition fstO where "fstO P Q ac = (fst ac, pick_middle P Q (fst ac) (snd ac))"
    2.96  definition sndO where "sndO P Q ac = (pick_middle P Q (fst ac) (snd ac), snd ac)"
    2.97  
    2.98 +definition fstOp where "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))"
    2.99 +definition sndOp where "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))"
   2.100 +
   2.101  lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
   2.102 -unfolding fstO_def
   2.103 -by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct1])
   2.104 +unfolding fstO_def by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct1])
   2.105 +
   2.106 +lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)"
   2.107 +unfolding fstOp_def mem_Collect_eq
   2.108 +by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct1])
   2.109  
   2.110  lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
   2.111  unfolding comp_def fstO_def by simp
   2.112  
   2.113 +lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc"
   2.114 +unfolding comp_def fstOp_def by simp
   2.115 +
   2.116  lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc"
   2.117  unfolding comp_def sndO_def by simp
   2.118  
   2.119 +lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc"
   2.120 +unfolding comp_def sndOp_def by simp
   2.121 +
   2.122  lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
   2.123  unfolding sndO_def
   2.124  by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct2])
   2.125  
   2.126 +lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)"
   2.127 +unfolding sndOp_def mem_Collect_eq
   2.128 +by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct2])
   2.129 +
   2.130  lemma csquare_fstO_sndO:
   2.131  "csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
   2.132  unfolding csquare_def fstO_def sndO_def using pick_middle by simp
   2.133  
   2.134 +lemma csquare_fstOp_sndOp:
   2.135 +"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
   2.136 +unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
   2.137 +
   2.138  lemma wppull_fstO_sndO:
   2.139  shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
   2.140  using pick_middle unfolding wppull_def fstO_def sndO_def relcomp_def by auto
   2.141  
   2.142 +lemma wppull_fstOp_sndOp:
   2.143 +shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q)) snd fst fst snd (fstOp P Q) (sndOp P Q)"
   2.144 +using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto
   2.145 +
   2.146  lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
   2.147  by (simp split: prod.split)
   2.148  
   2.149 @@ -142,11 +217,17 @@
   2.150  lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R"
   2.151  by auto
   2.152  
   2.153 +lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
   2.154 +by auto
   2.155 +
   2.156  lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
   2.157  unfolding o_def fun_eq_iff by simp
   2.158  
   2.159 -lemma eqset_imp_iff_pair: "A = B \<Longrightarrow> (a, b) \<in> A \<longleftrightarrow> (a, b) \<in> B"
   2.160 -by (rule eqset_imp_iff)
   2.161 +lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
   2.162 +  by auto
   2.163 +
   2.164 +lemma predicate2_cong: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
   2.165 +by metis
   2.166  
   2.167  lemma fun_cong_pair: "f = g \<Longrightarrow> f {(a, b). R a b} = g {(a, b). R a b}"
   2.168  by (rule fun_cong)
   2.169 @@ -161,4 +242,5 @@
   2.170  ML_file "Tools/bnf_def_tactics.ML"
   2.171  ML_file "Tools/bnf_def.ML"
   2.172  
   2.173 +
   2.174  end
     3.1 --- a/src/HOL/BNF/BNF_GFP.thy	Tue May 07 11:27:29 2013 +0200
     3.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Tue May 07 14:22:54 2013 +0200
     3.3 @@ -79,6 +79,9 @@
     3.4  lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}"
     3.5  by auto
     3.6  
     3.7 +lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
     3.8 +by auto
     3.9 +
    3.10  lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
    3.11  by auto
    3.12  
    3.13 @@ -100,6 +103,36 @@
    3.14  lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
    3.15  unfolding Gr_def by auto
    3.16  
    3.17 +lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
    3.18 +unfolding fun_eq_iff by auto
    3.19 +
    3.20 +lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
    3.21 +by auto
    3.22 +
    3.23 +lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    3.24 +by force
    3.25 +
    3.26 +lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
    3.27 +by auto
    3.28 +
    3.29 +lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
    3.30 +unfolding fun_eq_iff by auto
    3.31 +
    3.32 +lemmas conversep_in_rel_Id_on =
    3.33 +  trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]
    3.34 +
    3.35 +lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
    3.36 +unfolding fun_eq_iff by auto
    3.37 +
    3.38 +lemmas relcompp_in_rel_Id_on =
    3.39 +  trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]
    3.40 +
    3.41 +lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
    3.42 +unfolding Gr_def Grp_def fun_eq_iff by auto
    3.43 +
    3.44 +lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
    3.45 +unfolding fun_eq_iff by auto
    3.46 +
    3.47  definition relImage where
    3.48  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
    3.49  
     4.1 --- a/src/HOL/BNF/BNF_Util.thy	Tue May 07 11:27:29 2013 +0200
     4.2 +++ b/src/HOL/BNF/BNF_Util.thy	Tue May 07 14:22:54 2013 +0200
     4.3 @@ -60,6 +60,8 @@
     4.4  (* Operator: *)
     4.5  definition "Gr A f = {(a, f a) | a. a \<in> A}"
     4.6  
     4.7 +definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
     4.8 +
     4.9  ML_file "Tools/bnf_util.ML"
    4.10  ML_file "Tools/bnf_tactics.ML"
    4.11  
     5.1 --- a/src/HOL/BNF/Basic_BNFs.thy	Tue May 07 11:27:29 2013 +0200
     5.2 +++ b/src/HOL/BNF/Basic_BNFs.thy	Tue May 07 14:22:54 2013 +0200
     5.3 @@ -27,9 +27,12 @@
     5.4  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"
     5.5    unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
     5.6  
     5.7 +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"
     5.8 +  unfolding wpull_def Grp_def by auto
     5.9 +
    5.10  bnf ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
    5.11 -  "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
    5.12 -apply (auto simp: Gr_def fun_eq_iff natLeq_card_order natLeq_cinfinite)
    5.13 +  "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    5.14 +apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
    5.15  apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    5.16  apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    5.17  apply (rule ordLeq_transitive)
    5.18 @@ -46,8 +49,8 @@
    5.19  done
    5.20  
    5.21  bnf DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
    5.22 -  "op =::'a \<Rightarrow> 'a \<Rightarrow> bool"
    5.23 -apply (auto simp add: wpull_Gr_def Gr_def
    5.24 +  "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    5.25 +apply (auto simp add: wpull_Grp_def Grp_def
    5.26    card_order_csum natLeq_card_order card_of_card_order_on
    5.27    cinfinite_csum natLeq_cinfinite)
    5.28  apply (rule ordLess_imp_ordLeq)
    5.29 @@ -185,10 +188,10 @@
    5.30    qed
    5.31  next
    5.32    fix R S
    5.33 -  show "{p. sum_rel (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
    5.34 -        (Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O
    5.35 -        Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)"
    5.36 -  unfolding setl_def setr_def sum_rel_def Gr_def relcomp_unfold converse_unfold
    5.37 +  show "sum_rel R S =
    5.38 +        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
    5.39 +        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
    5.40 +  unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    5.41    by (fastforce split: sum.splits)
    5.42  qed (auto simp: sum_set_defs)
    5.43  
    5.44 @@ -284,10 +287,10 @@
    5.45      unfolding wpull_def by simp fast
    5.46  next
    5.47    fix R S
    5.48 -  show "{p. prod_rel (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
    5.49 -        (Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O
    5.50 -        Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)"
    5.51 -  unfolding prod_set_defs prod_rel_def Gr_def relcomp_unfold converse_unfold
    5.52 +  show "prod_rel R S =
    5.53 +        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
    5.54 +        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
    5.55 +  unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    5.56    by auto
    5.57  qed simp+
    5.58  
    5.59 @@ -385,10 +388,11 @@
    5.60    qed
    5.61  next
    5.62    fix R
    5.63 -  show "{p. fun_rel op = (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
    5.64 -        (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
    5.65 -  unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold
    5.66 -  by force
    5.67 +  show "fun_rel op = R =
    5.68 +        (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
    5.69 +         Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
    5.70 +  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
    5.71 +  by auto (force, metis pair_collapse)
    5.72  qed auto
    5.73  
    5.74  end
     6.1 --- a/src/HOL/BNF/More_BNFs.thy	Tue May 07 11:27:29 2013 +0200
     6.2 +++ b/src/HOL/BNF/More_BNFs.thy	Tue May 07 14:22:54 2013 +0200
     6.3 @@ -83,11 +83,12 @@
     6.4    thus False by simp
     6.5  next
     6.6    fix R
     6.7 -  show "{p. option_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
     6.8 -        (Gr {x. Option.set x \<subseteq> R} (Option.map fst))\<inverse> O Gr {x. Option.set x \<subseteq> R} (Option.map snd)"
     6.9 -  unfolding option_rel_unfold Gr_def relcomp_unfold converse_unfold
    6.10 +  show "option_rel R =
    6.11 +        (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
    6.12 +         Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
    6.13 +  unfolding option_rel_unfold Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
    6.14    by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
    6.15 -           split: option.splits) blast
    6.16 +           split: option.splits)
    6.17  qed
    6.18  
    6.19  lemma card_of_list_in:
    6.20 @@ -244,22 +245,22 @@
    6.21  
    6.22  lemma fset_rel_aux:
    6.23  "(\<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>
    6.24 - (a, b) \<in> (Gr {a. fset a \<subseteq> {(a, b). R a b}} (fmap fst))\<inverse> O
    6.25 -          Gr {a. fset a \<subseteq> {(a, b). R a b}} (fmap snd)" (is "?L = ?R")
    6.26 + ((Grp {a. fset a \<subseteq> {(a, b). R a b}} (fmap fst))\<inverse>\<inverse> OO
    6.27 +  Grp {a. fset a \<subseteq> {(a, b). R a b}} (fmap snd)) a b" (is "?L = ?R")
    6.28  proof
    6.29    assume ?L
    6.30    def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
    6.31    have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
    6.32    hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
    6.33 -  show ?R unfolding Gr_def relcomp_unfold converse_unfold
    6.34 -  proof (intro CollectI prod_caseI exI conjI)
    6.35 -    from * show "(R', a) = (R', fmap fst R')" using conjunct1[OF `?L`]
    6.36 -      by (clarify, transfer, auto simp add: image_def Int_def split: prod.splits)
    6.37 -    from * show "(R', b) = (R', fmap snd R')" using conjunct2[OF `?L`]
    6.38 -      by (clarify, transfer, auto simp add: image_def Int_def split: prod.splits)
    6.39 +  show ?R unfolding Grp_def relcompp.simps conversep.simps
    6.40 +  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
    6.41 +    from * show "a = fmap fst R'" using conjunct1[OF `?L`]
    6.42 +      by (transfer, auto simp add: image_def Int_def split: prod.splits)
    6.43 +    from * show "b = fmap snd R'" using conjunct2[OF `?L`]
    6.44 +      by (transfer, auto simp add: image_def Int_def split: prod.splits)
    6.45    qed (auto simp add: *)
    6.46  next
    6.47 -  assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
    6.48 +  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
    6.49    apply (simp add: subset_eq Ball_def)
    6.50    apply (rule conjI)
    6.51    apply (transfer, clarsimp, metis snd_conv)
    6.52 @@ -339,7 +340,7 @@
    6.53     apply (rule ordLeq_transitive[OF surj_imp_ordLeq[of _ abs_fset] list_in_bd])
    6.54     apply (auto simp: fset_def intro!: image_eqI[of _ abs_fset]) []
    6.55    apply (erule wpull_fmap)
    6.56 - apply (simp add: Gr_def relcomp_unfold converse_unfold fset_rel_def fset_rel_aux) 
    6.57 + apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_def fset_rel_aux) 
    6.58  apply transfer apply simp
    6.59  done
    6.60  
    6.61 @@ -419,27 +420,27 @@
    6.62  
    6.63  lemma cset_rel_aux:
    6.64  "(\<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>
    6.65 - (a, b) \<in> (Gr {x. rcset x \<subseteq> {(a, b). R a b}} (cIm fst))\<inverse> O
    6.66 -          Gr {x. rcset x \<subseteq> {(a, b). R a b}} (cIm snd)" (is "?L = ?R")
    6.67 + ((Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cIm fst))\<inverse>\<inverse> OO
    6.68 +          Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cIm snd)) a b" (is "?L = ?R")
    6.69  proof
    6.70    assume ?L
    6.71    def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
    6.72    (is "the_inv rcset ?L'")
    6.73    have "countable ?L'" by auto
    6.74    hence *: "rcset R' = ?L'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset)
    6.75 -  show ?R unfolding Gr_def relcomp_unfold converse_unfold
    6.76 -  proof (intro CollectI prod_caseI exI conjI)
    6.77 +  show ?R unfolding Grp_def relcompp.simps conversep.simps
    6.78 +  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
    6.79      have "rcset a = fst ` ({(x, y). R x y} \<inter> rcset a \<times> rcset b)" (is "_ = ?A")
    6.80      using conjunct1[OF `?L`] unfolding image_def by (auto simp add: Collect_Int_Times)
    6.81      hence "a = acset ?A" by (metis acset_rcset)
    6.82 -    thus "(R', a) = (R', cIm fst R')" unfolding cIm_def * by auto
    6.83 +    thus "a = cIm fst R'" unfolding cIm_def * by auto
    6.84      have "rcset b = snd ` ({(x, y). R x y} \<inter> rcset a \<times> rcset b)" (is "_ = ?B")
    6.85      using conjunct2[OF `?L`] unfolding image_def by (auto simp add: Collect_Int_Times)
    6.86      hence "b = acset ?B" by (metis acset_rcset)
    6.87 -    thus "(R', b) = (R', cIm snd R')" unfolding cIm_def * by auto
    6.88 +    thus "b = cIm snd R'" unfolding cIm_def * by auto
    6.89    qed (auto simp add: *)
    6.90  next
    6.91 -  assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
    6.92 +  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
    6.93    apply (simp add: subset_eq Ball_def)
    6.94    apply (rule conjI)
    6.95    apply (clarsimp, metis (lifting, no_types) rcset_map' image_iff surjective_pairing)
    6.96 @@ -511,9 +512,9 @@
    6.97    qed
    6.98  next
    6.99    fix R
   6.100 -  show "{p. cset_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
   6.101 -        (Gr {x. rcset x \<subseteq> R} (cIm fst))\<inverse> O Gr {x. rcset x \<subseteq> R} (cIm snd)"
   6.102 -  unfolding cset_rel_def cset_rel_aux by simp
   6.103 +  show "cset_rel R =
   6.104 +        (Grp {x. rcset x \<subseteq> Collect (split R)} (cIm fst))\<inverse>\<inverse> OO Grp {x. rcset x \<subseteq> Collect (split R)} (cIm snd)"
   6.105 +  unfolding cset_rel_def[abs_def] cset_rel_aux by simp
   6.106  qed (unfold cEmp_def, auto)
   6.107  
   6.108  
   6.109 @@ -1143,7 +1144,7 @@
   6.110  lemma multiset_map_Zero[simp]: "multiset_map f {#} = {#}" by simp
   6.111  
   6.112  lemma multiset_rel_Zero: "multiset_rel R {#} {#}"
   6.113 -unfolding multiset_rel_def Gr_def relcomp_unfold by auto
   6.114 +unfolding multiset_rel_def Grp_def by auto
   6.115  
   6.116  declare multiset.count[simp]
   6.117  declare mmap[simp]
   6.118 @@ -1196,7 +1197,7 @@
   6.119    }
   6.120    thus ?thesis
   6.121    using assms
   6.122 -  unfolding multiset_rel_def Gr_def relcomp_unfold by force
   6.123 +  unfolding multiset_rel_def Grp_def by force
   6.124  qed
   6.125  
   6.126  lemma multiset_rel'_imp_multiset_rel:
   6.127 @@ -1238,7 +1239,7 @@
   6.128  lemma multiset_rel_mcard:
   6.129  assumes "multiset_rel R M N"
   6.130  shows "mcard M = mcard N"
   6.131 -using assms unfolding multiset_rel_def relcomp_unfold Gr_def by auto
   6.132 +using assms unfolding multiset_rel_def Grp_def by auto
   6.133  
   6.134  lemma multiset_induct2[case_names empty addL addR]:
   6.135  assumes empty: "P {#} {#}"
   6.136 @@ -1299,14 +1300,14 @@
   6.137    obtain K where KM: "multiset_map fst K = M + {#a#}"
   6.138    and KN: "multiset_map snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   6.139    using assms
   6.140 -  unfolding multiset_rel_def Gr_def relcomp_unfold by auto
   6.141 +  unfolding multiset_rel_def Grp_def by auto
   6.142    obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
   6.143    and K1M: "multiset_map fst K1 = M" using msed_map_invR[OF KM] by auto
   6.144    obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "multiset_map snd K1 = N1"
   6.145    using msed_map_invL[OF KN[unfolded K]] by auto
   6.146    have Rab: "R a (snd ab)" using sK a unfolding K by auto
   6.147    have "multiset_rel R M N1" using sK K1M K1N1
   6.148 -  unfolding K multiset_rel_def Gr_def relcomp_unfold by auto
   6.149 +  unfolding K multiset_rel_def Grp_def by auto
   6.150    thus ?thesis using N Rab by auto
   6.151  qed
   6.152  
   6.153 @@ -1317,14 +1318,14 @@
   6.154    obtain K where KN: "multiset_map snd K = N + {#b#}"
   6.155    and KM: "multiset_map fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   6.156    using assms
   6.157 -  unfolding multiset_rel_def Gr_def relcomp_unfold by auto
   6.158 +  unfolding multiset_rel_def Grp_def by auto
   6.159    obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
   6.160    and K1N: "multiset_map snd K1 = N" using msed_map_invR[OF KN] by auto
   6.161    obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "multiset_map fst K1 = M1"
   6.162    using msed_map_invL[OF KM[unfolded K]] by auto
   6.163    have Rab: "R (fst ab) b" using sK b unfolding K by auto
   6.164    have "multiset_rel R M1 N" using sK K1N K1M1
   6.165 -  unfolding K multiset_rel_def Gr_def relcomp_unfold by auto
   6.166 +  unfolding K multiset_rel_def Grp_def by auto
   6.167    thus ?thesis using M Rab by auto
   6.168  qed
   6.169  
     7.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Tue May 07 11:27:29 2013 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Tue May 07 14:22:54 2013 +0200
     7.3 @@ -40,25 +40,22 @@
     7.4  type unfold_set = {
     7.5    map_unfolds: thm list,
     7.6    set_unfoldss: thm list list,
     7.7 -  rel_unfolds: thm list,
     7.8 -  srel_unfolds: thm list
     7.9 +  rel_unfolds: thm list
    7.10  };
    7.11  
    7.12 -val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = [], srel_unfolds = []};
    7.13 +val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
    7.14  
    7.15  fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
    7.16  fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
    7.17  
    7.18 -fun add_to_unfolds map sets rel srel
    7.19 -  {map_unfolds, set_unfoldss, rel_unfolds, srel_unfolds} =
    7.20 +fun add_to_unfolds map sets rel
    7.21 +  {map_unfolds, set_unfoldss, rel_unfolds} =
    7.22    {map_unfolds = add_to_thms map_unfolds map,
    7.23      set_unfoldss = adds_to_thms set_unfoldss sets,
    7.24 -    rel_unfolds = add_to_thms rel_unfolds rel,
    7.25 -    srel_unfolds = add_to_thms srel_unfolds srel};
    7.26 +    rel_unfolds = add_to_thms rel_unfolds rel};
    7.27  
    7.28  fun add_bnf_to_unfolds bnf =
    7.29 -  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf)
    7.30 -    (srel_def_of_bnf bnf);
    7.31 +  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf);
    7.32  
    7.33  val bdTN = "bdT";
    7.34  
    7.35 @@ -221,25 +218,24 @@
    7.36      fun map_wpull_tac _ =
    7.37        mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
    7.38  
    7.39 -    fun srel_O_Gr_tac _ =
    7.40 +    fun rel_OO_Grp_tac _ =
    7.41        let
    7.42 -        val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
    7.43 -        val outer_srel_Gr = srel_Gr_of_bnf outer RS sym;
    7.44 -        val outer_srel_cong = srel_cong_of_bnf outer;
    7.45 +        val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
    7.46 +        val outer_rel_cong = rel_cong_of_bnf outer;
    7.47          val thm =
    7.48 -          (trans OF [in_alt_thm RS @{thm O_Gr_cong},
    7.49 -             trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
    7.50 -               [trans OF [outer_srel_Gr RS @{thm arg_cong[of _ _ converse]},
    7.51 -                 srel_converse_of_bnf outer RS sym], outer_srel_Gr],
    7.52 -               trans OF [srel_O_of_bnf outer RS sym, outer_srel_cong OF
    7.53 -                 (map (fn bnf => srel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
    7.54 -          |> unfold_thms lthy (basic_thms @ srel_def_of_bnf outer :: map srel_def_of_bnf inners);
    7.55 +          (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
    7.56 +             trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
    7.57 +               [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
    7.58 +                 rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
    7.59 +               trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF
    7.60 +                 (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym)
    7.61 +          (*|> unfold_thms lthy (rel_def_of_bnf outer :: map rel_def_of_bnf inners)*);
    7.62        in
    7.63 -        unfold_thms_tac lthy basic_thms THEN rtac thm 1
    7.64 +        rtac thm 1
    7.65        end;
    7.66  
    7.67      val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
    7.68 -      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    7.69 +      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
    7.70  
    7.71      val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
    7.72  
    7.73 @@ -332,24 +328,24 @@
    7.74          (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
    7.75      fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
    7.76  
    7.77 -    fun srel_O_Gr_tac _ =
    7.78 +    fun rel_OO_Grp_tac _ =
    7.79        let
    7.80 -        val srel_Gr = srel_Gr_of_bnf bnf RS sym
    7.81 +        val rel_Grp = rel_Grp_of_bnf bnf RS sym
    7.82          val thm =
    7.83 -          (trans OF [in_alt_thm RS @{thm O_Gr_cong},
    7.84 -            trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
    7.85 -              [trans OF [srel_Gr RS @{thm arg_cong[of _ _ converse]},
    7.86 -                srel_converse_of_bnf bnf RS sym], srel_Gr],
    7.87 -              trans OF [srel_O_of_bnf bnf RS sym, srel_cong_of_bnf bnf OF
    7.88 -                (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
    7.89 -                 replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
    7.90 -          |> unfold_thms lthy (srel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
    7.91 +          (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
    7.92 +            trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
    7.93 +              [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]},
    7.94 +                rel_conversep_of_bnf bnf RS sym], rel_Grp],
    7.95 +              trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
    7.96 +                (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
    7.97 +                 replicate (live - n) @{thm Grp_fst_snd})]]] RS sym)
    7.98 +          (*|> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv})*);
    7.99        in
   7.100          rtac thm 1
   7.101        end;
   7.102  
   7.103      val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
   7.104 -      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   7.105 +      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
   7.106  
   7.107      val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
   7.108  
   7.109 @@ -432,11 +428,10 @@
   7.110      fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
   7.111      fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
   7.112  
   7.113 -    fun srel_O_Gr_tac _ =
   7.114 -      mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
   7.115 +    fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
   7.116  
   7.117      val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
   7.118 -      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   7.119 +      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
   7.120  
   7.121      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   7.122  
   7.123 @@ -509,11 +504,10 @@
   7.124        mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
   7.125      fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
   7.126  
   7.127 -    fun srel_O_Gr_tac _ =
   7.128 -      mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
   7.129 +    fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
   7.130  
   7.131      val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
   7.132 -      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   7.133 +      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_OO_Grp_tac;
   7.134  
   7.135      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   7.136  
   7.137 @@ -598,7 +592,6 @@
   7.138      val map_unfolds = #map_unfolds unfold_set;
   7.139      val set_unfoldss = #set_unfoldss unfold_set;
   7.140      val rel_unfolds = #rel_unfolds unfold_set;
   7.141 -    val srel_unfolds = #srel_unfolds unfold_set;
   7.142  
   7.143      val expand_maps =
   7.144        fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
   7.145 @@ -609,8 +602,7 @@
   7.146      val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
   7.147      val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
   7.148      val unfold_rels = unfold_thms lthy rel_unfolds;
   7.149 -    val unfold_srels = unfold_thms lthy srel_unfolds;
   7.150 -    val unfold_all = unfold_sets o unfold_maps o unfold_rels o unfold_srels;
   7.151 +    val unfold_all = unfold_sets o unfold_maps o unfold_rels;
   7.152      val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
   7.153      val bnf_sets = map (expand_maps o expand_sets)
   7.154        (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
   7.155 @@ -656,7 +648,7 @@
   7.156        (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
   7.157        (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
   7.158        (mk_tac (map_wpull_of_bnf bnf))
   7.159 -      (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
   7.160 +      (mk_tac (unfold_thms lthy [rel_def_of_bnf bnf] (rel_OO_Grp_of_bnf bnf)));
   7.161  
   7.162      val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   7.163  
     8.1 --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Tue May 07 11:27:29 2013 +0200
     8.2 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Tue May 07 14:22:54 2013 +0200
     8.3 @@ -36,7 +36,7 @@
     8.4    val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic
     8.5  
     8.6    val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
     8.7 -  val mk_simple_srel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic
     8.8 +  val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
     8.9    val mk_simple_wit_tac: thm list -> tactic
    8.10  end;
    8.11  
    8.12 @@ -52,8 +52,6 @@
    8.13  val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
    8.14  val card_of_Card_order = @{thm card_of_Card_order};
    8.15  val csum_Cnotzero1 = @{thm csum_Cnotzero1};
    8.16 -val csum_Cnotzero2 = @{thm csum_Cnotzero2};
    8.17 -val ctwo_Cnotzero = @{thm ctwo_Cnotzero};
    8.18  val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
    8.19  val ordIso_transitive = @{thm ordIso_transitive};
    8.20  val ordLeq_csum2 = @{thm ordLeq_csum2};
    8.21 @@ -389,9 +387,8 @@
    8.22    WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
    8.23    TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
    8.24  
    8.25 -fun mk_simple_srel_O_Gr_tac ctxt srel_def srel_O_Gr in_alt_thm =
    8.26 -  rtac (unfold_thms ctxt [srel_def]
    8.27 -    (trans OF [srel_O_Gr, in_alt_thm RS @{thm O_Gr_cong} RS sym])) 1;
    8.28 +fun mk_simple_rel_OO_Grp_tac rel_OO_Grp in_alt_thm =
    8.29 +  rtac (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
    8.30  
    8.31  fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
    8.32  
     9.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Tue May 07 11:27:29 2013 +0200
     9.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue May 07 14:22:54 2013 +0200
     9.3 @@ -28,7 +28,6 @@
     9.4    val relN: string
     9.5    val setN: string
     9.6    val mk_setN: int -> string
     9.7 -  val srelN: string
     9.8  
     9.9    val map_of_bnf: bnf -> term
    9.10    val sets_of_bnf: bnf -> term list
    9.11 @@ -39,7 +38,6 @@
    9.12    val mk_map_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    9.13    val mk_rel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    9.14    val mk_sets_of_bnf: typ list list -> typ list list -> bnf -> term list
    9.15 -  val mk_srel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    9.16    val mk_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list
    9.17  
    9.18    val bd_Card_order_of_bnf: bnf -> thm
    9.19 @@ -51,7 +49,7 @@
    9.20    val in_bd_of_bnf: bnf -> thm
    9.21    val in_cong_of_bnf: bnf -> thm
    9.22    val in_mono_of_bnf: bnf -> thm
    9.23 -  val in_srel_of_bnf: bnf -> thm
    9.24 +  val in_rel_of_bnf: bnf -> thm
    9.25    val map_comp'_of_bnf: bnf -> thm
    9.26    val map_comp_of_bnf: bnf -> thm
    9.27    val map_cong0_of_bnf: bnf -> thm
    9.28 @@ -62,21 +60,18 @@
    9.29    val map_wppull_of_bnf: bnf -> thm
    9.30    val map_wpull_of_bnf: bnf -> thm
    9.31    val rel_def_of_bnf: bnf -> thm
    9.32 +  val rel_Grp_of_bnf: bnf -> thm
    9.33 +  val rel_OO_of_bnf: bnf -> thm
    9.34 +  val rel_OO_Grp_of_bnf: bnf -> thm
    9.35 +  val rel_cong_of_bnf: bnf -> thm
    9.36 +  val rel_conversep_of_bnf: bnf -> thm
    9.37 +  val rel_mono_of_bnf: bnf -> thm
    9.38    val rel_eq_of_bnf: bnf -> thm
    9.39    val rel_flip_of_bnf: bnf -> thm
    9.40 -  val rel_srel_of_bnf: bnf -> thm
    9.41    val set_bd_of_bnf: bnf -> thm list
    9.42    val set_defs_of_bnf: bnf -> thm list
    9.43    val set_map'_of_bnf: bnf -> thm list
    9.44    val set_map_of_bnf: bnf -> thm list
    9.45 -  val srel_def_of_bnf: bnf -> thm
    9.46 -  val srel_Gr_of_bnf: bnf -> thm
    9.47 -  val srel_Id_of_bnf: bnf -> thm
    9.48 -  val srel_O_of_bnf: bnf -> thm
    9.49 -  val srel_O_Gr_of_bnf: bnf -> thm
    9.50 -  val srel_cong_of_bnf: bnf -> thm
    9.51 -  val srel_converse_of_bnf: bnf -> thm
    9.52 -  val srel_mono_of_bnf: bnf -> thm
    9.53    val wit_thms_of_bnf: bnf -> thm list
    9.54    val wit_thmss_of_bnf: bnf -> thm list list
    9.55  
    9.56 @@ -120,12 +115,12 @@
    9.57    set_bd: thm list,
    9.58    in_bd: thm,
    9.59    map_wpull: thm,
    9.60 -  srel_O_Gr: thm
    9.61 +  rel_OO_Grp: thm
    9.62  };
    9.63  
    9.64 -fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), srel) =
    9.65 +fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), rel) =
    9.66    {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
    9.67 -   bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, srel_O_Gr = srel};
    9.68 +   bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_OO_Grp = rel};
    9.69  
    9.70  fun dest_cons [] = raise Empty
    9.71    | dest_cons (x :: xs) = (x, xs);
    9.72 @@ -144,16 +139,16 @@
    9.73    ||> the_single
    9.74    |> mk_axioms';
    9.75  
    9.76 -fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull srel =
    9.77 -  [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, srel];
    9.78 +fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
    9.79 +  [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
    9.80  
    9.81  fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, in_bd,
    9.82 -  map_wpull, srel_O_Gr} =
    9.83 +  map_wpull, rel_OO_Grp} =
    9.84    zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd in_bd map_wpull
    9.85 -    srel_O_Gr;
    9.86 +    rel_OO_Grp;
    9.87  
    9.88  fun map_axioms f {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
    9.89 -  in_bd, map_wpull, srel_O_Gr} =
    9.90 +  in_bd, map_wpull, rel_OO_Grp} =
    9.91    {map_id = f map_id,
    9.92      map_comp = f map_comp,
    9.93      map_cong0 = f map_cong0,
    9.94 @@ -163,21 +158,20 @@
    9.95      set_bd = map f set_bd,
    9.96      in_bd = f in_bd,
    9.97      map_wpull = f map_wpull,
    9.98 -    srel_O_Gr = f srel_O_Gr};
    9.99 +    rel_OO_Grp = f rel_OO_Grp};
   9.100  
   9.101  val morph_axioms = map_axioms o Morphism.thm;
   9.102  
   9.103  type defs = {
   9.104    map_def: thm,
   9.105    set_defs: thm list,
   9.106 -  rel_def: thm,
   9.107 -  srel_def: thm
   9.108 +  rel_def: thm
   9.109  }
   9.110  
   9.111 -fun mk_defs map sets rel srel = {map_def = map, set_defs = sets, rel_def = rel, srel_def = srel};
   9.112 +fun mk_defs map sets rel = {map_def = map, set_defs = sets, rel_def = rel};
   9.113  
   9.114 -fun map_defs f {map_def, set_defs, rel_def, srel_def} =
   9.115 -  {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def, srel_def = f srel_def};
   9.116 +fun map_defs f {map_def, set_defs, rel_def} =
   9.117 +  {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def};
   9.118  
   9.119  val morph_defs = map_defs o Morphism.thm;
   9.120  
   9.121 @@ -188,47 +182,43 @@
   9.122    collect_set_map: thm lazy,
   9.123    in_cong: thm lazy,
   9.124    in_mono: thm lazy,
   9.125 -  in_srel: thm lazy,
   9.126 +  in_rel: thm lazy,
   9.127    map_comp': thm lazy,
   9.128    map_cong: thm lazy,
   9.129    map_id': thm lazy,
   9.130    map_wppull: thm lazy,
   9.131    rel_eq: thm lazy,
   9.132    rel_flip: thm lazy,
   9.133 -  rel_srel: thm lazy,
   9.134    set_map': thm lazy list,
   9.135 -  srel_cong: thm lazy,
   9.136 -  srel_mono: thm lazy,
   9.137 -  srel_Id: thm lazy,
   9.138 -  srel_Gr: thm lazy,
   9.139 -  srel_converse: thm lazy,
   9.140 -  srel_O: thm lazy
   9.141 +  rel_cong: thm lazy,
   9.142 +  rel_mono: thm lazy,
   9.143 +  rel_Grp: thm lazy,
   9.144 +  rel_conversep: thm lazy,
   9.145 +  rel_OO: thm lazy
   9.146  };
   9.147  
   9.148 -fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono in_srel
   9.149 -    map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_map' srel_cong srel_mono
   9.150 -    srel_Id srel_Gr srel_converse srel_O = {
   9.151 +fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono in_rel
   9.152 +    map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map' rel_cong rel_mono
   9.153 +    rel_Grp rel_conversep rel_OO = {
   9.154    bd_Card_order = bd_Card_order,
   9.155    bd_Cinfinite = bd_Cinfinite,
   9.156    bd_Cnotzero = bd_Cnotzero,
   9.157    collect_set_map = collect_set_map,
   9.158    in_cong = in_cong,
   9.159    in_mono = in_mono,
   9.160 -  in_srel = in_srel,
   9.161 +  in_rel = in_rel,
   9.162    map_comp' = map_comp',
   9.163    map_cong = map_cong,
   9.164    map_id' = map_id',
   9.165    map_wppull = map_wppull,
   9.166    rel_eq = rel_eq,
   9.167    rel_flip = rel_flip,
   9.168 -  rel_srel = rel_srel,
   9.169    set_map' = set_map',
   9.170 -  srel_cong = srel_cong,
   9.171 -  srel_mono = srel_mono,
   9.172 -  srel_Id = srel_Id,
   9.173 -  srel_Gr = srel_Gr,
   9.174 -  srel_converse = srel_converse,
   9.175 -  srel_O = srel_O};
   9.176 +  rel_cong = rel_cong,
   9.177 +  rel_mono = rel_mono,
   9.178 +  rel_Grp = rel_Grp,
   9.179 +  rel_conversep = rel_conversep,
   9.180 +  rel_OO = rel_OO};
   9.181  
   9.182  fun map_facts f {
   9.183    bd_Card_order,
   9.184 @@ -237,42 +227,38 @@
   9.185    collect_set_map,
   9.186    in_cong,
   9.187    in_mono,
   9.188 -  in_srel,
   9.189 +  in_rel,
   9.190    map_comp',
   9.191    map_cong,
   9.192    map_id',
   9.193    map_wppull,
   9.194    rel_eq,
   9.195    rel_flip,
   9.196 -  rel_srel,
   9.197    set_map',
   9.198 -  srel_cong,
   9.199 -  srel_mono,
   9.200 -  srel_Id,
   9.201 -  srel_Gr,
   9.202 -  srel_converse,
   9.203 -  srel_O} =
   9.204 +  rel_cong,
   9.205 +  rel_mono,
   9.206 +  rel_Grp,
   9.207 +  rel_conversep,
   9.208 +  rel_OO} =
   9.209    {bd_Card_order = f bd_Card_order,
   9.210      bd_Cinfinite = f bd_Cinfinite,
   9.211      bd_Cnotzero = f bd_Cnotzero,
   9.212      collect_set_map = Lazy.map f collect_set_map,
   9.213      in_cong = Lazy.map f in_cong,
   9.214      in_mono = Lazy.map f in_mono,
   9.215 -    in_srel = Lazy.map f in_srel,
   9.216 +    in_rel = Lazy.map f in_rel,
   9.217      map_comp' = Lazy.map f map_comp',
   9.218      map_cong = Lazy.map f map_cong,
   9.219      map_id' = Lazy.map f map_id',
   9.220      map_wppull = Lazy.map f map_wppull,
   9.221      rel_eq = Lazy.map f rel_eq,
   9.222      rel_flip = Lazy.map f rel_flip,
   9.223 -    rel_srel = Lazy.map f rel_srel,
   9.224      set_map' = map (Lazy.map f) set_map',
   9.225 -    srel_cong = Lazy.map f srel_cong,
   9.226 -    srel_mono = Lazy.map f srel_mono,
   9.227 -    srel_Id = Lazy.map f srel_Id,
   9.228 -    srel_Gr = Lazy.map f srel_Gr,
   9.229 -    srel_converse = Lazy.map f srel_converse,
   9.230 -    srel_O = Lazy.map f srel_O};
   9.231 +    rel_cong = Lazy.map f rel_cong,
   9.232 +    rel_mono = Lazy.map f rel_mono,
   9.233 +    rel_Grp = Lazy.map f rel_Grp,
   9.234 +    rel_conversep = Lazy.map f rel_conversep,
   9.235 +    rel_OO = Lazy.map f rel_OO};
   9.236  
   9.237  val morph_facts = map_facts o Morphism.thm;
   9.238  
   9.239 @@ -302,8 +288,7 @@
   9.240    facts: facts,
   9.241    nwits: int,
   9.242    wits: nonemptiness_witness list,
   9.243 -  rel: term,
   9.244 -  srel: term
   9.245 +  rel: term
   9.246  };
   9.247  
   9.248  (* getters *)
   9.249 @@ -357,13 +342,6 @@
   9.250      Term.subst_atomic_types
   9.251        ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#rel bnf_rep)
   9.252    end;
   9.253 -val srel_of_bnf = #srel o rep_bnf;
   9.254 -fun mk_srel_of_bnf Ds Ts Us bnf =
   9.255 -  let val bnf_rep = rep_bnf bnf;
   9.256 -  in
   9.257 -    Term.subst_atomic_types
   9.258 -      ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#srel bnf_rep)
   9.259 -  end;
   9.260  
   9.261  (*thms*)
   9.262  val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
   9.263 @@ -375,7 +353,7 @@
   9.264  val in_bd_of_bnf = #in_bd o #axioms o rep_bnf;
   9.265  val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
   9.266  val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
   9.267 -val in_srel_of_bnf = Lazy.force o #in_srel o #facts o rep_bnf;
   9.268 +val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
   9.269  val map_def_of_bnf = #map_def o #defs o rep_bnf;
   9.270  val map_id_of_bnf = #map_id o #axioms o rep_bnf;
   9.271  val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
   9.272 @@ -388,33 +366,30 @@
   9.273  val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
   9.274  val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
   9.275  val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
   9.276 -val rel_srel_of_bnf = Lazy.force o #rel_srel o #facts o rep_bnf;
   9.277  val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
   9.278  val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
   9.279  val set_map_of_bnf = #set_map o #axioms o rep_bnf;
   9.280  val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf;
   9.281 -val srel_cong_of_bnf = Lazy.force o #srel_cong o #facts o rep_bnf;
   9.282 -val srel_mono_of_bnf = Lazy.force o #srel_mono o #facts o rep_bnf;
   9.283 -val srel_def_of_bnf = #srel_def o #defs o rep_bnf;
   9.284 -val srel_Id_of_bnf = Lazy.force o #srel_Id o #facts o rep_bnf;
   9.285 -val srel_Gr_of_bnf = Lazy.force o #srel_Gr o #facts o rep_bnf;
   9.286 -val srel_converse_of_bnf = Lazy.force o #srel_converse o #facts o rep_bnf;
   9.287 -val srel_O_of_bnf = Lazy.force o #srel_O o #facts o rep_bnf;
   9.288 -val srel_O_Gr_of_bnf = #srel_O_Gr o #axioms o rep_bnf;
   9.289 +val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
   9.290 +val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
   9.291 +val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
   9.292 +val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
   9.293 +val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
   9.294 +val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf;
   9.295  val wit_thms_of_bnf = maps #prop o wits_of_bnf;
   9.296  val wit_thmss_of_bnf = map #prop o wits_of_bnf;
   9.297  
   9.298 -fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel srel =
   9.299 +fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel =
   9.300    BNF {name = name, T = T,
   9.301         live = live, lives = lives, lives' = lives', dead = dead, deads = deads,
   9.302         map = map, sets = sets, bd = bd,
   9.303         axioms = axioms, defs = defs, facts = facts,
   9.304 -       nwits = length wits, wits = wits, rel = rel, srel = srel};
   9.305 +       nwits = length wits, wits = wits, rel = rel};
   9.306  
   9.307  fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
   9.308    dead = dead, deads = deads, map = map, sets = sets, bd = bd,
   9.309    axioms = axioms, defs = defs, facts = facts,
   9.310 -  nwits = nwits, wits = wits, rel = rel, srel = srel}) =
   9.311 +  nwits = nwits, wits = wits, rel = rel}) =
   9.312    BNF {name = Morphism.binding phi name, T = Morphism.typ phi T,
   9.313      live = live, lives = List.map (Morphism.typ phi) lives,
   9.314      lives' = List.map (Morphism.typ phi) lives',
   9.315 @@ -426,7 +401,7 @@
   9.316      facts = morph_facts phi facts,
   9.317      nwits = nwits,
   9.318      wits = List.map (morph_witness phi) wits,
   9.319 -    rel = Morphism.term phi rel, srel = Morphism.term phi srel};
   9.320 +    rel = Morphism.term phi rel};
   9.321  
   9.322  fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...},
   9.323    BNF {T = T2, live = live2, dead = dead2, ...}) =
   9.324 @@ -460,15 +435,6 @@
   9.325        Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_pred2T instA instB))
   9.326          Vartab.empty;
   9.327    in Envir.subst_term (tyenv, Vartab.empty) rel end
   9.328 -  handle Type.TYPE_MATCH => error "Bad predicator";
   9.329 -
   9.330 -fun normalize_srel ctxt instTs instA instB srel =
   9.331 -  let
   9.332 -    val thy = Proof_Context.theory_of ctxt;
   9.333 -    val tyenv =
   9.334 -      Sign.typ_match thy (fastype_of srel, Library.foldr (op -->) (instTs, mk_relT (instA, instB)))
   9.335 -        Vartab.empty;
   9.336 -  in Envir.subst_term (tyenv, Vartab.empty) srel end
   9.337    handle Type.TYPE_MATCH => error "Bad relator";
   9.338  
   9.339  fun normalize_wit insts CA As wit =
   9.340 @@ -503,7 +469,6 @@
   9.341  val witN = "wit";
   9.342  fun mk_witN i = witN ^ nonzero_string_of_int i;
   9.343  val relN = "rel";
   9.344 -val srelN = "srel";
   9.345  
   9.346  val bd_card_orderN = "bd_card_order";
   9.347  val bd_cinfiniteN = "bd_cinfinite";
   9.348 @@ -513,7 +478,7 @@
   9.349  val collect_set_mapN = "collect_set_map";
   9.350  val in_bdN = "in_bd";
   9.351  val in_monoN = "in_mono";
   9.352 -val in_srelN = "in_srel";
   9.353 +val in_relN = "in_rel";
   9.354  val map_idN = "map_id";
   9.355  val map_id'N = "map_id'";
   9.356  val map_compN = "map_comp";
   9.357 @@ -523,16 +488,14 @@
   9.358  val map_wpullN = "map_wpull";
   9.359  val rel_eqN = "rel_eq";
   9.360  val rel_flipN = "rel_flip";
   9.361 -val rel_srelN = "rel_srel";
   9.362  val set_mapN = "set_map";
   9.363  val set_map'N = "set_map'";
   9.364  val set_bdN = "set_bd";
   9.365 -val srel_IdN = "srel_Id";
   9.366 -val srel_GrN = "srel_Gr";
   9.367 -val srel_converseN = "srel_converse";
   9.368 -val srel_monoN = "srel_mono"
   9.369 -val srel_ON = "srel_comp";
   9.370 -val srel_O_GrN = "srel_comp_Gr";
   9.371 +val rel_GrpN = "rel_Grp";
   9.372 +val rel_conversepN = "rel_conversep";
   9.373 +val rel_monoN = "rel_mono"
   9.374 +val rel_OON = "rel_compp";
   9.375 +val rel_OO_GrpN = "rel_compp_Grp";
   9.376  
   9.377  datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
   9.378  
   9.379 @@ -688,12 +651,12 @@
   9.380      fun mk_bnf_t As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
   9.381      fun mk_bnf_T As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
   9.382  
   9.383 -    val (setRTs, RTs) = map_split (`HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Bs');
   9.384 -    val setRTsAsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Cs);
   9.385 -    val setRTsBsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (Bs' ~~ Cs);
   9.386 -    val setRT's = map (HOLogic.mk_setT o HOLogic.mk_prodT) (Bs' ~~ As');
   9.387 -    val self_setRTs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ As');
   9.388 -    val QTs = map2 mk_pred2T As' Bs';
   9.389 +    val RTs = map HOLogic.mk_prodT (As' ~~ Bs');
   9.390 +    val pred2RTs = map2 mk_pred2T As' Bs';
   9.391 +    val pred2RTsAsCs = map2 mk_pred2T As' Cs;
   9.392 +    val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
   9.393 +    val pred2RT's = map2 mk_pred2T Bs' As';
   9.394 +    val self_pred2RTs = map2 mk_pred2T As' As';
   9.395  
   9.396      val CA' = mk_bnf_T As' CA;
   9.397      val CB' = mk_bnf_T Bs' CA;
   9.398 @@ -711,9 +674,9 @@
   9.399      val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
   9.400  
   9.401      val pre_names_lthy = lthy;
   9.402 -    val ((((((((((((((((((((((((fs, gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As),
   9.403 +    val (((((((((((((((((((((((fs, gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As),
   9.404        As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
   9.405 -      (Qs, Qs')), names_lthy) = pre_names_lthy
   9.406 +      names_lthy) = pre_names_lthy
   9.407        |> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
   9.408        ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
   9.409        ||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts)
   9.410 @@ -734,39 +697,30 @@
   9.411        ||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts)
   9.412        ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts)
   9.413        ||>> mk_Frees "b" As'
   9.414 -      ||>> mk_Frees' "r" setRTs
   9.415 -      ||>> mk_Frees "r" setRTs
   9.416 -      ||>> mk_Frees "s" setRTsBsCs
   9.417 -      ||>> mk_Frees' "P" QTs;
   9.418 +      ||>> mk_Frees' "R" pred2RTs
   9.419 +      ||>> mk_Frees "R" pred2RTs
   9.420 +      ||>> mk_Frees "S" pred2RTsBsCs;
   9.421  
   9.422      val fs_copy = map2 (retype_free o fastype_of) fs gs;
   9.423      val x_copy = retype_free CA' y;
   9.424  
   9.425 -    (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
   9.426 -    val O_Gr =
   9.427 +    val setRs =
   9.428 +      map3 (fn R => fn T => fn U =>
   9.429 +          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As' Bs';
   9.430 +
   9.431 +    (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
   9.432 +      Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
   9.433 +    val OO_Grp =
   9.434        let
   9.435          val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
   9.436          val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
   9.437 -        val bnf_in = mk_in (map Free Rs') (map (mk_bnf_t RTs) bnf_sets) CRs';
   9.438 +        val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
   9.439        in
   9.440 -        mk_rel_comp (mk_converse (mk_Gr bnf_in map1), mk_Gr bnf_in map2)
   9.441 +        mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2)
   9.442        end;
   9.443  
   9.444 -    fun mk_predicate_of_set x_name y_name t =
   9.445 -      let
   9.446 -        val (T, U) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of t));
   9.447 -        val x = Free (x_name, T);
   9.448 -        val y = Free (y_name, U);
   9.449 -      in fold_rev Term.lambda [x, y] (HOLogic.mk_mem (HOLogic.mk_prod (x, y), t)) end;
   9.450 -
   9.451 -    val sQs =
   9.452 -      map3 (fn Q => fn T => fn U =>
   9.453 -          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs';
   9.454 -
   9.455      val rel_rhs = (case raw_rel_opt of
   9.456 -        NONE =>
   9.457 -        fold_rev absfree Qs' (mk_predicate_of_set (fst x') (fst y')
   9.458 -          (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, sQs)))
   9.459 +        NONE => fold_rev Term.absfree Rs' OO_Grp
   9.460        | SOME raw_rel => prep_term no_defs_lthy raw_rel);
   9.461  
   9.462      val rel_bind_def =
   9.463 @@ -782,32 +736,12 @@
   9.464      val bnf_rel_def = Morphism.thm phi raw_rel_def;
   9.465      val bnf_rel = Morphism.term phi bnf_rel_term;
   9.466  
   9.467 -    fun mk_bnf_rel QTs CA' CB' = normalize_rel lthy QTs CA' CB' bnf_rel;
   9.468 -
   9.469 -    val rel = mk_bnf_rel QTs CA' CB';
   9.470 -
   9.471 -    val srel_rhs =
   9.472 -      fold_rev Term.absfree Rs' (HOLogic.Collect_const CA'CB' $
   9.473 -        Term.lambda p (Term.list_comb (rel, map (mk_predicate_of_set (fst x') (fst y')) Rs) $
   9.474 -        HOLogic.mk_fst p $ HOLogic.mk_snd p));
   9.475 -
   9.476 -    val srel_bind_def = (fn () => Binding.suffix_name ("_" ^ srelN) b, srel_rhs);
   9.477 +    fun mk_bnf_rel RTs CA' CB' = normalize_rel lthy RTs CA' CB' bnf_rel;
   9.478  
   9.479 -    val ((bnf_srel_term, raw_srel_def), (lthy, lthy_old)) =
   9.480 -      lthy
   9.481 -      |> maybe_define false srel_bind_def
   9.482 -      ||> `(maybe_restore lthy);
   9.483 -
   9.484 -    val phi = Proof_Context.export_morphism lthy_old lthy;
   9.485 -    val bnf_srel_def = Morphism.thm phi raw_srel_def;
   9.486 -    val bnf_srel = Morphism.term phi bnf_srel_term;
   9.487 -
   9.488 -    fun mk_bnf_srel setRTs CA' CB' = normalize_srel lthy setRTs CA' CB' bnf_srel;
   9.489 -
   9.490 -    val srel = mk_bnf_srel setRTs CA' CB';
   9.491 +    val rel = mk_bnf_rel pred2RTs CA' CB';
   9.492  
   9.493      val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @
   9.494 -        raw_wit_defs @ [raw_rel_def, raw_srel_def]) of
   9.495 +        raw_wit_defs @ [raw_rel_def]) of
   9.496          [] => ()
   9.497        | defs => Proof_Display.print_consts true lthy_old (K false)
   9.498            (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
   9.499 @@ -900,10 +834,10 @@
   9.500            (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull))
   9.501        end;
   9.502  
   9.503 -    val srel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (srel, Rs), O_Gr));
   9.504 +    val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
   9.505  
   9.506      val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_maps_goal card_order_bd_goal
   9.507 -      cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal;
   9.508 +      cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_OO_Grp_goal;
   9.509  
   9.510      fun mk_wit_goals (I, wit) =
   9.511        let
   9.512 @@ -953,11 +887,11 @@
   9.513  
   9.514          fun mk_in_mono () =
   9.515            let
   9.516 -            val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_subset) As As_copy;
   9.517 +            val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_leq) As As_copy;
   9.518              val in_mono_goal =
   9.519                fold_rev Logic.all (As @ As_copy)
   9.520                  (Logic.list_implies (prems_mono, HOLogic.mk_Trueprop
   9.521 -                  (mk_subset (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
   9.522 +                  (mk_leq (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
   9.523            in
   9.524              Goal.prove_sorry lthy [] [] in_mono_goal (K (mk_in_mono_tac live))
   9.525              |> Thm.close_derivation
   9.526 @@ -1038,41 +972,41 @@
   9.527  
   9.528          val map_wppull = Lazy.lazy mk_map_wppull;
   9.529  
   9.530 -        val srel_O_Grs = no_refl [#srel_O_Gr axioms];
   9.531 +        val rel_OO_Grps = no_refl [#rel_OO_Grp axioms];
   9.532  
   9.533 -        fun mk_srel_Gr () =
   9.534 +        fun mk_rel_Grp () =
   9.535            let
   9.536 -            val lhs = Term.list_comb (srel, map2 mk_Gr As fs);
   9.537 -            val rhs = mk_Gr (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
   9.538 +            val lhs = Term.list_comb (rel, map2 mk_Grp As fs);
   9.539 +            val rhs = mk_Grp (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
   9.540              val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
   9.541            in
   9.542              Goal.prove_sorry lthy [] [] goal
   9.543 -              (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
   9.544 +              (mk_rel_Grp_tac rel_OO_Grps (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
   9.545                  (Lazy.force map_comp') (map Lazy.force set_map'))
   9.546              |> Thm.close_derivation
   9.547            end;
   9.548  
   9.549 -        val srel_Gr = Lazy.lazy mk_srel_Gr;
   9.550 +        val rel_Grp = Lazy.lazy mk_rel_Grp;
   9.551  
   9.552 -        fun mk_srel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
   9.553 -        fun mk_srel_concl f = HOLogic.mk_Trueprop
   9.554 -          (f (Term.list_comb (srel, Rs), Term.list_comb (srel, Rs_copy)));
   9.555 +        fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
   9.556 +        fun mk_rel_concl f = HOLogic.mk_Trueprop
   9.557 +          (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy)));
   9.558  
   9.559 -        fun mk_srel_mono () =
   9.560 +        fun mk_rel_mono () =
   9.561            let
   9.562 -            val mono_prems = mk_srel_prems mk_subset;
   9.563 -            val mono_concl = mk_srel_concl (uncurry mk_subset);
   9.564 +            val mono_prems = mk_rel_prems mk_leq;
   9.565 +            val mono_concl = mk_rel_concl (uncurry mk_leq);
   9.566            in
   9.567              Goal.prove_sorry lthy [] []
   9.568                (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
   9.569 -              (mk_srel_mono_tac srel_O_Grs (Lazy.force in_mono))
   9.570 +              (mk_rel_mono_tac rel_OO_Grps (Lazy.force in_mono))
   9.571              |> Thm.close_derivation
   9.572            end;
   9.573  
   9.574 -        fun mk_srel_cong () =
   9.575 +        fun mk_rel_cong () =
   9.576            let
   9.577 -            val cong_prems = mk_srel_prems (curry HOLogic.mk_eq);
   9.578 -            val cong_concl = mk_srel_concl HOLogic.mk_eq;
   9.579 +            val cong_prems = mk_rel_prems (curry HOLogic.mk_eq);
   9.580 +            val cong_concl = mk_rel_concl HOLogic.mk_eq;
   9.581            in
   9.582              Goal.prove_sorry lthy [] []
   9.583                (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
   9.584 @@ -1080,120 +1014,103 @@
   9.585              |> Thm.close_derivation
   9.586            end;
   9.587  
   9.588 -        val srel_mono = Lazy.lazy mk_srel_mono;
   9.589 -        val srel_cong = Lazy.lazy mk_srel_cong;
   9.590 +        val rel_mono = Lazy.lazy mk_rel_mono;
   9.591 +        val rel_cong = Lazy.lazy mk_rel_cong;
   9.592  
   9.593 -        fun mk_srel_Id () =
   9.594 -          let val srelAsAs = mk_bnf_srel self_setRTs CA' CA' in
   9.595 +        fun mk_rel_eq () =
   9.596 +          let val relAsAs = mk_bnf_rel self_pred2RTs CA' CA' in
   9.597              Goal.prove_sorry lthy [] []
   9.598 -              (mk_Trueprop_eq (Term.list_comb (srelAsAs, map Id_const As'), Id_const CA'))
   9.599 -              (mk_srel_Id_tac live (Lazy.force srel_Gr) (#map_id axioms))
   9.600 +              (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
   9.601 +                HOLogic.eq_const CA'))
   9.602 +              (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms))
   9.603              |> Thm.close_derivation
   9.604            end;
   9.605  
   9.606 -        val srel_Id = Lazy.lazy mk_srel_Id;
   9.607 +        val rel_eq = Lazy.lazy mk_rel_eq;
   9.608  
   9.609 -        fun mk_srel_converse () =
   9.610 +        fun mk_rel_conversep () =
   9.611            let
   9.612 -            val srelBsAs = mk_bnf_srel setRT's CB' CA';
   9.613 -            val lhs = Term.list_comb (srelBsAs, map mk_converse Rs);
   9.614 -            val rhs = mk_converse (Term.list_comb (srel, Rs));
   9.615 -            val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
   9.616 +            val relBsAs = mk_bnf_rel pred2RT's CB' CA';
   9.617 +            val lhs = Term.list_comb (relBsAs, map mk_conversep Rs);
   9.618 +            val rhs = mk_conversep (Term.list_comb (rel, Rs));
   9.619 +            val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
   9.620              val le_thm = Goal.prove_sorry lthy [] [] le_goal
   9.621 -              (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
   9.622 +              (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
   9.623                  (Lazy.force map_comp') (map Lazy.force set_map'))
   9.624                |> Thm.close_derivation
   9.625              val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
   9.626            in
   9.627 -            Goal.prove_sorry lthy [] [] goal (fn _ => mk_srel_converse_tac le_thm)
   9.628 +            Goal.prove_sorry lthy [] [] goal
   9.629 +              (K (mk_rel_conversep_tac le_thm (Lazy.force rel_mono)))
   9.630              |> Thm.close_derivation
   9.631            end;
   9.632  
   9.633 -        val srel_converse = Lazy.lazy mk_srel_converse;
   9.634 +        val rel_conversep = Lazy.lazy mk_rel_conversep;
   9.635  
   9.636 -        fun mk_srel_O () =
   9.637 +        fun mk_rel_OO () =
   9.638            let
   9.639 -            val srelAsCs = mk_bnf_srel setRTsAsCs CA' CC';
   9.640 -            val srelBsCs = mk_bnf_srel setRTsBsCs CB' CC';
   9.641 -            val lhs = Term.list_comb (srelAsCs, map2 (curry mk_rel_comp) Rs Ss);
   9.642 -            val rhs = mk_rel_comp (Term.list_comb (srel, Rs), Term.list_comb (srelBsCs, Ss));
   9.643 +            val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC';
   9.644 +            val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC';
   9.645 +            val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss);
   9.646 +            val rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
   9.647              val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
   9.648            in
   9.649              Goal.prove_sorry lthy [] [] goal
   9.650 -              (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
   9.651 +              (mk_rel_OO_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
   9.652                  (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_map'))
   9.653              |> Thm.close_derivation
   9.654            end;
   9.655  
   9.656 -        val srel_O = Lazy.lazy mk_srel_O;
   9.657 +        val rel_OO = Lazy.lazy mk_rel_OO;
   9.658  
   9.659 -        fun mk_in_srel () =
   9.660 +        fun mk_in_rel () =
   9.661            let
   9.662 -            val bnf_in = mk_in Rs (map (mk_bnf_t RTs) bnf_sets) CRs';
   9.663 +            val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
   9.664              val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
   9.665              val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
   9.666              val map_fst_eq = HOLogic.mk_eq (map1 $ z, x);
   9.667              val map_snd_eq = HOLogic.mk_eq (map2 $ z, y);
   9.668 -            val lhs = HOLogic.mk_mem (HOLogic.mk_prod (x, y), Term.list_comb (srel, Rs));
   9.669 +            val lhs = Term.list_comb (rel, Rs) $ x $ y;
   9.670              val rhs =
   9.671                HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
   9.672                  HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
   9.673              val goal =
   9.674                fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
   9.675            in
   9.676 -            Goal.prove_sorry lthy [] [] goal (mk_in_srel_tac srel_O_Grs (length bnf_sets))
   9.677 +            Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac rel_OO_Grps)
   9.678              |> Thm.close_derivation
   9.679            end;
   9.680  
   9.681 -        val in_srel = Lazy.lazy mk_in_srel;
   9.682 -
   9.683 -        val eqset_imp_iff_pair = @{thm eqset_imp_iff_pair};
   9.684 -        val mem_Collect_etc = @{thms fst_conv mem_Collect_eq prod.cases snd_conv};
   9.685 -        val mem_Collect_etc' = @{thms fst_conv mem_Collect_eq pair_in_Id_conv snd_conv};
   9.686 +        val in_rel = Lazy.lazy mk_in_rel;
   9.687  
   9.688 -        fun mk_rel_srel () =
   9.689 -          unfold_thms lthy mem_Collect_etc
   9.690 -            (funpow live (fn thm => thm RS @{thm fun_cong_pair}) (bnf_srel_def RS meta_eq_to_obj_eq)
   9.691 -               RS eqset_imp_iff_pair RS sym)
   9.692 -          |> Drule.zero_var_indexes;
   9.693 -
   9.694 -        val rel_srel = Lazy.lazy mk_rel_srel;
   9.695 -
   9.696 -        fun mk_rel_eq () =
   9.697 -          unfold_thms lthy (bnf_srel_def :: mem_Collect_etc')
   9.698 -            (Lazy.force srel_Id RS @{thm arg_cong[of _ _ "%A x y. (x, y) : A"]})
   9.699 -          |> Drule.eta_contraction_rule;
   9.700 -
   9.701 -        val rel_eq = Lazy.lazy mk_rel_eq;
   9.702 +        val predicate2_cong = @{thm predicate2_cong};
   9.703 +        val mem_Collect_etc = @{thms fst_conv mem_Collect_eq prod.cases snd_conv};
   9.704  
   9.705          fun mk_rel_flip () =
   9.706            let
   9.707 -            val srel_converse_thm = Lazy.force srel_converse;
   9.708 -            val cts = map (SOME o certify lthy) sQs;
   9.709 -            val srel_converse_thm' = cterm_instantiate_pos cts srel_converse_thm;
   9.710 +            val rel_conversep_thm = Lazy.force rel_conversep;
   9.711 +            val cts = map (SOME o certify lthy) Rs;
   9.712 +            val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
   9.713            in
   9.714 -            unfold_thms lthy (bnf_srel_def :: @{thm converse_iff} :: mem_Collect_etc)
   9.715 -              (srel_converse_thm' RS eqset_imp_iff_pair)
   9.716 +            unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS predicate2_cong)
   9.717              |> singleton (Proof_Context.export names_lthy pre_names_lthy)
   9.718            end;
   9.719  
   9.720          val rel_flip = Lazy.lazy mk_rel_flip;
   9.721  
   9.722 -        val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def;
   9.723 +        val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
   9.724  
   9.725          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono
   9.726 -          in_srel map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_map'
   9.727 -          srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O;
   9.728 +          in_rel map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map'
   9.729 +          rel_cong rel_mono rel_Grp rel_conversep rel_OO;
   9.730  
   9.731          val wits = map2 mk_witness bnf_wits wit_thms;
   9.732  
   9.733          val bnf_rel =
   9.734            Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;
   9.735 -        val bnf_srel =
   9.736 -          Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) srel;
   9.737  
   9.738          val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts
   9.739 -          wits bnf_rel bnf_srel;
   9.740 +          wits bnf_rel;
   9.741        in
   9.742          (bnf, lthy
   9.743            |> (if fact_policy = Note_All then
   9.744 @@ -1208,7 +1125,7 @@
   9.745                      (collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
   9.746                      (in_bdN, [#in_bd axioms]),
   9.747                      (in_monoN, [Lazy.force (#in_mono facts)]),
   9.748 -                    (in_srelN, [Lazy.force (#in_srel facts)]),
   9.749 +                    (in_relN, [Lazy.force (#in_rel facts)]),
   9.750                      (map_compN, [#map_comp axioms]),
   9.751                      (map_idN, [#map_id axioms]),
   9.752                      (map_wpullN, [#map_wpull axioms]),
   9.753 @@ -1232,14 +1149,12 @@
   9.754                      (map_id'N, [Lazy.force (#map_id' facts)], []),
   9.755                      (rel_eqN, [Lazy.force (#rel_eq facts)], []),
   9.756                      (rel_flipN, [Lazy.force (#rel_flip facts)], []),
   9.757 -                    (rel_srelN, [Lazy.force (#rel_srel facts)], []),
   9.758                      (set_map'N, map Lazy.force (#set_map' facts), []),
   9.759 -                    (srel_O_GrN, srel_O_Grs, []),
   9.760 -                    (srel_IdN, [Lazy.force (#srel_Id facts)], []),
   9.761 -                    (srel_GrN, [Lazy.force (#srel_Gr facts)], []),
   9.762 -                    (srel_converseN, [Lazy.force (#srel_converse facts)], []),
   9.763 -                    (srel_monoN, [Lazy.force (#srel_mono facts)], []),
   9.764 -                    (srel_ON, [Lazy.force (#srel_O facts)], [])]
   9.765 +                    (rel_OO_GrpN, rel_OO_Grps, []),
   9.766 +                    (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
   9.767 +                    (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
   9.768 +                    (rel_monoN, [Lazy.force (#rel_mono facts)], []),
   9.769 +                    (rel_OON, [Lazy.force (#rel_OO facts)], [])]
   9.770                      |> filter_out (null o #2)
   9.771                      |> map (fn (thmN, thms, attrs) =>
   9.772                        ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)),
   9.773 @@ -1252,8 +1167,7 @@
   9.774        end;
   9.775  
   9.776      val one_step_defs =
   9.777 -      no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def,
   9.778 -        bnf_srel_def]);
   9.779 +      no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
   9.780    in
   9.781      (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
   9.782    end;
    10.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Tue May 07 11:27:29 2013 +0200
    10.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Tue May 07 14:22:54 2013 +0200
    10.3 @@ -16,16 +16,16 @@
    10.4    val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
    10.5    val mk_set_map': thm -> thm
    10.6  
    10.7 -  val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
    10.8 +  val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
    10.9      {prems: thm list, context: Proof.context} -> tactic
   10.10 -  val mk_srel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
   10.11 -  val mk_srel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
   10.12 +  val mk_rel_eq_tac: int -> thm -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
   10.13 +  val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
   10.14      {prems: thm list, context: Proof.context} -> tactic
   10.15 -  val mk_in_srel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
   10.16 -  val mk_srel_converse_tac: thm -> tactic
   10.17 -  val mk_srel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
   10.18 +  val mk_in_rel_tac: thm list -> {prems: 'b, context: Proof.context} -> tactic
   10.19 +  val mk_rel_conversep_tac: thm -> thm -> tactic
   10.20 +  val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
   10.21      {prems: thm list, context: Proof.context} -> tactic
   10.22 -  val mk_srel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
   10.23 +  val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
   10.24  end;
   10.25  
   10.26  structure BNF_Def_Tactics : BNF_DEF_TACTICS =
   10.27 @@ -71,86 +71,77 @@
   10.28          rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
   10.29          rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
   10.30  
   10.31 -fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_maps
   10.32 +fun mk_rel_Grp_tac rel_OO_Grps map_id map_cong0 map_id' map_comp set_maps
   10.33    {context = ctxt, prems = _} =
   10.34    let
   10.35      val n = length set_maps;
   10.36    in
   10.37      if null set_maps then
   10.38 -      unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
   10.39 -    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
   10.40 -      EVERY' [rtac equalityI, rtac subsetI,
   10.41 -        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
   10.42 -        REPEAT_DETERM o dtac Pair_eqD,
   10.43 -        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
   10.44 -        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
   10.45 -        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
   10.46 -        REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
   10.47 -          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   10.48 -          rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
   10.49 -          rtac (@{thm snd_conv} RS sym)],
   10.50 +      unfold_thms_tac ctxt ((map_id RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
   10.51 +      rtac @{thm Grp_UNIV_idI[OF refl]} 1
   10.52 +    else unfold_thms_tac ctxt rel_OO_Grps THEN
   10.53 +      EVERY' [rtac @{thm antisym}, rtac @{thm predicate2I},
   10.54 +        REPEAT_DETERM o
   10.55 +          eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
   10.56 +        hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
   10.57 +        REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac],
   10.58          rtac CollectI,
   10.59          CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
   10.60 -          rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
   10.61 -          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   10.62 -          stac @{thm fst_conv}, atac]) set_maps,
   10.63 -        rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
   10.64 -        REPEAT_DETERM o dtac Pair_eqD,
   10.65 -        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
   10.66 -        rtac @{thm relcompI}, rtac @{thm converseI},
   10.67 +          rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac])
   10.68 +        set_maps,
   10.69 +        rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE],
   10.70 +        hyp_subst_tac ctxt,
   10.71 +        rtac @{thm relcomppI}, rtac @{thm conversepI},
   10.72          EVERY' (map2 (fn convol => fn map_id =>
   10.73 -          EVERY' [rtac CollectI, rtac exI, rtac conjI,
   10.74 -            rtac Pair_eqI, rtac conjI, rtac refl, rtac sym,
   10.75 -            rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
   10.76 +          EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
   10.77              REPEAT_DETERM_N n o rtac (convol RS fun_cong),
   10.78              REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   10.79              rtac CollectI,
   10.80              CONJ_WRAP' (fn thm =>
   10.81                EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
   10.82 -                rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac])
   10.83 +                rtac @{thm convol_mem_GrpI[OF refl]}, etac set_mp, atac])
   10.84              set_maps])
   10.85            @{thms fst_convol snd_convol} [map_id', refl])] 1
   10.86    end;
   10.87  
   10.88 -fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
   10.89 -  unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
   10.90 -  (if n = 0 then rtac refl 1
   10.91 -  else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
   10.92 -    rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
   10.93 -    CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id] 1);
   10.94 +fun mk_rel_eq_tac n rel_Grp rel_cong map_id {context = ctxt, prems = _} =
   10.95 +  (EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN'
   10.96 +  rtac (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
   10.97 +  (if n = 0 then rtac refl
   10.98 +  else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ "Grp"]},
   10.99 +    rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI,
  10.100 +    CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id])) 1;
  10.101  
  10.102 -fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} =
  10.103 -  unfold_thms_tac ctxt srel_O_Grs THEN
  10.104 -    EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
  10.105 -      rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
  10.106 -      rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
  10.107 +fun mk_rel_mono_tac rel_OO_Grps in_mono {context = ctxt, prems = _} =
  10.108 +  unfold_thms_tac ctxt rel_OO_Grps THEN
  10.109 +    EVERY' [rtac @{thm relcompp_mono}, rtac @{thm iffD2[OF conversep_mono]},
  10.110 +      rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono},
  10.111 +      rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1;
  10.112  
  10.113 -fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_maps
  10.114 +fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
  10.115    {context = ctxt, prems = _} =
  10.116    let
  10.117      val n = length set_maps;
  10.118    in
  10.119 -    if null set_maps then
  10.120 -      unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
  10.121 -    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
  10.122 -      EVERY' [rtac @{thm subrelI},
  10.123 -        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
  10.124 -        REPEAT_DETERM o dtac Pair_eqD,
  10.125 -        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt, rtac @{thm converseI},
  10.126 -        rtac @{thm relcompI}, rtac @{thm converseI},
  10.127 -        EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
  10.128 -          rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
  10.129 +    if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1
  10.130 +    else unfold_thms_tac ctxt (rel_OO_Grps) THEN
  10.131 +      EVERY' [rtac @{thm predicate2I},
  10.132 +        REPEAT_DETERM o
  10.133 +          eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
  10.134 +        hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI},
  10.135 +        EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans,
  10.136            rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
  10.137            rtac (map_comp RS sym), rtac CollectI,
  10.138            CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
  10.139 -            etac @{thm flip_rel}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
  10.140 +            etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
  10.141    end;
  10.142  
  10.143 -fun mk_srel_converse_tac le_converse =
  10.144 -  EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
  10.145 -    rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
  10.146 +fun mk_rel_conversep_tac le_conversep rel_mono =
  10.147 +  EVERY' [rtac @{thm antisym}, rtac le_conversep, rtac @{thm xt1(6)}, rtac @{thm conversep_shift},
  10.148 +    rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
  10.149 +    REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
  10.150  
  10.151 -fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_maps
  10.152 +fun mk_rel_OO_tac rel_OO_Grs rel_eq map_cong0 map_wppull map_comp set_maps
  10.153    {context = ctxt, prems = _} =
  10.154    let
  10.155      val n = length set_maps;
  10.156 @@ -158,59 +149,48 @@
  10.157          CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
  10.158            rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps;
  10.159    in
  10.160 -    if null set_maps then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
  10.161 -    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
  10.162 -      EVERY' [rtac equalityI, rtac @{thm subrelI},
  10.163 -        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
  10.164 -        REPEAT_DETERM o dtac Pair_eqD,
  10.165 -        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
  10.166 -        rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
  10.167 -        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
  10.168 -        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
  10.169 -        REPEAT_DETERM_N n o rtac @{thm fst_fstO},
  10.170 -        in_tac @{thm fstO_in},
  10.171 -        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
  10.172 -        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
  10.173 -        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
  10.174 -          rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
  10.175 +    if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1
  10.176 +    else unfold_thms_tac ctxt rel_OO_Grs THEN
  10.177 +      EVERY' [rtac @{thm antisym}, rtac @{thm predicate2I},
  10.178 +        REPEAT_DETERM o
  10.179 +          eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
  10.180 +        hyp_subst_tac ctxt,
  10.181 +        rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
  10.182 +        rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
  10.183 +        REPEAT_DETERM_N n o rtac @{thm fst_fstOp},
  10.184 +        in_tac @{thm fstOp_in},
  10.185 +        rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
  10.186 +        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, 
  10.187 +          rtac ballE, rtac subst,
  10.188 +          rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE,
  10.189            etac set_mp, atac],
  10.190 -        in_tac @{thm fstO_in},
  10.191 -        rtac @{thm relcompI}, rtac @{thm converseI},
  10.192 -        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
  10.193 -        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
  10.194 +        in_tac @{thm fstOp_in},
  10.195 +        rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
  10.196 +        rtac trans, rtac map_comp, rtac map_cong0,
  10.197          REPEAT_DETERM_N n o rtac o_apply,
  10.198 -        in_tac @{thm sndO_in},
  10.199 -        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
  10.200 -        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
  10.201 -        REPEAT_DETERM_N n o rtac @{thm snd_sndO},
  10.202 -        in_tac @{thm sndO_in},
  10.203 -        rtac @{thm subrelI},
  10.204 -        REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
  10.205 -        REPEAT_DETERM o eresolve_tac [exE, conjE],
  10.206 -        REPEAT_DETERM o dtac Pair_eqD,
  10.207 -        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
  10.208 +        in_tac @{thm sndOp_in},
  10.209 +        rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
  10.210 +        REPEAT_DETERM_N n o rtac @{thm snd_sndOp},
  10.211 +        in_tac @{thm sndOp_in},
  10.212 +        rtac @{thm predicate2I},
  10.213 +        REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}],
  10.214 +        hyp_subst_tac ctxt,
  10.215          rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
  10.216 -        CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_maps,
  10.217 -        etac allE, etac impE, etac conjI, etac conjI, atac,
  10.218 +        CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps,
  10.219 +        etac allE, etac impE, etac conjI, etac conjI, etac sym,
  10.220          REPEAT_DETERM o eresolve_tac [bexE, conjE],
  10.221 -        rtac @{thm relcompI}, rtac @{thm converseI},
  10.222 -        EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
  10.223 -          rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
  10.224 +        rtac @{thm relcomppI}, rtac @{thm conversepI},
  10.225 +        EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans,
  10.226            rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
  10.227 -          rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
  10.228 +          rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
  10.229    end;
  10.230  
  10.231 -fun mk_in_srel_tac srel_O_Grs m {context = ctxt, prems = _} =
  10.232 -  let
  10.233 -    val ls' = replicate (Int.max (1, m)) ();
  10.234 -  in
  10.235 -    unfold_thms_tac ctxt (srel_O_Grs @
  10.236 -      @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
  10.237 -    EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI,
  10.238 -      rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
  10.239 -      REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
  10.240 -      REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
  10.241 -        CONJ_WRAP' (K atac) ls']] 1
  10.242 -  end;
  10.243 +fun mk_in_rel_tac rel_OO_Grs {context = ctxt, prems = _} =
  10.244 +  unfold_thms_tac ctxt rel_OO_Grs THEN
  10.245 +  EVERY' [rtac iffI,
  10.246 +    REPEAT_DETERM o eresolve_tac [@{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
  10.247 +    hyp_subst_tac ctxt, rtac exI, rtac conjI, atac, rtac conjI, rtac refl, rtac refl,
  10.248 +    REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},
  10.249 +    etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1;
  10.250  
  10.251  end;
    11.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue May 07 11:27:29 2013 +0200
    11.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue May 07 14:22:54 2013 +0200
    11.3 @@ -44,7 +44,7 @@
    11.4        Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
    11.5        mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
    11.6  val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
    11.7 -val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps};
    11.8 +val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps id_apply};
    11.9  
   11.10  val ss_if_True_False = simpset_of (ss_only @{thms if_True if_False} @{context});
   11.11  
    12.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue May 07 11:27:29 2013 +0200
    12.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue May 07 14:22:54 2013 +0200
    12.3 @@ -58,7 +58,6 @@
    12.4    val ctor_relN: string
    12.5    val ctor_set_inclN: string
    12.6    val ctor_set_set_inclN: string
    12.7 -  val ctor_srelN: string
    12.8    val disc_unfoldN: string
    12.9    val disc_unfold_iffN: string
   12.10    val disc_corecN: string
   12.11 @@ -77,9 +76,6 @@
   12.12    val dtor_relN: string
   12.13    val dtor_set_inclN: string
   12.14    val dtor_set_set_inclN: string
   12.15 -  val dtor_srelN: string
   12.16 -  val dtor_srel_coinductN: string
   12.17 -  val dtor_srel_strong_coinductN: string
   12.18    val dtor_strong_coinductN: string
   12.19    val dtor_unfoldN: string
   12.20    val dtor_unfold_uniqueN: string
   12.21 @@ -285,19 +281,15 @@
   12.22  val dtor_exhaustN = dtorN ^ "_" ^ exhaustN
   12.23  val ctor_relN = ctorN ^ "_" ^ relN
   12.24  val dtor_relN = dtorN ^ "_" ^ relN
   12.25 -val ctor_srelN = ctorN ^ "_" ^ srelN
   12.26 -val dtor_srelN = dtorN ^ "_" ^ srelN
   12.27  val inductN = "induct"
   12.28  val coinductN = coN ^ inductN
   12.29  val ctor_inductN = ctorN ^ "_" ^ inductN
   12.30  val ctor_induct2N = ctor_inductN ^ "2"
   12.31  val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
   12.32  val dtor_coinductN = dtorN ^ "_" ^ coinductN
   12.33 -val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN
   12.34  val strong_coinductN = "strong_" ^ coinductN
   12.35  val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN
   12.36  val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN
   12.37 -val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strong_coinductN
   12.38  val hsetN = "Hset"
   12.39  val hset_recN = hsetN ^ "_rec"
   12.40  val set_inclN = "set_incl"
    13.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue May 07 11:27:29 2013 +0200
    13.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue May 07 14:22:54 2013 +0200
    13.3 @@ -145,7 +145,7 @@
    13.4      val setssAs = mk_setss allAs;
    13.5      val setssAs' = transpose setssAs;
    13.6      val bis_setss = mk_setss (passiveAs @ RTs);
    13.7 -    val relsAsBs = map4 mk_srel_of_bnf Dss Ass Bss bnfs;
    13.8 +    val relsAsBs = map4 mk_rel_of_bnf Dss Ass Bss bnfs;
    13.9      val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
   13.10      val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
   13.11      val sum_bdT = fst (dest_relT (fastype_of sum_bd));
   13.12 @@ -226,14 +226,14 @@
   13.13      val map_wpulls = map map_wpull_of_bnf bnfs;
   13.14      val set_bdss = map set_bd_of_bnf bnfs;
   13.15      val set_map'ss = map set_map'_of_bnf bnfs;
   13.16 -    val srel_congs = map srel_cong_of_bnf bnfs;
   13.17 -    val srel_converses = map srel_converse_of_bnf bnfs;
   13.18 -    val srel_defs = map srel_def_of_bnf bnfs;
   13.19 -    val srel_Grs = map srel_Gr_of_bnf bnfs;
   13.20 -    val srel_Ids = map srel_Id_of_bnf bnfs;
   13.21 -    val srel_monos = map srel_mono_of_bnf bnfs;
   13.22 -    val srel_Os = map srel_O_of_bnf bnfs;
   13.23 -    val srel_O_Grs = map srel_O_Gr_of_bnf bnfs;
   13.24 +    val rel_congs = map rel_cong_of_bnf bnfs;
   13.25 +    val rel_converseps = map rel_conversep_of_bnf bnfs;
   13.26 +    val rel_defs = map rel_def_of_bnf bnfs;
   13.27 +    val rel_Grps = map rel_Grp_of_bnf bnfs;
   13.28 +    val rel_eqs = map rel_eq_of_bnf bnfs;
   13.29 +    val rel_monos = map rel_mono_of_bnf bnfs;
   13.30 +    val rel_OOs = map rel_OO_of_bnf bnfs;
   13.31 +    val rel_OO_Grps = map rel_OO_Grp_of_bnf bnfs;
   13.32  
   13.33      val timer = time (timer "Extracted terms & thms");
   13.34  
   13.35 @@ -341,7 +341,7 @@
   13.36        let
   13.37          val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
   13.38          fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
   13.39 -        fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_subset (set $ (s $ x)) B);
   13.40 +        fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
   13.41          val prems = map2 mk_prem zs Bs;
   13.42          val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) (As @ Bs) sets)
   13.43            ss zs setssAs;
   13.44 @@ -421,7 +421,7 @@
   13.45        let
   13.46          val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
   13.47          fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
   13.48 -          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_subset (mk_image f $ B1) B2)));
   13.49 +          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
   13.50          val image_goals = map3 mk_image_goal fs Bs B's;
   13.51          fun mk_elim_goal B mapAsBs f s s' x =
   13.52            fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
   13.53 @@ -439,7 +439,7 @@
   13.54  
   13.55      val mor_incl_thm =
   13.56        let
   13.57 -        val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy;
   13.58 +        val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
   13.59          val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
   13.60        in
   13.61          Goal.prove_sorry lthy [] []
   13.62 @@ -621,12 +621,12 @@
   13.63      val (set_incl_hset_thmss, set_hset_incl_hset_thmsss) =
   13.64        let
   13.65          fun mk_set_incl_hset s x set hset = fold_rev Logic.all (x :: ss)
   13.66 -          (HOLogic.mk_Trueprop (mk_subset (set $ (s $ x)) (hset $ x)));
   13.67 +          (HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (hset $ x)));
   13.68  
   13.69          fun mk_set_hset_incl_hset s x y set hset1 hset2 =
   13.70            fold_rev Logic.all (x :: y :: ss)
   13.71              (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (s $ y))),
   13.72 -            HOLogic.mk_Trueprop (mk_subset (hset1 $ x) (hset2 $ y))));
   13.73 +            HOLogic.mk_Trueprop (mk_leq (hset1 $ x) (hset2 $ y))));
   13.74  
   13.75          val set_incl_hset_goalss =
   13.76            map4 (fn s => fn x => fn sets => fn hsets =>
   13.77 @@ -672,8 +672,8 @@
   13.78          fun mk_set_incl_hin s x hsets1 set hsets2 T =
   13.79            fold_rev Logic.all (x :: ss @ As)
   13.80              (Logic.list_implies
   13.81 -              (map2 (fn hset => fn A => HOLogic.mk_Trueprop (mk_subset (hset $ x) A)) hsets1 As,
   13.82 -              HOLogic.mk_Trueprop (mk_subset (set $ (s $ x)) (mk_in As hsets2 T))));
   13.83 +              (map2 (fn hset => fn A => HOLogic.mk_Trueprop (mk_leq (hset $ x) A)) hsets1 As,
   13.84 +              HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (mk_in As hsets2 T))));
   13.85  
   13.86          val set_incl_hin_goalss =
   13.87            map4 (fn s => fn x => fn sets => fn hsets =>
   13.88 @@ -689,12 +689,12 @@
   13.89      val hset_minimal_thms =
   13.90        let
   13.91          fun mk_passive_prem set s x K =
   13.92 -          Logic.all x (HOLogic.mk_Trueprop (mk_subset (set $ (s $ x)) (K $ x)));
   13.93 +          Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (K $ x)));
   13.94  
   13.95          fun mk_active_prem s x1 K1 set x2 K2 =
   13.96            fold_rev Logic.all [x1, x2]
   13.97              (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (s $ x1))),
   13.98 -              HOLogic.mk_Trueprop (mk_subset (K2 $ x2) (K1 $ x1))));
   13.99 +              HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
  13.100  
  13.101          val premss = map2 (fn j => fn Ks =>
  13.102            map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) setssAs) ss zs Ks @
  13.103 @@ -704,7 +704,7 @@
  13.104  
  13.105          val hset_rec_minimal_thms =
  13.106            let
  13.107 -            fun mk_conjunct j T i K x = mk_subset (mk_hset_rec ss nat i j T $ x) (K $ x);
  13.108 +            fun mk_conjunct j T i K x = mk_leq (mk_hset_rec ss nat i j T $ x) (K $ x);
  13.109              fun mk_concl j T Ks = list_all_free zs
  13.110                (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks zs));
  13.111              val concls = map3 mk_concl ls passiveAs Kss;
  13.112 @@ -723,7 +723,7 @@
  13.113              goals ctss hset_rec_0ss' hset_rec_Sucss'
  13.114            end;
  13.115  
  13.116 -        fun mk_conjunct j T i K x = mk_subset (mk_hset ss i j T $ x) (K $ x);
  13.117 +        fun mk_conjunct j T i K x = mk_leq (mk_hset ss i j T $ x) (K $ x);
  13.118          fun mk_concl j T Ks = Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks zs);
  13.119          val concls = map3 mk_concl ls passiveAs Kss;
  13.120  
  13.121 @@ -793,7 +793,7 @@
  13.122      val bis_name = Binding.name_of bis_bind;
  13.123      val bis_def_bind = (Thm.def_binding bis_bind, []);
  13.124  
  13.125 -    fun mk_bis_le_conjunct R B1 B2 = mk_subset R (mk_Times (B1, B2));
  13.126 +    fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2));
  13.127      val bis_le = Library.foldr1 HOLogic.mk_conj (map3 mk_bis_le_conjunct Rs Bs B's)
  13.128  
  13.129      val bis_spec =
  13.130 @@ -849,13 +849,12 @@
  13.131          |> Thm.close_derivation
  13.132        end;
  13.133  
  13.134 -    val bis_srel_thm =
  13.135 +    val bis_rel_thm =
  13.136        let
  13.137 -        fun mk_conjunct R s s' b1 b2 srel =
  13.138 +        fun mk_conjunct R s s' b1 b2 rel =
  13.139            list_all_free [b1, b2] (HOLogic.mk_imp
  13.140              (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
  13.141 -            HOLogic.mk_mem (HOLogic.mk_prod (s $ b1, s' $ b2),
  13.142 -              Term.list_comb (srel, passive_Id_ons @ Rs))));
  13.143 +            Term.list_comb (rel, map mk_in_rel (passive_Id_ons @ Rs)) $ (s $ b1) $ (s' $ b2)));
  13.144  
  13.145          val rhs = HOLogic.mk_conj
  13.146            (bis_le, Library.foldr1 HOLogic.mk_conj
  13.147 @@ -864,7 +863,7 @@
  13.148          Goal.prove_sorry lthy [] []
  13.149            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
  13.150              (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
  13.151 -          (K (mk_bis_srel_tac lthy m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss))
  13.152 +          (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comp's map_cong0s set_map'ss))
  13.153          |> Thm.close_derivation
  13.154        end;
  13.155  
  13.156 @@ -874,7 +873,7 @@
  13.157            (Logic.mk_implies
  13.158              (HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
  13.159              HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
  13.160 -        (K (mk_bis_converse_tac m bis_srel_thm srel_congs srel_converses))
  13.161 +        (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converseps))
  13.162        |> Thm.close_derivation;
  13.163  
  13.164      val bis_O_thm =
  13.165 @@ -888,7 +887,7 @@
  13.166          Goal.prove_sorry lthy [] []
  13.167            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
  13.168              (Logic.list_implies (prems, concl)))
  13.169 -          (K (mk_bis_O_tac lthy m bis_srel_thm srel_congs srel_Os))
  13.170 +          (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs))
  13.171          |> Thm.close_derivation
  13.172        end;
  13.173  
  13.174 @@ -900,7 +899,7 @@
  13.175          Goal.prove_sorry lthy [] []
  13.176            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
  13.177              (Logic.list_implies ([coalg_prem, mor_prem], concl)))
  13.178 -          (mk_bis_Gr_tac bis_srel_thm srel_Grs mor_image_thms morE_thms coalg_in_thms)
  13.179 +          (mk_bis_Gr_tac bis_rel_thm rel_Grps mor_image_thms morE_thms coalg_in_thms)
  13.180          |> Thm.close_derivation
  13.181        end;
  13.182  
  13.183 @@ -988,7 +987,7 @@
  13.184  
  13.185      val incl_lsbis_thms =
  13.186        let
  13.187 -        fun mk_concl i R = HOLogic.mk_Trueprop (mk_subset R (mk_lsbis As Bs ss i));
  13.188 +        fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis As Bs ss i));
  13.189          val goals = map2 (fn i => fn R => fold_rev Logic.all (As @ Bs @ ss @ sRs)
  13.190            (Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
  13.191        in
  13.192 @@ -1160,7 +1159,7 @@
  13.193          val lhs = Term.list_comb (Free (isNode_name i, isNodeT), As @ [Kl, lab, kl]);
  13.194          val rhs = list_exists_free [x]
  13.195            (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
  13.196 -          map2 mk_subset passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
  13.197 +          map2 mk_leq passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
  13.198        in
  13.199          mk_Trueprop_eq (lhs, rhs)
  13.200        end;
  13.201 @@ -1184,7 +1183,7 @@
  13.202      val isTree =
  13.203        let
  13.204          val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl);
  13.205 -        val Field = mk_subset Kl (mk_Field (mk_clists sum_sbd));
  13.206 +        val Field = mk_leq Kl (mk_Field (mk_clists sum_sbd));
  13.207          val prefCl = mk_prefCl Kl;
  13.208  
  13.209          val tree = mk_Ball Kl (Term.absfree kl'
  13.210 @@ -1345,7 +1344,7 @@
  13.211  
  13.212                  fun mk_inner_conjunct j T i x set i' carT =
  13.213                    HOLogic.mk_imp (HOLogic.mk_conj (mk_Kl_lab carT, mk_lab_kl i x),
  13.214 -                    mk_subset (set $ x) (mk_hset strTAs i' j T $ Kl_lab));
  13.215 +                    mk_leq (set $ x) (mk_hset strTAs i' j T $ Kl_lab));
  13.216  
  13.217                  fun mk_conjunct j T i x set =
  13.218                    Library.foldr1 HOLogic.mk_conj (map2 (mk_inner_conjunct j T i x set) ks carTAs);
  13.219 @@ -1562,7 +1561,7 @@
  13.220  
  13.221      val Lev_sbd_thms =
  13.222        let
  13.223 -        fun mk_conjunct i z = mk_subset (mk_Lev ss nat i $ z) (mk_Field (mk_clists sum_sbd));
  13.224 +        fun mk_conjunct i z = mk_leq (mk_Lev ss nat i $ z) (mk_Field (mk_clists sum_sbd));
  13.225          val goal = list_all_free zs
  13.226            (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs));
  13.227  
  13.228 @@ -1654,7 +1653,7 @@
  13.229      val set_rv_Lev_thmsss = if m = 0 then replicate n (replicate n []) else
  13.230        let
  13.231          fun mk_case s sets z z_free = Term.absfree z_free (Library.foldr1 HOLogic.mk_conj
  13.232 -          (map2 (fn set => fn A => mk_subset (set $ (s $ z)) A) (take m sets) As));
  13.233 +          (map2 (fn set => fn A => mk_leq (set $ (s $ z)) A) (take m sets) As));
  13.234  
  13.235          fun mk_conjunct i z B = HOLogic.mk_imp
  13.236            (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), HOLogic.mk_mem (z, B)),
  13.237 @@ -1980,7 +1979,7 @@
  13.238        let
  13.239          val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs dtors TRs);
  13.240          val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  13.241 -          (map2 (fn R => fn T => mk_subset R (Id_const T)) TRs Ts));
  13.242 +          (map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
  13.243          val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl));
  13.244        in
  13.245          `split_conj_thm (Goal.prove_sorry lthy [] [] goal
  13.246 @@ -2205,49 +2204,46 @@
  13.247      val timer = time (timer "corec definitions & thms");
  13.248  
  13.249      (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
  13.250 -    val (dtor_map_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_coinduct_thm,
  13.251 -         dtor_map_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, dtor_strong_coinduct_thm) =
  13.252 +    val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm,
  13.253 +         dtor_map_strong_coinduct_thm, dtor_strong_coinduct_thm) =
  13.254        let
  13.255          val zs = Jzs1 @ Jzs2;
  13.256          val frees = phis @ zs;
  13.257  
  13.258 -        fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_Id_on passive_UNIVs;
  13.259 -
  13.260          fun mk_phi strong_eq phi z1 z2 = if strong_eq
  13.261            then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2)
  13.262              (HOLogic.mk_disj (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2))))
  13.263            else phi;
  13.264  
  13.265 -        fun phi_srels strong_eq = map4 (fn phi => fn T => fn z1 => fn z2 =>
  13.266 -          HOLogic.Collect_const (HOLogic.mk_prodT (T, T)) $
  13.267 -            HOLogic.mk_split (mk_phi strong_eq phi z1 z2)) phis Ts Jzs1 Jzs2;
  13.268 -
  13.269 -        val srels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
  13.270 +        fun phi_rels strong_eq =
  13.271 +          map3 (fn phi => fn z1 => fn z2 => mk_phi strong_eq phi z1 z2) phis Jzs1 Jzs2;
  13.272 +
  13.273 +        val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
  13.274  
  13.275          fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
  13.276          val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  13.277            (map3 mk_concl phis Jzs1 Jzs2));
  13.278  
  13.279 -        fun mk_srel_prem strong_eq phi dtor srel Jz Jz_copy =
  13.280 +        fun mk_rel_prem strong_eq phi dtor rel Jz Jz_copy =
  13.281            let
  13.282 -            val concl = HOLogic.mk_mem (HOLogic.mk_tuple [dtor $ Jz, dtor $ Jz_copy],
  13.283 -              Term.list_comb (srel, mk_Ids strong_eq @ phi_srels strong_eq));
  13.284 +            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phi_rels strong_eq) $
  13.285 +              (dtor $ Jz) $ (dtor $ Jz_copy);
  13.286            in
  13.287              HOLogic.mk_Trueprop
  13.288                (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
  13.289            end;
  13.290  
  13.291 -        val srel_prems = map5 (mk_srel_prem false) phis dtors srels Jzs Jzs_copy;
  13.292 -        val srel_strong_prems = map5 (mk_srel_prem true) phis dtors srels Jzs Jzs_copy;
  13.293 -
  13.294 -        val dtor_srel_coinduct_goal =
  13.295 -          fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl));
  13.296 -        val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []);
  13.297 -
  13.298 -        val dtor_srel_coinduct = unfold_thms lthy @{thms Id_on_UNIV}
  13.299 -          (Goal.prove_sorry lthy [] [] dtor_srel_coinduct_goal
  13.300 -            (K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
  13.301 -          |> Thm.close_derivation);
  13.302 +        val rel_prems = map5 (mk_rel_prem false) phis dtors rels Jzs Jzs_copy;
  13.303 +        val rel_strong_prems = map5 (mk_rel_prem true) phis dtors rels Jzs Jzs_copy;
  13.304 +
  13.305 +        val dtor_coinduct_goal =
  13.306 +          fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
  13.307 +        val coinduct_params = rev (Term.add_tfrees dtor_coinduct_goal []);
  13.308 +
  13.309 +        val dtor_coinduct =
  13.310 +          Goal.prove_sorry lthy [] [] dtor_coinduct_goal
  13.311 +            (K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs))
  13.312 +          |> Thm.close_derivation;
  13.313  
  13.314          fun mk_prem strong_eq phi dtor map_nth sets Jz Jz_copy FJz =
  13.315            let
  13.316 @@ -2277,19 +2273,18 @@
  13.317          val strong_prems = mk_prems true;
  13.318  
  13.319          val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl));
  13.320 -        val dtor_map_coinduct = Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal
  13.321 -          (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
  13.322 +        val dtor_map_coinduct =
  13.323 +          Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal
  13.324 +            (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
  13.325            |> Thm.close_derivation;
  13.326  
  13.327          val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
  13.328          val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
  13.329  
  13.330 -        val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
  13.331 +        val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
  13.332            (Goal.prove_sorry lthy [] []
  13.333 -            (fold_rev Logic.all zs (Logic.list_implies (srel_strong_prems, concl)))
  13.334 -            (fn _ =>
  13.335 -              mk_dtor_srel_strong_coinduct_tac lthy
  13.336 -                m cTs cts dtor_srel_coinduct srel_monos srel_Ids))
  13.337 +            (fold_rev Logic.all zs (Logic.list_implies (rel_strong_prems, concl)))
  13.338 +            (K (mk_dtor_strong_coinduct_tac lthy m cTs cts dtor_coinduct rel_monos rel_eqs)))
  13.339            |> Thm.close_derivation;
  13.340  
  13.341          val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
  13.342 @@ -2298,15 +2293,9 @@
  13.343              (K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def
  13.344                (tcoalg_thm RS bis_Id_on_thm))))
  13.345            |> Thm.close_derivation;
  13.346 -
  13.347 -        val rel_of_srel_thms =
  13.348 -          srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
  13.349 -
  13.350 -        val dtor_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_coinduct;
  13.351 -        val dtor_strong_coinduct = unfold_thms lthy rel_of_srel_thms dtor_srel_strong_coinduct;
  13.352        in
  13.353 -        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_srel_coinduct,
  13.354 -         dtor_coinduct, dtor_map_strong_coinduct, dtor_srel_strong_coinduct, dtor_strong_coinduct)
  13.355 +        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []),
  13.356 +         dtor_coinduct, dtor_map_strong_coinduct, dtor_strong_coinduct)
  13.357        end;
  13.358  
  13.359      val timer = time (timer "coinduction");
  13.360 @@ -2471,7 +2460,7 @@
  13.361  
  13.362              val le_goals = map
  13.363                (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
  13.364 -              (mk_goals (uncurry mk_subset));
  13.365 +              (mk_goals (uncurry mk_leq));
  13.366              val set_le_thmss = map split_conj_thm
  13.367                (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss =>
  13.368                  Goal.prove_sorry lthy [] [] goal
  13.369 @@ -2654,7 +2643,7 @@
  13.370          val pick_col_thmss =
  13.371            let
  13.372              fun mk_conjunct AX Jpair pick thePull col =
  13.373 -              HOLogic.mk_imp (HOLogic.mk_mem (Jpair, thePull), mk_subset (col $ (pick $ Jpair)) AX);
  13.374 +              HOLogic.mk_imp (HOLogic.mk_mem (Jpair, thePull), mk_leq (col $ (pick $ Jpair)) AX);
  13.375  
  13.376              fun mk_concl AX cols =
  13.377                list_all_free Jpairs (Library.foldr1 HOLogic.mk_conj
  13.378 @@ -2707,10 +2696,10 @@
  13.379            map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm
  13.380              mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss;
  13.381  
  13.382 -        val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
  13.383 +        val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
  13.384  
  13.385          val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
  13.386 -          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
  13.387 +          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_OO_Grp_tacs;
  13.388  
  13.389          val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
  13.390            let
  13.391 @@ -2915,57 +2904,38 @@
  13.392          val dtor_set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
  13.393          val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms;
  13.394  
  13.395 -        val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  13.396 -        val Jsrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Jbnfs;
  13.397          val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
  13.398          val Jrels = map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
  13.399  
  13.400 -        val JsrelRs = map (fn Jsrel => Term.list_comb (Jsrel, JRs)) Jsrels;
  13.401 -        val srelRs = map (fn srel => Term.list_comb (srel, JRs @ JsrelRs)) srels;
  13.402 -        val Jrelphis = map (fn Jsrel => Term.list_comb (Jsrel, Jphis)) Jrels;
  13.403 -        val relphis = map (fn srel => Term.list_comb (srel, Jphis @ Jrelphis)) rels;
  13.404 -
  13.405 -        val in_srels = map in_srel_of_bnf bnfs;
  13.406 -        val in_Jsrels = map in_srel_of_bnf Jbnfs;
  13.407 -        val Jsrel_defs = map srel_def_of_bnf Jbnfs;
  13.408 +        val Jrelphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jrels;
  13.409 +        val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels;
  13.410 +
  13.411 +        val in_rels = map in_rel_of_bnf bnfs;
  13.412 +        val in_Jrels = map in_rel_of_bnf Jbnfs;
  13.413          val Jrel_defs = map rel_def_of_bnf Jbnfs;
  13.414  
  13.415          val folded_dtor_map_thms = map fold_maps dtor_map_thms;
  13.416          val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss;
  13.417          val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss;
  13.418  
  13.419 -        val dtor_Jsrel_thms =
  13.420 +        val dtor_Jrel_thms =
  13.421            let
  13.422 -            fun mk_goal Jz Jz' dtor dtor' JsrelR srelR = fold_rev Logic.all (Jz :: Jz' :: JRs)
  13.423 -              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JsrelR),
  13.424 -                  HOLogic.mk_mem (HOLogic.mk_prod (dtor $ Jz, dtor' $ Jz'), srelR)));
  13.425 -            val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs;
  13.426 +            fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
  13.427 +              (mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')));
  13.428 +            val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
  13.429            in
  13.430 -            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
  13.431 +            map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
  13.432                fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
  13.433                fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
  13.434                Goal.prove_sorry lthy [] [] goal
  13.435 -                (K (mk_dtor_srel_tac lthy in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
  13.436 +                (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets
  13.437                    dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
  13.438                |> Thm.close_derivation)
  13.439 -            ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
  13.440 +            ks goals in_rels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
  13.441                dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss
  13.442                dtor_set_set_incl_thmsss
  13.443            end;
  13.444  
  13.445 -        val dtor_Jrel_thms =
  13.446 -          let
  13.447 -            fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
  13.448 -              (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz')));
  13.449 -            val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
  13.450 -          in
  13.451 -            map3 (fn goal => fn srel_def => fn dtor_Jsrel =>
  13.452 -              Goal.prove_sorry lthy [] [] goal
  13.453 -                (mk_ctor_or_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel)
  13.454 -              |> Thm.close_derivation)
  13.455 -            goals srel_defs dtor_Jsrel_thms
  13.456 -          end;
  13.457 -
  13.458          val timer = time (timer "additional properties");
  13.459  
  13.460          val ls' = if m = 1 then [0] else ls;
  13.461 @@ -2981,10 +2951,6 @@
  13.462            (dtor_relN, map single dtor_Jrel_thms),
  13.463            (dtor_set_inclN, dtor_set_incl_thmss),
  13.464            (dtor_set_set_inclN, map flat dtor_set_set_incl_thmsss)] @
  13.465 -          (if note_all then
  13.466 -             [(dtor_srelN, map single dtor_Jsrel_thms)]
  13.467 -           else
  13.468 -             []) @
  13.469            map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' folded_dtor_set_thmss
  13.470            |> maps (fn (thmN, thmss) =>
  13.471              map2 (fn b => fn thms =>
  13.472 @@ -2999,12 +2965,7 @@
  13.473          [(dtor_coinductN, [dtor_coinduct_thm]),
  13.474          (dtor_map_coinductN, [dtor_map_coinduct_thm]),
  13.475          (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
  13.476 -        (dtor_strong_coinductN, [dtor_strong_coinduct_thm])] @
  13.477 -        (if note_all then
  13.478 -           [(dtor_srel_coinductN, [dtor_srel_coinduct_thm]),
  13.479 -           (dtor_srel_strong_coinductN, [dtor_srel_strong_coinduct_thm])]
  13.480 -         else
  13.481 -           [])
  13.482 +        (dtor_strong_coinductN, [dtor_strong_coinduct_thm])]
  13.483          |> map (fn (thmN, thms) =>
  13.484            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
  13.485  
    14.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue May 07 11:27:29 2013 +0200
    14.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue May 07 14:22:54 2013 +0200
    14.3 @@ -18,7 +18,7 @@
    14.4    val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
    14.5    val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    14.6    val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
    14.7 -  val mk_bis_srel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
    14.8 +  val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
    14.9      thm list list -> tactic
   14.10    val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
   14.11      {prems: 'a, context: Proof.context} -> tactic
   14.12 @@ -46,10 +46,10 @@
   14.13    val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
   14.14      thm -> thm -> tactic
   14.15    val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
   14.16 -  val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
   14.17 -  val mk_dtor_srel_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
   14.18 +  val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
   14.19 +  val mk_dtor_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
   14.20      cterm option list -> thm -> thm list -> thm list -> tactic
   14.21 -  val mk_dtor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
   14.22 +  val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
   14.23      thm -> thm -> thm list -> thm list -> thm list list -> tactic
   14.24    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
   14.25      {prems: 'a, context: Proof.context} -> tactic
   14.26 @@ -259,50 +259,48 @@
   14.27    EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
   14.28      atac, atac, rtac (hset_def RS sym)] 1
   14.29  
   14.30 -fun mk_bis_srel_tac ctxt m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
   14.31 +fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comps map_cong0s set_mapss =
   14.32    let
   14.33 -    val n = length srel_O_Grs;
   14.34 -    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ srel_O_Grs);
   14.35 +    val n = length rel_OO_Grps;
   14.36 +    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
   14.37  
   14.38 -    fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) =
   14.39 +    fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
   14.40        EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
   14.41          etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
   14.42 -        rtac (srel_O_Gr RS equalityD2 RS set_mp),
   14.43 -        rtac @{thm relcompI}, rtac @{thm converseI},
   14.44 +        rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
   14.45 +        rtac @{thm relcomppI}, rtac @{thm conversepI},
   14.46          EVERY' (map (fn thm =>
   14.47 -          EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   14.48 -            rtac CollectI,
   14.49 +          EVERY' [rtac @{thm GrpI},
   14.50 +            rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
   14.51 +            REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac,
   14.52 +            REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
   14.53              CONJ_WRAP' (fn (i, thm) =>
   14.54                if i <= m
   14.55                then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
   14.56 -                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}]
   14.57 +                etac @{thm image_mono}, rtac @{thm image_subsetI},
   14.58 +                etac @{thm Collect_split_in_relI[OF Id_onI]}]
   14.59                else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
   14.60 -                rtac trans_fun_cong_image_id_id_apply, atac])
   14.61 -            (1 upto (m + n) ~~ set_maps),
   14.62 -            rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
   14.63 -            REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
   14.64 +                rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
   14.65 +            (1 upto (m + n) ~~ set_maps)])
   14.66            @{thms fst_diag_id snd_diag_id})];
   14.67  
   14.68 -    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) =
   14.69 +    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
   14.70        EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
   14.71          etac allE, etac allE, etac impE, atac,
   14.72 -        dtac (srel_O_Gr RS equalityD1 RS set_mp),
   14.73 -        REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
   14.74 -        REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
   14.75 -        REPEAT_DETERM o dtac Pair_eqD,
   14.76 -        REPEAT_DETERM o etac conjE,
   14.77 +        dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}),
   14.78 +        REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
   14.79 +          @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
   14.80          hyp_subst_tac ctxt,
   14.81 -        REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   14.82          rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   14.83          REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
   14.84          REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
   14.85 -        etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   14.86 +        atac, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   14.87          REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
   14.88          REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
   14.89          rtac trans, rtac map_cong0,
   14.90          REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
   14.91          REPEAT_DETERM_N n o rtac refl,
   14.92 -        etac sym, rtac CollectI,
   14.93 +        atac, rtac CollectI,
   14.94          CONJ_WRAP' (fn (i, thm) =>
   14.95            if i <= m
   14.96            then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
   14.97 @@ -316,45 +314,45 @@
   14.98        etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
   14.99    end;
  14.100  
  14.101 -fun mk_bis_converse_tac m bis_srel srel_congs srel_converses =
  14.102 -  EVERY' [stac bis_srel, dtac (bis_srel RS iffD1),
  14.103 +fun mk_bis_converse_tac m bis_rel rel_congs rel_converseps =
  14.104 +  EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
  14.105      REPEAT_DETERM o etac conjE, rtac conjI,
  14.106      CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
  14.107 -      rtac equalityD2, rtac @{thm converse_Times}])) srel_congs,
  14.108 -    CONJ_WRAP' (fn (srel_cong, srel_converse) =>
  14.109 -      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
  14.110 -        rtac (srel_cong RS trans),
  14.111 -        REPEAT_DETERM_N m o rtac (@{thm converse_Id_on} RS sym),
  14.112 -        REPEAT_DETERM_N (length srel_congs) o rtac refl,
  14.113 -        rtac srel_converse,
  14.114 +      rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
  14.115 +    CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
  14.116 +      EVERY' [rtac allI, rtac allI, rtac impI,
  14.117 +        rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
  14.118 +        REPEAT_DETERM_N m o rtac @{thm conversep_in_rel_Id_on},
  14.119 +        REPEAT_DETERM_N (length rel_congs) o rtac @{thm conversep_in_rel},
  14.120 +        rtac (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
  14.121          REPEAT_DETERM o etac allE,
  14.122 -        rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
  14.123 +        rtac @{thm conversepI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1;
  14.124  
  14.125 -fun mk_bis_O_tac ctxt m bis_srel srel_congs srel_Os =
  14.126 -  EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),
  14.127 +fun mk_bis_O_tac ctxt m bis_rel rel_congs rel_OOs =
  14.128 +  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
  14.129      REPEAT_DETERM o etac conjE, rtac conjI,
  14.130 -    CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
  14.131 -    CONJ_WRAP' (fn (srel_cong, srel_O) =>
  14.132 -      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
  14.133 -        rtac (srel_cong RS trans),
  14.134 -        REPEAT_DETERM_N m o rtac @{thm Id_on_Comp},
  14.135 -        REPEAT_DETERM_N (length srel_congs) o rtac refl,
  14.136 -        rtac srel_O,
  14.137 +    CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
  14.138 +    CONJ_WRAP' (fn (rel_cong, rel_OO) =>
  14.139 +      EVERY' [rtac allI, rtac allI, rtac impI,
  14.140 +        rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
  14.141 +        REPEAT_DETERM_N m o rtac @{thm relcompp_in_rel_Id_on},
  14.142 +        REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
  14.143 +        rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
  14.144          etac @{thm relcompE},
  14.145          REPEAT_DETERM o dtac Pair_eqD,
  14.146          etac conjE, hyp_subst_tac ctxt,
  14.147 -        REPEAT_DETERM o etac allE, rtac @{thm relcompI},
  14.148 -        etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
  14.149 +        REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
  14.150 +        etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
  14.151  
  14.152 -fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins
  14.153 +fun mk_bis_Gr_tac bis_rel rel_Grps mor_images morEs coalg_ins
  14.154    {context = ctxt, prems = _} =
  14.155 -  unfold_thms_tac ctxt (bis_srel :: @{thm Id_on_Gr} :: srel_Grs) THEN
  14.156 +  unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) THEN
  14.157    EVERY' [rtac conjI,
  14.158      CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
  14.159      CONJ_WRAP' (fn (coalg_in, morE) =>
  14.160 -      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrI}, etac coalg_in,
  14.161 -        etac @{thm GrD1}, etac (morE RS trans), etac @{thm GrD1},
  14.162 -        etac (@{thm GrD2} RS arg_cong)]) (coalg_ins ~~ morEs)] 1;
  14.163 +      EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrpI}, etac (morE RS trans),
  14.164 +        etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}])
  14.165 +    (coalg_ins ~~ morEs)] 1;
  14.166  
  14.167  fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} =
  14.168    let
  14.169 @@ -1130,26 +1128,31 @@
  14.170      (corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
  14.171    etac unfold_unique_mor 1;
  14.172  
  14.173 -fun mk_dtor_srel_coinduct_tac ks raw_coind bis_srel =
  14.174 -  EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI,
  14.175 -    CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
  14.176 -    CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI,
  14.177 -      REPEAT_DETERM o etac allE, etac mp, etac CollectE, etac @{thm splitD}])) ks,
  14.178 +fun mk_dtor_coinduct_tac m raw_coind bis_rel rel_congs =
  14.179 +  EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI,
  14.180 +    CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]}))
  14.181 +    rel_congs,
  14.182 +    CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI,
  14.183 +      REPEAT_DETERM o etac allE, rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
  14.184 +      REPEAT_DETERM_N m o rtac @{thm in_rel_Id_on_UNIV[symmetric]},
  14.185 +      REPEAT_DETERM_N (length rel_congs) o rtac @{thm in_rel_Collect_split_eq[symmetric]},
  14.186 +      etac mp, etac CollectE, etac @{thm splitD}])
  14.187 +    rel_congs,
  14.188      rtac impI, REPEAT_DETERM o etac conjE,
  14.189      CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
  14.190 -      rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
  14.191 +      rtac CollectI, etac @{thm prod_caseI}])) rel_congs] 1;
  14.192  
  14.193 -fun mk_dtor_srel_strong_coinduct_tac ctxt m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
  14.194 -  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_srel_coinduct),
  14.195 -    EVERY' (map2 (fn srel_mono => fn srel_Id =>
  14.196 +fun mk_dtor_strong_coinduct_tac ctxt m cTs cts dtor_coinduct rel_monos rel_eqs =
  14.197 +  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct),
  14.198 +    EVERY' (map2 (fn rel_mono => fn rel_eq =>
  14.199        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
  14.200 -        etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (srel_mono RS set_mp),
  14.201 -        REPEAT_DETERM_N m o rtac @{thm subset_refl},
  14.202 -        REPEAT_DETERM_N (length srel_monos) o rtac @{thm Id_subset},
  14.203 -        rtac (srel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
  14.204 -    srel_monos srel_Ids),
  14.205 +        etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (rel_mono RS @{thm predicate2D}),
  14.206 +        REPEAT_DETERM_N m o rtac @{thm order_refl},
  14.207 +        REPEAT_DETERM_N (length rel_monos) o rtac @{thm eq_subset},
  14.208 +        rtac (rel_eq RS sym RS @{thm eq_refl} RS @{thm predicate2D}), rtac refl])
  14.209 +    rel_monos rel_eqs),
  14.210      rtac impI, REPEAT_DETERM o etac conjE,
  14.211 -    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) srel_Ids] 1;
  14.212 +    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_eqs] 1;
  14.213  
  14.214  fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
  14.215    let
  14.216 @@ -1501,27 +1504,27 @@
  14.217    ALLGOALS (TRY o
  14.218      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
  14.219  
  14.220 -fun mk_dtor_srel_tac ctxt in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject
  14.221 +fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets dtor_inject
  14.222      dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
  14.223    let
  14.224      val m = length dtor_set_incls;
  14.225      val n = length dtor_set_set_inclss;
  14.226      val (passive_set_maps, active_set_maps) = chop m set_maps;
  14.227 -    val in_Jsrel = nth in_Jsrels (i - 1);
  14.228 +    val in_Jrel = nth in_Jrels (i - 1);
  14.229      val if_tac =
  14.230 -      EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  14.231 -        rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  14.232 +      EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  14.233 +        rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  14.234          EVERY' (map2 (fn set_map => fn set_incl =>
  14.235            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
  14.236              rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
  14.237              etac (set_incl RS @{thm subset_trans})])
  14.238          passive_set_maps dtor_set_incls),
  14.239 -        CONJ_WRAP' (fn (in_Jsrel, (set_map, dtor_set_set_incls)) =>
  14.240 -          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI},
  14.241 -            rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  14.242 +        CONJ_WRAP' (fn (in_Jrel, (set_map, dtor_set_set_incls)) =>
  14.243 +          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI,
  14.244 +            rtac @{thm prod_caseI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  14.245              CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
  14.246              rtac conjI, rtac refl, rtac refl])
  14.247 -        (in_Jsrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
  14.248 +        (in_Jrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
  14.249          CONJ_WRAP' (fn conv =>
  14.250            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
  14.251            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
  14.252 @@ -1529,30 +1532,38 @@
  14.253            rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
  14.254          @{thms fst_conv snd_conv}];
  14.255      val only_if_tac =
  14.256 -      EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  14.257 -        rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  14.258 +      EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  14.259 +        rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  14.260          CONJ_WRAP' (fn (dtor_set, passive_set_map) =>
  14.261            EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
  14.262              rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map,
  14.263              rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
  14.264              CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
  14.265 -              (fn (active_set_map, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
  14.266 +              (fn (active_set_map, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
  14.267                  rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
  14.268                  rtac active_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
  14.269                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
  14.270 -                dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
  14.271 +                dtac @{thm ssubst_mem[OF pair_collapse]},
  14.272 +                REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
  14.273 +                  @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
  14.274 +                hyp_subst_tac ctxt,
  14.275 +                dtac (in_Jrel RS iffD1),
  14.276                  dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
  14.277 -                dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
  14.278 -                hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  14.279 -            (rev (active_set_maps ~~ in_Jsrels))])
  14.280 +                TRY o
  14.281 +                  EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
  14.282 +                REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  14.283 +            (rev (active_set_maps ~~ in_Jrels))])
  14.284          (dtor_sets ~~ passive_set_maps),
  14.285          rtac conjI,
  14.286          REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
  14.287            rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
  14.288            rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
  14.289 -          EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
  14.290 -            dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
  14.291 -            dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jsrels),
  14.292 +          EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
  14.293 +            dtac @{thm ssubst_mem[OF pair_collapse]},
  14.294 +            REPEAT_DETERM o
  14.295 +              eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
  14.296 +            hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
  14.297 +            dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
  14.298            atac]]
  14.299    in
  14.300      EVERY' [rtac iffI, if_tac, only_if_tac] 1
    15.1 --- a/src/HOL/BNF/Tools/bnf_gfp_util.ML	Tue May 07 11:27:29 2013 +0200
    15.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_util.ML	Tue May 07 14:22:54 2013 +0200
    15.3 @@ -19,6 +19,7 @@
    15.4    val mk_congruent: term -> term -> term
    15.5    val mk_clists: term -> term
    15.6    val mk_Id_on: term -> term
    15.7 +  val mk_in_rel: term -> term
    15.8    val mk_equiv: term -> term -> term
    15.9    val mk_fromCard: term -> term -> term
   15.10    val mk_list_rec: term -> term -> term
   15.11 @@ -65,6 +66,11 @@
   15.12      val AAT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT AT);
   15.13    in Const (@{const_name Id_on}, AT --> AAT) $ A end;
   15.14  
   15.15 +fun mk_in_rel R =
   15.16 +  let
   15.17 +    val ((A, B), RT) = `dest_relT (fastype_of R);
   15.18 +  in Const (@{const_name in_rel}, RT --> mk_pred2T A B) $ R end;
   15.19 +
   15.20  fun mk_Times (A, B) =
   15.21    let val AT = HOLogic.dest_setT (fastype_of A);
   15.22    in mk_Sigma (A, Term.absdummy AT B) end;
    16.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Tue May 07 11:27:29 2013 +0200
    16.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Tue May 07 14:22:54 2013 +0200
    16.3 @@ -254,7 +254,7 @@
    16.4      val alg_set_thms =
    16.5        let
    16.6          val alg_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
    16.7 -        fun mk_prem x set B = HOLogic.mk_Trueprop (mk_subset (set $ x) B);
    16.8 +        fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
    16.9          fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
   16.10          val premss = map2 ((fn x => fn sets =>  map2 (mk_prem x) sets (As @ Bs))) xFs setssAs;
   16.11          val concls = map3 mk_concl ss xFs Bs;
   16.12 @@ -349,7 +349,7 @@
   16.13        let
   16.14          val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
   16.15          fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
   16.16 -          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_subset (mk_image f $ B1) B2)));
   16.17 +          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
   16.18          val image_goals = map3 mk_image_goal fs Bs B's;
   16.19          fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
   16.20            (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
   16.21 @@ -366,7 +366,7 @@
   16.22  
   16.23      val mor_incl_thm =
   16.24        let
   16.25 -        val prems = map2 (HOLogic.mk_Trueprop oo mk_subset) Bs Bs_copy;
   16.26 +        val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
   16.27          val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
   16.28        in
   16.29          Goal.prove_sorry lthy [] []
   16.30 @@ -392,7 +392,7 @@
   16.31  
   16.32      val mor_inv_thm =
   16.33        let
   16.34 -        fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_subset (mk_image inv_f $ B') B,
   16.35 +        fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_leq (mk_image inv_f $ B') B,
   16.36            HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
   16.37          val prems = map HOLogic.mk_Trueprop
   16.38            ([mk_mor Bs ss B's s's fs,
   16.39 @@ -672,7 +672,7 @@
   16.40            |> Thm.close_derivation;
   16.41  
   16.42          val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
   16.43 -        val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_subset min_algss Bs);
   16.44 +        val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
   16.45          val least_cT = certifyT lthy suc_bdT;
   16.46          val least_ct = certify lthy (Term.absfree idx' least_conjunction);
   16.47  
   16.48 @@ -748,7 +748,7 @@
   16.49          val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
   16.50          fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
   16.51            (fold_rev Logic.all (As @ Bs @ ss)
   16.52 -            (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_subset min_alg B))))
   16.53 +            (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B))))
   16.54            (K (mk_least_min_alg_tac def least_min_algs_thm))
   16.55            |> Thm.close_derivation;
   16.56  
   16.57 @@ -1695,10 +1695,10 @@
   16.58            in_incl_min_alg_thms card_of_min_alg_thms;
   16.59          val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
   16.60  
   16.61 -        val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
   16.62 +        val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
   16.63  
   16.64          val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
   16.65 -          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
   16.66 +          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_OO_Grp_tacs;
   16.67  
   16.68          val ctor_witss =
   16.69            let
   16.70 @@ -1745,20 +1745,15 @@
   16.71  
   16.72          val timer = time (timer "registered new datatypes as BNFs");
   16.73  
   16.74 -        val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
   16.75 -        val Isrels = map (mk_srel_of_bnf deads passiveAs passiveBs) Ibnfs;
   16.76          val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
   16.77          val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
   16.78  
   16.79 -        val IsrelRs = map (fn Isrel => Term.list_comb (Isrel, IRs)) Isrels;
   16.80 -        val srelRs = map (fn srel => Term.list_comb (srel, IRs @ IsrelRs)) srels;
   16.81 -        val Irelphis = map (fn Isrel => Term.list_comb (Isrel, Iphis)) Irels;
   16.82 -        val relphis = map (fn srel => Term.list_comb (srel, Iphis @ Irelphis)) rels;
   16.83 +        val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels;
   16.84 +        val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels;
   16.85  
   16.86 -        val in_srels = map in_srel_of_bnf bnfs;
   16.87 -        val in_Isrels = map in_srel_of_bnf Ibnfs;
   16.88 -        val srel_defs = map srel_def_of_bnf bnfs;
   16.89 -        val Isrel_defs = map srel_def_of_bnf Ibnfs;
   16.90 +        val in_rels = map in_rel_of_bnf bnfs;
   16.91 +        val in_Irels = map in_rel_of_bnf Ibnfs;
   16.92 +        val rel_defs = map rel_def_of_bnf bnfs;
   16.93          val Irel_defs = map rel_def_of_bnf Ibnfs;
   16.94  
   16.95          val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
   16.96 @@ -1767,38 +1762,24 @@
   16.97          val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss;
   16.98          val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss;
   16.99  
  16.100 -        val ctor_Isrel_thms =
  16.101 +        val ctor_Irel_thms =
  16.102            let
  16.103 -            fun mk_goal xF yF ctor ctor' IsrelR srelR = fold_rev Logic.all (xF :: yF :: IRs)
  16.104 -              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IsrelR),
  16.105 -                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), srelR)));
  16.106 -            val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs;
  16.107 +            fun mk_goal xF yF ctor ctor' Irelphi relphi = fold_rev Logic.all (xF :: yF :: Iphis)
  16.108 +              (mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF));
  16.109 +            val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
  16.110            in
  16.111 -            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
  16.112 +            map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
  16.113                fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
  16.114                fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
  16.115                Goal.prove_sorry lthy [] [] goal
  16.116 -               (K (mk_ctor_srel_tac lthy in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
  16.117 +               (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets
  16.118                   ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
  16.119                |> Thm.close_derivation)
  16.120 -            ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
  16.121 +            ks goals in_rels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
  16.122                ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss
  16.123                ctor_set_set_incl_thmsss
  16.124            end;
  16.125  
  16.126 -        val ctor_Irel_thms =
  16.127 -          let
  16.128 -            fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
  16.129 -              (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF));
  16.130 -            val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
  16.131 -          in
  16.132 -            map3 (fn goal => fn srel_def => fn ctor_Isrel =>
  16.133 -              Goal.prove_sorry lthy [] [] goal
  16.134 -                (mk_ctor_or_dtor_rel_tac srel_def Irel_defs Isrel_defs ctor_Isrel)
  16.135 -              |> Thm.close_derivation)
  16.136 -            goals srel_defs ctor_Isrel_thms
  16.137 -          end;
  16.138 -
  16.139          val timer = time (timer "additional properties");
  16.140  
  16.141          val ls' = if m = 1 then [0] else ls
  16.142 @@ -1813,10 +1794,6 @@
  16.143            (ctor_relN, map single ctor_Irel_thms),
  16.144            (ctor_set_inclN, ctor_set_incl_thmss),
  16.145            (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @
  16.146 -          (if note_all then
  16.147 -             [(ctor_srelN, map single ctor_Isrel_thms)]
  16.148 -           else
  16.149 -             []) @
  16.150            map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_ctor_set_thmss
  16.151            |> maps (fn (thmN, thmss) =>
  16.152              map2 (fn b => fn thms =>
    17.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Tue May 07 11:27:29 2013 +0200
    17.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Tue May 07 14:22:54 2013 +0200
    17.3 @@ -23,7 +23,7 @@
    17.4    val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
    17.5      {prems: 'a, context: Proof.context} -> tactic
    17.6    val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
    17.7 -  val mk_ctor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
    17.8 +  val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
    17.9      thm -> thm -> thm list -> thm list -> thm list list -> tactic
   17.10    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   17.11    val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
   17.12 @@ -774,32 +774,32 @@
   17.13            EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
   17.14              REPEAT_DETERM_N n o etac UnE]))))] 1);
   17.15  
   17.16 -fun mk_ctor_srel_tac ctxt in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
   17.17 +fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets ctor_inject
   17.18    ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
   17.19    let
   17.20      val m = length ctor_set_incls;
   17.21      val n = length ctor_set_set_inclss;
   17.22  
   17.23      val (passive_set_maps, active_set_maps) = chop m set_maps;
   17.24 -    val in_Isrel = nth in_Isrels (i - 1);
   17.25 +    val in_Irel = nth in_Irels (i - 1);
   17.26      val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
   17.27      val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
   17.28      val if_tac =
   17.29 -      EVERY' [dtac (in_Isrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
   17.30 -        rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   17.31 +      EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
   17.32 +        rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   17.33          EVERY' (map2 (fn set_map => fn ctor_set_incl =>
   17.34            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
   17.35              rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
   17.36              rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
   17.37          passive_set_maps ctor_set_incls),
   17.38 -        CONJ_WRAP' (fn (in_Isrel, (set_map, ctor_set_set_incls)) =>
   17.39 -          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI},
   17.40 -            rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   17.41 +        CONJ_WRAP' (fn (in_Irel, (set_map, ctor_set_set_incls)) =>
   17.42 +          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI,
   17.43 +            rtac @{thm prod_caseI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   17.44              CONJ_WRAP' (fn thm =>
   17.45                EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
   17.46              ctor_set_set_incls,
   17.47              rtac conjI, rtac refl, rtac refl])
   17.48 -        (in_Isrels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
   17.49 +        (in_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
   17.50          CONJ_WRAP' (fn conv =>
   17.51            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   17.52            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   17.53 @@ -808,29 +808,37 @@
   17.54            etac eq_arg_cong_ctor_dtor])
   17.55          fst_snd_convs];
   17.56      val only_if_tac =
   17.57 -      EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
   17.58 -        rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   17.59 +      EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
   17.60 +        rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   17.61          CONJ_WRAP' (fn (ctor_set, passive_set_map) =>
   17.62            EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least},
   17.63              rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
   17.64              rtac passive_set_map, rtac trans_fun_cong_image_id_id_apply, atac,
   17.65              CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
   17.66 -              (fn (active_set_map, in_Isrel) => EVERY' [rtac ord_eq_le_trans,
   17.67 +              (fn (active_set_map, in_Irel) => EVERY' [rtac ord_eq_le_trans,
   17.68                  rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map, rtac @{thm UN_least},
   17.69                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
   17.70 -                dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
   17.71 -                dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
   17.72 -                dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
   17.73 -                hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
   17.74 -            (rev (active_set_maps ~~ in_Isrels))])
   17.75 +                dtac @{thm ssubst_mem[OF pair_collapse]},
   17.76 +                REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
   17.77 +                  @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
   17.78 +                hyp_subst_tac ctxt,
   17.79 +                dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
   17.80 +                TRY o
   17.81 +                  EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
   17.82 +                REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
   17.83 +            (rev (active_set_maps ~~ in_Irels))])
   17.84          (ctor_sets ~~ passive_set_maps),
   17.85          rtac conjI,
   17.86          REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
   17.87            rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   17.88            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   17.89 -          EVERY' (map (fn in_Isrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
   17.90 -            dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
   17.91 -            dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Isrels),
   17.92 +          EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
   17.93 +            dtac @{thm ssubst_mem[OF pair_collapse]},
   17.94 +            REPEAT_DETERM o
   17.95 +              eresolve_tac (CollectE :: conjE :: @{thms prod_caseE iffD1[OF Pair_eq, elim_format]}),
   17.96 +            hyp_subst_tac ctxt,
   17.97 +            dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac])
   17.98 +          in_Irels),
   17.99            atac]]
  17.100    in
  17.101      EVERY' [rtac iffI, if_tac, only_if_tac] 1
    18.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Tue May 07 11:27:29 2013 +0200
    18.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Tue May 07 14:22:54 2013 +0200
    18.3 @@ -22,7 +22,6 @@
    18.4    val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
    18.5    val mk_Abs_inj_thm: thm -> thm
    18.6  
    18.7 -  val simple_srel_O_Gr_tac: Proof.context -> tactic
    18.8    val mk_ctor_or_dtor_rel_tac:
    18.9      thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
   18.10  
   18.11 @@ -86,9 +85,6 @@
   18.12      gen_tac
   18.13    end;
   18.14  
   18.15 -fun simple_srel_O_Gr_tac ctxt =
   18.16 -  unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
   18.17 -
   18.18  fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
   18.19    unfold_thms_tac ctxt IJrel_defs THEN
   18.20    rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
    19.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Tue May 07 11:27:29 2013 +0200
    19.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Tue May 07 14:22:54 2013 +0200
    19.3 @@ -77,6 +77,7 @@
    19.4    val mk_optionT: typ -> typ
    19.5    val mk_relT: typ * typ -> typ
    19.6    val dest_relT: typ -> typ * typ
    19.7 +  val dest_pred2T: typ -> typ * typ
    19.8    val mk_sumT: typ * typ -> typ
    19.9  
   19.10    val ctwo: term
   19.11 @@ -89,6 +90,7 @@
   19.12    val mk_Card_order: term -> term
   19.13    val mk_Field: term -> term
   19.14    val mk_Gr: term -> term -> term
   19.15 +  val mk_Grp: term -> term -> term
   19.16    val mk_IfN: typ -> term list -> term list -> term
   19.17    val mk_Trueprop_eq: term * term -> term
   19.18    val mk_UNION: term -> term -> term
   19.19 @@ -101,14 +103,16 @@
   19.20    val mk_cinfinite: term -> term
   19.21    val mk_collect: term list -> typ -> term
   19.22    val mk_converse: term -> term
   19.23 +  val mk_conversep: term -> term
   19.24    val mk_cprod: term -> term -> term
   19.25    val mk_csum: term -> term -> term
   19.26    val mk_dir_image: term -> term -> term
   19.27    val mk_image: term -> term
   19.28    val mk_in: term list -> term list -> typ -> term
   19.29 +  val mk_leq: term -> term -> term
   19.30    val mk_ordLeq: term -> term -> term
   19.31    val mk_rel_comp: term * term -> term
   19.32 -  val mk_subset: term -> term -> term
   19.33 +  val mk_rel_compp: term * term -> term
   19.34    val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
   19.35  
   19.36    val rapp: term -> term -> term
   19.37 @@ -386,6 +390,7 @@
   19.38  fun mk_optionT T = Type (@{type_name option}, [T]);
   19.39  val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT;
   19.40  val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT;
   19.41 +val dest_pred2T = apsnd Term.domain_type o Term.dest_funT;
   19.42  fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]);
   19.43  fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT;
   19.44  
   19.45 @@ -422,6 +427,23 @@
   19.46    let val ((AT, BT), FT) = `dest_funT (fastype_of f);
   19.47    in Const (@{const_name Gr}, HOLogic.mk_setT AT --> FT --> mk_relT (AT, BT)) $ A $ f end;
   19.48  
   19.49 +fun mk_conversep R =
   19.50 +  let
   19.51 +    val RT = dest_pred2T (fastype_of R);
   19.52 +    val RST = mk_pred2T (snd RT) (fst RT);
   19.53 +  in Const (@{const_name conversep}, fastype_of R --> RST) $ R end;
   19.54 +
   19.55 +fun mk_rel_compp (R, S) =
   19.56 +  let
   19.57 +    val RT = fastype_of R;
   19.58 +    val ST = fastype_of S;
   19.59 +    val RST = mk_pred2T (fst (dest_pred2T RT)) (snd (dest_pred2T ST));
   19.60 +  in Const (@{const_name relcompp}, RT --> ST --> RST) $ R $ S end;
   19.61 +
   19.62 +fun mk_Grp A f =
   19.63 +  let val ((AT, BT), FT) = `dest_funT (fastype_of f);
   19.64 +  in Const (@{const_name Grp}, HOLogic.mk_setT AT --> FT --> mk_pred2T AT BT) $ A $ f end;
   19.65 +
   19.66  fun mk_image f =
   19.67    let val (T, U) = dest_funT (fastype_of f);
   19.68    in Const (@{const_name image},
   19.69 @@ -528,7 +550,7 @@
   19.70          A $ B1 $ B2 $ f1 $ f2 $ e1 $ e2 $ p1 $ p2)
   19.71    end;
   19.72  
   19.73 -fun mk_subset t1 t2 =
   19.74 +fun mk_leq t1 t2 =
   19.75    Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;
   19.76  
   19.77  fun mk_card_binop binop typop t1 t2 =