author bulwahn Fri May 04 11:08:31 2012 +0200 (2012-05-04) changeset 47888 45bf22d8a81d parent 47887 4e9c06c194d9 child 47889 29212a4bb866
using the new transfer method to obtain abstract properties of RBT trees
```     1.1 --- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Wed May 02 22:05:59 2012 +0200
1.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri May 04 11:08:31 2012 +0200
1.3 @@ -8,6 +8,8 @@
1.4  imports Main "~~/src/HOL/Library/RBT_Impl"
1.5  begin
1.6
1.7 +(* TODO: Replace the ancient Library/RBT theory by this example of the lifting and transfer mechanism. *)
1.8 +
1.9  subsection {* Type definition *}
1.10
1.11  typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
1.12 @@ -77,23 +79,21 @@
1.13
1.14  subsection {* Abstract lookup properties *}
1.15
1.16 -(* TODO: obtain the following lemmas by lifting existing theorems. *)
1.17 -
1.18  lemma lookup_RBT:
1.19    "is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t"
1.20    by (simp add: lookup_def RBT_inverse)
1.21
1.22  lemma lookup_impl_of:
1.23    "rbt_lookup (impl_of t) = lookup t"
1.24 -  by (simp add: lookup_def)
1.25 +  by transfer (rule refl)
1.26
1.27  lemma entries_impl_of:
1.28    "RBT_Impl.entries (impl_of t) = entries t"
1.29 -  by (simp add: entries_def)
1.30 +  by transfer (rule refl)
1.31
1.32  lemma keys_impl_of:
1.33    "RBT_Impl.keys (impl_of t) = keys t"
1.34 -  by (simp add: keys_def)
1.35 +  by transfer (rule refl)
1.36
1.37  lemma lookup_empty [simp]:
1.38    "lookup empty = Map.empty"
1.39 @@ -101,43 +101,43 @@
1.40
1.41  lemma lookup_insert [simp]:
1.42    "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
1.43 -  by (simp add: insert_def lookup_RBT rbt_lookup_rbt_insert lookup_impl_of)
1.44 +  by transfer (rule rbt_lookup_rbt_insert)
1.45
1.46  lemma lookup_delete [simp]:
1.47    "lookup (delete k t) = (lookup t)(k := None)"
1.48 -  by (simp add: delete_def lookup_RBT rbt_lookup_rbt_delete lookup_impl_of restrict_complement_singleton_eq)
1.49 +  by transfer (simp add: rbt_lookup_rbt_delete restrict_complement_singleton_eq)
1.50
1.51  lemma map_of_entries [simp]:
1.52    "map_of (entries t) = lookup t"
1.53 -  by (simp add: entries_def map_of_entries lookup_impl_of)
1.54 +  by transfer (simp add: map_of_entries)
1.55
1.56  lemma entries_lookup:
1.57    "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
1.58 -  by (simp add: entries_def lookup_def entries_rbt_lookup)
1.59 +  by transfer (simp add: entries_rbt_lookup)
1.60
1.61  lemma lookup_bulkload [simp]:
1.62    "lookup (bulkload xs) = map_of xs"
1.63 -  by (simp add: bulkload_def lookup_RBT rbt_lookup_rbt_bulkload)
1.64 +  by transfer (rule rbt_lookup_rbt_bulkload)
1.65
1.66  lemma lookup_map_entry [simp]:
1.67    "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
1.68 -  by (simp add: map_entry_def lookup_RBT rbt_lookup_rbt_map_entry lookup_impl_of)
1.69 +  by transfer (rule rbt_lookup_rbt_map_entry)
1.70
1.71  lemma lookup_map [simp]:
1.72    "lookup (map f t) k = Option.map (f k) (lookup t k)"
1.73 -  by (simp add: map_def lookup_RBT rbt_lookup_map lookup_impl_of)
1.74 +  by transfer (rule rbt_lookup_map)
1.75
1.76  lemma fold_fold:
1.77    "fold f t = List.fold (prod_case f) (entries t)"
1.78 -  by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
1.79 +  by transfer (rule RBT_Impl.fold_def)
1.80
1.81  lemma impl_of_empty:
1.82    "impl_of empty = RBT_Impl.Empty"
1.83 -  by (simp add: empty_def RBT_inverse)
1.84 +  by transfer (rule refl)
1.85
1.86  lemma is_empty_empty [simp]:
1.87    "is_empty t \<longleftrightarrow> t = empty"
1.88 -  by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
1.89 +  unfolding is_empty_def by transfer (simp split: rbt.split)
1.90
1.91  lemma RBT_lookup_empty [simp]: (*FIXME*)
1.92    "rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
1.93 @@ -145,15 +145,15 @@
1.94
1.95  lemma lookup_empty_empty [simp]:
1.96    "lookup t = Map.empty \<longleftrightarrow> t = empty"
1.97 -  by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse)
1.98 +  by transfer (rule RBT_lookup_empty)
1.99
1.100  lemma sorted_keys [iff]:
1.101    "sorted (keys t)"
1.102 -  by (simp add: keys_def RBT_Impl.keys_def rbt_sorted_entries)
1.103 +  by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries)
1.104
1.105  lemma distinct_keys [iff]:
1.106    "distinct (keys t)"
1.107 -  by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
1.108 +  by transfer (simp add: RBT_Impl.keys_def distinct_entries)
1.109
1.110
1.111  end
1.112 \ No newline at end of file
```