src/HOL/Lifting_Option.thy
changeset 56525 b5b6ad5dc2ae
parent 56520 3373f5d1e074
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:18 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:32 2014 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Setup for Lifting/Transfer for the option type *}
     1.5  
     1.6  theory Lifting_Option
     1.7 -imports Lifting Partial_Function
     1.8 +imports Lifting Option
     1.9  begin
    1.10  
    1.11  subsection {* Relator and predicator properties *}
    1.12 @@ -17,64 +17,6 @@
    1.13      | _ \<Rightarrow> False)"
    1.14  by (auto split: prod.split option.split)
    1.15  
    1.16 -abbreviation (input) pred_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
    1.17 -  "pred_option \<equiv> case_option True"
    1.18 -
    1.19 -lemma rel_option_eq [relator_eq]:
    1.20 -  "rel_option (op =) = (op =)"
    1.21 -  by (simp add: rel_option_iff fun_eq_iff split: option.split)
    1.22 -
    1.23 -lemma rel_option_mono[relator_mono]:
    1.24 -  assumes "A \<le> B"
    1.25 -  shows "(rel_option A) \<le> (rel_option B)"
    1.26 -using assms by (auto simp: rel_option_iff split: option.splits)
    1.27 -
    1.28 -lemma rel_option_OO[relator_distr]:
    1.29 -  "(rel_option A) OO (rel_option B) = rel_option (A OO B)"
    1.30 -by (rule ext)+ (auto simp: rel_option_iff OO_def split: option.split)
    1.31 -
    1.32 -lemma Domainp_option[relator_domain]: 
    1.33 -  "Domainp (rel_option A) = (pred_option (Domainp A))"
    1.34 -unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
    1.35 -by (auto iff: fun_eq_iff split: option.split)
    1.36 -
    1.37 -lemma left_total_rel_option[transfer_rule]:
    1.38 -  "left_total R \<Longrightarrow> left_total (rel_option R)"
    1.39 -  unfolding left_total_def split_option_all split_option_ex by simp
    1.40 -
    1.41 -lemma left_unique_rel_option [transfer_rule]:
    1.42 -  "left_unique R \<Longrightarrow> left_unique (rel_option R)"
    1.43 -  unfolding left_unique_def split_option_all by simp
    1.44 -
    1.45 -lemma right_total_rel_option [transfer_rule]:
    1.46 -  "right_total R \<Longrightarrow> right_total (rel_option R)"
    1.47 -  unfolding right_total_def split_option_all split_option_ex by simp
    1.48 -
    1.49 -lemma right_unique_rel_option [transfer_rule]:
    1.50 -  "right_unique R \<Longrightarrow> right_unique (rel_option R)"
    1.51 -  unfolding right_unique_def split_option_all by simp
    1.52 -
    1.53 -lemma bi_total_rel_option [transfer_rule]:
    1.54 -  "bi_total R \<Longrightarrow> bi_total (rel_option R)"
    1.55 -  unfolding bi_total_def split_option_all split_option_ex by simp
    1.56 -
    1.57 -lemma bi_unique_rel_option [transfer_rule]:
    1.58 -  "bi_unique R \<Longrightarrow> bi_unique (rel_option R)"
    1.59 -  unfolding bi_unique_def split_option_all by simp
    1.60 -
    1.61 -lemma option_relator_eq_onp [relator_eq_onp]:
    1.62 -  "rel_option (eq_onp P) = eq_onp (pred_option P)"
    1.63 -  by (auto simp add: fun_eq_iff eq_onp_def split_option_all)
    1.64 -
    1.65 -subsection {* Quotient theorem for the Lifting package *}
    1.66 -
    1.67 -lemma Quotient_option[quot_map]:
    1.68 -  assumes "Quotient R Abs Rep T"
    1.69 -  shows "Quotient (rel_option R) (map_option Abs)
    1.70 -    (map_option Rep) (rel_option T)"
    1.71 -  using assms unfolding Quotient_alt_def rel_option_iff
    1.72 -  by (simp split: option.split)
    1.73 -
    1.74  subsection {* Transfer rules for the Transfer package *}
    1.75  
    1.76  context