src/HOL/Lifting_Sum.thy
author kuncar
Thu, 10 Apr 2014 17:48:33 +0200
changeset 56526 58ac520db7ae
parent 56525 b5b6ad5dc2ae
child 58889 5b7a9633cfa8
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_Sum.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 sum 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_Sum
55083
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 53026
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 sum 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 sum_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_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a"
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_sum_def fun_eq_iff sum_set_simps by auto
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
55943
5c2df04e97d1 renamed 'sum_rel' to 'rel_sum'
blanchet
parents: 55931
diff changeset
    22
lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55943
diff changeset
    23
  unfolding rel_fun_def by simp
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    24
55943
5c2df04e97d1 renamed 'sum_rel' to 'rel_sum'
blanchet
parents: 55931
diff changeset
    25
lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55943
diff changeset
    26
  unfolding rel_fun_def by simp
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    27
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55084
diff changeset
    28
lemma case_sum_transfer [transfer_rule]:
55943
5c2df04e97d1 renamed 'sum_rel' to 'rel_sum'
blanchet
parents: 55931
diff changeset
    29
  "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55943
diff changeset
    30
  unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
53012
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    31
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff changeset
    32
end
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
end