src/HOL/Lifting_Product.thy
author kuncar
Thu, 10 Apr 2014 17:48:32 +0200
changeset 56525 b5b6ad5dc2ae
parent 56520 3373f5d1e074
child 56526 58ac520db7ae
permissions -rw-r--r--
simplify and fix theories thanks to 356a5efdb278
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_Product.thy
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     2
    Author:     Brian Huffman and Ondrej Kuncar
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     3
*)
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
header {* Setup for Lifting/Transfer for the product type *}
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     6
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     7
theory Lifting_Product
55083
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 53012
diff changeset
     8
imports Lifting Basic_BNFs
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
     9
begin
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    10
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    11
subsection {* Transfer rules for the Transfer package *}
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    12
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    13
context
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    14
begin
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    15
interpretation lifting_syntax .
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    16
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    17
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55944
diff changeset
    18
  unfolding rel_fun_def rel_prod_def by simp
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    19
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    20
lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55944
diff changeset
    21
  unfolding rel_fun_def rel_prod_def by simp
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    22
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    23
lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55944
diff changeset
    24
  unfolding rel_fun_def rel_prod_def by simp
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    25
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55085
diff changeset
    26
lemma case_prod_transfer [transfer_rule]:
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    27
  "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55944
diff changeset
    28
  unfolding rel_fun_def rel_prod_def by simp
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    29
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    30
lemma curry_transfer [transfer_rule]:
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    31
  "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    32
  unfolding curry_def by transfer_prover
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    33
55932
68c5104d2204 renamed 'map_pair' to 'map_prod'
blanchet
parents: 55564
diff changeset
    34
lemma map_prod_transfer [transfer_rule]:
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    35
  "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D)
55932
68c5104d2204 renamed 'map_pair' to 'map_prod'
blanchet
parents: 55564
diff changeset
    36
    map_prod map_prod"
68c5104d2204 renamed 'map_pair' to 'map_prod'
blanchet
parents: 55564
diff changeset
    37
  unfolding map_prod_def [abs_def] by transfer_prover
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    38
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    39
lemma rel_prod_transfer [transfer_rule]:
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    40
  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    41
    rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55944
diff changeset
    42
  unfolding rel_fun_def by auto
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    43
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    44
end
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    45
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    46
end