src/HOL/Lifting_Option.thy
changeset 56092 1ba075db8fe4
parent 55945 e96383acecf9
child 56518 beb3b6851665
     1.1 --- a/src/HOL/Lifting_Option.thy	Thu Mar 13 13:18:14 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Option.thy	Thu Mar 13 13:18:14 2014 +0100
     1.3 @@ -17,8 +17,8 @@
     1.4      | _ \<Rightarrow> False)"
     1.5  by (auto split: prod.split option.split)
     1.6  
     1.7 -abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
     1.8 -  "option_pred \<equiv> case_option True"
     1.9 +abbreviation (input) pred_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
    1.10 +  "pred_option \<equiv> case_option True"
    1.11  
    1.12  lemma rel_option_eq [relator_eq]:
    1.13    "rel_option (op =) = (op =)"
    1.14 @@ -35,7 +35,7 @@
    1.15  
    1.16  lemma Domainp_option[relator_domain]:
    1.17    assumes "Domainp A = P"
    1.18 -  shows "Domainp (rel_option A) = (option_pred P)"
    1.19 +  shows "Domainp (rel_option A) = (pred_option P)"
    1.20  using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
    1.21  by (auto iff: fun_eq_iff split: option.split)
    1.22  
    1.23 @@ -64,7 +64,7 @@
    1.24    unfolding bi_unique_def split_option_all by simp
    1.25  
    1.26  lemma option_invariant_commute [invariant_commute]:
    1.27 -  "rel_option (Lifting.invariant P) = Lifting.invariant (option_pred P)"
    1.28 +  "rel_option (Lifting.invariant P) = Lifting.invariant (pred_option P)"
    1.29    by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all)
    1.30  
    1.31  subsection {* Quotient theorem for the Lifting package *}