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