merged two small theory files
authorblanchet
Fri Jun 27 10:11:44 2014 +0200 (2014-06-27)
changeset 57398882091eb1e9a
parent 57397 5004aca20821
child 57399 cfc19f0a6261
merged two small theory files
src/Doc/Datatypes/Datatypes.thy
src/HOL/BNF_Def.thy
src/HOL/BNF_Examples/Stream_Processor.thy
src/HOL/BNF_Util.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/FSet.thy
src/HOL/Lifting.thy
src/HOL/Transfer.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Jun 27 10:11:44 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Jun 27 10:11:44 2014 +0200
     1.3 @@ -2495,8 +2495,8 @@
     1.4      next
     1.5        fix R
     1.6        show "rel_fn R =
     1.7 -            (BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
     1.8 -             BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
     1.9 +            (BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
    1.10 +             BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
    1.11          unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
    1.12          apply transfer
    1.13          unfolding rel_fun_def subset_iff image_iff
     2.1 --- a/src/HOL/BNF_Def.thy	Fri Jun 27 10:11:44 2014 +0200
     2.2 +++ b/src/HOL/BNF_Def.thy	Fri Jun 27 10:11:44 2014 +0200
     2.3 @@ -1,5 +1,6 @@
     2.4  (*  Title:      HOL/BNF_Def.thy
     2.5      Author:     Dmitriy Traytel, TU Muenchen
     2.6 +    Author:     Jasmin Blanchette, TU Muenchen
     2.7      Copyright   2012
     2.8  
     2.9  Definition of bounded natural functors.
    2.10 @@ -8,12 +9,47 @@
    2.11  header {* Definition of Bounded Natural Functors *}
    2.12  
    2.13  theory BNF_Def
    2.14 -imports BNF_Util Fun_Def_Base
    2.15 +imports BNF_Cardinal_Arithmetic Fun_Def_Base
    2.16  keywords
    2.17    "print_bnfs" :: diag and
    2.18    "bnf" :: thy_goal
    2.19  begin
    2.20  
    2.21 +definition
    2.22 +  rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
    2.23 +where
    2.24 +  "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
    2.25 +
    2.26 +lemma rel_funI [intro]:
    2.27 +  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
    2.28 +  shows "rel_fun A B f g"
    2.29 +  using assms by (simp add: rel_fun_def)
    2.30 +
    2.31 +lemma rel_funD:
    2.32 +  assumes "rel_fun A B f g" and "A x y"
    2.33 +  shows "B (f x) (g y)"
    2.34 +  using assms by (simp add: rel_fun_def)
    2.35 +
    2.36 +definition collect where
    2.37 +"collect F x = (\<Union>f \<in> F. f x)"
    2.38 +
    2.39 +lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
    2.40 +by simp
    2.41 +
    2.42 +lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
    2.43 +by simp
    2.44 +
    2.45 +lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
    2.46 +unfolding bij_def inj_on_def by auto blast
    2.47 +
    2.48 +(* Operator: *)
    2.49 +definition "Gr A f = {(a, f a) | a. a \<in> A}"
    2.50 +
    2.51 +definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
    2.52 +
    2.53 +definition vimage2p where
    2.54 +  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
    2.55 +
    2.56  lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
    2.57    by (rule ext) (auto simp only: comp_apply collect_def)
    2.58  
    2.59 @@ -152,6 +188,8 @@
    2.60  lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
    2.61    unfolding vimage2p_def Grp_def by auto
    2.62  
    2.63 +ML_file "Tools/BNF/bnf_util.ML"
    2.64 +ML_file "Tools/BNF/bnf_tactics.ML"
    2.65  ML_file "Tools/BNF/bnf_def_tactics.ML"
    2.66  ML_file "Tools/BNF/bnf_def.ML"
    2.67  
     3.1 --- a/src/HOL/BNF_Examples/Stream_Processor.thy	Fri Jun 27 10:11:44 2014 +0200
     3.2 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Fri Jun 27 10:11:44 2014 +0200
     3.3 @@ -126,7 +126,7 @@
     3.4  (*will be provided by the package*)
     3.5  lemma sp\<^sub>\<mu>_rel_map_map[unfolded vimage2p_def, simp]:
     3.6    "rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') =
     3.7 -  rel_sp\<^sub>\<mu> (BNF_Util.vimage2p f1 g1 R1) (BNF_Util.vimage2p f2 g2 R2) sp sp'"
     3.8 +  rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'"
     3.9  by (tactic {*
    3.10    let val ks = 1 upto 2;
    3.11    in
     4.1 --- a/src/HOL/BNF_Util.thy	Fri Jun 27 10:11:44 2014 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,53 +0,0 @@
     4.4 -(*  Title:      HOL/BNF_Util.thy
     4.5 -    Author:     Dmitriy Traytel, TU Muenchen
     4.6 -    Author:     Jasmin Blanchette, TU Muenchen
     4.7 -    Copyright   2012
     4.8 -
     4.9 -Library for bounded natural functors.
    4.10 -*)
    4.11 -
    4.12 -header {* Library for Bounded Natural Functors *}
    4.13 -
    4.14 -theory BNF_Util
    4.15 -imports BNF_Cardinal_Arithmetic
    4.16 -begin
    4.17 -
    4.18 -definition
    4.19 -  rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
    4.20 -where
    4.21 -  "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
    4.22 -
    4.23 -lemma rel_funI [intro]:
    4.24 -  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
    4.25 -  shows "rel_fun A B f g"
    4.26 -  using assms by (simp add: rel_fun_def)
    4.27 -
    4.28 -lemma rel_funD:
    4.29 -  assumes "rel_fun A B f g" and "A x y"
    4.30 -  shows "B (f x) (g y)"
    4.31 -  using assms by (simp add: rel_fun_def)
    4.32 -
    4.33 -definition collect where
    4.34 -"collect F x = (\<Union>f \<in> F. f x)"
    4.35 -
    4.36 -lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
    4.37 -by simp
    4.38 -
    4.39 -lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
    4.40 -by simp
    4.41 -
    4.42 -lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
    4.43 -unfolding bij_def inj_on_def by auto blast
    4.44 -
    4.45 -(* Operator: *)
    4.46 -definition "Gr A f = {(a, f a) | a. a \<in> A}"
    4.47 -
    4.48 -definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
    4.49 -
    4.50 -definition vimage2p where
    4.51 -  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
    4.52 -
    4.53 -ML_file "Tools/BNF/bnf_util.ML"
    4.54 -ML_file "Tools/BNF/bnf_tactics.ML"
    4.55 -
    4.56 -end
     5.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Fri Jun 27 10:11:44 2014 +0200
     5.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Fri Jun 27 10:11:44 2014 +0200
     5.3 @@ -11,7 +11,7 @@
     5.4  imports Countable_Set Cardinal_Notations
     5.5  begin
     5.6  
     5.7 -abbreviation "Grp \<equiv> BNF_Util.Grp"
     5.8 +abbreviation "Grp \<equiv> BNF_Def.Grp"
     5.9  
    5.10  
    5.11  subsection{* Cardinal stuff *}
     6.1 --- a/src/HOL/Library/FSet.thy	Fri Jun 27 10:11:44 2014 +0200
     6.2 +++ b/src/HOL/Library/FSet.thy	Fri Jun 27 10:11:44 2014 +0200
     6.3 @@ -931,8 +931,8 @@
     6.4  
     6.5  lemma rel_fset_aux:
     6.6  "(\<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>
     6.7 - ((BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
     6.8 -  BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
     6.9 + ((BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
    6.10 +  BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
    6.11  proof
    6.12    assume ?L
    6.13    def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
     7.1 --- a/src/HOL/Lifting.thy	Fri Jun 27 10:11:44 2014 +0200
     7.2 +++ b/src/HOL/Lifting.thy	Fri Jun 27 10:11:44 2014 +0200
     7.3 @@ -163,7 +163,7 @@
     7.4  
     7.5  lemma Quotient_alt_def5:
     7.6    "Quotient R Abs Rep T \<longleftrightarrow>
     7.7 -    T \<le> BNF_Util.Grp UNIV Abs \<and> BNF_Util.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
     7.8 +    T \<le> BNF_Def.Grp UNIV Abs \<and> BNF_Def.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
     7.9    unfolding Quotient_alt_def4 Grp_def by blast
    7.10  
    7.11  lemma fun_quotient:
     8.1 --- a/src/HOL/Transfer.thy	Fri Jun 27 10:11:44 2014 +0200
     8.2 +++ b/src/HOL/Transfer.thy	Fri Jun 27 10:11:44 2014 +0200
     8.3 @@ -230,7 +230,7 @@
     8.4  definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
     8.5    where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
     8.6  
     8.7 -lemma eq_onp_Grp: "eq_onp P = BNF_Util.Grp (Collect P) id" 
     8.8 +lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id" 
     8.9  unfolding eq_onp_def Grp_def by auto 
    8.10  
    8.11  lemma eq_onp_to_eq: