src/HOL/Library/Quotient_Option.thy
author blanchet
Sun, 16 Feb 2014 21:33:28 +0100
changeset 55525 70b7e91fa1f9
parent 55466 786edc984c98
child 55564 e81ee43ab290
permissions -rw-r--r--
folded 'rel_option' into 'option_rel'
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
f1deaca15ca3 observe standard header format;
wenzelm
parents: 35222
diff changeset
     5
header {* Quotient infrastructure for the option type *}
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
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
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]
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    23
  rel_option_eq [id_simps]
40820
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents: 40542
diff changeset
    24
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents: 40542
diff changeset
    25
lemma option_symp:
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    26
  "symp R \<Longrightarrow> symp (rel_option R)"
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    27
  unfolding symp_def split_option_all
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    28
  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
    29
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents: 40542
diff changeset
    30
lemma option_transp:
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    31
  "transp R \<Longrightarrow> transp (rel_option R)"
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    32
  unfolding transp_def split_option_all
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    33
  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
    34
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents: 40542
diff changeset
    35
lemma option_equivp [quot_equiv]:
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    36
  "equivp R \<Longrightarrow> equivp (rel_option R)"
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    37
  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
    38
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents: 40542
diff changeset
    39
lemma option_quotient [quot_thm]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    40
  assumes "Quotient3 R Abs Rep"
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    41
  shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    42
  apply (rule Quotient3I)
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    43
  apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] rel_option_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
    44
  using Quotient3_rel [OF assms]
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    45
  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
    46
  done
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    47
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    48
declare [[mapQ3 option = (rel_option, option_quotient)]]
47094
1a7ad2601cb5 store the relational theorem for every relator
kuncar
parents: 45802
diff changeset
    49
40820
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents: 40542
diff changeset
    50
lemma option_None_rsp [quot_respect]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    51
  assumes q: "Quotient3 R Abs Rep"
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    52
  shows "rel_option R None None"
47624
16d433895d2e add new transfer rules and setup for lifting package
huffman
parents: 47455
diff changeset
    53
  by (rule None_transfer)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    54
40820
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents: 40542
diff changeset
    55
lemma option_Some_rsp [quot_respect]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    56
  assumes q: "Quotient3 R Abs Rep"
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    57
  shows "(R ===> rel_option R) Some Some"
47624
16d433895d2e add new transfer rules and setup for lifting package
huffman
parents: 47455
diff changeset
    58
  by (rule Some_transfer)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    59
40820
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents: 40542
diff changeset
    60
lemma option_None_prs [quot_preserve]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    61
  assumes q: "Quotient3 R Abs Rep"
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 53026
diff changeset
    62
  shows "map_option Abs None = None"
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    63
  by (rule Option.option.map(1))
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    64
40820
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules
haftmann
parents: 40542
diff changeset
    65
lemma option_Some_prs [quot_preserve]:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    66
  assumes q: "Quotient3 R Abs Rep"
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 53026
diff changeset
    67
  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
    68
  apply(simp add: fun_eq_iff)
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    69
  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
    70
  done
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
end