author | wenzelm |
Tue, 03 Sep 2013 01:12:40 +0200 | |
changeset 53374 | a14d2a854c02 |
parent 49947 | 29cd291bfea6 |
child 54611 | 31afce809794 |
permissions | -rw-r--r-- |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/Set_Comprehension_Pointfree_Tests.thy |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
2 |
Author: Lukas Bulwahn, Rafal Kolanski |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
3 |
Copyright 2012 TU Muenchen |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
4 |
*) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
5 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
6 |
header {* Tests for the set comprehension to pointfree simproc *} |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
7 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
8 |
theory Set_Comprehension_Pointfree_Tests |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
9 |
imports Main |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
10 |
begin |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
11 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
12 |
lemma |
49851
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
13 |
"finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
14 |
by simp |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
15 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
16 |
lemma |
49851
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
17 |
"finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
18 |
by simp |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
19 |
|
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
20 |
lemma |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
21 |
"finite B ==> finite A' ==> finite {f a b| a b. a : A \<and> a : A' \<and> b : B}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
22 |
by simp |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
23 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
24 |
lemma |
49851
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
25 |
"finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> b : B'}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
26 |
by simp |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
27 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
28 |
lemma |
49851
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
29 |
"finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
30 |
by simp |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
31 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
32 |
lemma |
49851
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
33 |
"finite A ==> finite B ==> finite C ==> finite D ==> |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
34 |
finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
35 |
by simp |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
36 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
37 |
lemma |
49851
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
38 |
"finite A ==> finite B ==> finite C ==> finite D ==> finite E ==> |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
39 |
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}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
40 |
by simp |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
41 |
|
49899
1f0b7d5bea4e
set_comprehension_pointfree simproc now handles the complicated test case; tuned
bulwahn
parents:
49876
diff
changeset
|
42 |
lemma |
49851
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
43 |
"finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow> |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
44 |
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'}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
45 |
by simp |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
46 |
|
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
47 |
lemma |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
48 |
"\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk> |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
49 |
\<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})" |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
50 |
by simp |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
51 |
|
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
52 |
lemma |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
53 |
"finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D)) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
54 |
\<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})" |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
55 |
by simp |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
56 |
|
49762
b5e355c41de3
adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc
bulwahn
parents:
48174
diff
changeset
|
57 |
lemma |
49766
65318db3087b
test case for set_comprehension_pointfree simproc succeeds now
bulwahn
parents:
49762
diff
changeset
|
58 |
"finite S ==> finite {s'. EX s:S. s' = f a e s}" |
65318db3087b
test case for set_comprehension_pointfree simproc succeeds now
bulwahn
parents:
49762
diff
changeset
|
59 |
by simp |
49762
b5e355c41de3
adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc
bulwahn
parents:
48174
diff
changeset
|
60 |
|
49851
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
61 |
lemma |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
62 |
"finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> a \<notin> Z}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
63 |
by simp |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
64 |
|
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
65 |
lemma |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
66 |
"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}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
67 |
by simp |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
68 |
|
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
69 |
lemma |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
70 |
"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}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
71 |
by simp |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
72 |
|
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
73 |
lemma |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
74 |
"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}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
75 |
by simp |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
76 |
|
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
77 |
lemma |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
78 |
"finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \<or> a : AA) \<and> b : B \<and> a \<notin> Z}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
79 |
by simp |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
80 |
|
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
81 |
lemma |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
82 |
"finite A1 ==> finite A2 ==> finite A3 ==> finite A4 ==> finite A5 ==> finite B ==> |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
83 |
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}" |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
84 |
apply simp |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
85 |
oops |
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
86 |
|
49853
875ed58b3b65
adding further test cases for the set_comprehension_pointfree simproc
bulwahn
parents:
49851
diff
changeset
|
87 |
lemma "finite B ==> finite {c. EX x. x : B & c = a * x}" |
875ed58b3b65
adding further test cases for the set_comprehension_pointfree simproc
bulwahn
parents:
49851
diff
changeset
|
88 |
by simp |
875ed58b3b65
adding further test cases for the set_comprehension_pointfree simproc
bulwahn
parents:
49851
diff
changeset
|
89 |
|
875ed58b3b65
adding further test cases for the set_comprehension_pointfree simproc
bulwahn
parents:
49851
diff
changeset
|
90 |
lemma |
875ed58b3b65
adding further test cases for the set_comprehension_pointfree simproc
bulwahn
parents:
49851
diff
changeset
|
91 |
"finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}" |
875ed58b3b65
adding further test cases for the set_comprehension_pointfree simproc
bulwahn
parents:
49851
diff
changeset
|
92 |
by simp |
875ed58b3b65
adding further test cases for the set_comprehension_pointfree simproc
bulwahn
parents:
49851
diff
changeset
|
93 |
|
49876
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
94 |
lemma |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
95 |
"finite S ==> inj (%(x, y). g x y) ==> finite {f x y| x y. g x y : S}" |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
96 |
by (auto intro: finite_vimageI) |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
97 |
|
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
98 |
lemma |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
99 |
"finite A ==> finite S ==> inj (%(x, y). g x y) ==> finite {f x y z | x y z. g x y : S & z : A}" |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
100 |
by (auto intro: finite_vimageI) |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
101 |
|
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
102 |
lemma |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
103 |
"finite S ==> finite A ==> inj (%(x, y). g x y) ==> inj (%(x, y). h x y) |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
104 |
==> finite {f a b c d | a b c d. g a c : S & h b d : A}" |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
105 |
by (auto intro: finite_vimageI) |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
106 |
|
49899
1f0b7d5bea4e
set_comprehension_pointfree simproc now handles the complicated test case; tuned
bulwahn
parents:
49876
diff
changeset
|
107 |
lemma |
1f0b7d5bea4e
set_comprehension_pointfree simproc now handles the complicated test case; tuned
bulwahn
parents:
49876
diff
changeset
|
108 |
assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}" |
1f0b7d5bea4e
set_comprehension_pointfree simproc now handles the complicated test case; tuned
bulwahn
parents:
49876
diff
changeset
|
109 |
using assms by (auto intro!: finite_vimageI simp add: inj_on_def) |
1f0b7d5bea4e
set_comprehension_pointfree simproc now handles the complicated test case; tuned
bulwahn
parents:
49876
diff
changeset
|
110 |
(* injectivity to be automated with further rules and automation *) |
49876
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
111 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
112 |
schematic_lemma (* check interaction with schematics *) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
113 |
"finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b} |
49851
4d33963962fa
adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully
bulwahn
parents:
49766
diff
changeset
|
114 |
= finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))" |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
115 |
by simp |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
116 |
|
48174
eb72f99737be
adding a challenging example in the examples file
bulwahn
parents:
48109
diff
changeset
|
117 |
|
49876
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
118 |
section {* Testing simproc in code generation *} |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
119 |
|
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
120 |
definition union :: "nat set => nat set => nat set" |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
121 |
where |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
122 |
"union A B = {x. x : A \<or> x : B}" |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
123 |
|
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
124 |
definition common_subsets :: "nat set => nat set => nat set set" |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
125 |
where |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
126 |
"common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}" |
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
127 |
|
49947
29cd291bfea6
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
bulwahn
parents:
49899
diff
changeset
|
128 |
definition products :: "nat set => nat set => nat set" |
29cd291bfea6
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
bulwahn
parents:
49899
diff
changeset
|
129 |
where |
29cd291bfea6
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
bulwahn
parents:
49899
diff
changeset
|
130 |
"products A B = {c. EX a b. a : A & b : B & c = a * b}" |
29cd291bfea6
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
bulwahn
parents:
49899
diff
changeset
|
131 |
|
29cd291bfea6
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
bulwahn
parents:
49899
diff
changeset
|
132 |
export_code products in Haskell file - |
29cd291bfea6
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
bulwahn
parents:
49899
diff
changeset
|
133 |
|
29cd291bfea6
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
bulwahn
parents:
49899
diff
changeset
|
134 |
export_code union common_subsets products in Haskell file - |
49876
8cbd8340a21e
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc
bulwahn
parents:
49853
diff
changeset
|
135 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
136 |
end |