author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 62954  c5d0fdc260fa 
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 

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

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

7 
theory Quotient_Option 
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 

55525  13 
lemma rel_option_map1: 
14 
"rel_option R (map_option f x) y \<longleftrightarrow> rel_option (\<lambda>x. R (f x)) x y" 

15 
by (simp add: rel_option_iff split: option.split) 

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

16 

55525  17 
lemma rel_option_map2: 
18 
"rel_option R x (map_option f y) \<longleftrightarrow> rel_option (\<lambda>x y. R x (f y)) x y" 

19 
by (simp add: rel_option_iff split: option.split) 

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

20 

55466  21 
declare 
22 
map_option.id [id_simps] 

56525  23 
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

24 

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

25 
lemma reflp_rel_option: 
e81ee43ab290
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
kuncar
parents:
55525
diff
changeset

26 
"reflp R \<Longrightarrow> reflp (rel_option R)" 
e81ee43ab290
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
kuncar
parents:
55525
diff
changeset

27 
unfolding reflp_def split_option_all by simp 
e81ee43ab290
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
kuncar
parents:
55525
diff
changeset

28 

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

29 
lemma option_symp: 
55525  30 
"symp R \<Longrightarrow> symp (rel_option R)" 
31 
unfolding symp_def split_option_all 

32 
by (simp only: option.rel_inject option.rel_distinct) fast 

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

33 

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

34 
lemma option_transp: 
55525  35 
"transp R \<Longrightarrow> transp (rel_option R)" 
36 
unfolding transp_def split_option_all 

37 
by (simp only: option.rel_inject option.rel_distinct) fast 

40820
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_equivp [quot_equiv]: 
55525  40 
"equivp R \<Longrightarrow> equivp (rel_option R)" 
41 
by (blast intro: equivpI reflp_rel_option 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

42 

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

43 
lemma option_quotient [quot_thm]: 
47308  44 
assumes "Quotient3 R Abs Rep" 
55525  45 
shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)" 
47308  46 
apply (rule Quotient3I) 
56525  47 
apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] option.rel_eq rel_option_map1 rel_option_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms]) 
47308  48 
using Quotient3_rel [OF assms] 
55525  49 
apply (simp add: rel_option_iff split: option.split) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

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

51 

55525  52 
declare [[mapQ3 option = (rel_option, option_quotient)]] 
47094  53 

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

54 
lemma option_None_rsp [quot_respect]: 
47308  55 
assumes q: "Quotient3 R Abs Rep" 
55525  56 
shows "rel_option R None None" 
58916  57 
by (rule option.ctr_transfer(1)) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

58 

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

59 
lemma option_Some_rsp [quot_respect]: 
47308  60 
assumes q: "Quotient3 R Abs Rep" 
55525  61 
shows "(R ===> rel_option R) Some Some" 
58916  62 
by (rule option.ctr_transfer(2)) 
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:
40542
diff
changeset

64 
lemma option_None_prs [quot_preserve]: 
47308  65 
assumes q: "Quotient3 R Abs Rep" 
55466  66 
shows "map_option Abs None = None" 
55525  67 
by (rule Option.option.map(1)) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

68 

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

69 
lemma option_Some_prs [quot_preserve]: 
47308  70 
assumes q: "Quotient3 R Abs Rep" 
55466  71 
shows "(Rep > map_option 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

72 
apply(simp add: fun_eq_iff) 
47308  73 
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

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

75 

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

76 
end 