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 *}
```