# HG changeset patch
# User bulwahn
# Date 1283853113 -7200
# Node ID edaf5a6ffa999576e730ae991c85c268750c2cb2
# Parent  a2775776be3f4524fe16e94ff83576b169600e56
using linear find_least instead of sorting in the mode analysis of the predicate compiler

diff -r a2775776be3f -r edaf5a6ffa99 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -187,7 +187,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-(*quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10]*)
+  quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample]
 oops
 
 subsection {* Lambda *}
diff -r a2775776be3f -r edaf5a6ffa99 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 07 11:51:53 2010 +0200
@@ -1123,9 +1123,13 @@
       raise Fail "all_input_of: not a predicate"
   end
 
-fun partial_hd [] = NONE
-  | partial_hd (x :: xs) = SOME x
-
+fun find_least ord xs =
+  let
+    fun find' x y = (case y of NONE => SOME x | SOME y' => if ord (x, y') = LESS then SOME x else y) 
+  in
+    fold find' xs NONE
+  end
+  
 fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
 val terms_vs = distinct (op =) o maps term_vs;
 
@@ -1362,17 +1366,16 @@
 fun select_mode_prem (mode_analysis_options : mode_analysis_options) (ctxt : Proof.context) pred
   pol (modes, (pos_modes, neg_modes)) vs ps =
   let
-    fun choose_mode_of_prem (Prem t) = partial_hd
-        (sort (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t))
+    fun choose_mode_of_prem (Prem t) =
+          find_least (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t)
       | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
-      | choose_mode_of_prem (Negprem t) = partial_hd
-          (sort (deriv_ord ctxt (not pol) pred modes t)
+      | choose_mode_of_prem (Negprem t) = find_least (deriv_ord ctxt (not pol) pred modes t)
           (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
-             (all_derivations_of ctxt neg_modes vs t)))
+             (all_derivations_of ctxt neg_modes vs t))
       | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem ctxt p)
   in
     if #reorder_premises mode_analysis_options then
-      partial_hd (sort (premise_ord ctxt pol pred modes) (ps ~~ map choose_mode_of_prem ps))
+      find_least (premise_ord ctxt pol pred modes) (ps ~~ map choose_mode_of_prem ps)
     else
       SOME (hd ps, choose_mode_of_prem (hd ps))
   end