author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 62954  c5d0fdc260fa 
child 67399  eab6ce8368fa 
permissions  rwrr 
47455  1 
(* Title: HOL/Library/Quotient_Sum.thy 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
53010
diff
changeset

2 
Author: Cezary Kaliszyk and Christian Urban 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

3 
*) 
35788  4 

60500  5 
section \<open>Quotient infrastructure for the sum type\<close> 
35788  6 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

7 
theory Quotient_Sum 
62954  8 
imports Quotient_Syntax 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

9 
begin 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

10 

60500  11 
subsection \<open>Rules for the Quotient package\<close> 
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset

12 

55943  13 
lemma rel_sum_map1: 
14 
"rel_sum R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y" 

58916  15 
by (rule sum.rel_map(1)) 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

16 

55943  17 
lemma rel_sum_map2: 
18 
"rel_sum R1 R2 x (map_sum f1 f2 y) \<longleftrightarrow> rel_sum (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y" 

58916  19 
by (rule sum.rel_map(2)) 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

20 

55931  21 
lemma map_sum_id [id_simps]: 
22 
"map_sum id id = id" 

23 
by (simp add: id_def map_sum.identity fun_eq_iff) 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

24 

55943  25 
lemma rel_sum_eq [id_simps]: 
26 
"rel_sum (op =) (op =) = (op =)" 

58916  27 
by (rule sum.rel_eq) 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

28 

55943  29 
lemma reflp_rel_sum: 
30 
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (rel_sum R1 R2)" 

31 
unfolding reflp_def split_sum_all rel_sum_simps by fast 

55564
e81ee43ab290
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
kuncar
parents:
53026
diff
changeset

32 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

33 
lemma sum_symp: 
55943  34 
"symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (rel_sum R1 R2)" 
35 
unfolding symp_def split_sum_all rel_sum_simps by fast 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

36 

fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

37 
lemma sum_transp: 
55943  38 
"transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (rel_sum R1 R2)" 
39 
unfolding transp_def split_sum_all rel_sum_simps by fast 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

40 

fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

41 
lemma sum_equivp [quot_equiv]: 
55943  42 
"equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (rel_sum R1 R2)" 
43 
by (blast intro: equivpI reflp_rel_sum sum_symp sum_transp elim: equivpE) 

47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

44 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

45 
lemma sum_quotient [quot_thm]: 
47308  46 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
47 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

55943  48 
shows "Quotient3 (rel_sum R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2)" 
47308  49 
apply (rule Quotient3I) 
55943  50 
apply (simp_all add: map_sum.compositionality comp_def map_sum.identity rel_sum_eq rel_sum_map1 rel_sum_map2 
47308  51 
Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) 
52 
using Quotient3_rel [OF q1] Quotient3_rel [OF q2] 

58916  53 
apply (fastforce elim!: rel_sum.cases simp add: comp_def split: sum.split) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

54 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

55 

55943  56 
declare [[mapQ3 sum = (rel_sum, sum_quotient)]] 
47094  57 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

58 
lemma sum_Inl_rsp [quot_respect]: 
47308  59 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
60 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

55943  61 
shows "(R1 ===> rel_sum R1 R2) Inl Inl" 
40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

62 
by auto 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

63 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

64 
lemma sum_Inr_rsp [quot_respect]: 
47308  65 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
66 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

55943  67 
shows "(R2 ===> rel_sum R1 R2) Inr Inr" 
40465
2989f9f3aa10
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

68 
by auto 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

69 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

70 
lemma sum_Inl_prs [quot_preserve]: 
47308  71 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
72 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

55931  73 
shows "(Rep1 > map_sum Abs1 Abs2) Inl = Inl" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

74 
apply(simp add: fun_eq_iff) 
47308  75 
apply(simp add: Quotient3_abs_rep[OF q1]) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

76 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

77 

40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40610
diff
changeset

78 
lemma sum_Inr_prs [quot_preserve]: 
47308  79 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
80 
assumes q2: "Quotient3 R2 Abs2 Rep2" 

55931  81 
shows "(Rep2 > map_sum Abs1 Abs2) Inr = Inr" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

82 
apply(simp add: fun_eq_iff) 
47308  83 
apply(simp add: Quotient3_abs_rep[OF q2]) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

84 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

85 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

86 
end 