src/HOL/Library/Quotient_Option.thy
author wenzelm
Mon, 11 Apr 2016 15:26:58 +0200
changeset 62954 c5d0fdc260fa
parent 60500 903bb1495239
permissions -rw-r--r--
tuned imports;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47455
26315a545e26 updated headers;
wenzelm
parents: 47308
diff changeset
     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
f1deaca15ca3 observe standard header format;
wenzelm
parents: 35222
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58916
diff changeset
     5
section \<open>Quotient infrastructure for the option type\<close>
35788
f1deaca15ca3 observe standard header format;
wenzelm
parents: 35222
diff changeset
     6
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
theory Quotient_Option
62954
c5d0fdc260fa tuned imports;
wenzelm
parents: 60500
diff changeset
     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
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58916
diff changeset
    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
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    13
lemma rel_option_map1:
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    14
  "rel_option R (map_option f x) y \<longleftrightarrow> rel_option (\<lambda>x. R (f x)) x y"
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    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
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    17
lemma rel_option_map2:
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    18
  "rel_option R x (map_option f y) \<longleftrightarrow> rel_option (\<lambda>x y. R x (f y)) x y"
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    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
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 53026
diff changeset
    21
declare
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 53026
diff changeset
    22
  map_option.id [id_simps]
56525
b5b6ad5dc2ae simplify and fix theories thanks to 356a5efdb278
kuncar
parents: 55564
diff changeset
    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
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    30
  "symp R \<Longrightarrow> symp (rel_option R)"
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    31
  unfolding symp_def split_option_all
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    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
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    35
  "transp R \<Longrightarrow> transp (rel_option R)"
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    36
  unfolding transp_def split_option_all
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    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
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    40
  "equivp R \<Longrightarrow> equivp (rel_option R)"
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    44
  assumes "Quotient3 R Abs Rep"
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    45
  shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    46
  apply (rule Quotient3I)
56525
b5b6ad5dc2ae simplify and fix theories thanks to 356a5efdb278
kuncar
parents: 55564
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    48
  using Quotient3_rel [OF assms]
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    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
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    52
declare [[mapQ3 option = (rel_option, option_quotient)]]
47094
1a7ad2601cb5 store the relational theorem for every relator
kuncar
parents: 45802
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    55
  assumes q: "Quotient3 R Abs Rep"
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    56
  shows "rel_option R None None"
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58881
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    60
  assumes q: "Quotient3 R Abs Rep"
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    61
  shows "(R ===> rel_option R) Some Some"
58916
229765cc3414 more complete fp_sugars for sum and prod;
traytel
parents: 58881
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    65
  assumes q: "Quotient3 R Abs Rep"
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 53026
diff changeset
    66
  shows "map_option Abs None = None"
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    70
  assumes q: "Quotient3 R Abs Rep"
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 53026
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    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