bundle lifting_syntax;
authorwenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343fb5d8a50c641
parent 63342 49fa6aaa4529
child 63344 c9910404cc8a
bundle lifting_syntax;
NEWS
src/HOL/Filter.thy
src/HOL/Groups_List.thy
src/HOL/Library/Complete_Partial_Order2.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Mapping.thy
src/HOL/Lifting.thy
src/HOL/Lifting_Set.thy
src/HOL/List.thy
src/HOL/Option.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/SPMF.thy
src/HOL/Quotient.thy
src/HOL/Quotient_Examples/Lift_FSet.thy
src/HOL/Transfer.thy
src/HOL/ex/Transfer_Int_Nat.thy
     1.1 --- a/NEWS	Tue Jun 21 17:35:45 2016 +0200
     1.2 +++ b/NEWS	Wed Jun 22 10:09:20 2016 +0200
     1.3 @@ -132,6 +132,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Former locale lifting_syntax is now a bundle, which is easier to
     1.8 +include in a local context or theorem statement, e.g. "context includes
     1.9 +lifting_syntax begin ... end". Minor INCOMPATIBILITY.
    1.10 +
    1.11  * Code generation for scala: ambiguous implicts in class diagrams
    1.12  are spelt out explicitly.
    1.13  
     2.1 --- a/src/HOL/Filter.thy	Tue Jun 21 17:35:45 2016 +0200
     2.2 +++ b/src/HOL/Filter.thy	Wed Jun 22 10:09:20 2016 +0200
     2.3 @@ -1192,7 +1192,8 @@
     2.4  
     2.5  subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
     2.6  
     2.7 -context begin interpretation lifting_syntax .
     2.8 +context includes lifting_syntax
     2.9 +begin
    2.10  
    2.11  definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
    2.12  where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
     3.1 --- a/src/HOL/Groups_List.thy	Tue Jun 21 17:35:45 2016 +0200
     3.2 +++ b/src/HOL/Groups_List.thy	Wed Jun 22 10:09:20 2016 +0200
     3.3 @@ -308,20 +308,14 @@
     3.4    "setsum f (set [m..<n]) = listsum (map f [m..<n])"
     3.5    by (simp add: interv_listsum_conv_setsum_set_nat)
     3.6  
     3.7 -context
     3.8 -begin
     3.9 -
    3.10 -interpretation lifting_syntax .
    3.11 -
    3.12  lemma listsum_transfer[transfer_rule]:
    3.13 +  includes lifting_syntax
    3.14    assumes [transfer_rule]: "A 0 0"
    3.15    assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
    3.16    shows "(list_all2 A ===> A) listsum listsum"
    3.17    unfolding listsum.eq_foldr [abs_def]
    3.18    by transfer_prover
    3.19  
    3.20 -end
    3.21 -
    3.22  
    3.23  subsection \<open>List product\<close>
    3.24  
     4.1 --- a/src/HOL/Library/Complete_Partial_Order2.thy	Tue Jun 21 17:35:45 2016 +0200
     4.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy	Wed Jun 22 10:09:20 2016 +0200
     4.3 @@ -9,14 +9,11 @@
     4.4    "~~/src/HOL/Library/Lattice_Syntax"
     4.5  begin
     4.6  
     4.7 -context begin interpretation lifting_syntax .
     4.8 -
     4.9  lemma chain_transfer [transfer_rule]:
    4.10 -  "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"
    4.11 +  includes lifting_syntax
    4.12 +  shows "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"
    4.13  unfolding chain_def[abs_def] by transfer_prover
    4.14  
    4.15 -end
    4.16 -
    4.17  lemma linorder_chain [simp, intro!]:
    4.18    fixes Y :: "_ :: linorder set"
    4.19    shows "Complete_Partial_Order.chain op \<le> Y"
     5.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Tue Jun 21 17:35:45 2016 +0200
     5.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Wed Jun 22 10:09:20 2016 +0200
     5.3 @@ -70,8 +70,6 @@
     5.4  instantiation cset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
     5.5  begin
     5.6  
     5.7 -interpretation lifting_syntax .
     5.8 -
     5.9  lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp
    5.10  
    5.11  lift_definition less_eq_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool"
    5.12 @@ -81,6 +79,7 @@
    5.13  where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a cset)"
    5.14  
    5.15  lemma less_cset_transfer[transfer_rule]:
    5.16 +  includes lifting_syntax
    5.17    assumes [transfer_rule]: "bi_unique A"
    5.18    shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \<subset> op <"
    5.19  unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover
    5.20 @@ -458,7 +457,8 @@
    5.21  
    5.22  text \<open>Unconditional transfer rules\<close>
    5.23  
    5.24 -context begin interpretation lifting_syntax .
    5.25 +context includes lifting_syntax
    5.26 +begin
    5.27  
    5.28  lemmas cempty_parametric [transfer_rule] = empty_transfer[Transfer.transferred]
    5.29  
     6.1 --- a/src/HOL/Library/FSet.thy	Tue Jun 21 17:35:45 2016 +0200
     6.2 +++ b/src/HOL/Library/FSet.thy	Wed Jun 22 10:09:20 2016 +0200
     6.3 @@ -29,8 +29,6 @@
     6.4  instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
     6.5  begin
     6.6  
     6.7 -interpretation lifting_syntax .
     6.8 -
     6.9  lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp
    6.10  
    6.11  lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer
    6.12 @@ -39,6 +37,7 @@
    6.13  definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
    6.14  
    6.15  lemma less_fset_transfer[transfer_rule]:
    6.16 +  includes lifting_syntax
    6.17    assumes [transfer_rule]: "bi_unique A"
    6.18    shows "((pcr_fset A) ===> (pcr_fset A) ===> op =) op \<subset> op <"
    6.19    unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover
    6.20 @@ -74,7 +73,8 @@
    6.21  instantiation fset :: (type) conditionally_complete_lattice
    6.22  begin
    6.23  
    6.24 -interpretation lifting_syntax .
    6.25 +context includes lifting_syntax
    6.26 +begin
    6.27  
    6.28  lemma right_total_Inf_fset_transfer:
    6.29    assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
    6.30 @@ -106,6 +106,8 @@
    6.31  lemma transfer_bdd_below[transfer_rule]: "(rel_set (pcr_fset op =) ===> op =) bdd_below bdd_below"
    6.32    by auto
    6.33  
    6.34 +end
    6.35 +
    6.36  instance
    6.37  proof
    6.38    fix x z :: "'a fset"
    6.39 @@ -174,11 +176,9 @@
    6.40  
    6.41  abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
    6.42  
    6.43 -context
    6.44 +context includes lifting_syntax
    6.45  begin
    6.46  
    6.47 -interpretation lifting_syntax .
    6.48 -
    6.49  lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
    6.50    parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
    6.51  
    6.52 @@ -808,11 +808,9 @@
    6.53  
    6.54  text \<open>Unconditional transfer rules\<close>
    6.55  
    6.56 -context
    6.57 +context includes lifting_syntax
    6.58  begin
    6.59  
    6.60 -interpretation lifting_syntax .
    6.61 -
    6.62  lemmas fempty_transfer [transfer_rule] = empty_transfer[Transfer.transferred]
    6.63  
    6.64  lemma finsert_transfer [transfer_rule]:
     7.1 --- a/src/HOL/Library/Mapping.thy	Tue Jun 21 17:35:45 2016 +0200
     7.2 +++ b/src/HOL/Library/Mapping.thy	Wed Jun 22 10:09:20 2016 +0200
     7.3 @@ -14,11 +14,9 @@
     7.4    "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"
     7.5    using map_add_map_of_foldr [of Map.empty] by auto
     7.6  
     7.7 -context
     7.8 +context includes lifting_syntax
     7.9  begin
    7.10  
    7.11 -interpretation lifting_syntax .
    7.12 -
    7.13  lemma empty_parametric:
    7.14    "(A ===> rel_option B) Map.empty Map.empty"
    7.15    by transfer_prover
    7.16 @@ -219,11 +217,9 @@
    7.17  
    7.18  end
    7.19  
    7.20 -context
    7.21 +context includes lifting_syntax
    7.22  begin
    7.23  
    7.24 -interpretation lifting_syntax .
    7.25 -
    7.26  lemma [transfer_rule]:
    7.27    assumes [transfer_rule]: "bi_total A"
    7.28    assumes [transfer_rule]: "bi_unique B"
     8.1 --- a/src/HOL/Lifting.thy	Tue Jun 21 17:35:45 2016 +0200
     8.2 +++ b/src/HOL/Lifting.thy	Wed Jun 22 10:09:20 2016 +0200
     8.3 @@ -16,9 +16,8 @@
     8.4  
     8.5  subsection \<open>Function map\<close>
     8.6  
     8.7 -context
     8.8 +context includes lifting_syntax
     8.9  begin
    8.10 -interpretation lifting_syntax .
    8.11  
    8.12  lemma map_fun_id:
    8.13    "(id ---> id) = id"
     9.1 --- a/src/HOL/Lifting_Set.thy	Tue Jun 21 17:35:45 2016 +0200
     9.2 +++ b/src/HOL/Lifting_Set.thy	Wed Jun 22 10:09:20 2016 +0200
     9.3 @@ -112,11 +112,9 @@
     9.4  
     9.5  subsubsection \<open>Unconditional transfer rules\<close>
     9.6  
     9.7 -context
     9.8 +context includes lifting_syntax
     9.9  begin
    9.10  
    9.11 -interpretation lifting_syntax .
    9.12 -
    9.13  lemma empty_transfer [transfer_rule]: "(rel_set A) {} {}"
    9.14    unfolding rel_set_def by simp
    9.15  
    10.1 --- a/src/HOL/List.thy	Tue Jun 21 17:35:45 2016 +0200
    10.2 +++ b/src/HOL/List.thy	Wed Jun 22 10:09:20 2016 +0200
    10.3 @@ -6829,9 +6829,8 @@
    10.4  
    10.5  subsubsection \<open>Transfer rules for the Transfer package\<close>
    10.6  
    10.7 -context
    10.8 +context includes lifting_syntax
    10.9  begin
   10.10 -interpretation lifting_syntax .
   10.11  
   10.12  lemma tl_transfer [transfer_rule]:
   10.13    "(list_all2 A ===> list_all2 A) tl tl"
    11.1 --- a/src/HOL/Option.thy	Tue Jun 21 17:35:45 2016 +0200
    11.2 +++ b/src/HOL/Option.thy	Wed Jun 22 10:09:20 2016 +0200
    11.3 @@ -314,11 +314,9 @@
    11.4  
    11.5  subsection \<open>Transfer rules for the Transfer package\<close>
    11.6  
    11.7 -context
    11.8 +context includes lifting_syntax
    11.9  begin
   11.10  
   11.11 -interpretation lifting_syntax .
   11.12 -
   11.13  lemma option_bind_transfer [transfer_rule]:
   11.14    "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   11.15      Option.bind Option.bind"
    12.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Jun 21 17:35:45 2016 +0200
    12.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jun 22 10:09:20 2016 +0200
    12.3 @@ -1775,7 +1775,8 @@
    12.4  lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}"
    12.5    by (simp add: set_pmf_binomial_eq)
    12.6  
    12.7 -context begin interpretation lifting_syntax .
    12.8 +context includes lifting_syntax
    12.9 +begin
   12.10  
   12.11  lemma bind_pmf_parametric [transfer_rule]:
   12.12    "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf"
    13.1 --- a/src/HOL/Probability/SPMF.thy	Tue Jun 21 17:35:45 2016 +0200
    13.2 +++ b/src/HOL/Probability/SPMF.thy	Wed Jun 22 10:09:20 2016 +0200
    13.3 @@ -158,7 +158,9 @@
    13.4  
    13.5  subsubsection \<open>A relator for sets that treats sets like predicates\<close>
    13.6  
    13.7 -context begin interpretation lifting_syntax .
    13.8 +context includes lifting_syntax
    13.9 +begin
   13.10 +
   13.11  definition rel_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
   13.12  where "rel_pred R A B = (R ===> op =) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B)"
   13.13  
   13.14 @@ -173,6 +175,7 @@
   13.15        because it blows up the search space for @{method transfer}
   13.16        (in combination with @{thm [source] Collect_transfer})\<close>
   13.17  by(simp add: rel_funI rel_predI)
   13.18 +
   13.19  end
   13.20  
   13.21  subsubsection \<open>Monotonicity rules\<close>
   13.22 @@ -720,7 +723,8 @@
   13.23  lemma spmf_rel_eq: "rel_spmf op = = op ="
   13.24  by(simp add: pmf.rel_eq option.rel_eq)
   13.25  
   13.26 -context begin interpretation lifting_syntax .
   13.27 +context includes lifting_syntax
   13.28 +begin
   13.29  
   13.30  lemma bind_spmf_parametric [transfer_rule]:
   13.31    "(rel_spmf A ===> (A ===> rel_spmf B) ===> rel_spmf B) bind_spmf bind_spmf"
   13.32 @@ -758,7 +762,9 @@
   13.33  lemma rel_pmf_return_pmfI: "P x y \<Longrightarrow> rel_pmf P (return_pmf x) (return_pmf y)"
   13.34  by(rule rel_pmf.intros[where pq="return_pmf (x, y)"])(simp_all)
   13.35  
   13.36 -context begin interpretation lifting_syntax .
   13.37 +context includes lifting_syntax
   13.38 +begin
   13.39 +
   13.40  text \<open>We do not yet have a relator for @{typ "'a measure"}, so we combine @{const measure} and @{const measure_pmf}\<close>
   13.41  lemma measure_pmf_parametric:
   13.42    "(rel_pmf A ===> rel_pred A ===> op =) (\<lambda>p. measure (measure_pmf p)) (\<lambda>q. measure (measure_pmf q))"
   13.43 @@ -778,6 +784,7 @@
   13.44  apply(erule measure_pmf_parametric[THEN rel_funD, THEN rel_funD])
   13.45  apply(auto simp add: rel_pred_def rel_fun_def elim: option.rel_cases)
   13.46  done
   13.47 +
   13.48  end
   13.49  
   13.50  subsection \<open>From @{typ "'a pmf"} to @{typ "'a spmf"}\<close>
   13.51 @@ -1785,7 +1792,8 @@
   13.52    \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. rel_spmf R (f x) (g x))"
   13.53  by(rule admissible_subst[OF admissible_rel_spmf, where f="\<lambda>x. (f x, g x)", simplified])(rule mcont_Pair)
   13.54  
   13.55 -context begin interpretation lifting_syntax .
   13.56 +context includes lifting_syntax
   13.57 +begin
   13.58  
   13.59  lemma fixp_spmf_parametric':
   13.60    assumes f: "\<And>x. monotone (ord_spmf op =) (ord_spmf op =) F"
   13.61 @@ -2032,7 +2040,9 @@
   13.62      by(auto simp add: spmf_of_set_def simp del: spmf_of_pmf_pmf_of_set intro: rel_pmf_of_set_bij)
   13.63  qed
   13.64  
   13.65 -context begin interpretation lifting_syntax .
   13.66 +context includes lifting_syntax
   13.67 +begin
   13.68 +
   13.69  lemma rel_spmf_of_set:
   13.70    assumes "bi_unique R"
   13.71    shows "(rel_set R ===> rel_spmf R) spmf_of_set spmf_of_set"
   13.72 @@ -2043,6 +2053,7 @@
   13.73      by(auto dest: bi_unique_rel_set_bij_betw)
   13.74    then show "rel_spmf R (spmf_of_set A) (spmf_of_set B)" by(rule rel_spmf_of_set_bij)
   13.75  qed
   13.76 +
   13.77  end
   13.78  
   13.79  lemma map_mem_spmf_of_set:
   13.80 @@ -2637,10 +2648,13 @@
   13.81    "lossless_spmf (TRY p ELSE q) \<longleftrightarrow> lossless_spmf p \<or> lossless_spmf q"
   13.82  by(auto simp add: try_spmf_def in_set_spmf lossless_iff_set_pmf_None split: option.splits)
   13.83  
   13.84 -context begin interpretation lifting_syntax .
   13.85 +context includes lifting_syntax
   13.86 +begin
   13.87 +
   13.88  lemma try_spmf_parametric [transfer_rule]:
   13.89    "(rel_spmf A ===> rel_spmf A ===> rel_spmf A) try_spmf try_spmf"
   13.90  unfolding try_spmf_def[abs_def] by transfer_prover
   13.91 +
   13.92  end
   13.93  
   13.94  lemma try_spmf_cong:
    14.1 --- a/src/HOL/Quotient.thy	Tue Jun 21 17:35:45 2016 +0200
    14.2 +++ b/src/HOL/Quotient.thy	Wed Jun 22 10:09:20 2016 +0200
    14.3 @@ -28,9 +28,8 @@
    14.4    shows "((op =) OOO R) = R"
    14.5    by (auto simp add: fun_eq_iff)
    14.6  
    14.7 -context
    14.8 +context includes lifting_syntax
    14.9  begin
   14.10 -interpretation lifting_syntax .
   14.11  
   14.12  subsection \<open>Quotient Predicate\<close>
   14.13  
   14.14 @@ -805,9 +804,8 @@
   14.15  lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
   14.16    by (simp add: Quot_True_def)
   14.17  
   14.18 -context 
   14.19 +context includes lifting_syntax
   14.20  begin
   14.21 -interpretation lifting_syntax .
   14.22  
   14.23  text \<open>Tactics for proving the lifted theorems\<close>
   14.24  ML_file "Tools/Quotient/quotient_tacs.ML"
    15.1 --- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Tue Jun 21 17:35:45 2016 +0200
    15.2 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Jun 22 10:09:20 2016 +0200
    15.3 @@ -25,9 +25,8 @@
    15.4  lemma equivp_list_eq: "equivp list_eq"
    15.5    by (intro equivpI reflp_list_eq symp_list_eq transp_list_eq)
    15.6  
    15.7 -context
    15.8 +context includes lifting_syntax
    15.9  begin
   15.10 -interpretation lifting_syntax .
   15.11  
   15.12  lemma list_eq_transfer [transfer_rule]:
   15.13    assumes [transfer_rule]: "bi_unique A"
    16.1 --- a/src/HOL/Transfer.thy	Tue Jun 21 17:35:45 2016 +0200
    16.2 +++ b/src/HOL/Transfer.thy	Wed Jun 22 10:09:20 2016 +0200
    16.3 @@ -11,15 +11,14 @@
    16.4  
    16.5  subsection \<open>Relator for function space\<close>
    16.6  
    16.7 -locale lifting_syntax
    16.8 +bundle lifting_syntax
    16.9  begin
   16.10 -  notation rel_fun (infixr "===>" 55)
   16.11 -  notation map_fun (infixr "--->" 55)
   16.12 +  notation rel_fun  (infixr "===>" 55)
   16.13 +  notation map_fun  (infixr "--->" 55)
   16.14  end
   16.15  
   16.16 -context
   16.17 +context includes lifting_syntax
   16.18  begin
   16.19 -interpretation lifting_syntax .
   16.20  
   16.21  lemma rel_funD2:
   16.22    assumes "rel_fun A B f g" and "A x x"
   16.23 @@ -236,9 +235,8 @@
   16.24  
   16.25  hide_const (open) Rel
   16.26  
   16.27 -context
   16.28 +context includes lifting_syntax
   16.29  begin
   16.30 -interpretation lifting_syntax .
   16.31  
   16.32  text \<open>Handling of domains\<close>
   16.33  
   16.34 @@ -365,9 +363,8 @@
   16.35  
   16.36  subsection \<open>Transfer rules\<close>
   16.37  
   16.38 -context
   16.39 +context includes lifting_syntax
   16.40  begin
   16.41 -interpretation lifting_syntax .
   16.42  
   16.43  lemma Domainp_forall_transfer [transfer_rule]:
   16.44    assumes "right_total A"
    17.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Tue Jun 21 17:35:45 2016 +0200
    17.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Wed Jun 22 10:09:20 2016 +0200
    17.3 @@ -20,9 +20,8 @@
    17.4  
    17.5  subsection \<open>Transfer rules\<close>
    17.6  
    17.7 -context
    17.8 +context includes lifting_syntax
    17.9  begin
   17.10 -interpretation lifting_syntax .
   17.11  
   17.12  lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
   17.13    unfolding ZN_def bi_unique_def by simp