src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
author wenzelm
Wed Jul 08 21:33:00 2015 +0200 (2015-07-08)
changeset 60696 8304fb4fb823
parent 59582 0fbed69ff081
child 60752 b48830b670a1
permissions -rw-r--r--
clarified context;
     1 (*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 
     4 Proof procedure for the compiler from predicates specified by intro/elim rules to equations.
     5 *)
     6 
     7 signature PREDICATE_COMPILE_PROOF =
     8 sig
     9   type indprem = Predicate_Compile_Aux.indprem;
    10   type mode = Predicate_Compile_Aux.mode
    11   val prove_pred : Predicate_Compile_Aux.options -> theory
    12     -> (string * (term list * indprem list) list) list
    13     -> (string * typ) list -> string -> bool * mode
    14     -> (term list * (indprem * Mode_Inference.mode_derivation) list) list * term
    15     -> Thm.thm
    16 end;
    17 
    18 structure Predicate_Compile_Proof : PREDICATE_COMPILE_PROOF =
    19 struct
    20 
    21 open Predicate_Compile_Aux;
    22 open Core_Data;
    23 open Mode_Inference;
    24 
    25 
    26 (* debug stuff *)
    27 
    28 fun trace_tac ctxt options s =
    29   if show_proof_trace options then print_tac ctxt s else Seq.single;
    30 
    31 fun assert_tac ctxt pos pred =
    32   COND pred all_tac (print_tac ctxt ("Assertion failed" ^ Position.here pos) THEN no_tac);
    33 
    34 
    35 (** special setup for simpset **)
    36 
    37 val HOL_basic_ss' =
    38   simpset_of (put_simpset HOL_basic_ss @{context}
    39     addsimps @{thms simp_thms Pair_eq}
    40     setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
    41     setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI})))
    42 
    43 
    44 (* auxillary functions *)
    45 
    46 (* returns true if t is an application of a datatype constructor *)
    47 (* which then consequently would be splitted *)
    48 fun is_constructor ctxt t =
    49   (case fastype_of t of
    50     Type (s, _) => s <> @{type_name fun} andalso can (Ctr_Sugar.dest_ctr ctxt s) t
    51   | _ => false)
    52 
    53 (* MAJOR FIXME:  prove_params should be simple
    54  - different form of introrule for parameters ? *)
    55 
    56 fun prove_param options ctxt nargs t deriv =
    57   let
    58     val (f, args) = strip_comb (Envir.eta_contract t)
    59     val mode = head_mode_of deriv
    60     val param_derivations = param_derivations_of deriv
    61     val ho_args = ho_args_of mode args
    62     val f_tac =
    63       (case f of
    64         Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
    65            [@{thm eval_pred}, predfun_definition_of ctxt name mode,
    66            @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
    67            @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
    68       | Free _ =>
    69         Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} =>
    70           let
    71             val prems' = maps dest_conjunct_prem (take nargs prems)
    72           in
    73             rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    74           end) ctxt 1
    75       | Abs _ => raise Fail "prove_param: No valid parameter term")
    76   in
    77     REPEAT_DETERM (rtac @{thm ext} 1)
    78     THEN trace_tac ctxt options "prove_param"
    79     THEN f_tac
    80     THEN trace_tac ctxt options "after prove_param"
    81     THEN (REPEAT_DETERM (assume_tac ctxt 1))
    82     THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
    83     THEN REPEAT_DETERM (rtac @{thm refl} 1)
    84   end
    85 
    86 fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
    87   (case strip_comb t of
    88     (Const (name, _), args) =>
    89       let
    90         val mode = head_mode_of deriv
    91         val introrule = predfun_intro_of ctxt name mode
    92         val param_derivations = param_derivations_of deriv
    93         val ho_args = ho_args_of mode args
    94       in
    95         trace_tac ctxt options "before intro rule:"
    96         THEN rtac introrule 1
    97         THEN trace_tac ctxt options "after intro rule"
    98         (* for the right assumption in first position *)
    99         THEN rotate_tac premposition 1
   100         THEN assume_tac ctxt 1
   101         THEN trace_tac ctxt options "parameter goal"
   102         (* work with parameter arguments *)
   103         THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
   104         THEN (REPEAT_DETERM (assume_tac ctxt 1))
   105       end
   106   | (Free _, _) =>
   107       trace_tac ctxt options "proving parameter call.."
   108       THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, concl, ...} =>
   109           let
   110             val param_prem = nth prems premposition
   111             val (param, _) = strip_comb (HOLogic.dest_Trueprop (Thm.prop_of param_prem))
   112             val prems' = maps dest_conjunct_prem (take nargs prems)
   113             fun param_rewrite prem =
   114               param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of prem)))
   115             val SOME rew_eq = find_first param_rewrite prems'
   116             val param_prem' = rewrite_rule ctxt'
   117               (map (fn th => th RS @{thm eq_reflection})
   118                 [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
   119               param_prem
   120           in
   121             rtac param_prem' 1
   122           end) ctxt 1
   123       THEN trace_tac ctxt options "after prove parameter call")
   124 
   125 fun SOLVED tac st = FILTER (fn st' => Thm.nprems_of st' = Thm.nprems_of st - 1) tac st
   126 
   127 fun prove_match options ctxt nargs out_ts =
   128   let
   129     val eval_if_P =
   130       @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp}
   131     fun get_case_rewrite t =
   132       if is_constructor ctxt t then
   133         let
   134           val SOME {case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t)))
   135         in
   136           fold (union Thm.eq_thm) (case_thms :: map get_case_rewrite (snd (strip_comb t))) []
   137         end
   138       else []
   139     val simprules = insert Thm.eq_thm @{thm "unit.case"} (insert Thm.eq_thm @{thm "prod.case"}
   140       (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
   141   (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   142   in
   143     (* make this simpset better! *)
   144     asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1
   145     THEN trace_tac ctxt options "after prove_match:"
   146     THEN (DETERM (TRY
   147            (rtac eval_if_P 1
   148            THEN (SUBPROOF (fn {prems, context = ctxt', ...} =>
   149              (REPEAT_DETERM (rtac @{thm conjI} 1
   150              THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1))))
   151              THEN trace_tac ctxt' options "if condition to be solved:"
   152              THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1
   153              THEN TRY (
   154                 let
   155                   val prems' = maps dest_conjunct_prem (take nargs prems)
   156                 in
   157                   rewrite_goal_tac ctxt'
   158                     (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   159                 end
   160              THEN REPEAT_DETERM (rtac @{thm refl} 1))
   161              THEN trace_tac ctxt' options "after if simp; in SUBPROOF") ctxt 1))))
   162     THEN trace_tac ctxt options "after if simplification"
   163   end;
   164 
   165 
   166 (* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
   167 
   168 fun prove_sidecond ctxt t =
   169   let
   170     fun preds_of t nameTs =
   171       (case strip_comb t of
   172         (Const (name, T), args) =>
   173           if is_registered ctxt name then (name, T) :: nameTs
   174             else fold preds_of args nameTs
   175       | _ => nameTs)
   176     val preds = preds_of t []
   177     val defs = map
   178       (fn (pred, T) => predfun_definition_of ctxt pred
   179         (all_input_of T))
   180         preds
   181   in
   182     simp_tac (put_simpset HOL_basic_ss ctxt
   183       addsimps (@{thms HOL.simp_thms eval_pred} @ defs)) 1
   184     (* need better control here! *)
   185   end
   186 
   187 fun prove_clause options ctxt nargs mode (_, clauses) (ts, moded_ps) =
   188   let
   189     val (in_ts, clause_out_ts) = split_mode mode ts;
   190     fun prove_prems out_ts [] =
   191         (prove_match options ctxt nargs out_ts)
   192         THEN trace_tac ctxt options "before simplifying assumptions"
   193         THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
   194         THEN trace_tac ctxt options "before single intro rule"
   195         THEN Subgoal.FOCUS_PREMS
   196            (fn {context = ctxt', prems, ...} =>
   197             let
   198               val prems' = maps dest_conjunct_prem (take nargs prems)
   199             in
   200               rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   201             end) ctxt 1
   202         THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
   203     | prove_prems out_ts ((p, deriv) :: ps) =
   204         let
   205           val premposition = (find_index (equal p) clauses) + nargs
   206           val mode = head_mode_of deriv
   207           val rest_tac =
   208             rtac @{thm bindI} 1
   209             THEN (case p of Prem t =>
   210               let
   211                 val (_, us) = strip_comb t
   212                 val (_, out_ts''') = split_mode mode us
   213                 val rec_tac = prove_prems out_ts''' ps
   214               in
   215                 trace_tac ctxt options "before clause:"
   216                 (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*)
   217                 THEN trace_tac ctxt options "before prove_expr:"
   218                 THEN prove_expr options ctxt nargs premposition (t, deriv)
   219                 THEN trace_tac ctxt options "after prove_expr:"
   220                 THEN rec_tac
   221               end
   222             | Negprem t =>
   223               let
   224                 val (t, args) = strip_comb t
   225                 val (_, out_ts''') = split_mode mode args
   226                 val rec_tac = prove_prems out_ts''' ps
   227                 val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
   228                 val neg_intro_rule =
   229                   Option.map (fn name =>
   230                     the (predfun_neg_intro_of ctxt name mode)) name
   231                 val param_derivations = param_derivations_of deriv
   232                 val params = ho_args_of mode args
   233               in
   234                 trace_tac ctxt options "before prove_neg_expr:"
   235                 THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
   236                   [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
   237                    @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
   238                 THEN (if (is_some name) then
   239                     trace_tac ctxt options "before applying not introduction rule"
   240                     THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
   241                       rtac (the neg_intro_rule) 1
   242                       THEN rtac (nth prems premposition) 1) ctxt 1
   243                     THEN trace_tac ctxt options "after applying not introduction rule"
   244                     THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
   245                     THEN (REPEAT_DETERM (assume_tac ctxt 1))
   246                   else
   247                     rtac @{thm not_predI'} 1
   248                     (* test: *)
   249                     THEN dtac @{thm sym} 1
   250                     THEN asm_full_simp_tac
   251                       (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1)
   252                     THEN simp_tac
   253                       (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
   254                 THEN rec_tac
   255               end
   256             | Sidecond t =>
   257              rtac @{thm if_predI} 1
   258              THEN trace_tac ctxt options "before sidecond:"
   259              THEN prove_sidecond ctxt t
   260              THEN trace_tac ctxt options "after sidecond:"
   261              THEN prove_prems [] ps)
   262         in (prove_match options ctxt nargs out_ts)
   263             THEN rest_tac
   264         end
   265     val prems_tac = prove_prems in_ts moded_ps
   266   in
   267     trace_tac ctxt options "Proving clause..."
   268     THEN rtac @{thm bindI} 1
   269     THEN rtac @{thm singleI} 1
   270     THEN prems_tac
   271   end
   272 
   273 fun select_sup 1 1 = []
   274   | select_sup _ 1 = [rtac @{thm supI1}]
   275   | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
   276 
   277 fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
   278   let
   279     val T = the (AList.lookup (op =) preds pred)
   280     val nargs = length (binder_types T)
   281     val pred_case_rule = the_elim_of ctxt pred
   282   in
   283     REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
   284     THEN trace_tac ctxt options "before applying elim rule"
   285     THEN etac (predfun_elim_of ctxt pred mode) 1
   286     THEN etac pred_case_rule 1
   287     THEN trace_tac ctxt options "after applying elim rule"
   288     THEN (EVERY (map
   289            (fn i => EVERY' (select_sup (length moded_clauses) i) i)
   290              (1 upto (length moded_clauses))))
   291     THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
   292     THEN trace_tac ctxt options "proved one direction"
   293   end
   294 
   295 
   296 (** Proof in the other direction **)
   297 
   298 fun prove_match2 options ctxt out_ts =
   299   let
   300     fun split_term_tac (Free _) = all_tac
   301       | split_term_tac t =
   302         if is_constructor ctxt t then
   303           let
   304             val SOME {case_thms, split_asm, ...} =
   305               Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t)))
   306             val num_of_constrs = length case_thms
   307             val (_, ts) = strip_comb t
   308           in
   309             trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
   310               " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
   311             THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
   312               THEN (trace_tac ctxt options "after splitting with split_asm rules")
   313             (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
   314               THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
   315               THEN (REPEAT_DETERM_N (num_of_constrs - 1)
   316                 (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
   317             THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2)
   318             THEN (EVERY (map split_term_tac ts))
   319           end
   320       else all_tac
   321   in
   322     split_term_tac (HOLogic.mk_tuple out_ts)
   323     THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt [@{thm "split_if_asm"}] 1)
   324     THEN (etac @{thm botE} 2))))
   325   end
   326 
   327 (* VERY LARGE SIMILIRATIY to function prove_param
   328 -- join both functions
   329 *)
   330 (* TODO: remove function *)
   331 
   332 fun prove_param2 options ctxt t deriv =
   333   let
   334     val (f, args) = strip_comb (Envir.eta_contract t)
   335     val mode = head_mode_of deriv
   336     val param_derivations = param_derivations_of deriv
   337     val ho_args = ho_args_of mode args
   338     val f_tac =
   339       (case f of
   340         Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
   341            (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
   342            :: @{thm "Product_Type.split_conv"}::[])) 1
   343       | Free _ => all_tac
   344       | _ => error "prove_param2: illegal parameter term")
   345   in
   346     trace_tac ctxt options "before simplification in prove_args:"
   347     THEN f_tac
   348     THEN trace_tac ctxt options "after simplification in prove_args"
   349     THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)
   350   end
   351 
   352 fun prove_expr2 options ctxt (t, deriv) =
   353   (case strip_comb t of
   354       (Const (name, _), args) =>
   355         let
   356           val mode = head_mode_of deriv
   357           val param_derivations = param_derivations_of deriv
   358           val ho_args = ho_args_of mode args
   359         in
   360           etac @{thm bindE} 1
   361           THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
   362           THEN trace_tac ctxt options "prove_expr2-before"
   363           THEN etac (predfun_elim_of ctxt name mode) 1
   364           THEN trace_tac ctxt options "prove_expr2"
   365           THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
   366           THEN trace_tac ctxt options "finished prove_expr2"
   367         end
   368       | _ => etac @{thm bindE} 1)
   369 
   370 fun prove_sidecond2 options ctxt t =
   371   let
   372     fun preds_of t nameTs =
   373       (case strip_comb t of
   374         (Const (name, T), args) =>
   375           if is_registered ctxt name then (name, T) :: nameTs
   376             else fold preds_of args nameTs
   377       | _ => nameTs)
   378     val preds = preds_of t []
   379     val defs = map
   380       (fn (pred, T) => predfun_definition_of ctxt pred
   381         (all_input_of T))
   382         preds
   383   in
   384     (* only simplify the one assumption *)
   385     full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
   386     (* need better control here! *)
   387     THEN trace_tac ctxt options "after sidecond2 simplification"
   388   end
   389 
   390 fun prove_clause2 options ctxt pred mode (ts, ps) i =
   391   let
   392     val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
   393     val (in_ts, _) = split_mode mode ts;
   394     val split_simpset =
   395       put_simpset HOL_basic_ss' ctxt
   396       addsimps [@{thm split_eta}, @{thm split_beta},
   397         @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
   398     fun prove_prems2 out_ts [] =
   399       trace_tac ctxt options "before prove_match2 - last call:"
   400       THEN prove_match2 options ctxt out_ts
   401       THEN trace_tac ctxt options "after prove_match2 - last call:"
   402       THEN (etac @{thm singleE} 1)
   403       THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
   404       THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
   405       THEN TRY (
   406         (REPEAT_DETERM (etac @{thm Pair_inject} 1))
   407         THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
   408 
   409         THEN SOLVED (trace_tac ctxt options "state before applying intro rule:"
   410         THEN (rtac pred_intro_rule
   411         (* How to handle equality correctly? *)
   412         THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching")
   413         THEN' (assume_tac ctxt ORELSE'
   414           ((CHANGED o asm_full_simp_tac split_simpset) THEN'
   415             (TRY o assume_tac ctxt))) THEN'
   416           (K (trace_tac ctxt options "state after pre-simplification:"))
   417         THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1))
   418     | prove_prems2 out_ts ((p, deriv) :: ps) =
   419       let
   420         val mode = head_mode_of deriv
   421         val rest_tac =
   422           (case p of
   423             Prem t =>
   424               let
   425                 val (_, us) = strip_comb t
   426                 val (_, out_ts''') = split_mode mode us
   427                 val rec_tac = prove_prems2 out_ts''' ps
   428               in
   429                 (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
   430               end
   431           | Negprem t =>
   432               let
   433                 val (_, args) = strip_comb t
   434                 val (_, out_ts''') = split_mode mode args
   435                 val rec_tac = prove_prems2 out_ts''' ps
   436                 val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
   437                 val param_derivations = param_derivations_of deriv
   438                 val ho_args = ho_args_of mode args
   439               in
   440                 trace_tac ctxt options "before neg prem 2"
   441                 THEN etac @{thm bindE} 1
   442                 THEN (if is_some name then
   443                     full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
   444                       [predfun_definition_of ctxt (the name) mode]) 1
   445                     THEN etac @{thm not_predE} 1
   446                     THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
   447                     THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
   448                   else
   449                     etac @{thm not_predE'} 1)
   450                 THEN rec_tac
   451               end
   452           | Sidecond t =>
   453               etac @{thm bindE} 1
   454               THEN etac @{thm if_predE} 1
   455               THEN prove_sidecond2 options ctxt t
   456               THEN prove_prems2 [] ps)
   457       in
   458         trace_tac ctxt options "before prove_match2:"
   459         THEN prove_match2 options ctxt out_ts
   460         THEN trace_tac ctxt options "after prove_match2:"
   461         THEN rest_tac
   462       end
   463     val prems_tac = prove_prems2 in_ts ps
   464   in
   465     trace_tac ctxt options "starting prove_clause2"
   466     THEN etac @{thm bindE} 1
   467     THEN (etac @{thm singleE'} 1)
   468     THEN (TRY (etac @{thm Pair_inject} 1))
   469     THEN trace_tac ctxt options "after singleE':"
   470     THEN prems_tac
   471   end;
   472 
   473 fun prove_other_direction options ctxt pred mode moded_clauses =
   474   let
   475     fun prove_clause clause i =
   476       (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
   477       THEN (prove_clause2 options ctxt pred mode clause i)
   478   in
   479     (DETERM (TRY (rtac @{thm unit.induct} 1)))
   480      THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
   481      THEN (rtac (predfun_intro_of ctxt pred mode) 1)
   482      THEN (REPEAT_DETERM (rtac @{thm refl} 2))
   483      THEN (
   484        if null moded_clauses then etac @{thm botE} 1
   485        else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
   486   end
   487 
   488 
   489 (** proof procedure **)
   490 
   491 fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) =
   492   let
   493     val ctxt = Proof_Context.init_global thy   (* FIXME proper context!? *)
   494     val clauses = (case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => [])
   495   in
   496     Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
   497       (if not (skip_proof options) then
   498         (fn _ =>
   499         rtac @{thm pred_iffI} 1
   500         THEN trace_tac ctxt options "after pred_iffI"
   501         THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
   502         THEN trace_tac ctxt options "proved one direction"
   503         THEN prove_other_direction options ctxt pred mode moded_clauses
   504         THEN trace_tac ctxt options "proved other direction")
   505       else (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)))
   506   end
   507 
   508 end