--- 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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool" where
-"sum_pred \<phi> \<psi> x y =
+definition sum_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool" where
+"sum_rel \<phi> \<psi> x y =
(case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
| Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
-bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_pred
+bnf_def sum_map [setl, setr] "\<lambda>_::'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 (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
+ show "{p. sum_rel (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
(Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O
Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)"
- unfolding setl_def setr_def sum_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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where
-"prod_pred \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)"
+definition prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where
+"prod_rel \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)"
-bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_pred
+bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> '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 (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
+ show "{p. prod_rel (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
(Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O
Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)"
- unfolding prod_set_defs prod_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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b) \<Rightarrow> bool" where
-"fun_pred \<phi> f g = (\<forall>x. \<phi> (f x) (g x))"
+definition fun_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b) \<Rightarrow> bool" where
+"fun_rel \<phi> f g = (\<forall>x. \<phi> (f x) (g x))"
bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
- fun_pred
+ fun_rel
proof
fix f show "id \<circ> f = id f" by simp
next
@@ -408,9 +408,9 @@
qed
next
fix R
- show "{p. fun_pred (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
+ show "{p. fun_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
(Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
- unfolding fun_pred_def Gr_def relcomp_unfold converse_unfold
+ unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold
by (auto intro!: exI dest!: in_mono)
qed auto
--- 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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool" where
-"option_pred R x_opt y_opt =
+definition option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool" where
+"option_rel R x_opt y_opt =
(case (x_opt, y_opt) of
(None, None) \<Rightarrow> True
| (Some x, Some y) \<Rightarrow> R x y
| _ \<Rightarrow> False)"
-bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_pred
+bnf_def Option.map [Option.set] "\<lambda>_::'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 (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
+ show "{p. option_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
(Gr {x. Option.set x \<subseteq> R} (Option.map fst))\<inverse> O Gr {x. Option.set x \<subseteq> R} (Option.map snd)"
- unfolding option_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 \<Longrightarrow> fset (the_inv fset A) = A"
by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
-definition fset_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" where
-"fset_pred R a b \<longleftrightarrow>
+definition fset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" where
+"fset_rel R a b \<longleftrightarrow>
(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and>
(\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
-lemma fset_pred_aux:
+lemma fset_rel_aux:
"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
(a, b) \<in> (Gr {a. fset a \<subseteq> {(a, b). R a b}} (map_fset fst))\<inverse> O
Gr {a. fset a \<subseteq> {(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] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_pred
+bnf_def map_fset [fset] "\<lambda>_::'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 (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
+ show "{p. fset_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
(Gr {x. fset x \<subseteq> R} (map_fset fst))\<inverse> O Gr {x. fset x \<subseteq> R} (map_fset snd)"
- unfolding fset_pred_def fset_pred_aux by simp
+ 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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
-"cset_pred R a b \<longleftrightarrow>
+definition cset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
+"cset_rel R a b \<longleftrightarrow>
(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
(\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)"
-lemma cset_pred_aux:
+lemma cset_rel_aux:
"(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t) \<longleftrightarrow>
(a, b) \<in> (Gr {x. rcset x \<subseteq> {(a, b). R a b}} (cIm fst))\<inverse> O
Gr {x. rcset x \<subseteq> {(a, b). R a b}} (cIm snd)" (is "?L = ?R")
@@ -572,7 +572,7 @@
by (metis Domain.intros Range.simps rcset_natural' fst_eq_Domain snd_eq_Range)
qed
-bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_pred
+bnf_def cIm [rcset] "\<lambda>_::'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 (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
+ show "{p. cset_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
(Gr {x. rcset x \<subseteq> R} (cIm fst))\<inverse> O Gr {x. rcset x \<subseteq> R} (cIm snd)"
- unfolding cset_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: "\<lbrakk>R a b; multiset_pred' R M N\<rbrakk> \<Longrightarrow> multiset_pred' R (M + {#a#}) (N + {#b#})"
+Plus: "\<lbrakk>R a b; multiset_rel' R M N\<rbrakk> \<Longrightarrow> multiset_rel' R (M + {#a#}) (N + {#b#})"
lemma multiset_map_Zero_iff[simp]: "multiset_map f M = {#} \<longleftrightarrow> 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 \<subseteq> {(x, y). R x y}"
hence "\<exists>ya. multiset_map fst y + {#a#} = multiset_map fst ya \<and>
@@ -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 \<Longrightarrow> 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 \<Longrightarrow> 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 "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> multiset_pred R M N1"
+lemma msed_rel_invL:
+assumes "multiset_rel R (M + {#a#}) N"
+shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> 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 \<subseteq> {(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 "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> multiset_pred R M1 N"
+lemma msed_rel_invR:
+assumes "multiset_rel R M (N + {#b#})"
+shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> 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 \<subseteq> {(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
--- 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\<sigma>(1) ... f\<sigma>(n)*)
val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
(Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
- (*%Q(1) ... Q(n). bnf.pred Q\<sigma>(1) ... Q\<sigma>(n)*)
- val pred = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
- (Term.list_comb (mk_pred_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
+ (*%Q(1) ... Q(n). bnf.rel Q\<sigma>(1) ... Q\<sigma>(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;
--- 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)
--- 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"
--- 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) =>
--- 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 =>
--- 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