using the new transfer method to obtain abstract properties of RBT trees
authorbulwahn
Fri May 04 11:08:31 2012 +0200 (2012-05-04)
changeset 4788845bf22d8a81d
parent 47887 4e9c06c194d9
child 47889 29212a4bb866
using the new transfer method to obtain abstract properties of RBT trees
src/HOL/Quotient_Examples/Lift_RBT.thy
     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