# HG changeset patch # User blanchet # Date 1348235609 -7200 # Node ID 8826d5a4332b56318ef34fc3c72e17438bc8de62 # Parent aeb0cc8889f262e85139cad3f439cdd0695b33c9 renamed "pred" to "rel" (relator) diff -r aeb0cc8889f2 -r 8826d5a4332b src/HOL/Codatatype/Basic_BNFs.thy --- a/src/HOL/Codatatype/Basic_BNFs.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Basic_BNFs.thy Fri Sep 21 15:53:29 2012 +0200 @@ -80,12 +80,12 @@ lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def] -definition sum_pred :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a + 'c \ 'b + 'd \ bool" where -"sum_pred \ \ x y = +definition sum_rel :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a + 'c \ 'b + 'd \ bool" where +"sum_rel \ \ x y = (case x of Inl a1 \ (case y of Inl a2 \ \ a1 a2 | Inr _ \ False) | Inr b1 \ (case y of Inl _ \ False | Inr b2 \ \ b1 b2))" -bnf_def sum_map [setl, setr] "\_::'a + 'b. natLeq" [Inl, Inr] sum_pred +bnf_def sum_map [setl, setr] "\_::'a + 'b. natLeq" [Inl, Inr] sum_rel proof - show "sum_map id id = id" by (rule sum_map.id) next @@ -196,10 +196,10 @@ qed next fix R S - show "{p. sum_pred (\x y. (x, y) \ R) (\x y. (x, y) \ S) (fst p) (snd p)} = + 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_pred_def Gr_def relcomp_unfold converse_unfold + unfolding setl_def setr_def sum_rel_def Gr_def relcomp_unfold converse_unfold by (fastforce split: sum.splits) qed (auto simp: sum_set_defs) @@ -221,10 +221,10 @@ lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] -definition prod_pred :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" where -"prod_pred \ \ p1 p2 = (case p1 of (a1, b1) \ case p2 of (a2, b2) \ \ a1 a2 \ \ b1 b2)" +definition prod_rel :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" where +"prod_rel \ \ p1 p2 = (case p1 of (a1, b1) \ case p2 of (a2, b2) \ \ a1 a2 \ \ b1 b2)" -bnf_def map_pair [fsts, snds] "\_::'a \ 'b. ctwo *c natLeq" [Pair] prod_pred +bnf_def map_pair [fsts, snds] "\_::'a \ 'b. ctwo *c natLeq" [Pair] prod_rel proof (unfold prod_set_defs) show "map_pair id id = id" by (rule map_pair.id) next @@ -301,10 +301,10 @@ unfolding wpull_def by simp fast next fix R S - show "{p. prod_pred (\x y. (x, y) \ R) (\x y. (x, y) \ S) (fst p) (snd p)} = + 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_pred_def Gr_def relcomp_unfold converse_unfold + unfolding prod_set_defs prod_rel_def Gr_def relcomp_unfold converse_unfold by auto qed simp+ @@ -344,11 +344,11 @@ ultimately show ?thesis using card_of_ordLeq by fast qed -definition fun_pred :: "('a \ 'b \ bool) \ ('c \ 'a) \ ('c \ 'b) \ bool" where -"fun_pred \ f g = (\x. \ (f x) (g x))" +definition fun_rel :: "('a \ 'b \ bool) \ ('c \ 'a) \ ('c \ 'b) \ bool" where +"fun_rel \ f g = (\x. \ (f x) (g x))" bnf_def "op \" [range] "\_:: 'a \ 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"] - fun_pred + fun_rel proof fix f show "id \ f = id f" by simp next @@ -408,9 +408,9 @@ qed next fix R - show "{p. fun_pred (\x y. (x, y) \ R) (fst p) (snd p)} = + show "{p. fun_rel (\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_pred_def Gr_def relcomp_unfold converse_unfold + unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold by (auto intro!: exI dest!: in_mono) qed auto diff -r aeb0cc8889f2 -r 8826d5a4332b src/HOL/Codatatype/More_BNFs.thy --- a/src/HOL/Codatatype/More_BNFs.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/More_BNFs.thy Fri Sep 21 15:53:29 2012 +0200 @@ -22,14 +22,14 @@ lemma option_rec_conv_option_case: "option_rec = option_case" by (simp add: fun_eq_iff split: option.split) -definition option_pred :: "('a \ 'b \ bool) \ 'a option \ 'b option \ bool" where -"option_pred R x_opt y_opt = +definition option_rel :: "('a \ 'b \ bool) \ 'a option \ 'b option \ bool" where +"option_rel R x_opt y_opt = (case (x_opt, y_opt) of (None, None) \ True | (Some x, Some y) \ R x y | _ \ False)" -bnf_def Option.map [Option.set] "\_::'a option. natLeq" ["None"] option_pred +bnf_def Option.map [Option.set] "\_::'a option. natLeq" ["None"] option_rel proof - show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split) next @@ -90,9 +90,9 @@ thus False by simp next fix R - show "{p. option_pred (\x y. (x, y) \ R) (fst p) (snd p)} = + 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_pred_def Gr_def relcomp_unfold converse_unfold + unfolding option_rel_def Gr_def relcomp_unfold converse_unfold by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some] split: option.splits) blast qed @@ -360,12 +360,12 @@ lemma fset_to_fset: "finite A \ fset (the_inv fset A) = A" by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset) -definition fset_pred :: "('a \ 'b \ bool) \ 'a fset \ 'b fset \ bool" where -"fset_pred R a b \ +definition fset_rel :: "('a \ 'b \ bool) \ 'a fset \ 'b fset \ bool" where +"fset_rel R a b \ (\t \ fset a. \u \ fset b. R t u) \ (\t \ fset b. \u \ fset a. R u t)" -lemma fset_pred_aux: +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}} (map_fset fst))\ O Gr {a. fset a \ {(a, b). R a b}} (map_fset snd)" (is "?L = ?R") @@ -389,7 +389,7 @@ by (clarsimp, metis fst_conv) qed -bnf_def map_fset [fset] "\_::'a fset. natLeq" ["{||}"] fset_pred +bnf_def map_fset [fset] "\_::'a fset. natLeq" ["{||}"] fset_rel proof - show "map_fset id = id" unfolding map_fset_def2 map_id o_id afset_rfset_id .. @@ -465,9 +465,9 @@ qed next fix R - show "{p. fset_pred (\x y. (x, y) \ R) (fst p) (snd p)} = + show "{p. fset_rel (\x y. (x, y) \ R) (fst p) (snd p)} = (Gr {x. fset x \ R} (map_fset fst))\ O Gr {x. fset x \ R} (map_fset snd)" - unfolding fset_pred_def fset_pred_aux by simp + unfolding fset_rel_def fset_rel_aux by simp qed auto (* Countable sets *) @@ -537,12 +537,12 @@ lemma rcset_natural': "rcset (cIm f x) = f ` rcset x" unfolding cIm_def[abs_def] by simp -definition cset_pred :: "('a \ 'b \ bool) \ 'a cset \ 'b cset \ bool" where -"cset_pred R a b \ +definition cset_rel :: "('a \ 'b \ bool) \ 'a cset \ 'b cset \ bool" where +"cset_rel R a b \ (\t \ rcset a. \u \ rcset b. R t u) \ (\t \ rcset b. \u \ rcset a. R u t)" -lemma cset_pred_aux: +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") @@ -572,7 +572,7 @@ by (metis Domain.intros Range.simps rcset_natural' fst_eq_Domain snd_eq_Range) qed -bnf_def cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] cset_pred +bnf_def cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] cset_rel proof - show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto next @@ -636,9 +636,9 @@ qed next fix R - show "{p. cset_pred (\x y. (x, y) \ R) (fst p) (snd p)} = + 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_pred_def cset_pred_aux by simp + unfolding cset_rel_def cset_rel_aux by simp qed (unfold cEmp_def, auto) @@ -1285,18 +1285,18 @@ qed qed (unfold set_of_empty, auto) -inductive multiset_pred' where -Zero: "multiset_pred' R {#} {#}" +inductive multiset_rel' where +Zero: "multiset_rel' R {#} {#}" | -Plus: "\R a b; multiset_pred' R M N\ \ multiset_pred' R (M + {#a#}) (N + {#b#})" +Plus: "\R a b; multiset_rel' R M N\ \ multiset_rel' R (M + {#a#}) (N + {#b#})" lemma multiset_map_Zero_iff[simp]: "multiset_map f M = {#} \ M = {#}" by (metis image_is_empty multiset.set_natural' set_of_eq_empty_iff) lemma multiset_map_Zero[simp]: "multiset_map f {#} = {#}" by simp -lemma multiset_pred_Zero: "multiset_pred R {#} {#}" -unfolding multiset_pred_def Gr_def relcomp_unfold by auto +lemma multiset_rel_Zero: "multiset_rel R {#} {#}" +unfolding multiset_rel_def Gr_def relcomp_unfold by auto declare multiset.count[simp] declare mmap[simp] @@ -1337,9 +1337,9 @@ by (simp, simp add: single_def) qed -lemma multiset_pred_Plus: -assumes ab: "R a b" and MN: "multiset_pred R M N" -shows "multiset_pred R (M + {#a#}) (N + {#b#})" +lemma multiset_rel_Plus: +assumes ab: "R a b" and MN: "multiset_rel R M N" +shows "multiset_rel R (M + {#a#}) (N + {#b#})" proof- {fix y assume "R a b" and "set_of y \ {(x, y). R x y}" hence "\ya. multiset_map fst y + {#a#} = multiset_map fst ya \ @@ -1349,13 +1349,13 @@ } thus ?thesis using assms - unfolding multiset_pred_def Gr_def relcomp_unfold by force + unfolding multiset_rel_def Gr_def relcomp_unfold by force qed -lemma multiset_pred'_imp_multiset_pred: -"multiset_pred' R M N \ multiset_pred R M N" -apply(induct rule: multiset_pred'.induct) -using multiset_pred_Zero multiset_pred_Plus by auto +lemma multiset_rel'_imp_multiset_rel: +"multiset_rel' R M N \ multiset_rel R M N" +apply(induct rule: multiset_rel'.induct) +using multiset_rel_Zero multiset_rel_Plus by auto lemma mcard_multiset_map[simp]: "mcard (multiset_map f M) = mcard M" proof- @@ -1388,10 +1388,10 @@ thus ?thesis unfolding A_def mcard_def multiset_map_def by (simp add: mmap_def) qed -lemma multiset_pred_mcard: -assumes "multiset_pred R M N" +lemma multiset_rel_mcard: +assumes "multiset_rel R M N" shows "mcard M = mcard N" -using assms unfolding multiset_pred_def relcomp_unfold Gr_def by auto +using assms unfolding multiset_rel_def relcomp_unfold Gr_def by auto lemma multiset_induct2[case_names empty addL addR]: assumes empty: "P {#} {#}" @@ -1445,67 +1445,67 @@ thus ?thesis using M fa by blast qed -lemma msed_pred_invL: -assumes "multiset_pred R (M + {#a#}) N" -shows "\ N1 b. N = N1 + {#b#} \ R a b \ multiset_pred R M N1" +lemma msed_rel_invL: +assumes "multiset_rel R (M + {#a#}) N" +shows "\ N1 b. N = N1 + {#b#} \ R a b \ multiset_rel R M N1" proof- 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_pred_def Gr_def relcomp_unfold by auto + unfolding multiset_rel_def Gr_def relcomp_unfold 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_pred R M N1" using sK K1M K1N1 - unfolding K multiset_pred_def Gr_def relcomp_unfold by auto + have "multiset_rel R M N1" using sK K1M K1N1 + unfolding K multiset_rel_def Gr_def relcomp_unfold by auto thus ?thesis using N Rab by auto qed -lemma msed_pred_invR: -assumes "multiset_pred R M (N + {#b#})" -shows "\ M1 a. M = M1 + {#a#} \ R a b \ multiset_pred R M1 N" +lemma msed_rel_invR: +assumes "multiset_rel R M (N + {#b#})" +shows "\ M1 a. M = M1 + {#a#} \ R a b \ multiset_rel R M1 N" proof- obtain K where KN: "multiset_map snd K = N + {#b#}" and KM: "multiset_map fst K = M" and sK: "set_of K \ {(a, b). R a b}" using assms - unfolding multiset_pred_def Gr_def relcomp_unfold by auto + unfolding multiset_rel_def Gr_def relcomp_unfold by auto obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b" and K1N: "multiset_map snd K1 = N" using msed_map_invR[OF KN] by auto obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "multiset_map fst K1 = M1" using msed_map_invL[OF KM[unfolded K]] by auto have Rab: "R (fst ab) b" using sK b unfolding K by auto - have "multiset_pred R M1 N" using sK K1N K1M1 - unfolding K multiset_pred_def Gr_def relcomp_unfold by auto + have "multiset_rel R M1 N" using sK K1N K1M1 + unfolding K multiset_rel_def Gr_def relcomp_unfold by auto thus ?thesis using M Rab by auto qed -lemma multiset_pred_imp_multiset_pred': -assumes "multiset_pred R M N" -shows "multiset_pred' R M N" +lemma multiset_rel_imp_multiset_rel': +assumes "multiset_rel R M N" +shows "multiset_rel' R M N" using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard]) case (less M) - have c: "mcard M = mcard N" using multiset_pred_mcard[OF less.prems] . + have c: "mcard M = mcard N" using multiset_rel_mcard[OF less.prems] . show ?case proof(cases "M = {#}") case True hence "N = {#}" using c by simp - thus ?thesis using True multiset_pred'.Zero by auto + thus ?thesis using True multiset_rel'.Zero by auto next case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split) - obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "multiset_pred R M1 N1" - using msed_pred_invL[OF less.prems[unfolded M]] by auto - have "multiset_pred' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp - thus ?thesis using multiset_pred'.Plus[of R a b, OF R] unfolding M N by simp + obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "multiset_rel R M1 N1" + using msed_rel_invL[OF less.prems[unfolded M]] by auto + have "multiset_rel' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp + thus ?thesis using multiset_rel'.Plus[of R a b, OF R] unfolding M N by simp qed qed -lemma multiset_pred_multiset_pred': -"multiset_pred R M N = multiset_pred' R M N" -using multiset_pred_imp_multiset_pred' multiset_pred'_imp_multiset_pred by auto +lemma multiset_rel_multiset_rel': +"multiset_rel R M N = multiset_rel' R M N" +using multiset_rel_imp_multiset_rel' multiset_rel'_imp_multiset_rel by auto -(* The main end product for multiset_pred: inductive characterization *) -theorems multiset_pred_induct[case_names empty add, induct pred: multiset_pred] = - multiset_pred'.induct[unfolded multiset_pred_multiset_pred'[symmetric]] +(* The main end product for multiset_rel: inductive characterization *) +theorems multiset_rel_induct[case_names empty add, induct pred: multiset_rel] = + multiset_rel'.induct[unfolded multiset_rel_multiset_rel'[symmetric]] end diff -r aeb0cc8889f2 -r 8826d5a4332b src/HOL/Codatatype/Tools/bnf_comp.ML --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -11,8 +11,8 @@ type unfold_set val empty_unfolds: unfold_set val map_unfolds_of: unfold_set -> thm list + val rel_unfolds_of: unfold_set -> thm list val set_unfoldss_of: unfold_set -> thm list list - val pred_unfolds_of: unfold_set -> thm list val srel_unfolds_of: unfold_set -> thm list val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> @@ -37,29 +37,29 @@ type unfold_set = { map_unfolds: thm list, set_unfoldss: thm list list, - pred_unfolds: thm list, + rel_unfolds: thm list, srel_unfolds: thm list }; -val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], srel_unfolds = []}; +val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = [], srel_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 pred srel - {map_unfolds, set_unfoldss, pred_unfolds, srel_unfolds} = +fun add_to_unfolds map sets rel srel + {map_unfolds, set_unfoldss, rel_unfolds, srel_unfolds} = {map_unfolds = add_to_thms map_unfolds map, set_unfoldss = adds_to_thms set_unfoldss sets, - pred_unfolds = add_to_thms pred_unfolds pred, + rel_unfolds = add_to_thms rel_unfolds rel, srel_unfolds = add_to_thms srel_unfolds srel}; fun add_bnf_to_unfolds bnf = - add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (pred_def_of_bnf bnf) + add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf) (srel_def_of_bnf bnf); val map_unfolds_of = #map_unfolds; val set_unfoldss_of = #set_unfoldss; -val pred_unfolds_of = #pred_unfolds; +val rel_unfolds_of = #rel_unfolds; val srel_unfolds_of = #srel_unfolds; val bdTN = "bdT"; @@ -121,11 +121,11 @@ (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer, map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o mk_map_of_bnf Ds As Bs) Dss inners)); - (*%Q1 ... Qn. outer.pred (inner_1.pred Q1 ... Qn) ... (inner_m.pred Q1 ... Qn)*) - val pred = fold_rev Term.abs Qs' - (Term.list_comb (mk_pred_of_bnf oDs CAs CBs outer, + (*%Q1 ... Qn. outer.rel (inner_1.rel Q1 ... Qn) ... (inner_m.rel Q1 ... Qn)*) + val rel = fold_rev Term.abs Qs' + (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer, map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o - mk_pred_of_bnf Ds As Bs) Dss inners)); + mk_rel_of_bnf Ds As Bs) Dss inners)); (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*) (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*) @@ -271,7 +271,7 @@ val (bnf', lthy') = bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) - (((((b, mapx), sets), bd), wits), SOME pred) lthy; + (((((b, mapx), sets), bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -303,8 +303,8 @@ (*bnf.map id ... id*) val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs); - (*bnf.pred (op =) ... (op =)*) - val pred = Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs); + (*bnf.rel (op =) ... (op =)*) + val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs); val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; val sets = drop n bnf_sets; @@ -369,7 +369,7 @@ val (bnf', lthy') = bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) - (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; + (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -400,8 +400,8 @@ (*%f1 ... fn. bnf.map*) val mapx = fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf); - (*%Q1 ... Qn. bnf.pred*) - val pred = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_pred_of_bnf Ds As Bs bnf); + (*%Q1 ... Qn. bnf.rel*) + val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf); val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets; @@ -453,7 +453,7 @@ val (bnf', lthy') = bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) - (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; + (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) @@ -486,9 +486,9 @@ (*%f(1) ... f(n). bnf.map f\(1) ... f\(n)*) val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs)) (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0)))); - (*%Q(1) ... Q(n). bnf.pred Q\(1) ... Q\(n)*) - val pred = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs)) - (Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0)))); + (*%Q(1) ... Q(n). bnf.rel Q\(1) ... Q\(n)*) + val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs)) + (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0)))); val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; val sets = permute bnf_sets; @@ -530,7 +530,7 @@ val (bnf', lthy') = bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) - (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; + (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -606,25 +606,25 @@ val map_unfolds = map_unfolds_of unfold_set; val set_unfoldss = set_unfoldss_of unfold_set; - val pred_unfolds = pred_unfolds_of unfold_set; + val rel_unfolds = rel_unfolds_of unfold_set; val srel_unfolds = srel_unfolds_of unfold_set; - val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) - map_unfolds); - val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) - set_unfoldss); - val expand_preds = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) - pred_unfolds); + val expand_maps = + fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds); + val expand_sets = + fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss); + val expand_rels = + fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds); val unfold_maps = fold (unfold_thms lthy o single) map_unfolds; val unfold_sets = fold (unfold_thms lthy) set_unfoldss; - val unfold_preds = unfold_thms lthy pred_unfolds; + 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_preds o unfold_srels; + val unfold_all = unfold_sets o unfold_maps o unfold_rels o unfold_srels; val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf); val bnf_sets = map (expand_maps o expand_sets) (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf); val bnf_bd = mk_bd_of_bnf Ds As bnf; - val bnf_pred = expand_preds (mk_pred_of_bnf Ds As Bs bnf); + val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf); val T = mk_T_of_bnf Ds As bnf; (*bd should only depend on dead type variables!*) @@ -674,7 +674,7 @@ val policy = user_policy Derive_All_Facts; val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads) - (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_pred) lthy; + (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy; in ((bnf', deads), lthy') end; diff -r aeb0cc8889f2 -r 8826d5a4332b src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 15:53:29 2012 +0200 @@ -23,8 +23,8 @@ val nwits_of_bnf: BNF -> int val mapN: string + val relN: string val setN: string - val predN: string val mk_setN: int -> string val srelN: string @@ -33,7 +33,7 @@ val mk_T_of_bnf: typ list -> typ list -> BNF -> typ val mk_bd_of_bnf: typ list -> typ list -> BNF -> term val mk_map_of_bnf: typ list -> typ list -> typ list -> BNF -> term - val mk_pred_of_bnf: typ list -> typ list -> 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 @@ -56,7 +56,7 @@ val map_id_of_bnf: BNF -> thm val map_wppull_of_bnf: BNF -> thm val map_wpull_of_bnf: BNF -> thm - val pred_def_of_bnf: BNF -> thm + val rel_def_of_bnf: BNF -> thm val set_bd_of_bnf: BNF -> thm list val set_defs_of_bnf: BNF -> thm list val set_natural'_of_bnf: BNF -> thm list @@ -160,14 +160,14 @@ type defs = { map_def: thm, set_defs: thm list, - pred_def: thm, + rel_def: thm, srel_def: thm } -fun mk_defs map sets pred srel = {map_def = map, set_defs = sets, pred_def = pred, srel_def = srel}; +fun mk_defs map sets rel srel = {map_def = map, set_defs = sets, rel_def = rel, srel_def = srel}; -fun map_defs f {map_def, set_defs, pred_def, srel_def} = - {map_def = f map_def, set_defs = map f set_defs, pred_def = f pred_def, srel_def = f srel_def}; +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}; val morph_defs = map_defs o Morphism.thm; @@ -276,7 +276,7 @@ facts: facts, nwits: int, wits: nonemptiness_witness list, - pred: term, + rel: term, srel: term }; @@ -324,12 +324,12 @@ map2 (fn (Ds, Ts) => apsnd (Term.subst_atomic_types ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)))) (Dss ~~ Tss) wits end; -val pred_of_bnf = #pred o rep_bnf; -fun mk_pred_of_bnf Ds Ts Us bnf = +val rel_of_bnf = #rel o rep_bnf; +fun mk_rel_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)) (#pred bnf_rep) + ((#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 = @@ -358,7 +358,7 @@ val map_cong_of_bnf = #map_cong o #axioms o rep_bnf; val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf; val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf; -val pred_def_of_bnf = #pred_def o #defs o rep_bnf; +val rel_def_of_bnf = #rel_def o #defs 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_natural_of_bnf = #set_natural o #axioms o rep_bnf; @@ -374,17 +374,17 @@ 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 pred srel = +fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel srel = 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, pred = pred, srel = srel}; + nwits = length wits, wits = wits, rel = rel, srel = srel}; 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, pred = pred, srel = srel}) = + nwits = nwits, wits = wits, rel = rel, srel = srel}) = 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', @@ -396,7 +396,7 @@ facts = morph_facts phi facts, nwits = nwits, wits = List.map (morph_witness phi) wits, - pred = Morphism.term phi pred, srel = Morphism.term phi srel}; + rel = Morphism.term phi rel, srel = Morphism.term phi srel}; fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...}, BNF {T = T2, live = live2, dead = dead2, ...}) = @@ -423,13 +423,13 @@ val params = Term.add_tvar_namesT T []; in Term.subst_TVars ((A :: params) ~~ (instA :: insts)) set end; -fun normalize_pred ctxt instTs instA instB pred = +fun normalize_rel ctxt instTs instA instB rel = let val thy = Proof_Context.theory_of ctxt; val tyenv = - Sign.typ_match thy (fastype_of pred, Library.foldr (op -->) (instTs, mk_pred2T instA instB)) + Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_pred2T instA instB)) Vartab.empty; - in Envir.subst_term (tyenv, Vartab.empty) pred end + in Envir.subst_term (tyenv, Vartab.empty) rel end handle Type.TYPE_MATCH => error "Bad predicator"; fun normalize_srel ctxt instTs instA instB srel = @@ -472,7 +472,7 @@ val bdN = "bd"; val witN = "wit"; fun mk_witN i = witN ^ nonzero_string_of_int i; -val predN = "pred"; +val relN = "rel"; val srelN = "srel"; val bd_card_orderN = "bd_card_order"; @@ -516,7 +516,7 @@ (* Define new BNFs *) fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt - (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_pred_opt) no_defs_lthy = + (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy = let val fact_policy = mk_fact_policy no_defs_lthy; val b = qualify raw_b; @@ -623,7 +623,7 @@ (*TODO: further checks of type of bnf_map*) (*TODO: check types of bnf_sets*) (*TODO: check type of bnf_bd*) - (*TODO: check type of bnf_pred*) + (*TODO: check type of bnf_rel*) val ((((((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), domTs), ranTs), ranTs'), ranTs''), (Ts, T)) = lthy @@ -714,31 +714,31 @@ val y = Free (y_name, U); in fold_rev Term.lambda [x, y] (HOLogic.mk_mem (HOLogic.mk_prod (x, y), t)) end; - val pred_rhs = (case raw_pred_opt of + 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, map3 (fn Q => fn T => fn U => HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs'))) - | SOME raw_pred => prep_term no_defs_lthy raw_pred); + | SOME raw_rel => prep_term no_defs_lthy raw_rel); - val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs); + val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs); - val ((bnf_pred_term, raw_pred_def), (lthy, lthy_old)) = + val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) = lthy - |> maybe_define (is_some raw_pred_opt) pred_bind_def + |> maybe_define (is_some raw_rel_opt) rel_bind_def ||> `(maybe_restore lthy); val phi = Proof_Context.export_morphism lthy_old lthy; - val bnf_pred_def = Morphism.thm phi raw_pred_def; - val bnf_pred = Morphism.term phi bnf_pred_term; + val bnf_rel_def = Morphism.thm phi raw_rel_def; + val bnf_rel = Morphism.term phi bnf_rel_term; - fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy QTs CA' CB' bnf_pred; + fun mk_bnf_rel QTs CA' CB' = normalize_rel lthy QTs CA' CB' bnf_rel; - val pred = mk_bnf_pred QTs CA' CB'; + 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 (pred, map (mk_predicate_of_set (fst x') (fst y')) Rs) $ + 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); @@ -757,7 +757,7 @@ val srel = mk_bnf_srel setRTs CA' CB'; val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @ - raw_wit_defs @ [raw_pred_def, raw_srel_def]) of + raw_wit_defs @ [raw_rel_def, raw_srel_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); @@ -1090,7 +1090,7 @@ val in_srel = mk_lazy mk_in_srel; - val defs = mk_defs bnf_map_def bnf_set_defs bnf_pred_def bnf_srel_def; + val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def; val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id @@ -1098,13 +1098,13 @@ val wits = map2 mk_witness bnf_wits wit_thms; - val bnf_pred = - Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) pred; + 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_pred bnf_srel; + wits bnf_rel bnf_srel; in (bnf, lthy |> (if fact_policy = Note_All_Facts_and_Axioms then @@ -1160,7 +1160,7 @@ end; val one_step_defs = - no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_pred_def, + no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def, bnf_srel_def]); in (key, goals, wit_goalss, after_qed, lthy, one_step_defs) diff -r aeb0cc8889f2 -r 8826d5a4332b src/HOL/Codatatype/Tools/bnf_fp.ML --- a/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -62,11 +62,11 @@ val min_algN: string val morN: string val nchotomyN: string - val pred_coinductN: string - val pred_simpN: string - val pred_strong_coinductN: string val recN: string val recsN: string + val rel_coinductN: string + val rel_simpN: string + val rel_strong_coinductN: string val rvN: string val sel_unfoldsN: string val sel_corecsN: string @@ -222,14 +222,14 @@ val ctor_inductN = ctorN ^ "_" ^ inductN val ctor_induct2N = ctor_inductN ^ "2" val dtor_coinductN = dtorN ^ "_" ^ coinductN -val pred_coinductN = predN ^ "_" ^ coinductN +val rel_coinductN = relN ^ "_" ^ coinductN val srel_coinductN = srelN ^ "_" ^ coinductN val simpN = "_simp"; val srel_simpN = srelN ^ simpN; -val pred_simpN = predN ^ simpN; +val rel_simpN = relN ^ simpN; val strongN = "strong_" val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN -val pred_strong_coinductN = predN ^ "_" ^ strongN ^ coinductN +val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN val srel_strong_coinductN = srelN ^ "_" ^ strongN ^ coinductN val hsetN = "Hset" val hset_recN = hsetN ^ "_rec" diff -r aeb0cc8889f2 -r 8826d5a4332b src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -2178,8 +2178,8 @@ val timer = time (timer "corec definitions & thms"); - val (dtor_coinduct_thm, coinduct_params, srel_coinduct_thm, pred_coinduct_thm, - dtor_strong_coinduct_thm, srel_strong_coinduct_thm, pred_strong_coinduct_thm) = + val (dtor_coinduct_thm, coinduct_params, srel_coinduct_thm, rel_coinduct_thm, + dtor_strong_coinduct_thm, srel_strong_coinduct_thm, rel_strong_coinduct_thm) = let val zs = Jzs1 @ Jzs2; val frees = phis @ zs; @@ -2269,14 +2269,14 @@ (tcoalg_thm RS bis_diag_thm)))) |> Thm.close_derivation; - val pred_of_srel_thms = + val rel_of_srel_thms = srel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv}; - val pred_coinduct = unfold_thms lthy pred_of_srel_thms srel_coinduct; - val pred_strong_coinduct = unfold_thms lthy pred_of_srel_thms srel_strong_coinduct; + val rel_coinduct = unfold_thms lthy rel_of_srel_thms srel_coinduct; + val rel_strong_coinduct = unfold_thms lthy rel_of_srel_thms srel_strong_coinduct; in - (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), srel_coinduct, pred_coinduct, - dtor_strong_coinduct, srel_strong_coinduct, pred_strong_coinduct) + (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), srel_coinduct, rel_coinduct, + dtor_strong_coinduct, srel_strong_coinduct, rel_strong_coinduct) end; val timer = time (timer "coinduction"); @@ -2882,18 +2882,18 @@ 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 preds = map2 (fn Ds => mk_pred_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; - val Jpreds = map (mk_pred_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 JrelRs = map (fn Jsrel => Term.list_comb (Jsrel, JRs)) Jsrels; val relRs = map (fn srel => Term.list_comb (srel, JRs @ JrelRs)) srels; - val Jpredphis = map (fn Jsrel => Term.list_comb (Jsrel, Jphis)) Jpreds; - val predphis = map (fn srel => Term.list_comb (srel, Jphis @ Jpredphis)) preds; + val Jpredphis = map (fn Jsrel => Term.list_comb (Jsrel, Jphis)) Jrels; + val predphis = map (fn srel => Term.list_comb (srel, Jphis @ Jpredphis)) 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 Jpred_defs = map pred_def_of_bnf Jbnfs; + val Jrel_defs = map rel_def_of_bnf Jbnfs; val folded_map_simp_thms = map fold_maps map_simp_thms; val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss; @@ -2917,7 +2917,7 @@ dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss end; - val Jpred_simp_thms = + val Jrel_simp_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'))); @@ -2925,7 +2925,7 @@ in map3 (fn goal => fn srel_def => fn Jsrel_simp => Skip_Proof.prove lthy [] [] goal - (mk_pred_simp_tac srel_def Jpred_defs Jsrel_defs Jsrel_simp) + (mk_rel_simp_tac srel_def Jrel_defs Jsrel_defs Jsrel_simp) |> Thm.close_derivation) goals srel_defs Jsrel_simp_thms end; @@ -2942,7 +2942,7 @@ val Jbnf_notes = [(map_simpsN, map single folded_map_simp_thms), - (pred_simpN, map single Jpred_simp_thms), + (rel_simpN, map single Jrel_simp_thms), (set_inclN, set_incl_thmss), (set_set_inclN, map flat set_set_incl_thmsss), (srel_simpN, map single Jsrel_simp_thms)] @ @@ -2958,8 +2958,8 @@ val common_notes = [(dtor_coinductN, [dtor_coinduct_thm]), (dtor_strong_coinductN, [dtor_strong_coinduct_thm]), - (pred_coinductN, [pred_coinduct_thm]), - (pred_strong_coinductN, [pred_strong_coinduct_thm]), + (rel_coinductN, [rel_coinduct_thm]), + (rel_strong_coinductN, [rel_strong_coinduct_thm]), (srel_coinductN, [srel_coinduct_thm]), (srel_strong_coinductN, [srel_strong_coinduct_thm])] |> map (fn (thmN, thms) => diff -r aeb0cc8889f2 -r 8826d5a4332b src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200 @@ -1722,19 +1722,19 @@ 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 preds = map2 (fn Ds => mk_pred_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; - val Ipreds = map (mk_pred_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 IrelRs = map (fn Isrel => Term.list_comb (Isrel, IRs)) Isrels; val relRs = map (fn srel => Term.list_comb (srel, IRs @ IrelRs)) srels; - val Ipredphis = map (fn Isrel => Term.list_comb (Isrel, Iphis)) Ipreds; - val predphis = map (fn srel => Term.list_comb (srel, Iphis @ Ipredphis)) preds; + val Ipredphis = map (fn Isrel => Term.list_comb (Isrel, Iphis)) Irels; + val predphis = map (fn srel => Term.list_comb (srel, Iphis @ Ipredphis)) 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 Ipred_defs = map pred_def_of_bnf Ibnfs; + val Irel_defs = map rel_def_of_bnf Ibnfs; val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss; val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss; @@ -1760,7 +1760,7 @@ ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss end; - val Ipred_simp_thms = + val Irel_simp_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)); @@ -1768,7 +1768,7 @@ in map3 (fn goal => fn srel_def => fn Isrel_simp => Skip_Proof.prove lthy [] [] goal - (mk_pred_simp_tac srel_def Ipred_defs Isrel_defs Isrel_simp) + (mk_rel_simp_tac srel_def Irel_defs Isrel_defs Isrel_simp) |> Thm.close_derivation) goals srel_defs Isrel_simp_thms end; @@ -1787,7 +1787,7 @@ (set_inclN, set_incl_thmss), (set_set_inclN, map flat set_set_incl_thmsss), (srel_simpN, map single Isrel_simp_thms), - (pred_simpN, map single Ipred_simp_thms)] @ + (rel_simpN, map single Irel_simp_thms)] @ map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => diff -r aeb0cc8889f2 -r 8826d5a4332b src/HOL/Codatatype/Tools/bnf_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Fri Sep 21 15:53:29 2012 +0200 @@ -27,7 +27,7 @@ val mk_Abs_inj_thm: thm -> thm val simple_srel_O_Gr_tac: Proof.context -> tactic - val mk_pred_simp_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> + val mk_rel_simp_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic val mk_map_comp_id_tac: thm -> tactic @@ -101,9 +101,9 @@ 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_pred_simp_tac srel_def IJpred_defs IJsrel_defs srel_simp {context = ctxt, prems = _} = - unfold_thms_tac ctxt IJpred_defs THEN - subst_tac ctxt [unfold_thms ctxt (IJpred_defs @ IJsrel_defs @ +fun mk_rel_simp_tac srel_def IJrel_defs IJsrel_defs srel_simp {context = ctxt, prems = _} = + unfold_thms_tac ctxt IJrel_defs THEN + subst_tac ctxt [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @ @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) srel_simp] 1 THEN unfold_thms_tac ctxt (srel_def :: @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv