# HG changeset patch # User bulwahn # Date 1244660676 -7200 # Node ID b63d253ed9e21386bad258d8905e2a5f8175d3ef # Parent f7379ea2c9494575c3d48c831b0dfbf4a017446c code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function diff -r f7379ea2c949 -r b63d253ed9e2 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Wed Jun 10 10:42:24 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Wed Jun 10 21:04:36 2009 +0200 @@ -8,11 +8,9 @@ | "odd n \ even (Suc n)" -(* -code_pred even - using assms by (rule even.cases) -*) -setup {* Predicate_Compile.add_equations @{const_name even} *} + +code_pred even . + thm odd.equation thm even.equation @@ -31,15 +29,7 @@ "rev [] []" | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" -setup {* Predicate_Compile.add_equations @{const_name rev} *} - -thm rev.equation -thm append.equation - -(* -code_pred append - using assms by (rule append.cases) -*) +code_pred rev . thm append.equation @@ -54,36 +44,39 @@ | "f x \ partition f xs ys zs \ partition f (x # xs) (x # ys) zs" | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" -setup {* Predicate_Compile.add_equations @{const_name partition} *} -(* -code_pred partition - using assms by (rule partition.cases) -*) +ML {* reset Predicate_Compile.do_proofs *} + +code_pred partition . thm partition.equation +ML {* set Predicate_Compile.do_proofs *} +(* TODO: requires to handle abstractions in parameter positions correctly *) (*FIXME values 10 "{(ys, zs). partition (\n. n mod 2 = 0) - [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"*) + [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" *) + +thm tranclp.intros -setup {* Predicate_Compile.add_equations @{const_name tranclp} *} (* -code_pred tranclp - using assms by (rule tranclp.cases) +lemma [code_pred_intros]: +"r a b ==> tranclp r a b" +"r a b ==> tranclp r b c ==> tranclp r a c" +by auto *) +code_pred tranclp . + thm tranclp.equation inductive succ :: "nat \ nat \ bool" where "succ 0 1" | "succ m n \ succ (Suc m) (Suc n)" -setup {* Predicate_Compile.add_equations @{const_name succ} *} -(* -code_pred succ - using assms by (rule succ.cases) -*) +code_pred succ . + thm succ.equation +(* TODO: requires alternative rules for trancl *) (* values 20 "{n. tranclp succ 10 n}" values "{n. tranclp succ n 10}" diff -r f7379ea2c949 -r b63d253ed9e2 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Wed Jun 10 10:42:24 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Wed Jun 10 21:04:36 2009 +0200 @@ -37,13 +37,17 @@ fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); -fun debug_tac msg = (fn st => (tracing msg; Seq.single st)); +fun new_print_tac s = Tactical.print_tac s +fun debug_tac msg = (fn st => (Output.tracing msg; Seq.single st)); val do_proofs = ref true; fun mycheat_tac thy i st = (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st +fun remove_last_goal thy st = + (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st + (* reference to preprocessing of InductiveSet package *) val ind_set_codegen_preproc = InductiveSetPackage.codegen_preproc; @@ -733,21 +737,27 @@ val args = map Free (argnames ~~ (Ts1' @ Ts2)) val (params, io_args) = chop nparams args val (inargs, outargs) = get_args (snd mode) io_args + val param_names = Name.variant_list argnames + (map (fn i => "p" ^ string_of_int i) (1 upto nparams)) + val param_vs = map Free (param_names ~~ Ts1) val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ (fst mode)) [] - val predprop = HOLogic.mk_Trueprop (list_comb (pred, params' @ io_args)) + val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ io_args)) + val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ io_args)) + val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params') val funargs = params @ inargs val funpropE = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs), if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs)) val funpropI = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs), mk_tuple outargs)) - val introtrm = Logic.mk_implies (predprop, funpropI) + val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI) + val _ = Output.tracing (Syntax.string_of_term_global thy introtrm) val simprules = [defthm, @{thm eval_pred}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}] val unfolddef_tac = (Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1) - val introthm = Goal.prove (ProofContext.init thy) (argnames @ ["y"]) [] introtrm (fn {...} => unfolddef_tac) + val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y"]) [] introtrm (fn {...} => unfolddef_tac) val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)); - val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predprop, P)], P) - val elimthm = Goal.prove (ProofContext.init thy) (argnames @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac) + val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P) + val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac) in (introthm, elimthm) end; @@ -859,7 +869,16 @@ fun prove_param thy modes (NONE, t) = all_tac | prove_param thy modes (m as SOME (Mode (mode, is, ms)), t) = - let + REPEAT_DETERM (etac @{thm thin_rl} 1) + THEN REPEAT_DETERM (rtac @{thm ext} 1) + THEN (rtac @{thm iffI} 1) + THEN new_print_tac "prove_param" + (* proof in one direction *) + THEN (atac 1) + (* proof in the other direction *) + THEN (atac 1) + THEN new_print_tac "after prove_param" +(* let val (f, args) = strip_comb t val (params, _) = chop (length ms) args val f_tac = case f of @@ -872,11 +891,10 @@ print_tac "before simplification in prove_args:" THEN f_tac THEN print_tac "after simplification in prove_args" - (* work with parameter arguments *) THEN (EVERY (map (prove_param thy modes) (ms ~~ params))) THEN (REPEAT_DETERM (atac 1)) end - +*) fun prove_expr thy modes (SOME (Mode (mode, is, ms)), t, us) (premposition : int) = (case strip_comb t of (Const (name, T), args) => @@ -897,8 +915,10 @@ (* for the right assumption in first position *) THEN rotate_tac premposition 1 THEN rtac introrule 1 - THEN print_tac "after intro rule" + THEN new_print_tac "after intro rule" (* work with parameter arguments *) + THEN (atac 1) + THEN (new_print_tac "parameter goal") THEN (EVERY (map (prove_param thy modes) (ms ~~ args1))) THEN (REPEAT_DETERM (atac 1)) end) else error "Prove expr if case not implemented" @@ -1041,6 +1061,7 @@ (fn i => EVERY' (select_sup (length clauses) i) i) (1 upto (length clauses)))) THEN (EVERY (map (prove_clause thy nargs all_vs param_vs modes mode) clauses)) + THEN new_print_tac "proved one direction" end; (*******************************************************************************************************) @@ -1073,7 +1094,8 @@ (* VERY LARGE SIMILIRATIY to function prove_param -- join both functions -*) +*) +(* fun prove_param2 thy modes (NONE, t) = all_tac | prove_param2 thy modes (m as SOME (Mode (mode, is, ms)), t) = let val (f, args) = strip_comb t @@ -1087,9 +1109,9 @@ print_tac "before simplification in prove_args:" THEN f_tac THEN print_tac "after simplification in prove_args" - (* work with parameter arguments *) THEN (EVERY (map (prove_param2 thy modes) (ms ~~ params))) end +*) fun prove_expr2 thy modes (SOME (Mode (mode, is, ms)), t) = (case strip_comb t of @@ -1097,8 +1119,14 @@ if AList.defined op = modes name then etac @{thm bindE} 1 THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))) + 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 (EVERY (map (prove_param2 thy modes) (ms ~~ args))) + THEN new_print_tac "prove_expr2" + (* TODO -- FIXME: replace remove_last_goal*) + THEN (EVERY (replicate (length args) (remove_last_goal thy))) + THEN new_print_tac "finished prove_expr2" + (* THEN (EVERY (map (prove_param thy modes) (ms ~~ args))) *) else error "Prove expr2 if case not implemented" | _ => etac @{thm bindE} 1) | prove_expr2 _ _ _ = error "Prove expr2 not implemented" @@ -1177,7 +1205,7 @@ THEN (if is_some name then full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, js)]) 1 THEN etac @{thm not_predE} 1 - THEN (EVERY (map (prove_param2 thy modes) (param_modes ~~ params))) + THEN (EVERY (map (prove_param thy modes) (param_modes ~~ params))) else etac @{thm not_predE'} 1) THEN rec_tac @@ -1252,6 +1280,7 @@ fun prepare_intrs thy prednames = let + (* FIXME: preprocessing moved to fetch_pred_data *) val intrs = map (preprocess_intro thy) (maps (intros_of thy) prednames) |> ind_set_codegen_preproc thy (*FIXME preprocessor |> map (Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]))*) @@ -1336,7 +1365,7 @@ (* generation of case rules from user-given introduction rules *) -fun mk_casesrule introrules nparams ctxt = +fun mk_casesrule ctxt nparams introrules = let val intros = map prop_of introrules val (pred, (params, args)) = strip_intro_concl nparams (hd intros) @@ -1356,10 +1385,7 @@ in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs)) val cases = map mk_case intros - val (_, ctxt3) = ProofContext.add_assms_i Assumption.assume_export - [((Binding.name AutoBind.assmsN, []), map (fn t => (t, [])) (assm :: cases))] - ctxt2 - in (pred, prop, ctxt3) end; + in Logic.list_implies (assm :: cases, prop) end; (* code dependency graph *) @@ -1417,38 +1443,22 @@ (* TODO: must create state to prove multiple cases *) fun generic_code_pred prep_const raw_const lthy = let - val thy = (ProofContext.theory_of lthy) + val thy = ProofContext.theory_of lthy val const = prep_const thy raw_const - val lthy' = lthy - val thy' = PredData.map (Graph.extend (dependencies_of thy) const) thy + val lthy' = LocalTheory.theory (PredData.map (Graph.extend (dependencies_of thy) const)) lthy + val thy' = ProofContext.theory_of lthy' val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy') val _ = Output.tracing ("preds: " ^ commas preds) - (* - fun mk_elim pred = + fun mk_cases const = let - val nparams = nparams_of thy pred - val intros = intros_of thy pred - val (((tfrees, frees), fact), lthy'') = - Variable.import_thms true intros lthy'; - val (pred, prop, lthy''') = mk_casesrule fact nparams lthy'' - in (pred, prop, lthy''') end; - - val (predname, _) = dest_Const pred - *) - val nparams = nparams_of thy' const - val intros = intros_of thy' const - val (((tfrees, frees), fact), lthy'') = - Variable.import_thms true intros lthy'; - val (pred, prop, lthy''') = mk_casesrule fact nparams lthy'' - val (predname, _) = dest_Const pred - fun after_qed [[th]] lthy''' = - lthy''' - |> LocalTheory.note Thm.generatedK - ((Binding.empty, []), [th]) - |> snd - |> LocalTheory.theory (add_equations_of [predname]) + val nparams = nparams_of thy' const + val intros = intros_of thy' const + in mk_casesrule lthy' nparams intros end + val cases_rules = map mk_cases preds + fun after_qed thms = + LocalTheory.theory (fold set_elim (map the_single thms) #> add_equations const) in - Proof.theorem_i NONE after_qed [[(prop, [])]] lthy''' + Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy' end; structure P = OuterParse