author | blanchet |
Wed, 12 Feb 2014 08:35:57 +0100 | |
changeset 55414 | eab03e9cee8a |
parent 55084 | 8ee9aabb2bca |
child 55564 | e81ee43ab290 |
permissions | -rw-r--r-- |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
1 |
(* Title: HOL/Lifting_Sum.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 sum 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_Sum |
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 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55084
diff
changeset
|
13 |
abbreviation (input) "sum_pred \<equiv> case_sum" |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
14 |
|
55084 | 15 |
lemmas sum_rel_eq[relator_eq] = sum.rel_eq |
16 |
lemmas sum_rel_mono[relator_mono] = sum.rel_mono |
|
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
17 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
18 |
lemma sum_rel_OO[relator_distr]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
19 |
"(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)" |
55084 | 20 |
by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
21 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
22 |
lemma Domainp_sum[relator_domain]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
23 |
assumes "Domainp R1 = P1" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
24 |
assumes "Domainp R2 = P2" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
25 |
shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
26 |
using assms |
53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset
|
27 |
by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
28 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
29 |
lemma reflp_sum_rel[reflexivity_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
30 |
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)" |
53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset
|
31 |
unfolding reflp_def split_sum_all sum_rel_simps by fast |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
32 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
33 |
lemma left_total_sum_rel[reflexivity_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
34 |
"left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
35 |
using assms unfolding left_total_def split_sum_all split_sum_ex by simp |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
36 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
37 |
lemma left_unique_sum_rel [reflexivity_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
38 |
"left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
39 |
using assms unfolding left_unique_def split_sum_all by simp |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
40 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
41 |
lemma right_total_sum_rel [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
42 |
"right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
43 |
unfolding right_total_def split_sum_all split_sum_ex by simp |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
44 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
45 |
lemma right_unique_sum_rel [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
46 |
"right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (sum_rel R1 R2)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
47 |
unfolding right_unique_def split_sum_all by simp |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
48 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
49 |
lemma bi_total_sum_rel [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
50 |
"bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (sum_rel R1 R2)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
51 |
using assms unfolding bi_total_def split_sum_all split_sum_ex by simp |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
52 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
53 |
lemma bi_unique_sum_rel [transfer_rule]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
54 |
"bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
55 |
using assms unfolding bi_unique_def split_sum_all by simp |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
56 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
57 |
lemma sum_invariant_commute [invariant_commute]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
58 |
"sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" |
53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset
|
59 |
by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_def split: sum.split) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
60 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
61 |
subsection {* Quotient theorem for the Lifting package *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
62 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
63 |
lemma Quotient_sum[quot_map]: |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
64 |
assumes "Quotient R1 Abs1 Rep1 T1" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
65 |
assumes "Quotient R2 Abs2 Rep2 T2" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
66 |
shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
67 |
(sum_map Rep1 Rep2) (sum_rel T1 T2)" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
68 |
using assms unfolding Quotient_alt_def |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
69 |
by (simp add: split_sum_all) |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
70 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
71 |
subsection {* Transfer rules for the Transfer package *} |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
72 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
73 |
context |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
74 |
begin |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
75 |
interpretation lifting_syntax . |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
76 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
77 |
lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
78 |
unfolding fun_rel_def by simp |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
79 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
80 |
lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr" |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
81 |
unfolding fun_rel_def by simp |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
82 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55084
diff
changeset
|
83 |
lemma case_sum_transfer [transfer_rule]: |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55084
diff
changeset
|
84 |
"((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) case_sum case_sum" |
53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset
|
85 |
unfolding fun_rel_def sum_rel_def by (simp split: sum.split) |
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
86 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
87 |
end |
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
88 |
|
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset
|
89 |
end |