simplify proofs because of the stronger reflexivity prover
authorkuncar
Tue Feb 18 23:03:50 2014 +0100 (2014-02-18)
changeset 55565f663fc1e653b
parent 55564 e81ee43ab290
child 55568 d7f411651bed
simplify proofs because of the stronger reflexivity prover
src/HOL/IMP/Abs_Int2_ivl.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/DAList.thy
src/HOL/Library/FSet.thy
src/HOL/Library/FinFun.thy
src/HOL/Library/Float.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Quotient_Examples/Lift_DList.thy
     1.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Tue Feb 18 23:03:49 2014 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Tue Feb 18 23:03:50 2014 +0100
     1.3 @@ -30,8 +30,7 @@
     1.4  lemma \<gamma>_ivl_nice: "\<gamma>_ivl[l,h] = {i. l \<le> Fin i \<and> Fin i \<le> h}"
     1.5  by transfer (simp add: \<gamma>_rep_def)
     1.6  
     1.7 -lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)"
     1.8 -by(auto simp: eq_ivl_def)
     1.9 +lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" .
    1.10  
    1.11  lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool"
    1.12    is "\<lambda>i (l,h). l \<le> Fin i \<and> Fin i \<le> h"
     2.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Tue Feb 18 23:03:49 2014 +0100
     2.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Tue Feb 18 23:03:50 2014 +0100
     2.3 @@ -69,7 +69,7 @@
     2.4    rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
     2.5  
     2.6  lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
     2.7 -  ..
     2.8 +  .
     2.9  lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
    2.10    by (rule countable_empty)
    2.11  lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
     3.1 --- a/src/HOL/Library/DAList.thy	Tue Feb 18 23:03:49 2014 +0100
     3.2 +++ b/src/HOL/Library/DAList.thy	Tue Feb 18 23:03:50 2014 +0100
     3.3 @@ -39,7 +39,7 @@
     3.4  
     3.5  subsection {* Primitive operations *}
     3.6  
     3.7 -lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of  ..
     3.8 +lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of  .
     3.9  
    3.10  lift_definition empty :: "('key, 'value) alist" is "[]" by simp
    3.11  
     4.1 --- a/src/HOL/Library/FSet.thy	Tue Feb 18 23:03:49 2014 +0100
     4.2 +++ b/src/HOL/Library/FSet.thy	Tue Feb 18 23:03:50 2014 +0100
     4.3 @@ -34,7 +34,7 @@
     4.4  lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp 
     4.5  
     4.6  lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer 
     4.7 -  by simp
     4.8 +  .
     4.9  
    4.10  definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
    4.11  
    4.12 @@ -164,7 +164,7 @@
    4.13    "{|x|}"     == "CONST finsert x {||}"
    4.14  
    4.15  lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member 
    4.16 -  parametric member_transfer by simp
    4.17 +  parametric member_transfer .
    4.18  
    4.19  abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
    4.20  
    4.21 @@ -187,12 +187,12 @@
    4.22  by (subst compose_rel_to_Domainp [OF _ finite_transfer]) (auto intro: transfer_raw finite_subset 
    4.23    simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq)
    4.24  
    4.25 -lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer by simp
    4.26 +lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer .
    4.27  
    4.28  lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "|`|" 90) is image 
    4.29    parametric image_transfer by simp
    4.30  
    4.31 -lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem ..
    4.32 +lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem .
    4.33  
    4.34  (* FIXME why is not invariant here unfolded ? *)
    4.35  lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
    4.36 @@ -202,10 +202,10 @@
    4.37  by (subst(asm) compose_rel_to_Domainp [OF _ finite_transfer])
    4.38    (auto intro: transfer_raw simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq invariant_def)
    4.39  
    4.40 -lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer ..
    4.41 -lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer ..
    4.42 +lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
    4.43 +lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
    4.44  
    4.45 -lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold ..
    4.46 +lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold .
    4.47  
    4.48  
    4.49  subsection {* Transferred lemmas from Set.thy *}
    4.50 @@ -774,7 +774,7 @@
    4.51  subsubsection {* Relator and predicator properties *}
    4.52  
    4.53  lift_definition fset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is set_rel
    4.54 -parametric set_rel_transfer ..
    4.55 +parametric set_rel_transfer .
    4.56  
    4.57  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) 
    4.58    \<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
    4.59 @@ -837,8 +837,6 @@
    4.60      by (rename_tac A, rule_tac x="f |`| A" in exI, blast)
    4.61  qed
    4.62  
    4.63 -lemmas reflp_fset_rel[reflexivity_rule] = reflp_set_rel[Transfer.transferred]
    4.64 -
    4.65  lemma right_total_fset_rel[transfer_rule]: "right_total A \<Longrightarrow> right_total (fset_rel A)"
    4.66  unfolding right_total_def 
    4.67  apply transfer
     5.1 --- a/src/HOL/Library/FinFun.thy	Tue Feb 18 23:03:49 2014 +0100
     5.2 +++ b/src/HOL/Library/FinFun.thy	Tue Feb 18 23:03:50 2014 +0100
     5.3 @@ -411,7 +411,7 @@
     5.4  qed
     5.5  
     5.6  lift_definition finfun_default :: "'a \<Rightarrow>f 'b \<Rightarrow> 'b"
     5.7 -is "finfun_default_aux" ..
     5.8 +is "finfun_default_aux" .
     5.9  
    5.10  lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
    5.11  by transfer (erule finite_finfun_default_aux)
     6.1 --- a/src/HOL/Library/Float.thy	Tue Feb 18 23:03:49 2014 +0100
     6.2 +++ b/src/HOL/Library/Float.thy	Tue Feb 18 23:03:50 2014 +0100
     6.3 @@ -161,11 +161,11 @@
     6.4  lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
     6.5  declare sgn_float.rep_eq[simp]
     6.6  
     6.7 -lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
     6.8 +lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" .
     6.9  
    6.10 -lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
    6.11 +lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" .
    6.12  declare less_eq_float.rep_eq[simp]
    6.13 -lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
    6.14 +lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" .
    6.15  declare less_float.rep_eq[simp]
    6.16  
    6.17  instance
    6.18 @@ -466,7 +466,7 @@
    6.19    by transfer (simp add: sgn_times)
    6.20  hide_fact (open) compute_float_sgn
    6.21  
    6.22 -lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" ..
    6.23 +lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .
    6.24  
    6.25  lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
    6.26    by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
    6.27 @@ -476,7 +476,7 @@
    6.28    by transfer (simp add: field_simps)
    6.29  hide_fact (open) compute_float_less
    6.30  
    6.31 -lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" ..
    6.32 +lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" .
    6.33  
    6.34  lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
    6.35    by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
    6.36 @@ -486,7 +486,7 @@
    6.37    by transfer (simp add: field_simps)
    6.38  hide_fact (open) compute_float_le
    6.39  
    6.40 -lift_definition is_float_zero :: "float \<Rightarrow> bool"  is "op = 0 :: real \<Rightarrow> bool" by simp
    6.41 +lift_definition is_float_zero :: "float \<Rightarrow> bool"  is "op = 0 :: real \<Rightarrow> bool" .
    6.42  
    6.43  lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
    6.44    by transfer (auto simp add: is_float_zero_def)
    6.45 @@ -1533,7 +1533,7 @@
    6.46  lemma real_of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
    6.47    unfolding nprt_def inf_float_def min_def inf_real_def by auto
    6.48  
    6.49 -lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
    6.50 +lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor .
    6.51  
    6.52  lemma compute_int_floor_fl[code]:
    6.53    "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
     7.1 --- a/src/HOL/Library/Multiset.thy	Tue Feb 18 23:03:49 2014 +0100
     7.2 +++ b/src/HOL/Library/Multiset.thy	Tue Feb 18 23:03:50 2014 +0100
     7.3 @@ -268,8 +268,8 @@
     7.4  instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
     7.5  begin
     7.6  
     7.7 -lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)"
     7.8 -by simp
     7.9 +lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" .
    7.10 +
    7.11  lemmas mset_le_def = less_eq_multiset_def
    7.12  
    7.13  definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
     8.1 --- a/src/HOL/Library/RBT.thy	Tue Feb 18 23:03:49 2014 +0100
     8.2 +++ b/src/HOL/Library/RBT.thy	Tue Feb 18 23:03:50 2014 +0100
     8.3 @@ -38,8 +38,7 @@
     8.4  setup_lifting type_definition_rbt
     8.5  print_theorems
     8.6  
     8.7 -lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" 
     8.8 -by simp
     8.9 +lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" .
    8.10  
    8.11  lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty 
    8.12  by (simp add: empty_def)
    8.13 @@ -50,29 +49,25 @@
    8.14  lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete" 
    8.15  by simp
    8.16  
    8.17 -lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
    8.18 -by simp
    8.19 +lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries .
    8.20 +
    8.21 +lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys .
    8.22  
    8.23 -lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys 
    8.24 -by simp
    8.25 +lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload" ..
    8.26  
    8.27 -lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload" 
    8.28 -by simp
    8.29 -
    8.30 -lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry 
    8.31 +lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
    8.32  by simp
    8.33  
    8.34  lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'c) rbt" is RBT_Impl.map
    8.35  by simp
    8.36  
    8.37 -lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold 
    8.38 -by simp
    8.39 +lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold .
    8.40  
    8.41  lift_definition union :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union"
    8.42  by (simp add: rbt_union_is_rbt)
    8.43  
    8.44  lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
    8.45 -  is RBT_Impl.foldi by simp
    8.46 +  is RBT_Impl.foldi .
    8.47  
    8.48  subsection {* Derived operations *}
    8.49  
     9.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Feb 18 23:03:49 2014 +0100
     9.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Feb 18 23:03:50 2014 +0100
     9.3 @@ -423,7 +423,7 @@
     9.4  (** abstract **)
     9.5  
     9.6  lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
     9.7 -  is rbt_fold1_keys by simp
     9.8 +  is rbt_fold1_keys .
     9.9  
    9.10  lemma fold1_keys_def_alt:
    9.11    "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
    9.12 @@ -441,9 +441,9 @@
    9.13  
    9.14  (* minimum *)
    9.15  
    9.16 -lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
    9.17 +lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min .
    9.18  
    9.19 -lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
    9.20 +lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt .
    9.21  
    9.22  lemma r_min_alt_def: "r_min t = fold1_keys min t"
    9.23  by transfer (simp add: rbt_min_def)
    9.24 @@ -479,9 +479,9 @@
    9.25  
    9.26  (* maximum *)
    9.27  
    9.28 -lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
    9.29 +lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max .
    9.30  
    9.31 -lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
    9.32 +lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt .
    9.33  
    9.34  lemma r_max_alt_def: "r_max t = fold1_keys max t"
    9.35  by transfer (simp add: rbt_max_def)
    10.1 --- a/src/HOL/Quotient_Examples/Lift_DList.thy	Tue Feb 18 23:03:49 2014 +0100
    10.2 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Tue Feb 18 23:03:50 2014 +0100
    10.3 @@ -35,20 +35,15 @@
    10.4  
    10.5  text {* Derived operations: *}
    10.6  
    10.7 -lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null
    10.8 -by simp
    10.9 +lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null .
   10.10  
   10.11 -lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member
   10.12 -by simp
   10.13 +lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member .
   10.14  
   10.15 -lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length
   10.16 -by simp
   10.17 +lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length .
   10.18  
   10.19 -lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold
   10.20 -by simp
   10.21 +lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold .
   10.22  
   10.23 -lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr
   10.24 -by simp
   10.25 +lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr .
   10.26  
   10.27  lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
   10.28  proof -