author  blanchet 
Sun, 16 Feb 2014 21:33:28 +0100  
changeset 55525  70b7e91fa1f9 
parent 55466  786edc984c98 
child 55564  e81ee43ab290 
permissions  rwrr 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

1 
(* Title: HOL/Lifting_Option.thy 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

2 
Author: Brian Huffman and Ondrej Kuncar 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55090
diff
changeset

3 
Author: Andreas Lochbihler, Karlsruhe Institute of Technology 
53012
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 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

6 
header {* Setup for Lifting/Transfer for the option type *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

7 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

8 
theory Lifting_Option 
55090
9475b16e520b
technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'
blanchet
parents:
55089
diff
changeset

9 
imports Lifting Partial_Function 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

10 
begin 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

11 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

12 
subsection {* Relator and predicator properties *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

13 

55525  14 
lemma rel_option_iff: 
15 
"rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

16 
 (Some x, Some y) \<Rightarrow> R x y 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

17 
 _ \<Rightarrow> False)" 
55525  18 
by (auto split: prod.split option.split) 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

19 

53026
e1a548c11845
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
traytel
parents:
53012
diff
changeset

20 
abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where 
55404
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55129
diff
changeset

21 
"option_pred \<equiv> case_option True" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

22 

55525  23 
lemma rel_option_eq [relator_eq]: 
24 
"rel_option (op =) = (op =)" 

25 
by (simp add: rel_option_iff fun_eq_iff split: option.split) 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

26 

55525  27 
lemma rel_option_mono[relator_mono]: 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

28 
assumes "A \<le> B" 
55525  29 
shows "(rel_option A) \<le> (rel_option B)" 
30 
using assms by (auto simp: rel_option_iff split: option.splits) 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

31 

55525  32 
lemma rel_option_OO[relator_distr]: 
33 
"(rel_option A) OO (rel_option B) = rel_option (A OO B)" 

34 
by (rule ext)+ (auto simp: rel_option_iff OO_def split: option.split) 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

35 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

36 
lemma Domainp_option[relator_domain]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

37 
assumes "Domainp A = P" 
55525  38 
shows "Domainp (rel_option A) = (option_pred P)" 
39 
using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def] 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

40 
by (auto iff: fun_eq_iff split: option.split) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

41 

55525  42 
lemma reflp_rel_option[reflexivity_rule]: 
43 
"reflp R \<Longrightarrow> reflp (rel_option R)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

44 
unfolding reflp_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

45 

55525  46 
lemma left_total_rel_option[reflexivity_rule]: 
47 
"left_total R \<Longrightarrow> left_total (rel_option R)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

48 
unfolding left_total_def split_option_all split_option_ex by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

49 

55525  50 
lemma left_unique_rel_option [reflexivity_rule]: 
51 
"left_unique R \<Longrightarrow> left_unique (rel_option R)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

52 
unfolding left_unique_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

53 

55525  54 
lemma right_total_rel_option [transfer_rule]: 
55 
"right_total R \<Longrightarrow> right_total (rel_option R)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

56 
unfolding right_total_def split_option_all split_option_ex by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

57 

55525  58 
lemma right_unique_rel_option [transfer_rule]: 
59 
"right_unique R \<Longrightarrow> right_unique (rel_option R)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

60 
unfolding right_unique_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

61 

55525  62 
lemma bi_total_rel_option [transfer_rule]: 
63 
"bi_total R \<Longrightarrow> bi_total (rel_option R)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

64 
unfolding bi_total_def split_option_all split_option_ex by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

65 

55525  66 
lemma bi_unique_rel_option [transfer_rule]: 
67 
"bi_unique R \<Longrightarrow> bi_unique (rel_option R)" 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

68 
unfolding bi_unique_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

69 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

70 
lemma option_invariant_commute [invariant_commute]: 
55525  71 
"rel_option (Lifting.invariant P) = Lifting.invariant (option_pred P)" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

72 
by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

73 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

74 
subsection {* Quotient theorem for the Lifting package *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

75 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

76 
lemma Quotient_option[quot_map]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

77 
assumes "Quotient R Abs Rep T" 
55525  78 
shows "Quotient (rel_option R) (map_option Abs) 
79 
(map_option Rep) (rel_option T)" 

80 
using assms unfolding Quotient_alt_def rel_option_iff 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

81 
by (simp split: option.split) 
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 
subsection {* Transfer rules for the Transfer package *} 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

84 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

85 
context 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

86 
begin 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

87 
interpretation lifting_syntax . 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

88 

55525  89 
lemma None_transfer [transfer_rule]: "(rel_option A) None None" 
90 
by (rule option.rel_inject) 

53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

91 

55525  92 
lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

93 
unfolding fun_rel_def by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

94 

55404
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55129
diff
changeset

95 
lemma case_option_transfer [transfer_rule]: 
55525  96 
"(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option" 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

97 
unfolding fun_rel_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

98 

55466  99 
lemma map_option_transfer [transfer_rule]: 
55525  100 
"((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option" 
55466  101 
unfolding map_option_case[abs_def] by transfer_prover 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

102 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

103 
lemma option_bind_transfer [transfer_rule]: 
55525  104 
"(rel_option A ===> (A ===> rel_option B) ===> rel_option B) 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

105 
Option.bind Option.bind" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

106 
unfolding fun_rel_def split_option_all by simp 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

107 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

108 
end 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

109 

cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

110 
end 