author  kuncar 
Thu, 10 Apr 2014 17:48:33 +0200  
changeset 56526  58ac520db7ae 
parent 56525  b5b6ad5dc2ae 
child 58889  5b7a9633cfa8 
permissions  rwrr 
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  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  22 
lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl" 
55945  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  25 
lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr" 
55945  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  29 
"((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum" 
55945  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 