author | haftmann |
Thu, 25 Jul 2013 08:57:16 +0200 | |
changeset 52729 | 412c9e0381a1 |
parent 51994 | 82cc2aeb7d13 |
child 53010 | ec5e6f69bd65 |
permissions | -rw-r--r-- |
47455 | 1 |
(* Title: HOL/Library/Quotient_Option.thy |
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
2 |
Author: Cezary Kaliszyk, Christian Urban and Brian Huffman |
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 |
|
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
11 |
subsection {* Relator for option type *} |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
12 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
fun |
40542
9a173a22771c
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
haftmann
parents:
40464
diff
changeset
|
14 |
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
|
15 |
where |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
"option_rel R None None = True" |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
| "option_rel R (Some x) None = False" |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
| "option_rel R None (Some x) = False" |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
| "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
|
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 |
|
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
|
27 |
fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
28 |
where |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
29 |
"option_pred R None = True" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
30 |
| "option_pred R (Some x) = R x" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
31 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
32 |
lemma option_pred_unfold: |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
33 |
"option_pred P x = (case x of None \<Rightarrow> True |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
34 |
| Some x \<Rightarrow> P x)" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
35 |
by (cases x) simp_all |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
36 |
|
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
37 |
lemma option_rel_map1: |
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
38 |
"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
|
39 |
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
|
40 |
|
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
41 |
lemma option_rel_map2: |
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
42 |
"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
|
43 |
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
|
44 |
|
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
45 |
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
|
46 |
"Option.map id = id" |
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
47 |
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
|
48 |
|
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
49 |
lemma option_rel_eq [id_simps, relator_eq]: |
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
50 |
"option_rel (op =) = (op =)" |
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
51 |
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
|
52 |
|
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
53 |
lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
54 |
by (metis option.exhaust) (* TODO: move to Option.thy *) |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
55 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
56 |
lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
57 |
by (metis option.exhaust) (* TODO: move to Option.thy *) |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
58 |
|
51377 | 59 |
lemma option_rel_mono[relator_mono]: |
60 |
assumes "A \<le> B" |
|
61 |
shows "(option_rel A) \<le> (option_rel B)" |
|
62 |
using assms by (auto simp: option_rel_unfold split: option.splits) |
|
63 |
||
64 |
lemma option_rel_OO[relator_distr]: |
|
65 |
"(option_rel A) OO (option_rel B) = option_rel (A OO B)" |
|
66 |
by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split) |
|
67 |
||
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
|
68 |
lemma Domainp_option[relator_domain]: |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
69 |
assumes "Domainp A = P" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
70 |
shows "Domainp (option_rel A) = (option_pred P)" |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
71 |
using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def] |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
72 |
by (auto iff: fun_eq_iff split: option.split) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51377
diff
changeset
|
73 |
|
51994 | 74 |
lemma reflp_option_rel[reflexivity_rule]: |
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
75 |
"reflp R \<Longrightarrow> reflp (option_rel R)" |
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
76 |
unfolding reflp_def split_option_all by simp |
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
77 |
|
51994 | 78 |
lemma left_total_option_rel[reflexivity_rule]: |
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47936
diff
changeset
|
79 |
"left_total R \<Longrightarrow> left_total (option_rel R)" |
51994 | 80 |
unfolding left_total_def split_option_all split_option_ex by simp |
81 |
||
82 |
lemma left_unique_option_rel [reflexivity_rule]: |
|
83 |
"left_unique R \<Longrightarrow> left_unique (option_rel R)" |
|
84 |
unfolding left_unique_def split_option_all by simp |
|
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47936
diff
changeset
|
85 |
|
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
86 |
lemma option_symp: |
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
87 |
"symp R \<Longrightarrow> symp (option_rel R)" |
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
88 |
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
|
89 |
|
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
90 |
lemma option_transp: |
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
91 |
"transp R \<Longrightarrow> transp (option_rel R)" |
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
92 |
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
|
93 |
|
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
94 |
lemma option_equivp [quot_equiv]: |
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
95 |
"equivp R \<Longrightarrow> equivp (option_rel R)" |
51994 | 96 |
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
|
97 |
|
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
98 |
lemma right_total_option_rel [transfer_rule]: |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
99 |
"right_total R \<Longrightarrow> right_total (option_rel R)" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
100 |
unfolding right_total_def split_option_all split_option_ex by simp |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
101 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
102 |
lemma right_unique_option_rel [transfer_rule]: |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
103 |
"right_unique R \<Longrightarrow> right_unique (option_rel R)" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
104 |
unfolding right_unique_def split_option_all by simp |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
105 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
106 |
lemma bi_total_option_rel [transfer_rule]: |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
107 |
"bi_total R \<Longrightarrow> bi_total (option_rel R)" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
108 |
unfolding bi_total_def split_option_all split_option_ex by simp |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
109 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
110 |
lemma bi_unique_option_rel [transfer_rule]: |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
111 |
"bi_unique R \<Longrightarrow> bi_unique (option_rel R)" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
112 |
unfolding bi_unique_def split_option_all by simp |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
113 |
|
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47634
diff
changeset
|
114 |
subsection {* Transfer rules for transfer package *} |
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
115 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
116 |
lemma None_transfer [transfer_rule]: "(option_rel A) None None" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
117 |
by simp |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
118 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
119 |
lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
120 |
unfolding fun_rel_def by simp |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
121 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
122 |
lemma option_case_transfer [transfer_rule]: |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
123 |
"(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
124 |
unfolding fun_rel_def split_option_all by simp |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
125 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
126 |
lemma option_map_transfer [transfer_rule]: |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
127 |
"((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map" |
47635
ebb79474262c
rename 'correspondence' method to 'transfer_prover'
huffman
parents:
47634
diff
changeset
|
128 |
unfolding Option.map_def by transfer_prover |
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
129 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
130 |
lemma option_bind_transfer [transfer_rule]: |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
131 |
"(option_rel A ===> (A ===> option_rel B) ===> option_rel B) |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
132 |
Option.bind Option.bind" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
133 |
unfolding fun_rel_def split_option_all by simp |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
134 |
|
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
135 |
subsection {* Setup for lifting package *} |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
136 |
|
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47635
diff
changeset
|
137 |
lemma Quotient_option[quot_map]: |
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
138 |
assumes "Quotient R Abs Rep T" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
139 |
shows "Quotient (option_rel R) (Option.map Abs) |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
140 |
(Option.map Rep) (option_rel T)" |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
141 |
using assms unfolding Quotient_alt_def option_rel_unfold |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
142 |
by (simp split: option.split) |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
143 |
|
47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
144 |
lemma option_invariant_commute [invariant_commute]: |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
145 |
"option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)" |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
146 |
apply (simp add: fun_eq_iff Lifting.invariant_def) |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
147 |
apply (intro allI) |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
148 |
apply (case_tac x rule: option.exhaust) |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
149 |
apply (case_tac xa rule: option.exhaust) |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
150 |
apply auto[2] |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
151 |
apply (case_tac xa rule: option.exhaust) |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
152 |
apply auto |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
153 |
done |
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47624
diff
changeset
|
154 |
|
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
155 |
subsection {* Rules for quotient package *} |
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
156 |
|
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
157 |
lemma option_quotient [quot_thm]: |
47308 | 158 |
assumes "Quotient3 R Abs Rep" |
159 |
shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" |
|
160 |
apply (rule Quotient3I) |
|
161 |
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]) |
|
162 |
using Quotient3_rel [OF assms] |
|
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
163 |
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
|
164 |
done |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
165 |
|
47308 | 166 |
declare [[mapQ3 option = (option_rel, option_quotient)]] |
47094 | 167 |
|
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
168 |
lemma option_None_rsp [quot_respect]: |
47308 | 169 |
assumes q: "Quotient3 R Abs Rep" |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
170 |
shows "option_rel R None None" |
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
171 |
by (rule None_transfer) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
172 |
|
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
173 |
lemma option_Some_rsp [quot_respect]: |
47308 | 174 |
assumes q: "Quotient3 R Abs Rep" |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
175 |
shows "(R ===> option_rel R) Some Some" |
47624
16d433895d2e
add new transfer rules and setup for lifting package
huffman
parents:
47455
diff
changeset
|
176 |
by (rule Some_transfer) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
177 |
|
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
178 |
lemma option_None_prs [quot_preserve]: |
47308 | 179 |
assumes q: "Quotient3 R Abs Rep" |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
180 |
shows "Option.map Abs None = None" |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
181 |
by simp |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
182 |
|
40820
fd9c98ead9a9
more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents:
40542
diff
changeset
|
183 |
lemma option_Some_prs [quot_preserve]: |
47308 | 184 |
assumes q: "Quotient3 R Abs Rep" |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
185 |
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
|
186 |
apply(simp add: fun_eq_iff) |
47308 | 187 |
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
|
188 |
done |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
189 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
190 |
end |