src/HOL/Library/FSet.thy
changeset 63343 fb5d8a50c641
parent 63331 247eac9758dd
child 63622 7fb02cee1cba
     1.1 --- a/src/HOL/Library/FSet.thy	Tue Jun 21 17:35:45 2016 +0200
     1.2 +++ b/src/HOL/Library/FSet.thy	Wed Jun 22 10:09:20 2016 +0200
     1.3 @@ -29,8 +29,6 @@
     1.4  instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
     1.5  begin
     1.6  
     1.7 -interpretation lifting_syntax .
     1.8 -
     1.9  lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp
    1.10  
    1.11  lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer
    1.12 @@ -39,6 +37,7 @@
    1.13  definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
    1.14  
    1.15  lemma less_fset_transfer[transfer_rule]:
    1.16 +  includes lifting_syntax
    1.17    assumes [transfer_rule]: "bi_unique A"
    1.18    shows "((pcr_fset A) ===> (pcr_fset A) ===> op =) op \<subset> op <"
    1.19    unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover
    1.20 @@ -74,7 +73,8 @@
    1.21  instantiation fset :: (type) conditionally_complete_lattice
    1.22  begin
    1.23  
    1.24 -interpretation lifting_syntax .
    1.25 +context includes lifting_syntax
    1.26 +begin
    1.27  
    1.28  lemma right_total_Inf_fset_transfer:
    1.29    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
    1.30 @@ -106,6 +106,8 @@
    1.31  lemma transfer_bdd_below[transfer_rule]: "(rel_set (pcr_fset op =) ===> op =) bdd_below bdd_below"
    1.32    by auto
    1.33  
    1.34 +end
    1.35 +
    1.36  instance
    1.37  proof
    1.38    fix x z :: "'a fset"
    1.39 @@ -174,11 +176,9 @@
    1.40  
    1.41  abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
    1.42  
    1.43 -context
    1.44 +context includes lifting_syntax
    1.45  begin
    1.46  
    1.47 -interpretation lifting_syntax .
    1.48 -
    1.49  lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
    1.50    parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
    1.51  
    1.52 @@ -808,11 +808,9 @@
    1.53  
    1.54  text \<open>Unconditional transfer rules\<close>
    1.55  
    1.56 -context
    1.57 +context includes lifting_syntax
    1.58  begin
    1.59  
    1.60 -interpretation lifting_syntax .
    1.61 -
    1.62  lemmas fempty_transfer [transfer_rule] = empty_transfer[Transfer.transferred]
    1.63  
    1.64  lemma finsert_transfer [transfer_rule]: