# HG changeset patch
# User bulwahn
# Date 1285667991 -7200
# Node ID 02fb709ab3cb65d2fdce676844b2ab7979b66ea8
# Parent  c2a76ec6e2d9ac3f3b89c96300bb5e6e4dacdb3c
handling higher-order relations in output terms; improving proof procedure; added test case

diff -r c2a76ec6e2d9 -r 02fb709ab3cb src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 28 11:59:50 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 28 11:59:51 2010 +0200
@@ -1483,6 +1483,21 @@
 
 thm detect_switches9.equation
 
+text {* The higher-order predicate r is in an output term *}
+
+datatype result = Result bool
+
+inductive fixed_relation :: "'a => bool"
+
+inductive test_relation_in_output_terms :: "('a => bool) => 'a => result => bool"
+where
+  "test_relation_in_output_terms r x (Result (r x))"
+| "test_relation_in_output_terms r x (Result (fixed_relation x))"
+
+code_pred test_relation_in_output_terms .
+
+
+thm test_relation_in_output_terms.equation
 
 
 end
diff -r c2a76ec6e2d9 -r 02fb709ab3cb src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 11:59:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 11:59:51 2010 +0200
@@ -1717,9 +1717,11 @@
               fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
             val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
               out_ts'' (names', map (rpair []) vs);
+            val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments
+              ctxt param_modes) out_ts
           in
             compile_match constr_vs (eqs @ eqs') out_ts'''
-              (mk_single compfuns (HOLogic.mk_tuple out_ts))
+              (mk_single compfuns (HOLogic.mk_tuple processed_out_ts))
           end
       | compile_prems out_ts vs names ((p, deriv) :: ps) =
           let
@@ -2274,12 +2276,14 @@
     if valid_expr expr then
       ((*tracing "expression is valid";*) Seq.single st)
     else
-      ((*tracing "expression is not valid";*) Seq.empty) (*error "check_format: wrong format"*)
+      ((*tracing "expression is not valid";*) Seq.empty) (* error "check_format: wrong format" *)
   end
 
-fun prove_match options ctxt out_ts =
+fun prove_match options ctxt nargs out_ts =
   let
     val thy = ProofContext.theory_of ctxt
+    val eval_if_P =
+      @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} 
     fun get_case_rewrite t =
       if (is_constructor thy t) then let
         val case_rewrites = (#case_rewrites (Datatype.the_info thy
@@ -2293,10 +2297,20 @@
      (* make this simpset better! *)
     asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
     THEN print_tac options "after prove_match:"
-    THEN (DETERM (TRY (EqSubst.eqsubst_tac ctxt [0] [@{thm HOL.if_P}] 1
+    THEN (DETERM (TRY (rtac eval_if_P 1
            THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
            THEN print_tac options "if condition to be solved:"
-           THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac options "after if simp; in SOLVED:"))
+           THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1
+           THEN Subgoal.FOCUS_PREMS
+             (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+              let
+                val prems' = maps dest_conjunct_prem (take nargs prems)
+              in
+                MetaSimplifier.rewrite_goal_tac
+                  (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+              end) ctxt 1
+           THEN REPEAT_DETERM (rtac @{thm refl} 1)
+           THEN print_tac options "after if simp; in SOLVED:"))
            THEN check_format thy
            THEN print_tac options "after if simplification - a TRY block")))
     THEN print_tac options "after if simplification"
@@ -2326,10 +2340,18 @@
   let
     val (in_ts, clause_out_ts) = split_mode mode ts;
     fun prove_prems out_ts [] =
-      (prove_match options ctxt out_ts)
+      (prove_match options ctxt nargs out_ts)
       THEN print_tac options "before simplifying assumptions"
       THEN asm_full_simp_tac HOL_basic_ss' 1
       THEN print_tac options "before single intro rule"
+      THEN Subgoal.FOCUS_PREMS
+             (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+              let
+                val prems' = maps dest_conjunct_prem (take nargs prems)
+              in
+                MetaSimplifier.rewrite_goal_tac
+                  (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+              end) ctxt 1
       THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
     | prove_prems out_ts ((p, deriv) :: ps) =
       let
@@ -2388,7 +2410,7 @@
            THEN prove_sidecond ctxt t
            THEN print_tac options "after sidecond:"
            THEN prove_prems [] ps)
-      in (prove_match options ctxt out_ts)
+      in (prove_match options ctxt nargs out_ts)
           THEN rest_tac
       end;
     val prems_tac = prove_prems in_ts moded_ps