author | blanchet |
Thu, 06 Mar 2014 15:40:33 +0100 | |
changeset 55945 | e96383acecf9 |
parent 55944 | 7ab8f003fe41 |
child 56092 | 1ba075db8fe4 |
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 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
13 |
definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
14 |
where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
15 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
16 |
lemma prod_pred_apply [simp]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
17 |
"prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
18 |
by (simp add: prod_pred_def) |
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 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
27 |
lemma Domainp_prod[relator_domain]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
28 |
assumes "Domainp T1 = P1" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
29 |
assumes "Domainp T2 = P2" |
55944 | 30 |
shows "Domainp (rel_prod T1 T2) = (prod_pred P1 P2)" |
31 |
using assms unfolding rel_prod_def prod_pred_def by blast |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
32 |
|
55944 | 33 |
lemma left_total_rel_prod [reflexivity_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
34 |
assumes "left_total R1" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
35 |
assumes "left_total R2" |
55944 | 36 |
shows "left_total (rel_prod R1 R2)" |
37 |
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
|
38 |
|
55944 | 39 |
lemma left_unique_rel_prod [reflexivity_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
40 |
assumes "left_unique R1" and "left_unique R2" |
55944 | 41 |
shows "left_unique (rel_prod R1 R2)" |
42 |
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
|
43 |
|
55944 | 44 |
lemma right_total_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
45 |
assumes "right_total R1" and "right_total R2" |
55944 | 46 |
shows "right_total (rel_prod R1 R2)" |
47 |
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
|
48 |
|
55944 | 49 |
lemma right_unique_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
50 |
assumes "right_unique R1" and "right_unique R2" |
55944 | 51 |
shows "right_unique (rel_prod R1 R2)" |
52 |
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
|
53 |
|
55944 | 54 |
lemma bi_total_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
55 |
assumes "bi_total R1" and "bi_total R2" |
55944 | 56 |
shows "bi_total (rel_prod R1 R2)" |
57 |
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
|
58 |
|
55944 | 59 |
lemma bi_unique_rel_prod [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
60 |
assumes "bi_unique R1" and "bi_unique R2" |
55944 | 61 |
shows "bi_unique (rel_prod R1 R2)" |
62 |
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
|
63 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
64 |
lemma prod_invariant_commute [invariant_commute]: |
55944 | 65 |
"rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)" |
66 |
by (simp add: fun_eq_iff rel_prod_def prod_pred_def Lifting.invariant_def) blast |
|
53012
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 |
subsection {* Quotient theorem for the Lifting package *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
69 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
70 |
lemma Quotient_prod[quot_map]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
71 |
assumes "Quotient R1 Abs1 Rep1 T1" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
72 |
assumes "Quotient R2 Abs2 Rep2 T2" |
55944 | 73 |
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
|
74 |
using assms unfolding Quotient_alt_def by auto |
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 |
subsection {* Transfer rules for the Transfer package *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
77 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
78 |
context |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
79 |
begin |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
80 |
interpretation lifting_syntax . |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
81 |
|
55944 | 82 |
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair" |
55945 | 83 |
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
|
84 |
|
55944 | 85 |
lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst" |
55945 | 86 |
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
|
87 |
|
55944 | 88 |
lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd" |
55945 | 89 |
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
|
90 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55085
diff
changeset
|
91 |
lemma case_prod_transfer [transfer_rule]: |
55944 | 92 |
"((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod" |
55945 | 93 |
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
|
94 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
95 |
lemma curry_transfer [transfer_rule]: |
55944 | 96 |
"((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
|
97 |
unfolding curry_def by transfer_prover |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
98 |
|
55932 | 99 |
lemma map_prod_transfer [transfer_rule]: |
55944 | 100 |
"((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D) |
55932 | 101 |
map_prod map_prod" |
102 |
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
|
103 |
|
55944 | 104 |
lemma rel_prod_transfer [transfer_rule]: |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
105 |
"((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> |
55944 | 106 |
rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod" |
55945 | 107 |
unfolding rel_fun_def by auto |
53012
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 |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
110 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
111 |
end |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
112 |