author | kuncar |
Thu, 10 Apr 2014 17:48:15 +0200 | |
changeset 56520 | 3373f5d1e074 |
parent 56519 | c1048f5bbb45 |
child 56525 | b5b6ad5dc2ae |
permissions | -rw-r--r-- |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
1 |
(* Title: HOL/Lifting_Product.thy |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
2 |
Author: Brian Huffman and Ondrej Kuncar |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
3 |
*) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
4 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
5 |
header {* Setup for Lifting/Transfer for the product type *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
6 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
7 |
theory Lifting_Product |
55083 | 8 |
imports Lifting Basic_BNFs |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
9 |
begin |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
10 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
11 |
subsection {* Relator and predicator properties *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
12 |
|
56092
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset
|
13 |
definition pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset
|
14 |
where "pred_prod R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
15 |
|
56092
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset
|
16 |
lemma pred_prod_apply [simp]: |
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset
|
17 |
"pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b" |
1ba075db8fe4
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
blanchet
parents:
55945
diff
changeset
|
18 |
by (simp add: pred_prod_def) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
19 |
|
55944 | 20 |
lemmas rel_prod_eq[relator_eq] = prod.rel_eq |
21 |
lemmas rel_prod_mono[relator_mono] = prod.rel_mono |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
22 |
|
55944 | 23 |
lemma rel_prod_OO[relator_distr]: |
24 |
"(rel_prod A B) OO (rel_prod C D) = rel_prod (A OO C) (B OO D)" |
|
25 |
by (rule ext)+ (auto simp: rel_prod_def OO_def) |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
26 |
|
56520
3373f5d1e074
abstract Domainp in relator_domain rules => more natural statement of the rule
kuncar
parents:
56519
diff
changeset
|
27 |
lemma Domainp_prod[relator_domain]: |
3373f5d1e074
abstract Domainp in relator_domain rules => more natural statement of the rule
kuncar
parents:
56519
diff
changeset
|
28 |
"Domainp (rel_prod T1 T2) = (pred_prod (Domainp T1) (Domainp T2))" |
3373f5d1e074
abstract Domainp in relator_domain rules => more natural statement of the rule
kuncar
parents:
56519
diff
changeset
|
29 |
unfolding rel_prod_def pred_prod_def by blast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
30 |
|
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56092
diff
changeset
|
31 |
lemma left_total_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
32 |
assumes "left_total R1" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
33 |
assumes "left_total R2" |
55944 | 34 |
shows "left_total (rel_prod R1 R2)" |
35 |
using assms unfolding left_total_def rel_prod_def by auto |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
36 |
|
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56092
diff
changeset
|
37 |
lemma left_unique_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
38 |
assumes "left_unique R1" and "left_unique R2" |
55944 | 39 |
shows "left_unique (rel_prod R1 R2)" |
40 |
using assms unfolding left_unique_def rel_prod_def by auto |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
41 |
|
55944 | 42 |
lemma right_total_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
43 |
assumes "right_total R1" and "right_total R2" |
55944 | 44 |
shows "right_total (rel_prod R1 R2)" |
45 |
using assms unfolding right_total_def rel_prod_def by auto |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
46 |
|
55944 | 47 |
lemma right_unique_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
48 |
assumes "right_unique R1" and "right_unique R2" |
55944 | 49 |
shows "right_unique (rel_prod R1 R2)" |
50 |
using assms unfolding right_unique_def rel_prod_def by auto |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
51 |
|
55944 | 52 |
lemma bi_total_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
53 |
assumes "bi_total R1" and "bi_total R2" |
55944 | 54 |
shows "bi_total (rel_prod R1 R2)" |
55 |
using assms unfolding bi_total_def rel_prod_def by auto |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
56 |
|
55944 | 57 |
lemma bi_unique_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
58 |
assumes "bi_unique R1" and "bi_unique R2" |
55944 | 59 |
shows "bi_unique (rel_prod R1 R2)" |
60 |
using assms unfolding bi_unique_def rel_prod_def by auto |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
61 |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
62 |
lemma prod_relator_eq_onp [relator_eq_onp]: |
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
63 |
"rel_prod (eq_onp P1) (eq_onp P2) = eq_onp (pred_prod P1 P2)" |
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
64 |
by (simp add: fun_eq_iff rel_prod_def pred_prod_def eq_onp_def) blast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
65 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
66 |
subsection {* Quotient theorem for the Lifting package *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
67 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
68 |
lemma Quotient_prod[quot_map]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
69 |
assumes "Quotient R1 Abs1 Rep1 T1" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
70 |
assumes "Quotient R2 Abs2 Rep2 T2" |
55944 | 71 |
shows "Quotient (rel_prod R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (rel_prod T1 T2)" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
72 |
using assms unfolding Quotient_alt_def by auto |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
73 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
74 |
subsection {* Transfer rules for the Transfer package *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
75 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
76 |
context |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
77 |
begin |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
78 |
interpretation lifting_syntax . |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
79 |
|
55944 | 80 |
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair" |
55945 | 81 |
unfolding rel_fun_def rel_prod_def by simp |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
82 |
|
55944 | 83 |
lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst" |
55945 | 84 |
unfolding rel_fun_def rel_prod_def by simp |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
85 |
|
55944 | 86 |
lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd" |
55945 | 87 |
unfolding rel_fun_def rel_prod_def by simp |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
88 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55085
diff
changeset
|
89 |
lemma case_prod_transfer [transfer_rule]: |
55944 | 90 |
"((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod" |
55945 | 91 |
unfolding rel_fun_def rel_prod_def by simp |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
92 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
93 |
lemma curry_transfer [transfer_rule]: |
55944 | 94 |
"((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
95 |
unfolding curry_def by transfer_prover |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
96 |
|
55932 | 97 |
lemma map_prod_transfer [transfer_rule]: |
55944 | 98 |
"((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D) |
55932 | 99 |
map_prod map_prod" |
100 |
unfolding map_prod_def [abs_def] by transfer_prover |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
101 |
|
55944 | 102 |
lemma rel_prod_transfer [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
103 |
"((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> |
55944 | 104 |
rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod" |
55945 | 105 |
unfolding rel_fun_def by auto |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
106 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
107 |
end |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
108 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
109 |
end |