# HG changeset patch # User Andreas Lochbihler # Date 1334314173 -7200 # Node ID ab606e685d5227c195936d27f1b3a0a9749389df # Parent 2ada2be850cb521052764aecaa90030a5f17d6ea adapt to changes in RBT_Impl diff -r 2ada2be850cb -r ab606e685d52 src/HOL/Imperative_HOL/ex/SatChecker.thy --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Apr 13 11:45:30 2012 +0200 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Fri Apr 13 12:49:33 2012 +0200 @@ -675,21 +675,21 @@ primrec tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \ Lit \ ClauseId \ Clause \ Clause Heap" where "tres_thm t (l, j) cli = - (case (RBT_Impl.lookup t j) of + (case (rbt_lookup t j) of None \ raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'') | Some clj \ res_thm' l cli clj)" fun tdoProofStep :: " ProofStep \ ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \ ((ClauseId, Clause) RBT_Impl.rbt * Clause list) Heap" where "tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) = - (case (RBT_Impl.lookup t i) of + (case (rbt_lookup t i) of None \ raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') | Some cli \ do { result \ foldM (tres_thm t) rs cli; - return ((RBT_Impl.insert saveTo result t), rcl) + return ((rbt_insert saveTo result t), rcl) })" -| "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)" -| "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)" +| "tdoProofStep (Delete cid) (t, rcl) = return ((rbt_delete cid t), rcl)" +| "tdoProofStep (Root cid clause) (t, rcl) = return (rbt_insert cid (sort clause) t, (remdups(sort clause)) # rcl)" | "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" | "tdoProofStep (ProofDone b) (t, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" @@ -698,7 +698,7 @@ "tchecker n p i = do { rcs \ foldM (tdoProofStep) p (RBT_Impl.Empty, []); - (if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs) + (if (rbt_lookup (fst rcs) i) = Some [] then return (snd rcs) else raise(''No empty clause'')) }" diff -r 2ada2be850cb -r ab606e685d52 src/HOL/Quotient_Examples/Lift_RBT.thy --- a/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Apr 13 11:45:30 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Apr 13 12:49:33 2012 +0200 @@ -37,16 +37,16 @@ setup_lifting type_definition_rbt -lift_definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" is "RBT_Impl.lookup" +lift_definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" is "rbt_lookup" by simp lift_definition empty :: "('a\linorder, 'b) rbt" is RBT_Impl.Empty by (simp add: empty_def) -lift_definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" is "RBT_Impl.insert" +lift_definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" is "rbt_insert" by simp -lift_definition delete :: "'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" is "RBT_Impl.delete" +lift_definition delete :: "'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" is "rbt_delete" by simp lift_definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" is RBT_Impl.entries @@ -55,10 +55,10 @@ lift_definition keys :: "('a\linorder, 'b) rbt \ 'a list" is RBT_Impl.keys by simp -lift_definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" is "RBT_Impl.bulkload" +lift_definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" is "rbt_bulkload" by simp -lift_definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is RBT_Impl.map_entry +lift_definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is rbt_map_entry by simp lift_definition map :: "('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is RBT_Impl.map @@ -80,11 +80,11 @@ (* TODO: obtain the following lemmas by lifting existing theorems. *) lemma lookup_RBT: - "is_rbt t \ lookup (RBT t) = RBT_Impl.lookup t" + "is_rbt t \ lookup (RBT t) = rbt_lookup t" by (simp add: lookup_def RBT_inverse) lemma lookup_impl_of: - "RBT_Impl.lookup (impl_of t) = lookup t" + "rbt_lookup (impl_of t) = lookup t" by (simp add: lookup_def) lemma entries_impl_of: @@ -101,11 +101,11 @@ lemma lookup_insert [simp]: "lookup (insert k v t) = (lookup t)(k \ v)" - by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of) + by (simp add: insert_def lookup_RBT rbt_lookup_rbt_insert lookup_impl_of) lemma lookup_delete [simp]: "lookup (delete k t) = (lookup t)(k := None)" - by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq) + by (simp add: delete_def lookup_RBT rbt_lookup_rbt_delete lookup_impl_of restrict_complement_singleton_eq) lemma map_of_entries [simp]: "map_of (entries t) = lookup t" @@ -113,19 +113,19 @@ lemma entries_lookup: "entries t1 = entries t2 \ lookup t1 = lookup t2" - by (simp add: entries_def lookup_def entries_lookup) + by (simp add: entries_def lookup_def entries_rbt_lookup) lemma lookup_bulkload [simp]: "lookup (bulkload xs) = map_of xs" - by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload) + by (simp add: bulkload_def lookup_RBT rbt_lookup_rbt_bulkload) lemma lookup_map_entry [simp]: "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))" - by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of) + by (simp add: map_entry_def lookup_RBT rbt_lookup_rbt_map_entry lookup_impl_of) lemma lookup_map [simp]: "lookup (map f t) k = Option.map (f k) (lookup t k)" - by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of) + by (simp add: map_def lookup_RBT rbt_lookup_map lookup_impl_of) lemma fold_fold: "fold f t = List.fold (prod_case f) (entries t)" @@ -140,7 +140,7 @@ by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split) lemma RBT_lookup_empty [simp]: (*FIXME*) - "RBT_Impl.lookup t = Map.empty \ t = RBT_Impl.Empty" + "rbt_lookup t = Map.empty \ t = RBT_Impl.Empty" by (cases t) (auto simp add: fun_eq_iff) lemma lookup_empty_empty [simp]: @@ -149,7 +149,7 @@ lemma sorted_keys [iff]: "sorted (keys t)" - by (simp add: keys_def RBT_Impl.keys_def sorted_entries) + by (simp add: keys_def RBT_Impl.keys_def rbt_sorted_entries) lemma distinct_keys [iff]: "distinct (keys t)"