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