author  blanchet 
Mon, 20 Jan 2014 23:43:42 +0100  
changeset 55090  9475b16e520b 
parent 55089  181751ad852f 
child 55129  26bd1cba3ab5 
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 
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 option 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_Option 
55090
9475b16e520b
technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'
blanchet
parents:
55089
diff
changeset

8 
imports Lifting Partial_Function 
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 

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

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

14 
option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

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

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

18 
 _ \<Rightarrow> False)" 
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 
lemma option_rel_simps[simp]: 
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

21 
"option_rel R None None = True" 
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

22 
"option_rel R (Some x) None = False" 
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

23 
"option_rel R None (Some y) = False" 
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

24 
"option_rel R (Some x) (Some y) = R x y" 
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

25 
unfolding option_rel_def by simp_all 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

26 

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

27 
abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where 
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

28 
"option_pred \<equiv> option_case True" 
53012
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 option_rel_eq [relator_eq]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

31 
"option_rel (op =) = (op =)" 
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

32 
by (simp add: option_rel_def fun_eq_iff split: option.split) 
53012
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 option_rel_mono[relator_mono]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

35 
assumes "A \<le> B" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

36 
shows "(option_rel A) \<le> (option_rel B)" 
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

37 
using assms by (auto simp: option_rel_def split: option.splits) 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

38 

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

39 
lemma option_rel_OO[relator_distr]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

40 
"(option_rel A) OO (option_rel B) = option_rel (A OO B)" 
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

41 
by (rule ext)+ (auto simp: option_rel_def OO_def split: option.split) 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

42 

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

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

44 
assumes "Domainp A = P" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

45 
shows "Domainp (option_rel A) = (option_pred P)" 
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

46 
using assms unfolding Domainp_iff[abs_def] option_rel_def[abs_def] 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

48 

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

49 
lemma reflp_option_rel[reflexivity_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

50 
"reflp R \<Longrightarrow> reflp (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

52 

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

53 
lemma left_total_option_rel[reflexivity_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

54 
"left_total R \<Longrightarrow> left_total (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

55 
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

56 

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

57 
lemma left_unique_option_rel [reflexivity_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

58 
"left_unique R \<Longrightarrow> left_unique (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

60 

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

61 
lemma right_total_option_rel [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

62 
"right_total R \<Longrightarrow> right_total (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

63 
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

64 

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

65 
lemma right_unique_option_rel [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

66 
"right_unique R \<Longrightarrow> right_unique (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

68 

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

69 
lemma bi_total_option_rel [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

70 
"bi_total R \<Longrightarrow> bi_total (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

71 
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

72 

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

73 
lemma bi_unique_option_rel [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

74 
"bi_unique R \<Longrightarrow> bi_unique (option_rel R)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

75 
unfolding bi_unique_def split_option_all by simp 
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 option_invariant_commute [invariant_commute]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

78 
"option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

79 
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

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_option[quot_map]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

84 
assumes "Quotient R Abs Rep T" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

85 
shows "Quotient (option_rel R) (Option.map Abs) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

86 
(Option.map Rep) (option_rel T)" 
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

87 
using assms unfolding Quotient_alt_def option_rel_def 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

88 
by (simp split: option.split) 
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 None_transfer [transfer_rule]: "(option_rel A) None None" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

97 
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 Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

100 
unfolding fun_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 option_case_transfer [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

103 
"(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

105 

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

106 
lemma option_map_transfer [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

107 
"((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map" 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

108 
unfolding Option.map_def by transfer_prover 
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 
lemma option_bind_transfer [transfer_rule]: 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

111 
"(option_rel A ===> (A ===> option_rel B) ===> option_rel B) 
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
diff
changeset

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

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

114 

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

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

116 

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

117 
end 