author  kuncar 
Fri, 09 Dec 2011 18:07:04 +0100  
changeset 45802  b16f976db515 
parent 41372  551eb49a6e91 
child 47094  1a7ad2601cb5 
permissions  rwrr 
35788  1 
(* Title: HOL/Library/Quotient_Option.thy 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

3 
*) 
35788  4 

5 
header {* Quotient infrastructure for the option type *} 

6 

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

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

8 
imports Main Quotient_Syntax 
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 

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

11 
fun 
40542
9a173a22771c
regeneralized type of option_rel and sum_rel (accident from 2989f9f3aa10)
haftmann
parents:
40464
diff
changeset

12 
option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

14 
"option_rel R None None = True" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

15 
 "option_rel R (Some x) None = False" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

16 
 "option_rel R None (Some x) = False" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

17 
 "option_rel R (Some x) (Some y) = R x y" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

18 

45802  19 
declare [[map option = option_rel]] 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

20 

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

21 
lemma option_rel_unfold: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

22 
"option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

23 
 (Some x, Some y) \<Rightarrow> R x y 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

24 
 _ \<Rightarrow> False)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

25 
by (cases x) (cases y, simp_all)+ 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

26 

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

27 
lemma option_rel_map1: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

28 
"option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

29 
by (simp add: option_rel_unfold split: option.split) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

30 

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

31 
lemma option_rel_map2: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

32 
"option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

33 
by (simp add: option_rel_unfold split: option.split) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

34 

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

35 
lemma option_map_id [id_simps]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

36 
"Option.map id = id" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

37 
by (simp add: id_def Option.map.identity fun_eq_iff) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

38 

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

39 
lemma option_rel_eq [id_simps]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

40 
"option_rel (op =) = (op =)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

41 
by (simp add: option_rel_unfold fun_eq_iff split: option.split) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

42 

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

43 
lemma option_reflp: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

44 
"reflp R \<Longrightarrow> reflp (option_rel R)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

45 
by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

46 

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

47 
lemma option_symp: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

48 
"symp R \<Longrightarrow> symp (option_rel R)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

49 
by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

50 

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

51 
lemma option_transp: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

52 
"transp R \<Longrightarrow> transp (option_rel R)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

53 
by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

54 

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

55 
lemma option_equivp [quot_equiv]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

56 
"equivp R \<Longrightarrow> equivp (option_rel R)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

57 
by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE) 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

58 

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

59 
lemma option_quotient [quot_thm]: 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

60 
assumes "Quotient R Abs Rep" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

61 
shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

62 
apply (rule QuotientI) 
41372  63 
apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms]) 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

64 
using Quotient_rel [OF assms] 
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

65 
apply (simp add: option_rel_unfold split: option.split) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

67 

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

68 
lemma option_None_rsp [quot_respect]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

69 
assumes q: "Quotient R Abs Rep" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

70 
shows "option_rel R None None" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

72 

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

73 
lemma option_Some_rsp [quot_respect]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

74 
assumes q: "Quotient R Abs Rep" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

75 
shows "(R ===> option_rel R) Some Some" 
40464
e1db06cf6254
type annotations in specifications; fun_rel_def is no simp rule by default
haftmann
parents:
39302
diff
changeset

76 
by auto 
35222
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:
40542
diff
changeset

78 
lemma option_None_prs [quot_preserve]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

79 
assumes q: "Quotient R Abs Rep" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

80 
shows "Option.map Abs None = None" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

82 

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

83 
lemma option_Some_prs [quot_preserve]: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

84 
assumes q: "Quotient R Abs Rep" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

85 
shows "(Rep > Option.map Abs) Some = Some" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

86 
apply(simp add: fun_eq_iff) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

87 
apply(simp add: Quotient_abs_rep[OF q]) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

89 

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

90 
end 