author  kuncar 
Thu, 10 Apr 2014 17:48:15 +0200  
changeset 56519  c1048f5bbb45 
parent 56518  beb3b6851665 
child 56520  3373f5d1e074 
permissions  rwrr 
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 

55943  15 
lemmas rel_sum_eq[relator_eq] = sum.rel_eq 
16 
lemmas rel_sum_mono[relator_mono] = sum.rel_mono 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

17 

55943  18 
lemma rel_sum_OO[relator_distr]: 
19 
"(rel_sum A B) OO (rel_sum C D) = rel_sum (A OO C) (B OO D)" 

20 
by (rule ext)+ (auto simp add: rel_sum_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" 
55943  25 
shows "Domainp (rel_sum R1 R2) = (sum_pred P1 P2)" 
53012
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 

56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
55945
diff
changeset

29 
lemma left_total_rel_sum[transfer_rule]: 
55943  30 
"left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (rel_sum R1 R2)" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

31 
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

32 

56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
55945
diff
changeset

33 
lemma left_unique_rel_sum [transfer_rule]: 
55943  34 
"left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (rel_sum R1 R2)" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

35 
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

36 

55943  37 
lemma right_total_rel_sum [transfer_rule]: 
38 
"right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (rel_sum R1 R2)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

39 
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

40 

55943  41 
lemma right_unique_rel_sum [transfer_rule]: 
42 
"right_unique R1 \<Longrightarrow> right_unique R2 \<Longrightarrow> right_unique (rel_sum R1 R2)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

43 
unfolding right_unique_def split_sum_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

44 

55943  45 
lemma bi_total_rel_sum [transfer_rule]: 
46 
"bi_total R1 \<Longrightarrow> bi_total R2 \<Longrightarrow> bi_total (rel_sum R1 R2)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

47 
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

48 

55943  49 
lemma bi_unique_rel_sum [transfer_rule]: 
50 
"bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (rel_sum R1 R2)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

51 
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

52 

56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

53 
lemma sum_relator_eq_onp [relator_eq_onp]: 
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

54 
"rel_sum (eq_onp P1) (eq_onp P2) = eq_onp (sum_pred P1 P2)" 
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56518
diff
changeset

55 
by (auto simp add: fun_eq_iff eq_onp_def rel_sum_def split: sum.split) 
53012
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 
subsection {* Quotient theorem for the Lifting package *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

58 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

59 
lemma Quotient_sum[quot_map]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

60 
assumes "Quotient R1 Abs1 Rep1 T1" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

61 
assumes "Quotient R2 Abs2 Rep2 T2" 
55943  62 
shows "Quotient (rel_sum R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2) (rel_sum T1 T2)" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

63 
using assms unfolding Quotient_alt_def 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

64 
by (simp add: split_sum_all) 
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 {* Transfer rules for the Transfer 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 
context 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

69 
begin 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

70 
interpretation lifting_syntax . 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

71 

55943  72 
lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl" 
55945  73 
unfolding rel_fun_def by simp 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

74 

55943  75 
lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr" 
55945  76 
unfolding rel_fun_def by simp 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

77 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55084
diff
changeset

78 
lemma case_sum_transfer [transfer_rule]: 
55943  79 
"((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum" 
55945  80 
unfolding rel_fun_def rel_sum_def by (simp split: sum.split) 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

81 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

82 
end 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

83 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

84 
end 