# HG changeset patch # User wenzelm # Date 1397035961 -7200 # Node ID 16d00478b518fa2a8a332eef3196026d65ae7a44 # Parent 884e8f37492c2a218cefd5837dd7b9643cec2822 more conventional tactic programming; tuned; diff -r 884e8f37492c -r 16d00478b518 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Apr 09 10:44:06 2014 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Apr 09 11:32:41 2014 +0200 @@ -25,20 +25,11 @@ (* debug stuff *) -fun print_tac options s = - if show_proof_trace options then Tactical.print_tac s else Seq.single; - - -(** auxiliary **) +fun trace_tac options s = + if show_proof_trace options then print_tac s else Seq.single; -datatype assertion = Max_number_of_subgoals of int - -fun assert_tac (Max_number_of_subgoals i) st = - if (nprems_of st <= i) then Seq.single st - else - raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :\n" ^ - Pretty.string_of (Pretty.chunks - (Goal_Display.pretty_goals_without_context st))) +fun assert_tac pos pred = + COND pred all_tac (print_tac ("Assertion failed" ^ Position.here pos) THEN no_tac); (** special setup for simpset **) @@ -75,7 +66,7 @@ @{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 | Free _ => - Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} => + Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} => let val prems' = maps dest_conjunct_prem (take nargs prems) in @@ -84,9 +75,9 @@ | Abs _ => raise Fail "prove_param: No valid parameter term") in REPEAT_DETERM (rtac @{thm ext} 1) - THEN print_tac options "prove_param" - THEN f_tac - THEN print_tac options "after prove_param" + THEN trace_tac options "prove_param" + THEN f_tac + THEN trace_tac options "after prove_param" THEN (REPEAT_DETERM (atac 1)) THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations)) THEN REPEAT_DETERM (rtac @{thm refl} 1) @@ -101,20 +92,20 @@ val param_derivations = param_derivations_of deriv val ho_args = ho_args_of mode args in - print_tac options "before intro rule:" + trace_tac options "before intro rule:" THEN rtac introrule 1 - THEN print_tac options "after intro rule" + THEN trace_tac options "after intro rule" (* for the right assumption in first position *) THEN rotate_tac premposition 1 THEN atac 1 - THEN print_tac options "parameter goal" + THEN trace_tac options "parameter goal" (* work with parameter arguments *) THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations)) THEN (REPEAT_DETERM (atac 1)) end | (Free _, _) => - print_tac options "proving parameter call.." - THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} => + trace_tac options "proving parameter call.." + THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, concl, ...} => let val param_prem = nth prems premposition val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem)) @@ -129,14 +120,14 @@ in rtac param_prem' 1 end) ctxt 1 - THEN print_tac options "after prove parameter call") + THEN trace_tac options "after prove parameter call") fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st fun prove_match options ctxt nargs out_ts = let val eval_if_P = - @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} + @{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 ctxt t then let @@ -151,13 +142,13 @@ in (* make this simpset better! *) asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1 - THEN print_tac options "after prove_match:" - THEN (DETERM (TRY + THEN trace_tac options "after prove_match:" + THEN (DETERM (TRY (rtac eval_if_P 1 - THEN (SUBPROOF (fn {context, params, prems, asms, concl, schematics} => + THEN (SUBPROOF (fn {prems, ...} => (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)))) - THEN print_tac options "if condition to be solved:" + THEN trace_tac options "if condition to be solved:" THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1 THEN TRY ( let @@ -167,8 +158,8 @@ (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 end THEN REPEAT_DETERM (rtac @{thm refl} 1)) - THEN print_tac options "after if simp; in SUBPROOF") ctxt 1)))) - THEN print_tac options "after if simplification" + THEN trace_tac options "after if simp; in SUBPROOF") ctxt 1)))) + THEN trace_tac options "after if simplification" end; @@ -187,7 +178,7 @@ (fn (pred, T) => predfun_definition_of ctxt pred (all_input_of T)) preds - in + in simp_tac (put_simpset HOL_basic_ss ctxt addsimps (@{thms HOL.simp_thms eval_pred} @ defs)) 1 (* need better control here! *) @@ -198,11 +189,11 @@ val (in_ts, clause_out_ts) = split_mode mode ts; fun prove_prems out_ts [] = (prove_match options ctxt nargs out_ts) - THEN print_tac options "before simplifying assumptions" + THEN trace_tac options "before simplifying assumptions" THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1 - THEN print_tac options "before single intro rule" + THEN trace_tac options "before single intro rule" THEN Subgoal.FOCUS_PREMS - (fn {context = ctxt', params, prems, asms, concl, schematics} => + (fn {context = ctxt', prems, ...} => let val prems' = maps dest_conjunct_prem (take nargs prems) in @@ -221,11 +212,11 @@ val (_, out_ts''') = split_mode mode us val rec_tac = prove_prems out_ts''' ps in - print_tac options "before clause:" + trace_tac options "before clause:" (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*) - THEN print_tac options "before prove_expr:" + THEN trace_tac options "before prove_expr:" THEN prove_expr options ctxt nargs premposition (t, deriv) - THEN print_tac options "after prove_expr:" + THEN trace_tac options "after prove_expr:" THEN rec_tac end | Negprem t => @@ -240,17 +231,16 @@ val param_derivations = param_derivations_of deriv val params = ho_args_of mode args in - print_tac options "before prove_neg_expr:" + trace_tac options "before prove_neg_expr:" THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 THEN (if (is_some name) then - print_tac options "before applying not introduction rule" - THEN Subgoal.FOCUS_PREMS - (fn {context, params = params, prems, asms, concl, schematics} => - rtac (the neg_intro_rule) 1 - THEN rtac (nth prems premposition) 1) ctxt 1 - THEN print_tac options "after applying not introduction rule" + trace_tac options "before applying not introduction rule" + THEN Subgoal.FOCUS_PREMS (fn {prems, ...} => + rtac (the neg_intro_rule) 1 + THEN rtac (nth prems premposition) 1) ctxt 1 + THEN trace_tac options "after applying not introduction rule" THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations)) THEN (REPEAT_DETERM (atac 1)) else @@ -265,16 +255,16 @@ end | Sidecond t => rtac @{thm if_predI} 1 - THEN print_tac options "before sidecond:" + THEN trace_tac options "before sidecond:" THEN prove_sidecond ctxt t - THEN print_tac options "after sidecond:" + THEN trace_tac options "after sidecond:" THEN prove_prems [] ps) in (prove_match options ctxt nargs out_ts) THEN rest_tac end val prems_tac = prove_prems in_ts moded_ps in - print_tac options "Proving clause..." + trace_tac options "Proving clause..." THEN rtac @{thm bindI} 1 THEN rtac @{thm singleI} 1 THEN prems_tac @@ -291,15 +281,15 @@ val pred_case_rule = the_elim_of ctxt pred in REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})) - THEN print_tac options "before applying elim rule" + THEN trace_tac options "before applying elim rule" THEN etac (predfun_elim_of ctxt pred mode) 1 THEN etac pred_case_rule 1 - THEN print_tac options "after applying elim rule" + THEN trace_tac options "after applying elim rule" THEN (EVERY (map - (fn i => EVERY' (select_sup (length moded_clauses) i) i) + (fn i => EVERY' (select_sup (length moded_clauses) i) i) (1 upto (length moded_clauses)))) THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses)) - THEN print_tac options "proved one direction" + THEN trace_tac options "proved one direction" end @@ -316,15 +306,15 @@ val num_of_constrs = length case_thms val (_, ts) = strip_comb t in - print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ + trace_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm) THEN TRY (Splitter.split_asm_tac [split_asm] 1 - THEN (print_tac options "after splitting with split_asm rules") + THEN (trace_tac options "after splitting with split_asm rules") (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1) THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*) THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))) - THEN (assert_tac (Max_number_of_subgoals 2)) + THEN assert_tac @{here} (fn st => Thm.nprems_of st <= 2) THEN (EVERY (map split_term_tac ts)) end else all_tac @@ -334,7 +324,7 @@ THEN (etac @{thm botE} 2)))) end -(* VERY LARGE SIMILIRATIY to function prove_param +(* VERY LARGE SIMILIRATIY to function prove_param -- join both functions *) (* TODO: remove function *) @@ -347,19 +337,19 @@ val ho_args = ho_args_of mode args val f_tac = (case f of - Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps + Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (@{thm eval_pred}::(predfun_definition_of ctxt name mode) :: @{thm "Product_Type.split_conv"}::[])) 1 | Free _ => all_tac | _ => error "prove_param2: illegal parameter term") in - print_tac options "before simplification in prove_args:" + trace_tac options "before simplification in prove_args:" THEN f_tac - THEN print_tac options "after simplification in prove_args" + THEN trace_tac options "after simplification in prove_args" THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations) end -fun prove_expr2 options ctxt (t, deriv) = +fun prove_expr2 options ctxt (t, deriv) = (case strip_comb t of (Const (name, _), args) => let @@ -369,11 +359,11 @@ in etac @{thm bindE} 1 THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))) - THEN print_tac options "prove_expr2-before" + THEN trace_tac options "prove_expr2-before" THEN etac (predfun_elim_of ctxt name mode) 1 - THEN print_tac options "prove_expr2" + THEN trace_tac options "prove_expr2" THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) - THEN print_tac options "finished prove_expr2" + THEN trace_tac options "finished prove_expr2" end | _ => etac @{thm bindE} 1) @@ -387,16 +377,16 @@ | _ => nameTs) val preds = preds_of t [] val defs = map - (fn (pred, T) => predfun_definition_of ctxt pred + (fn (pred, T) => predfun_definition_of ctxt pred (all_input_of T)) preds in (* only simplify the one assumption *) - full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1 + full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1 (* need better control here! *) - THEN print_tac options "after sidecond2 simplification" + THEN trace_tac options "after sidecond2 simplification" end - + fun prove_clause2 options ctxt pred mode (ts, ps) i = let val pred_intro_rule = nth (intros_of ctxt pred) (i - 1) @@ -406,23 +396,23 @@ addsimps [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] fun prove_prems2 out_ts [] = - print_tac options "before prove_match2 - last call:" + trace_tac options "before prove_match2 - last call:" THEN prove_match2 options ctxt out_ts - THEN print_tac options "after prove_match2 - last call:" + THEN trace_tac options "after prove_match2 - last call:" THEN (etac @{thm singleE} 1) THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1)) THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1) THEN TRY ( (REPEAT_DETERM (etac @{thm Pair_inject} 1)) THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1) - - THEN SOLVED (print_tac options "state before applying intro rule:" + + THEN SOLVED (trace_tac options "state before applying intro rule:" THEN (rtac pred_intro_rule (* How to handle equality correctly? *) - THEN_ALL_NEW (K (print_tac options "state before assumption matching") + THEN_ALL_NEW (K (trace_tac options "state before assumption matching") THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_simpset) THEN' (TRY o atac))) - THEN' (K (print_tac options "state after pre-simplification:")) - THEN' (K (print_tac options "state after assumption matching:")))) 1)) + THEN' (K (trace_tac options "state after pre-simplification:")) + THEN' (K (trace_tac options "state after assumption matching:")))) 1)) | prove_prems2 out_ts ((p, deriv) :: ps) = let val mode = head_mode_of deriv @@ -445,7 +435,7 @@ val param_derivations = param_derivations_of deriv val ho_args = ho_args_of mode args in - print_tac options "before neg prem 2" + trace_tac options "before neg prem 2" THEN etac @{thm bindE} 1 THEN (if is_some name then full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @@ -456,28 +446,28 @@ else etac @{thm not_predE'} 1) THEN rec_tac - end + end | Sidecond t => etac @{thm bindE} 1 THEN etac @{thm if_predE} 1 THEN prove_sidecond2 options ctxt t THEN prove_prems2 [] ps) in - print_tac options "before prove_match2:" + trace_tac options "before prove_match2:" THEN prove_match2 options ctxt out_ts - THEN print_tac options "after prove_match2:" + THEN trace_tac options "after prove_match2:" THEN rest_tac end - val prems_tac = prove_prems2 in_ts ps + val prems_tac = prove_prems2 in_ts ps in - print_tac options "starting prove_clause2" + trace_tac options "starting prove_clause2" THEN etac @{thm bindE} 1 THEN (etac @{thm singleE'} 1) THEN (TRY (etac @{thm Pair_inject} 1)) - THEN print_tac options "after singleE':" + THEN trace_tac options "after singleE':" THEN prems_tac end; - + fun prove_other_direction options ctxt pred mode moded_clauses = let fun prove_clause clause i = @@ -505,11 +495,11 @@ (if not (skip_proof options) then (fn _ => rtac @{thm pred_iffI} 1 - THEN print_tac options "after pred_iffI" + THEN trace_tac options "after pred_iffI" THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses - THEN print_tac options "proved one direction" + THEN trace_tac options "proved one direction" THEN prove_other_direction options ctxt pred mode moded_clauses - THEN print_tac options "proved other direction") + THEN trace_tac options "proved other direction") else (fn _ => ALLGOALS Skip_Proof.cheat_tac)) end