src/HOL/Lifting_Product.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58448 a1d4e7473c98
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Lifting_Product.thy
     2     Author:     Brian Huffman and Ondrej Kuncar
     3 *)
     4 
     5 header {* Setup for Lifting/Transfer for the product type *}
     6 
     7 theory Lifting_Product
     8 imports Lifting Basic_BNFs
     9 begin
    10 
    11 (* The following lemma can be deleted when product is added to FP sugar *)
    12 lemma prod_pred_inject [simp]:
    13   "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
    14   unfolding pred_prod_def fun_eq_iff prod_set_simps by blast
    15 
    16 subsection {* Transfer rules for the Transfer package *}
    17 
    18 context
    19 begin
    20 interpretation lifting_syntax .
    21 
    22 declare Pair_transfer [transfer_rule]
    23 declare fst_transfer [transfer_rule]
    24 declare snd_transfer [transfer_rule]
    25 declare case_prod_transfer [transfer_rule]
    26 
    27 lemma curry_transfer [transfer_rule]:
    28   "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
    29   unfolding curry_def by transfer_prover
    30 
    31 lemma map_prod_transfer [transfer_rule]:
    32   "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D)
    33     map_prod map_prod"
    34   unfolding map_prod_def [abs_def] by transfer_prover
    35 
    36 lemma rel_prod_transfer [transfer_rule]:
    37   "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
    38     rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
    39   unfolding rel_fun_def by auto
    40 
    41 end
    42 
    43 end