src/HOL/Lifting_Product.thy
author haftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 58410 6d46ad54a2ab
parent 56526 58ac520db7ae
child 58444 ed95293f14b6
permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
kuncar@53012
     1
(*  Title:      HOL/Lifting_Product.thy
kuncar@53012
     2
    Author:     Brian Huffman and Ondrej Kuncar
kuncar@53012
     3
*)
kuncar@53012
     4
kuncar@53012
     5
header {* Setup for Lifting/Transfer for the product type *}
kuncar@53012
     6
kuncar@53012
     7
theory Lifting_Product
blanchet@55083
     8
imports Lifting Basic_BNFs
kuncar@53012
     9
begin
kuncar@53012
    10
kuncar@56526
    11
(* The following lemma can be deleted when product is added to FP sugar *)
kuncar@56526
    12
lemma prod_pred_inject [simp]:
kuncar@56526
    13
  "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
kuncar@56526
    14
  unfolding pred_prod_def fun_eq_iff prod_set_simps by blast
kuncar@56526
    15
kuncar@53012
    16
subsection {* Transfer rules for the Transfer package *}
kuncar@53012
    17
kuncar@53012
    18
context
kuncar@53012
    19
begin
kuncar@53012
    20
interpretation lifting_syntax .
kuncar@53012
    21
blanchet@55944
    22
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
blanchet@55945
    23
  unfolding rel_fun_def rel_prod_def by simp
kuncar@53012
    24
blanchet@55944
    25
lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
blanchet@55945
    26
  unfolding rel_fun_def rel_prod_def by simp
kuncar@53012
    27
blanchet@55944
    28
lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
blanchet@55945
    29
  unfolding rel_fun_def rel_prod_def by simp
kuncar@53012
    30
blanchet@55414
    31
lemma case_prod_transfer [transfer_rule]:
blanchet@55944
    32
  "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
blanchet@55945
    33
  unfolding rel_fun_def rel_prod_def by simp
kuncar@53012
    34
kuncar@53012
    35
lemma curry_transfer [transfer_rule]:
blanchet@55944
    36
  "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
kuncar@53012
    37
  unfolding curry_def by transfer_prover
kuncar@53012
    38
blanchet@55932
    39
lemma map_prod_transfer [transfer_rule]:
blanchet@55944
    40
  "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D)
blanchet@55932
    41
    map_prod map_prod"
blanchet@55932
    42
  unfolding map_prod_def [abs_def] by transfer_prover
kuncar@53012
    43
blanchet@55944
    44
lemma rel_prod_transfer [transfer_rule]:
kuncar@53012
    45
  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
blanchet@55944
    46
    rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
blanchet@55945
    47
  unfolding rel_fun_def by auto
kuncar@53012
    48
kuncar@53012
    49
end
kuncar@53012
    50
kuncar@53012
    51
end