src/HOL/Library/Quotient_Option.thy
author traytel
Tue, 13 Aug 2013 18:22:55 +0200
changeset 53026 e1a548c11845
parent 53012 cb82606b8215
child 55466 786edc984c98
permissions -rw-r--r--
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
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
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
82cc2aeb7d13 stronger reflexivity prover
kuncar
parents: 51956
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    42
  assumes "Quotient3 R Abs Rep"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    43
  shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    44
  apply (rule Quotient3I)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    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])
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    50
declare [[mapQ3 option = (option_rel, option_quotient)]]
47094
1a7ad2601cb5 store the relational theorem for every relator
kuncar
parents: 45802
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    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
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47094
diff changeset
    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