--- a/src/HOL/BNF/BNF.thy Mon Mar 18 10:28:42 2013 +0100
+++ b/src/HOL/BNF/BNF.thy Mon Mar 18 11:05:33 2013 +0100
@@ -13,4 +13,8 @@
imports More_BNFs
begin
+hide_const (open) Gr collect fsts snds setl setr
+ convol thePull pick_middle fstO sndO csquare inver
+ image2 relImage relInvImage prefCl PrefCl Succ Shift shift
+
end
--- a/src/HOL/BNF/BNF_GFP.thy Mon Mar 18 10:28:42 2013 +0100
+++ b/src/HOL/BNF/BNF_GFP.thy Mon Mar 18 11:05:33 2013 +0100
@@ -276,23 +276,14 @@
unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
(* pick according to the weak pullback *)
-definition pickWP_pred where
-"pickWP_pred A p1 p2 b1 b2 a \<equiv> a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
-
definition pickWP where
-"pickWP A p1 p2 b1 b2 \<equiv> SOME a. pickWP_pred A p1 p2 b1 b2 a"
+"pickWP A p1 p2 b1 b2 \<equiv> SOME a. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
lemma pickWP_pred:
assumes "wpull A B1 B2 f1 f2 p1 p2" and
"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
-shows "\<exists> a. pickWP_pred A p1 p2 b1 b2 a"
-using assms unfolding wpull_def pickWP_pred_def by blast
-
-lemma pickWP_pred_pickWP:
-assumes "wpull A B1 B2 f1 f2 p1 p2" and
-"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
-shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)"
-unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred])
+shows "\<exists> a. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
+using assms unfolding wpull_def by blast
lemma pickWP:
assumes "wpull A B1 B2 f1 f2 p1 p2" and
@@ -300,7 +291,7 @@
shows "pickWP A p1 p2 b1 b2 \<in> A"
"p1 (pickWP A p1 p2 b1 b2) = b1"
"p2 (pickWP A p1 p2 b1 b2) = b2"
-using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+
+unfolding pickWP_def using assms someI_ex[OF pickWP_pred] by fastforce+
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
unfolding Field_card_of csum_def by auto
--- a/src/HOL/BNF/Basic_BNFs.thy Mon Mar 18 10:28:42 2013 +0100
+++ b/src/HOL/BNF/Basic_BNFs.thy Mon Mar 18 11:05:33 2013 +0100
@@ -24,11 +24,12 @@
lemma natLeq_cinfinite: "cinfinite natLeq"
unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
+lemma wpull_Gr_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Gr B1 f1 O (Gr B2 f2)\<inverse> \<subseteq> (Gr A p1)\<inverse> O Gr A p2"
+ unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
+
bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
"\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
-apply auto
-apply (rule natLeq_card_order)
-apply (rule natLeq_cinfinite)
+apply (auto simp: Gr_def fun_eq_iff 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)
@@ -48,18 +49,13 @@
apply (rule ordLeq_csum2)
apply (rule Card_order_ctwo)
apply (rule natLeq_Card_order)
-apply (auto simp: Gr_def fun_eq_iff)
done
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)
-apply (rule card_of_card_order_on)
-apply (rule cinfinite_csum)
-apply (rule disjI1)
-apply (rule natLeq_cinfinite)
+apply (auto simp add: wpull_Gr_def Gr_def
+ card_order_csum natLeq_card_order card_of_card_order_on
+ cinfinite_csum natLeq_cinfinite)
apply (rule ordLess_imp_ordLeq)
apply (rule ordLess_ordLeq_trans)
apply (rule ordLess_ctwo_cexp)
@@ -69,7 +65,6 @@
apply (rule card_of_Card_order)
apply (rule ctwo_Cnotzero)
apply (rule card_of_Card_order)
-apply (auto simp: Id_def Gr_def fun_eq_iff)
done
definition setl :: "'a + 'b \<Rightarrow> 'a set" where
@@ -344,11 +339,8 @@
ultimately show ?thesis using card_of_ordLeq by fast
qed
-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_rel
+ "fun_rel op ="
proof
fix f show "id \<circ> f = id f" by simp
next
@@ -408,10 +400,10 @@
qed
next
fix R
- show "{p. fun_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
+ show "{p. fun_rel op = (\<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_rel_def Gr_def relcomp_unfold converse_unfold
- by (auto intro!: exI dest!: in_mono)
+ by force
qed auto
end
--- a/src/HOL/BNF/More_BNFs.thy Mon Mar 18 10:28:42 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy Mon Mar 18 11:05:33 2013 +0100
@@ -22,13 +22,6 @@
lemma option_rec_conv_option_case: "option_rec = option_case"
by (simp add: fun_eq_iff split: option.split)
-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_rel
proof -
show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
@@ -92,7 +85,7 @@
fix R
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_rel_def Gr_def relcomp_unfold converse_unfold
+ unfolding option_rel_unfold 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
@@ -286,9 +279,6 @@
lemma abs_fset_rep_fset[simp]: "abs_fset (rep_fset x) = x"
by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
-lemma wpull_Gr_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Gr B1 f1 O (Gr B2 f2)\<inverse> \<subseteq> (Gr A p1)\<inverse> O Gr A p2"
- unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
-
lemma wpull_image:
assumes "wpull A B1 B2 f1 f2 p1 p2"
shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"