--- a/NEWS Tue Jun 21 17:35:45 2016 +0200
+++ b/NEWS Wed Jun 22 10:09:20 2016 +0200
@@ -132,6 +132,10 @@
*** HOL ***
+* Former locale lifting_syntax is now a bundle, which is easier to
+include in a local context or theorem statement, e.g. "context includes
+lifting_syntax begin ... end". Minor INCOMPATIBILITY.
+
* Code generation for scala: ambiguous implicts in class diagrams
are spelt out explicitly.
--- a/src/HOL/Filter.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Filter.thy Wed Jun 22 10:09:20 2016 +0200
@@ -1192,7 +1192,8 @@
subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
--- a/src/HOL/Groups_List.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Groups_List.thy Wed Jun 22 10:09:20 2016 +0200
@@ -308,20 +308,14 @@
"setsum f (set [m..<n]) = listsum (map f [m..<n])"
by (simp add: interv_listsum_conv_setsum_set_nat)
-context
-begin
-
-interpretation lifting_syntax .
-
lemma listsum_transfer[transfer_rule]:
+ includes lifting_syntax
assumes [transfer_rule]: "A 0 0"
assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
shows "(list_all2 A ===> A) listsum listsum"
unfolding listsum.eq_foldr [abs_def]
by transfer_prover
-end
-
subsection \<open>List product\<close>
--- a/src/HOL/Library/Complete_Partial_Order2.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Wed Jun 22 10:09:20 2016 +0200
@@ -9,14 +9,11 @@
"~~/src/HOL/Library/Lattice_Syntax"
begin
-context begin interpretation lifting_syntax .
-
lemma chain_transfer [transfer_rule]:
- "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"
+ includes lifting_syntax
+ shows "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain"
unfolding chain_def[abs_def] by transfer_prover
-end
-
lemma linorder_chain [simp, intro!]:
fixes Y :: "_ :: linorder set"
shows "Complete_Partial_Order.chain op \<le> Y"
--- a/src/HOL/Library/Countable_Set_Type.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy Wed Jun 22 10:09:20 2016 +0200
@@ -70,8 +70,6 @@
instantiation cset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
begin
-interpretation lifting_syntax .
-
lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp
lift_definition less_eq_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool"
@@ -81,6 +79,7 @@
where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a cset)"
lemma less_cset_transfer[transfer_rule]:
+ includes lifting_syntax
assumes [transfer_rule]: "bi_unique A"
shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \<subset> op <"
unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover
@@ -458,7 +457,8 @@
text \<open>Unconditional transfer rules\<close>
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
lemmas cempty_parametric [transfer_rule] = empty_transfer[Transfer.transferred]
--- a/src/HOL/Library/FSet.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Library/FSet.thy Wed Jun 22 10:09:20 2016 +0200
@@ -29,8 +29,6 @@
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
begin
-interpretation lifting_syntax .
-
lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp
lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer
@@ -39,6 +37,7 @@
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
lemma less_fset_transfer[transfer_rule]:
+ includes lifting_syntax
assumes [transfer_rule]: "bi_unique A"
shows "((pcr_fset A) ===> (pcr_fset A) ===> op =) op \<subset> op <"
unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover
@@ -74,7 +73,8 @@
instantiation fset :: (type) conditionally_complete_lattice
begin
-interpretation lifting_syntax .
+context includes lifting_syntax
+begin
lemma right_total_Inf_fset_transfer:
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
@@ -106,6 +106,8 @@
lemma transfer_bdd_below[transfer_rule]: "(rel_set (pcr_fset op =) ===> op =) bdd_below bdd_below"
by auto
+end
+
instance
proof
fix x z :: "'a fset"
@@ -174,11 +176,9 @@
abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
-
lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
@@ -808,11 +808,9 @@
text \<open>Unconditional transfer rules\<close>
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
-
lemmas fempty_transfer [transfer_rule] = empty_transfer[Transfer.transferred]
lemma finsert_transfer [transfer_rule]:
--- a/src/HOL/Library/Mapping.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Library/Mapping.thy Wed Jun 22 10:09:20 2016 +0200
@@ -14,11 +14,9 @@
"map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"
using map_add_map_of_foldr [of Map.empty] by auto
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
-
lemma empty_parametric:
"(A ===> rel_option B) Map.empty Map.empty"
by transfer_prover
@@ -219,11 +217,9 @@
end
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
-
lemma [transfer_rule]:
assumes [transfer_rule]: "bi_total A"
assumes [transfer_rule]: "bi_unique B"
--- a/src/HOL/Lifting.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Lifting.thy Wed Jun 22 10:09:20 2016 +0200
@@ -16,9 +16,8 @@
subsection \<open>Function map\<close>
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
lemma map_fun_id:
"(id ---> id) = id"
--- a/src/HOL/Lifting_Set.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Lifting_Set.thy Wed Jun 22 10:09:20 2016 +0200
@@ -112,11 +112,9 @@
subsubsection \<open>Unconditional transfer rules\<close>
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
-
lemma empty_transfer [transfer_rule]: "(rel_set A) {} {}"
unfolding rel_set_def by simp
--- a/src/HOL/List.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/List.thy Wed Jun 22 10:09:20 2016 +0200
@@ -6829,9 +6829,8 @@
subsubsection \<open>Transfer rules for the Transfer package\<close>
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
lemma tl_transfer [transfer_rule]:
"(list_all2 A ===> list_all2 A) tl tl"
--- a/src/HOL/Option.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Option.thy Wed Jun 22 10:09:20 2016 +0200
@@ -314,11 +314,9 @@
subsection \<open>Transfer rules for the Transfer package\<close>
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
-
lemma option_bind_transfer [transfer_rule]:
"(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
Option.bind Option.bind"
--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Jun 22 10:09:20 2016 +0200
@@ -1775,7 +1775,8 @@
lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}"
by (simp add: set_pmf_binomial_eq)
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
lemma bind_pmf_parametric [transfer_rule]:
"(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf"
--- a/src/HOL/Probability/SPMF.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy Wed Jun 22 10:09:20 2016 +0200
@@ -158,7 +158,9 @@
subsubsection \<open>A relator for sets that treats sets like predicates\<close>
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
+
definition rel_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
where "rel_pred R A B = (R ===> op =) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B)"
@@ -173,6 +175,7 @@
because it blows up the search space for @{method transfer}
(in combination with @{thm [source] Collect_transfer})\<close>
by(simp add: rel_funI rel_predI)
+
end
subsubsection \<open>Monotonicity rules\<close>
@@ -720,7 +723,8 @@
lemma spmf_rel_eq: "rel_spmf op = = op ="
by(simp add: pmf.rel_eq option.rel_eq)
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
lemma bind_spmf_parametric [transfer_rule]:
"(rel_spmf A ===> (A ===> rel_spmf B) ===> rel_spmf B) bind_spmf bind_spmf"
@@ -758,7 +762,9 @@
lemma rel_pmf_return_pmfI: "P x y \<Longrightarrow> rel_pmf P (return_pmf x) (return_pmf y)"
by(rule rel_pmf.intros[where pq="return_pmf (x, y)"])(simp_all)
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
+
text \<open>We do not yet have a relator for @{typ "'a measure"}, so we combine @{const measure} and @{const measure_pmf}\<close>
lemma measure_pmf_parametric:
"(rel_pmf A ===> rel_pred A ===> op =) (\<lambda>p. measure (measure_pmf p)) (\<lambda>q. measure (measure_pmf q))"
@@ -778,6 +784,7 @@
apply(erule measure_pmf_parametric[THEN rel_funD, THEN rel_funD])
apply(auto simp add: rel_pred_def rel_fun_def elim: option.rel_cases)
done
+
end
subsection \<open>From @{typ "'a pmf"} to @{typ "'a spmf"}\<close>
@@ -1785,7 +1792,8 @@
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. rel_spmf R (f x) (g x))"
by(rule admissible_subst[OF admissible_rel_spmf, where f="\<lambda>x. (f x, g x)", simplified])(rule mcont_Pair)
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
lemma fixp_spmf_parametric':
assumes f: "\<And>x. monotone (ord_spmf op =) (ord_spmf op =) F"
@@ -2032,7 +2040,9 @@
by(auto simp add: spmf_of_set_def simp del: spmf_of_pmf_pmf_of_set intro: rel_pmf_of_set_bij)
qed
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
+
lemma rel_spmf_of_set:
assumes "bi_unique R"
shows "(rel_set R ===> rel_spmf R) spmf_of_set spmf_of_set"
@@ -2043,6 +2053,7 @@
by(auto dest: bi_unique_rel_set_bij_betw)
then show "rel_spmf R (spmf_of_set A) (spmf_of_set B)" by(rule rel_spmf_of_set_bij)
qed
+
end
lemma map_mem_spmf_of_set:
@@ -2637,10 +2648,13 @@
"lossless_spmf (TRY p ELSE q) \<longleftrightarrow> lossless_spmf p \<or> lossless_spmf q"
by(auto simp add: try_spmf_def in_set_spmf lossless_iff_set_pmf_None split: option.splits)
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
+
lemma try_spmf_parametric [transfer_rule]:
"(rel_spmf A ===> rel_spmf A ===> rel_spmf A) try_spmf try_spmf"
unfolding try_spmf_def[abs_def] by transfer_prover
+
end
lemma try_spmf_cong:
--- a/src/HOL/Quotient.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Quotient.thy Wed Jun 22 10:09:20 2016 +0200
@@ -28,9 +28,8 @@
shows "((op =) OOO R) = R"
by (auto simp add: fun_eq_iff)
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
subsection \<open>Quotient Predicate\<close>
@@ -805,9 +804,8 @@
lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
by (simp add: Quot_True_def)
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
text \<open>Tactics for proving the lifted theorems\<close>
ML_file "Tools/Quotient/quotient_tacs.ML"
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Jun 22 10:09:20 2016 +0200
@@ -25,9 +25,8 @@
lemma equivp_list_eq: "equivp list_eq"
by (intro equivpI reflp_list_eq symp_list_eq transp_list_eq)
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
lemma list_eq_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
--- a/src/HOL/Transfer.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Transfer.thy Wed Jun 22 10:09:20 2016 +0200
@@ -11,15 +11,14 @@
subsection \<open>Relator for function space\<close>
-locale lifting_syntax
+bundle lifting_syntax
begin
- notation rel_fun (infixr "===>" 55)
- notation map_fun (infixr "--->" 55)
+ notation rel_fun (infixr "===>" 55)
+ notation map_fun (infixr "--->" 55)
end
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
lemma rel_funD2:
assumes "rel_fun A B f g" and "A x x"
@@ -236,9 +235,8 @@
hide_const (open) Rel
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
text \<open>Handling of domains\<close>
@@ -365,9 +363,8 @@
subsection \<open>Transfer rules\<close>
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
lemma Domainp_forall_transfer [transfer_rule]:
assumes "right_total A"
--- a/src/HOL/ex/Transfer_Int_Nat.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Wed Jun 22 10:09:20 2016 +0200
@@ -20,9 +20,8 @@
subsection \<open>Transfer rules\<close>
-context
+context includes lifting_syntax
begin
-interpretation lifting_syntax .
lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
unfolding ZN_def bi_unique_def by simp