author kuncar Tue Feb 18 23:03:50 2014 +0100 (2014-02-18) changeset 55565 f663fc1e653b parent 55564 e81ee43ab290 child 55568 d7f411651bed
simplify proofs because of the stronger reflexivity prover
 src/HOL/IMP/Abs_Int2_ivl.thy file | annotate | diff | revisions src/HOL/Library/Countable_Set_Type.thy file | annotate | diff | revisions src/HOL/Library/DAList.thy file | annotate | diff | revisions src/HOL/Library/FSet.thy file | annotate | diff | revisions src/HOL/Library/FinFun.thy file | annotate | diff | revisions src/HOL/Library/Float.thy file | annotate | diff | revisions src/HOL/Library/Multiset.thy file | annotate | diff | revisions src/HOL/Library/RBT.thy file | annotate | diff | revisions src/HOL/Library/RBT_Set.thy file | annotate | diff | revisions src/HOL/Quotient_Examples/Lift_DList.thy file | annotate | diff | revisions
```     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.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.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 -
```