src/HOL/Lifting_Product.thy
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 56526 58ac520db7ae
child 58444 ed95293f14b6
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
     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 lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
    23   unfolding rel_fun_def rel_prod_def by simp
    24 
    25 lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
    26   unfolding rel_fun_def rel_prod_def by simp
    27 
    28 lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
    29   unfolding rel_fun_def rel_prod_def by simp
    30 
    31 lemma case_prod_transfer [transfer_rule]:
    32   "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
    33   unfolding rel_fun_def rel_prod_def by simp
    34 
    35 lemma curry_transfer [transfer_rule]:
    36   "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
    37   unfolding curry_def by transfer_prover
    38 
    39 lemma map_prod_transfer [transfer_rule]:
    40   "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D)
    41     map_prod map_prod"
    42   unfolding map_prod_def [abs_def] by transfer_prover
    43 
    44 lemma rel_prod_transfer [transfer_rule]:
    45   "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
    46     rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
    47   unfolding rel_fun_def by auto
    48 
    49 end
    50 
    51 end