src/HOL/Lifting_Option.thy
author wenzelm
Sun, 02 Nov 2014 18:21:45 +0100
changeset 58889 5b7a9633cfa8
parent 56525 b5b6ad5dc2ae
permissions -rw-r--r--
modernized header uniformly as section;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     1
(*  Title:      HOL/Lifting_Option.thy
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     2
    Author:     Brian Huffman and Ondrej Kuncar
55129
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55090
diff changeset
     3
    Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     4
*)
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     5
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 56525
diff changeset
     6
section {* Setup for Lifting/Transfer for the option type *}
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     7
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     8
theory Lifting_Option
56525
b5b6ad5dc2ae simplify and fix theories thanks to 356a5efdb278
kuncar
parents: 56520
diff changeset
     9
imports Lifting Option
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    10
begin
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    11
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    12
subsection {* Relator and predicator properties *}
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    13
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    14
lemma rel_option_iff:
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    15
  "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    16
    | (Some x, Some y) \<Rightarrow> R x y
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    17
    | _ \<Rightarrow> False)"
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    18
by (auto split: prod.split option.split)
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    19
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    20
subsection {* Transfer rules for the Transfer package *}
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    21
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    22
context
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    23
begin
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    24
interpretation lifting_syntax .
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    25
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    26
lemma None_transfer [transfer_rule]: "(rel_option A) None None"
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    27
  by (rule option.rel_inject)
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    28
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    29
lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55564
diff changeset
    30
  unfolding rel_fun_def by simp
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    31
55404
5cb95b79a51f transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
blanchet
parents: 55129
diff changeset
    32
lemma case_option_transfer [transfer_rule]:
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    33
  "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55564
diff changeset
    34
  unfolding rel_fun_def split_option_all by simp
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    35
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55404
diff changeset
    36
lemma map_option_transfer [transfer_rule]:
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    37
  "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55404
diff changeset
    38
  unfolding map_option_case[abs_def] by transfer_prover
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    39
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    40
lemma option_bind_transfer [transfer_rule]:
55525
70b7e91fa1f9 folded 'rel_option' into 'option_rel'
blanchet
parents: 55466
diff changeset
    41
  "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    42
    Option.bind Option.bind"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55564
diff changeset
    43
  unfolding rel_fun_def split_option_all by simp
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    44
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    45
end
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    46
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    47
end