src/HOL/Lifting_Product.thy
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55415 05f5fdb8d093
parent 55414 eab03e9cee8a
child 55564 e81ee43ab290
permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
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@53012
    11
subsection {* Relator and predicator properties *}
kuncar@53012
    12
kuncar@53012
    13
definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
kuncar@53012
    14
where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
kuncar@53012
    15
kuncar@53012
    16
lemma prod_pred_apply [simp]:
kuncar@53012
    17
  "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
kuncar@53012
    18
  by (simp add: prod_pred_def)
kuncar@53012
    19
blanchet@55085
    20
lemmas prod_rel_eq[relator_eq] = prod.rel_eq
blanchet@55085
    21
lemmas prod_rel_mono[relator_mono] = prod.rel_mono
kuncar@53012
    22
kuncar@53012
    23
lemma prod_rel_OO[relator_distr]:
kuncar@53012
    24
  "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
kuncar@53012
    25
by (rule ext)+ (auto simp: prod_rel_def OO_def)
kuncar@53012
    26
kuncar@53012
    27
lemma Domainp_prod[relator_domain]:
kuncar@53012
    28
  assumes "Domainp T1 = P1"
kuncar@53012
    29
  assumes "Domainp T2 = P2"
kuncar@53012
    30
  shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
kuncar@53012
    31
using assms unfolding prod_rel_def prod_pred_def by blast
kuncar@53012
    32
kuncar@53012
    33
lemma reflp_prod_rel [reflexivity_rule]:
kuncar@53012
    34
  assumes "reflp R1"
kuncar@53012
    35
  assumes "reflp R2"
kuncar@53012
    36
  shows "reflp (prod_rel R1 R2)"
kuncar@53012
    37
using assms by (auto intro!: reflpI elim: reflpE)
kuncar@53012
    38
kuncar@53012
    39
lemma left_total_prod_rel [reflexivity_rule]:
kuncar@53012
    40
  assumes "left_total R1"
kuncar@53012
    41
  assumes "left_total R2"
kuncar@53012
    42
  shows "left_total (prod_rel R1 R2)"
kuncar@53012
    43
  using assms unfolding left_total_def prod_rel_def by auto
kuncar@53012
    44
kuncar@53012
    45
lemma left_unique_prod_rel [reflexivity_rule]:
kuncar@53012
    46
  assumes "left_unique R1" and "left_unique R2"
kuncar@53012
    47
  shows "left_unique (prod_rel R1 R2)"
kuncar@53012
    48
  using assms unfolding left_unique_def prod_rel_def by auto
kuncar@53012
    49
kuncar@53012
    50
lemma right_total_prod_rel [transfer_rule]:
kuncar@53012
    51
  assumes "right_total R1" and "right_total R2"
kuncar@53012
    52
  shows "right_total (prod_rel R1 R2)"
kuncar@53012
    53
  using assms unfolding right_total_def prod_rel_def by auto
kuncar@53012
    54
kuncar@53012
    55
lemma right_unique_prod_rel [transfer_rule]:
kuncar@53012
    56
  assumes "right_unique R1" and "right_unique R2"
kuncar@53012
    57
  shows "right_unique (prod_rel R1 R2)"
kuncar@53012
    58
  using assms unfolding right_unique_def prod_rel_def by auto
kuncar@53012
    59
kuncar@53012
    60
lemma bi_total_prod_rel [transfer_rule]:
kuncar@53012
    61
  assumes "bi_total R1" and "bi_total R2"
kuncar@53012
    62
  shows "bi_total (prod_rel R1 R2)"
kuncar@53012
    63
  using assms unfolding bi_total_def prod_rel_def by auto
kuncar@53012
    64
kuncar@53012
    65
lemma bi_unique_prod_rel [transfer_rule]:
kuncar@53012
    66
  assumes "bi_unique R1" and "bi_unique R2"
kuncar@53012
    67
  shows "bi_unique (prod_rel R1 R2)"
kuncar@53012
    68
  using assms unfolding bi_unique_def prod_rel_def by auto
kuncar@53012
    69
kuncar@53012
    70
lemma prod_invariant_commute [invariant_commute]: 
kuncar@53012
    71
  "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
kuncar@53012
    72
  by (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) blast
kuncar@53012
    73
kuncar@53012
    74
subsection {* Quotient theorem for the Lifting package *}
kuncar@53012
    75
kuncar@53012
    76
lemma Quotient_prod[quot_map]:
kuncar@53012
    77
  assumes "Quotient R1 Abs1 Rep1 T1"
kuncar@53012
    78
  assumes "Quotient R2 Abs2 Rep2 T2"
kuncar@53012
    79
  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
kuncar@53012
    80
    (map_pair Rep1 Rep2) (prod_rel T1 T2)"
kuncar@53012
    81
  using assms unfolding Quotient_alt_def by auto
kuncar@53012
    82
kuncar@53012
    83
subsection {* Transfer rules for the Transfer package *}
kuncar@53012
    84
kuncar@53012
    85
context
kuncar@53012
    86
begin
kuncar@53012
    87
interpretation lifting_syntax .
kuncar@53012
    88
kuncar@53012
    89
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
kuncar@53012
    90
  unfolding fun_rel_def prod_rel_def by simp
kuncar@53012
    91
kuncar@53012
    92
lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst"
kuncar@53012
    93
  unfolding fun_rel_def prod_rel_def by simp
kuncar@53012
    94
kuncar@53012
    95
lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
kuncar@53012
    96
  unfolding fun_rel_def prod_rel_def by simp
kuncar@53012
    97
blanchet@55414
    98
lemma case_prod_transfer [transfer_rule]:
blanchet@55414
    99
  "((A ===> B ===> C) ===> prod_rel A B ===> C) case_prod case_prod"
kuncar@53012
   100
  unfolding fun_rel_def prod_rel_def by simp
kuncar@53012
   101
kuncar@53012
   102
lemma curry_transfer [transfer_rule]:
kuncar@53012
   103
  "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
kuncar@53012
   104
  unfolding curry_def by transfer_prover
kuncar@53012
   105
kuncar@53012
   106
lemma map_pair_transfer [transfer_rule]:
kuncar@53012
   107
  "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
kuncar@53012
   108
    map_pair map_pair"
kuncar@53012
   109
  unfolding map_pair_def [abs_def] by transfer_prover
kuncar@53012
   110
kuncar@53012
   111
lemma prod_rel_transfer [transfer_rule]:
kuncar@53012
   112
  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
kuncar@53012
   113
    prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel"
kuncar@53012
   114
  unfolding fun_rel_def by auto
kuncar@53012
   115
kuncar@53012
   116
end
kuncar@53012
   117
kuncar@53012
   118
end
kuncar@53012
   119