author  traytel 
Tue, 13 Aug 2013 18:22:55 +0200  
changeset 53026  e1a548c11845 
parent 53012  cb82606b8215 
child 55466  786edc984c98 
permissions  rwrr 
47455  1 
(* Title: HOL/Library/Quotient_Option.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 

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 

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

11 
subsection {* Rules for the Quotient package *} 
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 

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

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

14 
"option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y" 
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

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

16 

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

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

18 
"option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y" 
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

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

20 

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

21 
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

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

23 
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

24 

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

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

26 
"option_rel (op =) = (op =)" 
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 (simp add: option_rel_def fun_eq_iff split: option.split) 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

28 

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

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

30 
"symp R \<Longrightarrow> symp (option_rel R)" 
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 symp_def split_option_all option_rel_simps by fast 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

32 

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

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

34 
"transp R \<Longrightarrow> transp (option_rel R)" 
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

35 
unfolding transp_def split_option_all option_rel_simps by fast 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

36 

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

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

38 
"equivp R \<Longrightarrow> equivp (option_rel R)" 
51994  39 
by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE) 
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset

40 

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

41 
lemma option_quotient [quot_thm]: 
47308  42 
assumes "Quotient3 R Abs Rep" 
43 
shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" 

44 
apply (rule Quotient3I) 

45 
apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms]) 

46 
using Quotient3_rel [OF 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

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

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

49 

47308  50 
declare [[mapQ3 option = (option_rel, option_quotient)]] 
47094  51 

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

52 
lemma option_None_rsp [quot_respect]: 
47308  53 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

54 
shows "option_rel R None None" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

55 
by (rule None_transfer) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

56 

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

57 
lemma option_Some_rsp [quot_respect]: 
47308  58 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

59 
shows "(R ===> option_rel R) Some Some" 
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset

60 
by (rule Some_transfer) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

61 

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

62 
lemma option_None_prs [quot_preserve]: 
47308  63 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

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

66 

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

67 
lemma option_Some_prs [quot_preserve]: 
47308  68 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

69 
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

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

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

73 

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

74 
end 