src/HOL/Library/Countable_Set_Type.thy
changeset 67399 eab6ce8368fa
parent 67006 b1278ed3cd46
child 68406 6beb45f6cf67
     1.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  lemma less_cset_transfer[transfer_rule]:
     1.5    includes lifting_syntax
     1.6    assumes [transfer_rule]: "bi_unique A"
     1.7 -  shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \<subset> op <"
     1.8 +  shows "((pcr_cset A) ===> (pcr_cset A) ===> (=)) (\<subset>) (<)"
     1.9  unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover
    1.10  
    1.11  lift_definition sup_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset"
    1.12 @@ -104,12 +104,12 @@
    1.13  abbreviation cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" where "cInt xs ys \<equiv> inf xs ys"
    1.14  abbreviation cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" where "cDiff xs ys \<equiv> minus xs ys"
    1.15  
    1.16 -lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
    1.17 +lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "(\<in>)" parametric member_transfer
    1.18    .
    1.19  lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
    1.20    by (rule countable_insert)
    1.21  abbreviation csingle :: "'a \<Rightarrow> 'a cset" where "csingle x \<equiv> cinsert x cempty"
    1.22 -lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
    1.23 +lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "(`)" parametric image_transfer
    1.24    by (rule countable_image)
    1.25  lift_definition cBall :: "'a cset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
    1.26  lift_definition cBex :: "'a cset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
    1.27 @@ -480,15 +480,15 @@
    1.28    unfolding rel_fun_def rel_cset_iff by blast
    1.29  
    1.30  lemma cBall_parametric [transfer_rule]:
    1.31 -  "(rel_cset A ===> (A ===> op =) ===> op =) cBall cBall"
    1.32 +  "(rel_cset A ===> (A ===> (=)) ===> (=)) cBall cBall"
    1.33    unfolding rel_cset_iff rel_fun_def by blast
    1.34  
    1.35  lemma cBex_parametric [transfer_rule]:
    1.36 -  "(rel_cset A ===> (A ===> op =) ===> op =) cBex cBex"
    1.37 +  "(rel_cset A ===> (A ===> (=)) ===> (=)) cBex cBex"
    1.38    unfolding rel_cset_iff rel_fun_def by blast
    1.39  
    1.40  lemma rel_cset_parametric [transfer_rule]:
    1.41 -  "((A ===> B ===> op =) ===> rel_cset A ===> rel_cset B ===> op =) rel_cset rel_cset"
    1.42 +  "((A ===> B ===> (=)) ===> rel_cset A ===> rel_cset B ===> (=)) rel_cset rel_cset"
    1.43    unfolding rel_fun_def
    1.44    using rel_set_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred, where A = A and B = B]
    1.45    by simp
    1.46 @@ -496,7 +496,7 @@
    1.47  text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close>
    1.48  
    1.49  lemma cin_parametric [transfer_rule]:
    1.50 -  "bi_unique A \<Longrightarrow> (A ===> rel_cset A ===> op =) cin cin"
    1.51 +  "bi_unique A \<Longrightarrow> (A ===> rel_cset A ===> (=)) cin cin"
    1.52  unfolding rel_fun_def rel_cset_iff bi_unique_def by metis
    1.53  
    1.54  lemma cInt_parametric [transfer_rule]:
    1.55 @@ -511,7 +511,7 @@
    1.56  using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
    1.57  
    1.58  lemma csubset_parametric [transfer_rule]:
    1.59 -  "bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> op =) csubset_eq csubset_eq"
    1.60 +  "bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> (=)) csubset_eq csubset_eq"
    1.61  unfolding rel_fun_def
    1.62  using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
    1.63  
    1.64 @@ -595,7 +595,7 @@
    1.65    fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
    1.66    thus "cimage f C = cimage g C" including cset.lifting by transfer force
    1.67  next
    1.68 -  fix f show "rcset \<circ> cimage f = op ` f \<circ> rcset" including cset.lifting by transfer' fastforce
    1.69 +  fix f show "rcset \<circ> cimage f = (`) f \<circ> rcset" including cset.lifting by transfer' fastforce
    1.70  next
    1.71    show "card_order natLeq" by (rule natLeq_card_order)
    1.72  next