# HG changeset patch
# User kuncar
# Date 1392761030 -3600
# Node ID f663fc1e653ba3a8ec6adada0b5ee03519e2261b
# Parent  e81ee43ab2901e081b944ed7774f7e188a2f841a
simplify proofs because of the stronger reflexivity prover

diff -r e81ee43ab290 -r f663fc1e653b src/HOL/IMP/Abs_Int2_ivl.thy
--- 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"
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Library/Countable_Set_Type.thy
--- 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
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Library/DAList.thy
--- 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
 
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Library/FSet.thy
--- 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
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Library/FinFun.thy
--- 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)
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Library/Float.thy
--- 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))))"
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Library/Multiset.thy
--- 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
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Library/RBT.thy
--- 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 *}
 
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Library/RBT_Set.thy
--- 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)
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Quotient_Examples/Lift_DList.thy
--- 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 -