--- a/src/HOL/IMP/Abs_Int2_ivl.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Tue Feb 18 23:03:50 2014 +0100
@@ -30,8 +30,7 @@
lemma \<gamma>_ivl_nice: "\<gamma>_ivl[l,h] = {i. l \<le> Fin i \<and> Fin i \<le> h}"
by transfer (simp add: \<gamma>_rep_def)
-lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)"
-by(auto simp: eq_ivl_def)
+lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" .
lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool"
is "\<lambda>i (l,h). l \<le> Fin i \<and> Fin i \<le> h"
--- a/src/HOL/Library/Countable_Set_Type.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Tue Feb 18 23:03:50 2014 +0100
@@ -69,7 +69,7 @@
rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
- ..
+ .
lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
by (rule countable_empty)
lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
--- a/src/HOL/Library/DAList.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/DAList.thy Tue Feb 18 23:03:50 2014 +0100
@@ -39,7 +39,7 @@
subsection {* Primitive operations *}
-lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of ..
+lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of .
lift_definition empty :: "('key, 'value) alist" is "[]" by simp
--- a/src/HOL/Library/FSet.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/FSet.thy Tue Feb 18 23:03:50 2014 +0100
@@ -34,7 +34,7 @@
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
- by simp
+ .
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
@@ -164,7 +164,7 @@
"{|x|}" == "CONST finsert x {||}"
lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member
- parametric member_transfer by simp
+ parametric member_transfer .
abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
@@ -187,12 +187,12 @@
by (subst compose_rel_to_Domainp [OF _ finite_transfer]) (auto intro: transfer_raw finite_subset
simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq)
-lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer by simp
+lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer .
lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "|`|" 90) is image
parametric image_transfer by simp
-lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem ..
+lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem .
(* FIXME why is not invariant here unfolded ? *)
lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
@@ -202,10 +202,10 @@
by (subst(asm) compose_rel_to_Domainp [OF _ finite_transfer])
(auto intro: transfer_raw simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq invariant_def)
-lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer ..
-lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer ..
+lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
+lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
-lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold ..
+lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold .
subsection {* Transferred lemmas from Set.thy *}
@@ -774,7 +774,7 @@
subsubsection {* Relator and predicator properties *}
lift_definition fset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is set_rel
-parametric set_rel_transfer ..
+parametric set_rel_transfer .
lemma fset_rel_alt_def: "fset_rel R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y)
\<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
@@ -837,8 +837,6 @@
by (rename_tac A, rule_tac x="f |`| A" in exI, blast)
qed
-lemmas reflp_fset_rel[reflexivity_rule] = reflp_set_rel[Transfer.transferred]
-
lemma right_total_fset_rel[transfer_rule]: "right_total A \<Longrightarrow> right_total (fset_rel A)"
unfolding right_total_def
apply transfer
--- a/src/HOL/Library/FinFun.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/FinFun.thy Tue Feb 18 23:03:50 2014 +0100
@@ -411,7 +411,7 @@
qed
lift_definition finfun_default :: "'a \<Rightarrow>f 'b \<Rightarrow> 'b"
-is "finfun_default_aux" ..
+is "finfun_default_aux" .
lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
by transfer (erule finite_finfun_default_aux)
--- a/src/HOL/Library/Float.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/Float.thy Tue Feb 18 23:03:50 2014 +0100
@@ -161,11 +161,11 @@
lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
declare sgn_float.rep_eq[simp]
-lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
+lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" .
-lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
+lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" .
declare less_eq_float.rep_eq[simp]
-lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
+lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" .
declare less_float.rep_eq[simp]
instance
@@ -466,7 +466,7 @@
by transfer (simp add: sgn_times)
hide_fact (open) compute_float_sgn
-lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" ..
+lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .
lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
@@ -476,7 +476,7 @@
by transfer (simp add: field_simps)
hide_fact (open) compute_float_less
-lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" ..
+lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" .
lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
@@ -486,7 +486,7 @@
by transfer (simp add: field_simps)
hide_fact (open) compute_float_le
-lift_definition is_float_zero :: "float \<Rightarrow> bool" is "op = 0 :: real \<Rightarrow> bool" by simp
+lift_definition is_float_zero :: "float \<Rightarrow> bool" is "op = 0 :: real \<Rightarrow> bool" .
lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
by transfer (auto simp add: is_float_zero_def)
@@ -1533,7 +1533,7 @@
lemma real_of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
unfolding nprt_def inf_float_def min_def inf_real_def by auto
-lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
+lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor .
lemma compute_int_floor_fl[code]:
"int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
--- a/src/HOL/Library/Multiset.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Feb 18 23:03:50 2014 +0100
@@ -268,8 +268,8 @@
instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
begin
-lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)"
-by simp
+lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" .
+
lemmas mset_le_def = less_eq_multiset_def
definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
--- a/src/HOL/Library/RBT.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/RBT.thy Tue Feb 18 23:03:50 2014 +0100
@@ -38,8 +38,7 @@
setup_lifting type_definition_rbt
print_theorems
-lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup"
-by simp
+lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" .
lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty
by (simp add: empty_def)
@@ -50,29 +49,25 @@
lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete"
by simp
-lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
-by simp
+lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries .
+
+lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys .
-lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys
-by simp
+lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload" ..
-lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload"
-by simp
-
-lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
+lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
by simp
lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'c) rbt" is RBT_Impl.map
by simp
-lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is RBT_Impl.fold
-by simp
+lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is RBT_Impl.fold .
lift_definition union :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union"
by (simp add: rbt_union_is_rbt)
lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
- is RBT_Impl.foldi by simp
+ is RBT_Impl.foldi .
subsection {* Derived operations *}
--- a/src/HOL/Library/RBT_Set.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/RBT_Set.thy Tue Feb 18 23:03:50 2014 +0100
@@ -423,7 +423,7 @@
(** abstract **)
lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
- is rbt_fold1_keys by simp
+ is rbt_fold1_keys .
lemma fold1_keys_def_alt:
"fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
@@ -441,9 +441,9 @@
(* minimum *)
-lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
+lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min .
-lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
+lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt .
lemma r_min_alt_def: "r_min t = fold1_keys min t"
by transfer (simp add: rbt_min_def)
@@ -479,9 +479,9 @@
(* maximum *)
-lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
+lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max .
-lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
+lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt .
lemma r_max_alt_def: "r_max t = fold1_keys max t"
by transfer (simp add: rbt_max_def)
--- a/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 18 23:03:50 2014 +0100
@@ -35,20 +35,15 @@
text {* Derived operations: *}
-lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null
-by simp
+lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null .
-lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member
-by simp
+lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member .
-lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length
-by simp
+lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length .
-lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold
-by simp
+lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold .
-lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr
-by simp
+lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr .
lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
proof -