# HG changeset patch
# User traytel
# Date 1363601133 -3600
# Node ID a6ebb12cc0035e334d84a366e41317ea4245e379
# Parent  1c9538a04e639bd77f4f7e59caeb6585e293be87
hide internal constants; tuned proofs

diff -r 1c9538a04e63 -r a6ebb12cc003 src/HOL/BNF/BNF.thy
--- 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
diff -r 1c9538a04e63 -r a6ebb12cc003 src/HOL/BNF/BNF_GFP.thy
--- 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
diff -r 1c9538a04e63 -r a6ebb12cc003 src/HOL/BNF/Basic_BNFs.thy
--- 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
diff -r 1c9538a04e63 -r a6ebb12cc003 src/HOL/BNF/More_BNFs.thy
--- 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)"