added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations

--- a/src/HOL/HOL.thy	Tue Apr 20 13:44:28 2010 -0700
+++ b/src/HOL/HOL.thy	Wed Apr 21 12:10:52 2010 +0200
@@ -2061,19 +2061,22 @@
   val name = "code_pred_def"
   val description = "alternative definitions of constants for the Predicate Compiler"
 )
-*}
-
-ML {*
 structure Predicate_Compile_Inline_Defs = Named_Thms
 (
   val name = "code_pred_inline"
   val description = "inlining definitions for the Predicate Compiler"
 )
+structure Predicate_Compile_Simps = Named_Thms
+(
+  val name = "code_pred_simp"
+  val description = "simplification rules for the optimisations in the Predicate Compiler"
+)
 *}
 
 setup {*
   Predicate_Compile_Alternative_Defs.setup
   #> Predicate_Compile_Inline_Defs.setup
+  #> Predicate_Compile_Simps.setup
 *}
 
 

--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Apr 20 13:44:28 2010 -0700
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Apr 21 12:10:52 2010 +0200
@@ -141,7 +141,7 @@
   "less_nat 0 (Suc y)"
 | "less_nat x y ==> less_nat (Suc x) (Suc y)"
 
-lemma [code_pred_inline]:
+lemma less_nat[code_pred_inline]:
   "x < y = less_nat x y"
 apply (rule iffI)
 apply (induct x arbitrary: y)
@@ -228,6 +228,16 @@
     done
 qed
 
+section {* Simplification rules for optimisation *}
+
+lemma [code_pred_simp]: "\<not> False == True"
+by auto
+
+lemma [code_pred_simp]: "\<not> True == False"
+by auto
+
+lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
+unfolding less_nat[symmetric] by auto
 
 
 end
\ No newline at end of file

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Apr 20 13:44:28 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 21 12:10:52 2010 +0200
@@ -18,17 +18,9 @@
 val present_graph = Unsynchronized.ref false
 
 val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref
-  
 
 open Predicate_Compile_Aux;
 
-(* Some last processing *)
-
-fun remove_pointless_clauses intro =
-  if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
-    []
-  else [intro]
-
 fun print_intross options thy msg intross =
   if show_intermediate_results options then
     tracing (msg ^ 
@@ -121,9 +113,11 @@
       val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
       val _ = print_step options ("Looking for specialisations in " ^ commas (map fst intross8) ^ "...")
       val (intross9, thy3) = Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
-      val _ = print_intross options thy3 "introduction rules before registering: " intross9
+      val _ = print_intross options thy3 "introduction rules after specialisations: " intross9
+      val intross10 = map_specs (map_filter (peephole_optimisation thy3)) intross9
+      val _ = print_intross options thy3 "introduction rules before registering: " intross10
       val _ = print_step options "Registering introduction rules..."
-      val thy4 = fold Predicate_Compile_Core.register_intros intross9 thy3
+      val thy4 = fold Predicate_Compile_Core.register_intros intross10 thy3
     in
       thy4
     end;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Apr 20 13:44:28 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 12:10:52 2010 +0200
@@ -135,6 +135,8 @@
   val expand_tuples : theory -> thm -> thm
   val eta_contract_ho_arguments : theory -> thm -> thm
   val remove_equalities : theory -> thm -> thm
+  val remove_pointless_clauses : thm -> thm list
+  val peephole_optimisation : theory -> thm -> thm option
 end;
 
 structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
@@ -513,6 +515,20 @@
     (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
   end;
 
+fun map_premises f intro =
+  let
+    val (premises, head) = Logic.strip_horn intro
+  in
+    Logic.list_implies (map f premises, head)
+  end
+
+fun map_filter_premises f intro =
+  let
+    val (premises, head) = Logic.strip_horn intro
+  in
+    Logic.list_implies (map_filter f premises, head)
+  end
+
 fun maps_premises f intro =
   let
     val (premises, head) = Logic.strip_horn intro
@@ -810,4 +826,25 @@
     map_term thy remove_eqs intro
   end
 
+(* Some last processing *)
+
+fun remove_pointless_clauses intro =
+  if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
+    []
+  else [intro]
+
+(* some peephole optimisations *)
+
+fun peephole_optimisation thy intro =
+  let
+    val process = MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init thy))
+    fun process_False intro_t =
+      if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
+    fun process_True intro_t =
+      map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t
+  in
+    Option.map (Skip_Proof.make_thm thy)
+      (process_False (process_True (prop_of (process intro))))
+  end
+
 end;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Tue Apr 20 13:44:28 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Apr 21 12:10:52 2010 +0200
@@ -107,7 +107,9 @@
     val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
       [list_comb (pred, pats), list_comb (specialised_const, result_pats)]
     val thy'' = Specialisations.map (Item_Net.update (t, specialised_t)) thy'
-    val ([spec], thy''') = find_specialisations black_list [(constname, exported_intros)] thy''
+    val optimised_intros =
+      map_filter (Predicate_Compile_Aux.peephole_optimisation thy'') exported_intros
+    val ([spec], thy''') = find_specialisations black_list [(constname, optimised_intros)] thy''
     val thy'''' = Predicate_Compile_Core.register_intros spec thy'''
   in
     thy''''