# HG changeset patch # User bulwahn # Date 1269243013 -3600 # Node ID 362bfc2ca0ee855fccb49bc2f333f77eeb4e9979 # Parent f8f882329a98bc5c2c50f0aeeae8e4a312f61edc adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises diff -r f8f882329a98 -r 362bfc2ca0ee src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 08:30:13 2010 +0100 @@ -189,13 +189,14 @@ datatype predfun_data = PredfunData of { definition : thm, intro : thm, - elim : thm + elim : thm, + neg_intro : thm option }; fun rep_predfun_data (PredfunData data) = data; -fun mk_predfun_data (definition, intro, elim) = - PredfunData {definition = definition, intro = intro, elim = elim} +fun mk_predfun_data (definition, ((intro, elim), neg_intro)) = + PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro} datatype pred_data = PredData of { intros : thm list, @@ -291,6 +292,8 @@ val predfun_elim_of = #elim ooo the_predfun_data +val predfun_neg_intro_of = #neg_intro ooo the_predfun_data + (* diagnostic display functions *) fun print_modes options thy modes = @@ -470,7 +473,7 @@ in (HOLogic.mk_prod (t1, t2), st'') end - | mk_args2 (T as Type ("fun", _)) (params, ctxt) = + (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) = let val (S, U) = strip_type T in @@ -482,36 +485,80 @@ in (Free (x, T), (params, ctxt')) end - end + end*) | mk_args2 T (params, ctxt) = let val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt in (Free (x, T), (params, ctxt')) end - + fun mk_casesrule ctxt pred introrules = let + (* TODO: can be simplified if parameters are not treated specially ? *) val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt + (* TODO: distinct required ? -- test case with more than one parameter! *) + val params = distinct (op aconv) params val intros = map prop_of intros_th val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1 val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) val argsT = binder_types (fastype_of pred) + (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *) val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2) fun mk_case intro = let val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro val prems = Logic.strip_imp_prems intro - val eqprems = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args - val frees = (fold o fold_aterms) - (fn t as Free _ => - if member (op aconv) params t then I else insert (op aconv) t - | _ => I) (args @ prems) [] + val eqprems = + map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args + val frees = map Free (fold Term.add_frees (args @ prems) []) in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs)) val cases = map mk_case intros in Logic.list_implies (assm :: cases, prop) end; +fun dest_conjunct_prem th = + case HOLogic.dest_Trueprop (prop_of th) of + (Const ("op &", _) $ t $ t') => + dest_conjunct_prem (th RS @{thm conjunct1}) + @ dest_conjunct_prem (th RS @{thm conjunct2}) + | _ => [th] + +fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule = + let + val thy = ProofContext.theory_of ctxt + val nargs = length (binder_types (fastype_of pred)) + fun PEEK f dependent_tactic st = dependent_tactic (f st) st + fun meta_eq_of th = th RS @{thm eq_reflection} + val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}] + fun instantiate i n {context = ctxt, params = p, prems = prems, + asms = a, concl = cl, schematics = s} = + let + val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems) + val case_th = MetaSimplifier.simplify true + (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) + (nth cases (i - 1)) + val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems + val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th)) + val (_, tenv) = fold (Pattern.match thy) pats (Vartab.empty, Vartab.empty) + fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t) + val inst = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) + val thesis = Thm.instantiate ([], inst) case_th OF (replicate nargs @{thm refl}) OF prems' + in + (rtac thesis 1) + end + val tac = + etac pre_cases_rule 1 + THEN + (PEEK nprems_of + (fn n => + ALLGOALS (fn i => + MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i + THEN (SUBPROOF (instantiate i n) ctxt i)))) + in + Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac) + end + (** preprocessing rules **) fun imp_prems_conv cv ct = @@ -552,7 +599,7 @@ val bigeq = (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}]) (cterm_of thy elimrule'))) - val tac = (fn _ => Skip_Proof.cheat_tac thy) + val tac = (fn _ => Skip_Proof.cheat_tac thy) val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac in Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt) @@ -575,11 +622,14 @@ val index = find_index (fn s => s = name) (#names (fst info)) val pre_elim = nth (#elims result) index val pred = nth (#preds result) index + val nparams = length (Inductive.params_of (#raw_induct result)) (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams (expand_tuples_elim pre_elim))*) + (* FIXME: missing Inductive Set preprocessing *) + val ctxt = ProofContext.init thy + val elim_t = mk_casesrule ctxt pred intros val elim = - (Drule.export_without_context o Skip_Proof.make_thm thy) - (mk_casesrule (ProofContext.init thy) pred intros) + prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t in mk_pred_data ((intros, SOME elim), no_compilation) end @@ -1630,7 +1680,7 @@ val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod) (fn T => fn (param_vs, names) => - if is_param_type T then + if is_param_type T then (Free (hd param_vs, T), (tl param_vs, names)) else let @@ -1743,8 +1793,24 @@ val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P) val elimthm = Goal.prove (ProofContext.init thy) (argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac) + val opt_neg_introthm = + if is_all_input mode then + let + val neg_predpropI = HOLogic.mk_Trueprop (HOLogic.mk_not (list_comb (pred, args'))) + val neg_funpropI = + HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval + (PredicateCompFuns.mk_not (list_comb (funtrm, inargs)), HOLogic.unit)) + val neg_introtrm = Logic.list_implies (neg_predpropI :: param_eqs, neg_funpropI) + val tac = + Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps + (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1 + THEN rtac @{thm Predicate.singleI} 1 + in SOME (Goal.prove (ProofContext.init thy) (argnames @ hoarg_names') [] + neg_introtrm (fn _ => tac)) + end + else NONE in - (introthm, elimthm) + ((introthm, elimthm), opt_neg_introthm) end fun create_constname_of_mode options thy prefix name T mode = @@ -1780,11 +1846,11 @@ val ([definition], thy') = thy |> Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |> PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])] - val (intro, elim) = + val rules as ((intro, elim), _) = create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy' in thy' |> set_function_name Pred name mode mode_cname - |> add_predfun_data name mode (definition, intro, elim) + |> add_predfun_data name mode (definition, rules) |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd |> Theory.checkpoint @@ -1834,7 +1900,7 @@ (* MAJOR FIXME: prove_params should be simple - different form of introrule for parameters ? *) -fun prove_param options thy t deriv = +fun prove_param options thy nargs t deriv = let val (f, args) = strip_comb (Envir.eta_contract t) val mode = head_mode_of deriv @@ -1842,21 +1908,32 @@ val ho_args = ho_args_of mode args val f_tac = case f of Const (name, T) => simp_tac (HOL_basic_ss addsimps - ([@{thm eval_pred}, (predfun_definition_of thy name mode), - @{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"}, - @{thm "snd_conv"}, @{thm pair_collapse}, @{thm "Product_Type.split_conv"}])) 1 - | Free _ => TRY (rtac @{thm refl} 1) - | Abs _ => error "prove_param: No valid parameter term" + [@{thm eval_pred}, predfun_definition_of thy name mode, + @{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, + @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 + | Free _ => + (* rewrite with parameter equation *) + (* test: *) + Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems = prems, + asms = a, concl = concl, schematics = s} => + 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) (ProofContext.init thy) 1 (* FIXME: proper context handling *) + | 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 simplification in prove_args" + THEN f_tac + THEN print_tac' options "after prove_param" THEN (REPEAT_DETERM (atac 1)) - THEN (EVERY (map2 (prove_param options thy) ho_args param_derivations)) + THEN (EVERY (map2 (prove_param options thy nargs) ho_args param_derivations)) + THEN REPEAT_DETERM (rtac @{thm refl} 1) end -fun prove_expr options thy (premposition : int) (t, deriv) = +fun prove_expr options thy nargs (premposition : int) (t, deriv) = case strip_comb t of (Const (name, T), args) => let @@ -1866,25 +1943,36 @@ val ho_args = ho_args_of mode args in print_tac' options "before intro rule:" + THEN rtac introrule 1 + THEN print_tac' options "after intro rule" (* for the right assumption in first position *) THEN rotate_tac premposition 1 - THEN debug_tac (Display.string_of_thm (ProofContext.init thy) introrule) - THEN rtac introrule 1 - THEN print_tac' options "after intro rule" - (* work with parameter arguments *) THEN atac 1 THEN print_tac' options "parameter goal" - THEN (EVERY (map2 (prove_param options thy) ho_args param_derivations)) + (* work with parameter arguments *) + THEN (EVERY (map2 (prove_param options thy nargs) ho_args param_derivations)) THEN (REPEAT_DETERM (atac 1)) end - | _ => - asm_full_simp_tac - (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"}, - @{thm "snd_conv"}, @{thm pair_collapse}]) 1 - THEN (atac 1) + | (Free _, _) => + print_tac' options "proving parameter call.." + THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems = prems, + asms = a, concl = cl, schematics = s} => + let + val param_prem = nth prems premposition + val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem)) + val prems' = maps dest_conjunct_prem (take nargs prems) + fun param_rewrite prem = + param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem))) + val SOME rew_eq = find_first param_rewrite prems' + val param_prem' = MetaSimplifier.rewrite_rule + (map (fn th => th RS @{thm eq_reflection}) + [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}]) + param_prem + in + rtac param_prem' 1 + end) (ProofContext.init thy) 1 (* FIXME: proper context handling *) THEN print_tac' options "after prove parameter call" - fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st @@ -1972,7 +2060,7 @@ print_tac' options "before clause:" (*THEN asm_simp_tac HOL_basic_ss 1*) THEN print_tac' options "before prove_expr:" - THEN prove_expr options thy premposition (t, deriv) + THEN prove_expr options thy nargs premposition (t, deriv) THEN print_tac' options "after prove_expr:" THEN rec_tac end @@ -1982,6 +2070,8 @@ val (_, out_ts''') = split_mode mode args val rec_tac = prove_prems out_ts''' ps val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) + val neg_intro_rule = + Option.map (fn name => the (predfun_neg_intro_of thy name mode)) name val param_derivations = param_derivations_of deriv val params = ho_args_of mode args in @@ -1990,22 +2080,18 @@ [@{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 unfolding definition " ^ - (Display.string_of_thm_global thy - (predfun_definition_of thy (the name) mode))) - - THEN simp_tac (HOL_basic_ss addsimps - [predfun_definition_of thy (the name) mode]) 1 - THEN rtac @{thm not_predI} 1 - THEN print_tac' options "after applying rule not_predI" - THEN full_simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}, - @{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, - @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 - THEN (REPEAT_DETERM (atac 1)) - THEN (EVERY (map2 (prove_param options thy) params param_derivations)) + print_tac' options "before applying not introduction rule" + THEN rotate_tac premposition 1 + THEN etac (the neg_intro_rule) 1 + THEN rotate_tac (~premposition) 1 + THEN print_tac' options "after applying not introduction rule" + THEN (EVERY (map2 (prove_param options thy nargs) params param_derivations)) THEN (REPEAT_DETERM (atac 1)) else - rtac @{thm not_predI'} 1) + rtac @{thm not_predI'} 1 + (* test: *) + THEN dtac @{thm sym} 1 + THEN asm_full_simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1) THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 THEN rec_tac end @@ -2040,6 +2126,7 @@ THEN print_tac' options "before applying elim rule" THEN etac (predfun_elim_of thy pred mode) 1 THEN etac pred_case_rule 1 + THEN print_tac' options "after applying elim rule" THEN (EVERY (map (fn i => EVERY' (select_sup (length moded_clauses) i) i) (1 upto (length moded_clauses)))) @@ -2115,9 +2202,7 @@ etac @{thm bindE} 1 THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))) THEN print_tac "prove_expr2-before" - THEN (debug_tac (Syntax.string_of_term_global thy - (prop_of (predfun_elim_of thy name mode)))) - THEN (etac (predfun_elim_of thy name mode) 1) + THEN etac (predfun_elim_of thy name mode) 1 THEN print_tac "prove_expr2" THEN (EVERY (map2 (prove_param2 thy) ho_args param_derivations)) THEN print_tac "finished prove_expr2" diff -r f8f882329a98 -r 362bfc2ca0ee src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Mon Mar 22 08:30:13 2010 +0100 @@ -93,11 +93,12 @@ case list_all2 from this show thesis apply - - apply (case_tac xa) apply (case_tac xb) + apply (case_tac xc) apply auto - apply (case_tac xb) + apply (case_tac xc) apply auto + apply fastsimp done qed