more standard theory name;
authorwenzelm
Fri Feb 21 21:08:03 2014 +0100 (2014-02-21)
changeset 5566312448c179851
parent 55662 b45af39fcdae
child 55664 bab10fb557c2
more standard theory name;
src/HOL/ROOT
src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy
src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
     1.1 --- a/src/HOL/ROOT	Fri Feb 21 20:54:13 2014 +0100
     1.2 +++ b/src/HOL/ROOT	Fri Feb 21 21:08:03 2014 +0100
     1.3 @@ -570,7 +570,7 @@
     1.4      Simproc_Tests
     1.5      Executable_Relation
     1.6      FinFunPred
     1.7 -    Set_Comprehension_Pointfree_Tests
     1.8 +    Set_Comprehension_Pointfree_Examples
     1.9      Parallel_Example
    1.10      IArray_Examples
    1.11      SVC_Oracle
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy	Fri Feb 21 21:08:03 2014 +0100
     2.3 @@ -0,0 +1,140 @@
     2.4 +(*  Title:      HOL/ex/Set_Comprehension_Pointfree_Examples.thy
     2.5 +    Author:     Lukas Bulwahn, Rafal Kolanski
     2.6 +    Copyright   2012 TU Muenchen
     2.7 +*)
     2.8 +
     2.9 +header {* Examples for the set comprehension to pointfree simproc *}
    2.10 +
    2.11 +theory Set_Comprehension_Pointfree_Examples
    2.12 +imports Main
    2.13 +begin
    2.14 +
    2.15 +declare [[simproc add: finite_Collect]]
    2.16 +
    2.17 +lemma
    2.18 +  "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}"
    2.19 +  by simp
    2.20 +
    2.21 +lemma
    2.22 +  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B}"
    2.23 +  by simp
    2.24 +  
    2.25 +lemma
    2.26 +  "finite B ==> finite A' ==> finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
    2.27 +  by simp
    2.28 +
    2.29 +lemma
    2.30 +  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
    2.31 +  by simp
    2.32 +
    2.33 +lemma
    2.34 +  "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
    2.35 +  by simp
    2.36 +
    2.37 +lemma
    2.38 +  "finite A ==> finite B ==> finite C ==> finite D ==>
    2.39 +     finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
    2.40 +  by simp
    2.41 +
    2.42 +lemma
    2.43 +  "finite A ==> finite B ==> finite C ==> finite D ==> finite E ==>
    2.44 +    finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"
    2.45 +  by simp
    2.46 +
    2.47 +lemma
    2.48 +  "finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow>
    2.49 +    finite {f a d c b e | e b c d a. b : B \<and> a : A \<and> e : E' \<and> c : C \<and> d : D \<and> e : E \<and> b : B'}"
    2.50 +  by simp
    2.51 +
    2.52 +lemma
    2.53 +  "\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk>
    2.54 +  \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
    2.55 +  by simp
    2.56 +
    2.57 +lemma
    2.58 +  "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D))
    2.59 +  \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
    2.60 +  by simp
    2.61 +
    2.62 +lemma
    2.63 +  "finite S ==> finite {s'. EX s:S. s' = f a e s}"
    2.64 +  by simp
    2.65 +
    2.66 +lemma
    2.67 +  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> a \<notin> Z}"
    2.68 +  by simp
    2.69 +
    2.70 +lemma
    2.71 +  "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> b : B \<and> (x,y) \<in> R}"
    2.72 +by simp
    2.73 +
    2.74 +lemma
    2.75 +  "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> (x,y) \<in> R \<and> b : B}"
    2.76 +by simp
    2.77 +
    2.78 +lemma
    2.79 +  "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \<and> (x,y) \<in> R \<and> b : B}"
    2.80 +by simp
    2.81 +
    2.82 +lemma
    2.83 +  "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \<or> a : AA) \<and> b : B \<and> a \<notin> Z}"
    2.84 +by simp
    2.85 +
    2.86 +lemma
    2.87 +  "finite A1 ==> finite A2 ==> finite A3 ==> finite A4 ==> finite A5 ==> finite B ==>
    2.88 +     finite {f a b c | a b c. ((a : A1 \<and> a : A2) \<or> (a : A3 \<and> (a : A4 \<or> a : A5))) \<and> b : B \<and> a \<notin> Z}"
    2.89 +apply simp
    2.90 +oops
    2.91 +
    2.92 +lemma "finite B ==> finite {c. EX x. x : B & c = a * x}"
    2.93 +by simp
    2.94 +
    2.95 +lemma
    2.96 +  "finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
    2.97 +by simp
    2.98 +
    2.99 +lemma
   2.100 +  "finite S ==> inj (%(x, y). g x y) ==> finite {f x y| x y. g x y : S}"
   2.101 +  by (auto intro: finite_vimageI)
   2.102 +
   2.103 +lemma
   2.104 +  "finite A ==> finite S ==> inj (%(x, y). g x y) ==> finite {f x y z | x y z. g x y : S & z : A}"
   2.105 +  by (auto intro: finite_vimageI)
   2.106 +
   2.107 +lemma
   2.108 +  "finite S ==> finite A ==> inj (%(x, y). g x y) ==> inj (%(x, y). h x y)
   2.109 +    ==> finite {f a b c d | a b c d. g a c : S & h b d : A}"
   2.110 +  by (auto intro: finite_vimageI)
   2.111 +
   2.112 +lemma
   2.113 +  assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
   2.114 +using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
   2.115 +  (* injectivity to be automated with further rules and automation *)
   2.116 +
   2.117 +schematic_lemma (* check interaction with schematics *)
   2.118 +  "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
   2.119 +   = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
   2.120 +  by simp
   2.121 +
   2.122 +declare [[simproc del: finite_Collect]]
   2.123 +
   2.124 +
   2.125 +section {* Testing simproc in code generation *}
   2.126 +
   2.127 +definition union :: "nat set => nat set => nat set"
   2.128 +where
   2.129 +  "union A B = {x. x : A \<or> x : B}"
   2.130 +
   2.131 +definition common_subsets :: "nat set => nat set => nat set set"
   2.132 +where
   2.133 +  "common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}"
   2.134 +
   2.135 +definition products :: "nat set => nat set => nat set"
   2.136 +where
   2.137 +  "products A B = {c. EX a b. a : A & b : B & c = a * b}"
   2.138 +
   2.139 +export_code products in Haskell
   2.140 +
   2.141 +export_code union common_subsets products in Haskell
   2.142 +
   2.143 +end
     3.1 --- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Fri Feb 21 20:54:13 2014 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,140 +0,0 @@
     3.4 -(*  Title:      HOL/ex/Set_Comprehension_Pointfree_Tests.thy
     3.5 -    Author:     Lukas Bulwahn, Rafal Kolanski
     3.6 -    Copyright   2012 TU Muenchen
     3.7 -*)
     3.8 -
     3.9 -header {* Tests for the set comprehension to pointfree simproc *}
    3.10 -
    3.11 -theory Set_Comprehension_Pointfree_Tests
    3.12 -imports Main
    3.13 -begin
    3.14 -
    3.15 -declare [[simproc add: finite_Collect]]
    3.16 -
    3.17 -lemma
    3.18 -  "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}"
    3.19 -  by simp
    3.20 -
    3.21 -lemma
    3.22 -  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B}"
    3.23 -  by simp
    3.24 -  
    3.25 -lemma
    3.26 -  "finite B ==> finite A' ==> finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
    3.27 -  by simp
    3.28 -
    3.29 -lemma
    3.30 -  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
    3.31 -  by simp
    3.32 -
    3.33 -lemma
    3.34 -  "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
    3.35 -  by simp
    3.36 -
    3.37 -lemma
    3.38 -  "finite A ==> finite B ==> finite C ==> finite D ==>
    3.39 -     finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
    3.40 -  by simp
    3.41 -
    3.42 -lemma
    3.43 -  "finite A ==> finite B ==> finite C ==> finite D ==> finite E ==>
    3.44 -    finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"
    3.45 -  by simp
    3.46 -
    3.47 -lemma
    3.48 -  "finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow>
    3.49 -    finite {f a d c b e | e b c d a. b : B \<and> a : A \<and> e : E' \<and> c : C \<and> d : D \<and> e : E \<and> b : B'}"
    3.50 -  by simp
    3.51 -
    3.52 -lemma
    3.53 -  "\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk>
    3.54 -  \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
    3.55 -  by simp
    3.56 -
    3.57 -lemma
    3.58 -  "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D))
    3.59 -  \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
    3.60 -  by simp
    3.61 -
    3.62 -lemma
    3.63 -  "finite S ==> finite {s'. EX s:S. s' = f a e s}"
    3.64 -  by simp
    3.65 -
    3.66 -lemma
    3.67 -  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> a \<notin> Z}"
    3.68 -  by simp
    3.69 -
    3.70 -lemma
    3.71 -  "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> b : B \<and> (x,y) \<in> R}"
    3.72 -by simp
    3.73 -
    3.74 -lemma
    3.75 -  "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> (x,y) \<in> R \<and> b : B}"
    3.76 -by simp
    3.77 -
    3.78 -lemma
    3.79 -  "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \<and> (x,y) \<in> R \<and> b : B}"
    3.80 -by simp
    3.81 -
    3.82 -lemma
    3.83 -  "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \<or> a : AA) \<and> b : B \<and> a \<notin> Z}"
    3.84 -by simp
    3.85 -
    3.86 -lemma
    3.87 -  "finite A1 ==> finite A2 ==> finite A3 ==> finite A4 ==> finite A5 ==> finite B ==>
    3.88 -     finite {f a b c | a b c. ((a : A1 \<and> a : A2) \<or> (a : A3 \<and> (a : A4 \<or> a : A5))) \<and> b : B \<and> a \<notin> Z}"
    3.89 -apply simp
    3.90 -oops
    3.91 -
    3.92 -lemma "finite B ==> finite {c. EX x. x : B & c = a * x}"
    3.93 -by simp
    3.94 -
    3.95 -lemma
    3.96 -  "finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
    3.97 -by simp
    3.98 -
    3.99 -lemma
   3.100 -  "finite S ==> inj (%(x, y). g x y) ==> finite {f x y| x y. g x y : S}"
   3.101 -  by (auto intro: finite_vimageI)
   3.102 -
   3.103 -lemma
   3.104 -  "finite A ==> finite S ==> inj (%(x, y). g x y) ==> finite {f x y z | x y z. g x y : S & z : A}"
   3.105 -  by (auto intro: finite_vimageI)
   3.106 -
   3.107 -lemma
   3.108 -  "finite S ==> finite A ==> inj (%(x, y). g x y) ==> inj (%(x, y). h x y)
   3.109 -    ==> finite {f a b c d | a b c d. g a c : S & h b d : A}"
   3.110 -  by (auto intro: finite_vimageI)
   3.111 -
   3.112 -lemma
   3.113 -  assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
   3.114 -using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
   3.115 -  (* injectivity to be automated with further rules and automation *)
   3.116 -
   3.117 -schematic_lemma (* check interaction with schematics *)
   3.118 -  "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
   3.119 -   = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
   3.120 -  by simp
   3.121 -
   3.122 -declare [[simproc del: finite_Collect]]
   3.123 -
   3.124 -
   3.125 -section {* Testing simproc in code generation *}
   3.126 -
   3.127 -definition union :: "nat set => nat set => nat set"
   3.128 -where
   3.129 -  "union A B = {x. x : A \<or> x : B}"
   3.130 -
   3.131 -definition common_subsets :: "nat set => nat set => nat set set"
   3.132 -where
   3.133 -  "common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}"
   3.134 -
   3.135 -definition products :: "nat set => nat set => nat set"
   3.136 -where
   3.137 -  "products A B = {c. EX a b. a : A & b : B & c = a * b}"
   3.138 -
   3.139 -export_code products in Haskell
   3.140 -
   3.141 -export_code union common_subsets products in Haskell
   3.142 -
   3.143 -end