1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 28 11:59:50 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 28 11:59:51 2010 +0200
     1.3 @@ -1483,6 +1483,21 @@
     1.4  
     1.5  thm detect_switches9.equation
     1.6  
     1.7 +text {* The higher-order predicate r is in an output term *}
     1.8 +
     1.9 +datatype result = Result bool
    1.10 +
    1.11 +inductive fixed_relation :: "'a => bool"
    1.12 +
    1.13 +inductive test_relation_in_output_terms :: "('a => bool) => 'a => result => bool"
    1.14 +where
    1.15 +  "test_relation_in_output_terms r x (Result (r x))"
    1.16 +| "test_relation_in_output_terms r x (Result (fixed_relation x))"
    1.17 +
    1.18 +code_pred test_relation_in_output_terms .
    1.19 +
    1.20 +
    1.21 +thm test_relation_in_output_terms.equation
    1.22  
    1.23  
    1.24  end

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 11:59:50 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 28 11:59:51 2010 +0200
     2.3 @@ -1717,9 +1717,11 @@
     2.4                fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
     2.5              val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
     2.6                out_ts'' (names', map (rpair []) vs);
     2.7 +            val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments
     2.8 +              ctxt param_modes) out_ts
     2.9            in
    2.10              compile_match constr_vs (eqs @ eqs') out_ts'''
    2.11 -              (mk_single compfuns (HOLogic.mk_tuple out_ts))
    2.12 +              (mk_single compfuns (HOLogic.mk_tuple processed_out_ts))
    2.13            end
    2.14        | compile_prems out_ts vs names ((p, deriv) :: ps) =
    2.15            let
    2.16 @@ -2274,12 +2276,14 @@
    2.17      if valid_expr expr then
    2.18        ((*tracing "expression is valid";*) Seq.single st)
    2.19      else
    2.20 -      ((*tracing "expression is not valid";*) Seq.empty) (*error "check_format: wrong format"*)
    2.21 +      ((*tracing "expression is not valid";*) Seq.empty) (* error "check_format: wrong format" *)
    2.22    end
    2.23  
    2.24 -fun prove_match options ctxt out_ts =
    2.25 +fun prove_match options ctxt nargs out_ts =
    2.26    let
    2.27      val thy = ProofContext.theory_of ctxt
    2.28 +    val eval_if_P =
    2.29 +      @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} 
    2.30      fun get_case_rewrite t =
    2.31        if (is_constructor thy t) then let
    2.32          val case_rewrites = (#case_rewrites (Datatype.the_info thy
    2.33 @@ -2293,10 +2297,20 @@
    2.34       (* make this simpset better! *)
    2.35      asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
    2.36      THEN print_tac options "after prove_match:"
    2.37 -    THEN (DETERM (TRY (EqSubst.eqsubst_tac ctxt [0] [@{thm HOL.if_P}] 1
    2.38 +    THEN (DETERM (TRY (rtac eval_if_P 1
    2.39             THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
    2.40             THEN print_tac options "if condition to be solved:"
    2.41 -           THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac options "after if simp; in SOLVED:"))
    2.42 +           THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1
    2.43 +           THEN Subgoal.FOCUS_PREMS
    2.44 +             (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
    2.45 +              let
    2.46 +                val prems' = maps dest_conjunct_prem (take nargs prems)
    2.47 +              in
    2.48 +                MetaSimplifier.rewrite_goal_tac
    2.49 +                  (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    2.50 +              end) ctxt 1
    2.51 +           THEN REPEAT_DETERM (rtac @{thm refl} 1)
    2.52 +           THEN print_tac options "after if simp; in SOLVED:"))
    2.53             THEN check_format thy
    2.54             THEN print_tac options "after if simplification - a TRY block")))
    2.55      THEN print_tac options "after if simplification"
    2.56 @@ -2326,10 +2340,18 @@
    2.57    let
    2.58      val (in_ts, clause_out_ts) = split_mode mode ts;
    2.59      fun prove_prems out_ts [] =
    2.60 -      (prove_match options ctxt out_ts)
    2.61 +      (prove_match options ctxt nargs out_ts)
    2.62        THEN print_tac options "before simplifying assumptions"
    2.63        THEN asm_full_simp_tac HOL_basic_ss' 1
    2.64        THEN print_tac options "before single intro rule"
    2.65 +      THEN Subgoal.FOCUS_PREMS
    2.66 +             (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
    2.67 +              let
    2.68 +                val prems' = maps dest_conjunct_prem (take nargs prems)
    2.69 +              in
    2.70 +                MetaSimplifier.rewrite_goal_tac
    2.71 +                  (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    2.72 +              end) ctxt 1
    2.73        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
    2.74      | prove_prems out_ts ((p, deriv) :: ps) =
    2.75        let
    2.76 @@ -2388,7 +2410,7 @@
    2.77             THEN prove_sidecond ctxt t
    2.78             THEN print_tac options "after sidecond:"
    2.79             THEN prove_prems [] ps)
    2.80 -      in (prove_match options ctxt out_ts)
    2.81 +      in (prove_match options ctxt nargs out_ts)
    2.82            THEN rest_tac
    2.83        end;
    2.84      val prems_tac = prove_prems in_ts moded_ps