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