src/HOL/Lifting_Product.thy
author kuncar
Thu, 10 Apr 2014 17:48:33 +0200
changeset 56526 58ac520db7ae
parent 56525 b5b6ad5dc2ae
child 58444 ed95293f14b6
permissions -rw-r--r--
add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons
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
56526
58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons
kuncar
parents: 56525
diff changeset
    11
(* The following lemma can be deleted when product is added to FP sugar *)
58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons
kuncar
parents: 56525
diff changeset
    12
lemma prod_pred_inject [simp]:
58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons
kuncar
parents: 56525
diff changeset
    13
  "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons
kuncar
parents: 56525
diff changeset
    14
  unfolding pred_prod_def fun_eq_iff prod_set_simps by blast
58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons
kuncar
parents: 56525
diff changeset
    15
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    16
subsection {* Transfer rules for the Transfer package *}
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    17
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    18
context
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    19
begin
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    20
interpretation lifting_syntax .
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    21
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    22
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
    23
  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
    24
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    25
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
    26
  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
    27
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    28
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
    29
  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
    30
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55085
diff changeset
    31
lemma case_prod_transfer [transfer_rule]:
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    32
  "((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
    33
  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
    34
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    35
lemma curry_transfer [transfer_rule]:
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    36
  "((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
    37
  unfolding curry_def by transfer_prover
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    38
55932
68c5104d2204 renamed 'map_pair' to 'map_prod'
blanchet
parents: 55564
diff changeset
    39
lemma map_prod_transfer [transfer_rule]:
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    40
  "((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
    41
    map_prod map_prod"
68c5104d2204 renamed 'map_pair' to 'map_prod'
blanchet
parents: 55564
diff changeset
    42
  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
    43
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    44
lemma rel_prod_transfer [transfer_rule]:
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    45
  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
55944
7ab8f003fe41 renamed 'prod_rel' to 'rel_prod'
blanchet
parents: 55932
diff changeset
    46
    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
    47
  unfolding rel_fun_def by auto
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    48
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    49
end
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    50
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    51
end