# HG changeset patch
# User bulwahn
# Date 1258615551 -3600
# Node ID 1344e9bb611e67c5235860017cead2f5d04ea848
# Parent  9aa8e961f850841f119224453160ee82c3550315
changing the proof procedure for parameters; adding a testcase for negation and parameters; adopting print_tac to the latest function print_tac' in the predicate compiler

diff -r 9aa8e961f850 -r 1344e9bb611e src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 19 08:25:47 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 19 08:25:51 2009 +0100
@@ -1674,8 +1674,8 @@
 
 (* MAJOR FIXME:  prove_params should be simple
  - different form of introrule for parameters ? *)
-fun prove_param thy NONE t = TRY (rtac @{thm refl} 1)
-  | prove_param thy (m as SOME (Mode (mode, is, ms))) t =
+fun prove_param options thy NONE t = TRY (rtac @{thm refl} 1)
+  | prove_param options thy (m as SOME (Mode (mode, is, ms))) t =
   let
     val  (f, args) = strip_comb (Envir.eta_contract t)
     val (params, _) = chop (length ms) args
@@ -1687,16 +1687,15 @@
     | Free _ => TRY (rtac @{thm refl} 1)
     | Abs _ => error "prove_param: No valid parameter term"
   in
-    REPEAT_DETERM (etac @{thm thin_rl} 1)
-    THEN REPEAT_DETERM (rtac @{thm ext} 1)
-    THEN print_tac "prove_param"
+    REPEAT_DETERM (rtac @{thm ext} 1)
+    THEN print_tac' options "prove_param"
     THEN f_tac
-    THEN print_tac "after simplification in prove_args"
-    THEN (EVERY (map2 (prove_param thy) ms params))
+    THEN print_tac' options "after simplification in prove_args"
+    THEN (EVERY (map2 (prove_param options thy) ms params))
     THEN (REPEAT_DETERM (atac 1))
   end
 
-fun prove_expr thy (Mode (mode, is, ms), t, us) (premposition : int) =
+fun prove_expr options thy (Mode (mode, is, ms), t, us) (premposition : int) =
   case strip_comb t of
     (Const (name, T), args) =>  
       let
@@ -1704,16 +1703,16 @@
         val (args1, args2) = chop (length ms) args
       in
         rtac @{thm bindI} 1
-        THEN print_tac "before intro rule:"
+        THEN print_tac' options "before intro rule:"
         (* for the right assumption in first position *)
         THEN rotate_tac premposition 1
         THEN debug_tac (Display.string_of_thm (ProofContext.init thy) introrule)
         THEN rtac introrule 1
-        THEN print_tac "after intro rule"
+        THEN print_tac' options "after intro rule"
         (* work with parameter arguments *)
-        THEN (atac 1)
-        THEN (print_tac "parameter goal")
-        THEN (EVERY (map2 (prove_param thy) ms args1))
+        THEN atac 1
+        THEN print_tac' options "parameter goal"
+        THEN (EVERY (map2 (prove_param options thy) ms args1))
         THEN (REPEAT_DETERM (atac 1))
       end
   | _ => rtac @{thm bindI} 1
@@ -1721,7 +1720,7 @@
       (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
          @{thm "snd_conv"}, @{thm pair_collapse}]) 1
     THEN (atac 1)
-    THEN print_tac "after prove parameter call"
+    THEN print_tac' options "after prove parameter call"
     
 
 fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; 
@@ -1773,9 +1772,9 @@
     val (in_ts, clause_out_ts) = split_smode is ts;
     fun prove_prems out_ts [] =
       (prove_match thy out_ts)
-      THEN print_tac "before simplifying assumptions"
+      THEN print_tac' options "before simplifying assumptions"
       THEN asm_full_simp_tac HOL_basic_ss' 1
-      THEN print_tac "before single intro rule"
+      THEN print_tac' options "before single intro rule"
       THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
     | prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
       let
@@ -1785,11 +1784,11 @@
               val (_, out_ts''') = split_smode is us
               val rec_tac = prove_prems out_ts''' ps
             in
-              print_tac "before clause:"
+              print_tac' options "before clause:"
               THEN asm_simp_tac HOL_basic_ss 1
-              THEN print_tac "before prove_expr:"
-              THEN prove_expr thy (mode, t, us) premposition
-              THEN print_tac "after prove_expr:"
+              THEN print_tac' options "before prove_expr:"
+              THEN prove_expr options thy (mode, t, us) premposition
+              THEN print_tac' options "after prove_expr:"
               THEN rec_tac
             end
           | Negprem (us, t) =>
@@ -1800,13 +1799,18 @@
               val (_, params) = strip_comb t
             in
               rtac @{thm bindI} 1
+              THEN print_tac' options "before prove_neg_expr:"
               THEN (if (is_some name) then
-                  simp_tac (HOL_basic_ss addsimps
+                  print_tac' options ("before unfolding definition " ^
+                    (Display.string_of_thm_global thy
+                      (predfun_definition_of thy (the name) (iss, is))))
+                  THEN simp_tac (HOL_basic_ss addsimps
                     [predfun_definition_of thy (the name) (iss, is)]) 1
                   THEN rtac @{thm not_predI} 1
+                  THEN print_tac' options "after applying rule not_predI"
                   THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
                   THEN (REPEAT_DETERM (atac 1))
-                  THEN (EVERY (map2 (prove_param thy) param_modes params))
+                  THEN (EVERY (map2 (prove_param options thy) param_modes params))
                 else
                   rtac @{thm not_predI'} 1)
                   THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
@@ -1815,9 +1819,9 @@
           | Sidecond t =>
            rtac @{thm bindI} 1
            THEN rtac @{thm if_predI} 1
-           THEN print_tac "before sidecond:"
+           THEN print_tac' options "before sidecond:"
            THEN prove_sidecond thy modes t
-           THEN print_tac "after sidecond:"
+           THEN print_tac' options "after sidecond:"
            THEN prove_prems [] ps)
       in (prove_match thy out_ts)
           THEN rest_tac
@@ -1848,7 +1852,7 @@
            (fn i => EVERY' (select_sup (length moded_clauses) i) i) 
              (1 upto (length moded_clauses))))
     THEN (EVERY (map2 (prove_clause options thy nargs modes mode) clauses moded_clauses))
-    THEN print_tac "proved one direction"
+    THEN print_tac' options "proved one direction"
   end;
 
 (** Proof in the other direction **)
diff -r 9aa8e961f850 -r 1344e9bb611e src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 19 08:25:47 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 19 08:25:51 2009 +0100
@@ -479,6 +479,8 @@
 
 subsection {* transitive predicate *}
 
+text {* Also look at the tabled transitive closure in the Library *}
+
 code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
   (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool,
   (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
@@ -512,6 +514,28 @@
 values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
 values 20 "{(n, m). tranclp succ n m}"
 
+inductive example_graph :: "int => int => bool"
+where
+  "example_graph 0 1"
+| "example_graph 1 2"
+| "example_graph 1 3"
+| "example_graph 4 7"
+| "example_graph 4 5"
+| "example_graph 5 6"
+| "example_graph 7 6"
+| "example_graph 7 8"
+ 
+inductive not_reachable_in_example_graph :: "int => int => bool"
+where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
+
+code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
+
+thm not_reachable_in_example_graph.equation
+
+value "not_reachable_in_example_graph 0 3"
+value "not_reachable_in_example_graph 4 8"
+value "not_reachable_in_example_graph 5 6"
+
 subsection {* IMP *}
 
 types