--- a/src/HOL/Codatatype/Basic_BNFs.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Basic_BNFs.thy Thu Sep 20 02:42:49 2012 +0200
@@ -25,7 +25,7 @@
unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
- "id :: ('a \<times> 'b) set \<Rightarrow> ('a \<times> 'b) set"
+ "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
apply auto
apply (rule natLeq_card_order)
apply (rule natLeq_cinfinite)
@@ -51,10 +51,8 @@
apply (auto simp: Gr_def fun_eq_iff)
done
-definition DEADID_rel :: "('a \<times> 'a) set" where
-"DEADID_rel = {p. \<exists>x. p = (x, x)}"
-
-bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] DEADID_rel
+bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
+ "op =::'a \<Rightarrow> 'a \<Rightarrow> bool"
apply (auto simp add: wpull_id)
apply (rule card_order_csum)
apply (rule natLeq_card_order)
@@ -71,7 +69,7 @@
apply (rule card_of_Card_order)
apply (rule ctwo_Cnotzero)
apply (rule card_of_Card_order)
-apply (auto simp: DEADID_rel_def Id_def Gr_def fun_eq_iff)
+apply (auto simp: Id_def Gr_def fun_eq_iff)
done
definition setl :: "'a + 'b \<Rightarrow> 'a set" where
@@ -82,13 +80,12 @@
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
-definition sum_rel :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a + 'c) \<times> ('b + 'd)) set" where
-"sum_rel R S =
- {x. case x of (Inl a, Inl c) \<Rightarrow> (a, c) \<in> R
- | (Inr b, Inr d) \<Rightarrow> (b, d) \<in> S
- | _ \<Rightarrow> False}"
+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 =
+ (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_rel
+bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_pred
proof -
show "sum_map id id = id" by (rule sum_map.id)
next
@@ -199,10 +196,10 @@
qed
next
fix R S
- show "sum_rel R S =
- (Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O
- Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)"
- unfolding setl_def setr_def sum_rel_def Gr_def relcomp_unfold converse_unfold
+ show "{p. sum_pred (\<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
by (fastforce split: sum.splits)
qed (auto simp: sum_set_defs)
@@ -224,10 +221,10 @@
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
-definition prod_rel :: "('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> (('a \<times> 'c) \<times> 'b \<times> 'd) set" where
-"prod_rel R S = {((a, c), b, d) | a b c d. (a, b) \<in> R \<and> (c, d) \<in> S}"
+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)"
-bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel
+bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_pred
proof (unfold prod_set_defs)
show "map_pair id id = id" by (rule map_pair.id)
next
@@ -304,10 +301,10 @@
unfolding wpull_def by simp fast
next
fix R S
- show "prod_rel R S =
- (Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O
- Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)"
- unfolding prod_set_defs prod_rel_def Gr_def relcomp_unfold converse_unfold
+ show "{p. prod_pred (\<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
by auto
qed simp+
@@ -347,11 +344,11 @@
ultimately show ?thesis using card_of_ordLeq by fast
qed
-definition fun_rel :: "('a \<times> 'b) set \<Rightarrow> (('c \<Rightarrow> 'a) \<times> ('c \<Rightarrow> 'b)) set" where
-"fun_rel R = {(f, g) | f g. \<forall>x. (f x, g x) \<in> R}"
+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))"
bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
- fun_rel
+ fun_pred
proof
fix f show "id \<circ> f = id f" by simp
next
@@ -410,8 +407,10 @@
using wpull_cat[OF p c r] by simp metis
qed
next
- fix R show "fun_rel R = (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
- unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold
+ fix R
+ show "{p. fun_pred (\<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
by (auto intro!: exI dest!: in_mono)
qed auto