diff -r 3f617d7a2691 -r 890fbfef6d6b CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Tue Mar 10 13:20:46 2009 +0000 +++ b/CookBook/Package/Ind_Code.thy Wed Mar 11 01:43:28 2009 +0000 @@ -94,13 +94,14 @@ The actual definitions are made in Line 7. *} -subsection {* Introduction Rules *} + +subsection {* Induction Principles *} ML{*fun inst_spec ct = Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} text {* - Instantiates the @{text "x"} in @{thm spec[no_vars]} with a @{ML_type cterm}. + Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}. *} text {* @@ -110,44 +111,72 @@ lemma "\x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \ True" apply (tactic {* EVERY' (map (dtac o inst_spec) [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*}) +txt {* \begin{minipage}{\textwidth} + @{subgoals} + \end{minipage}*} (*<*)oops(*>*) + +lemma + assumes "even n" + shows "P 0 \ + (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" +apply(atomize (full)) +apply(cut_tac prems) +apply(unfold even_def) +apply(drule spec[where x=P]) +apply(drule spec[where x=Q]) +apply(assumption) +done + text {* The tactic for proving the induction rules: *} ML{*fun induction_tac defs prems insts = - EVERY1 [ObjectLogic.full_atomize_tac, + EVERY1 [K (print_tac "start"), + ObjectLogic.full_atomize_tac, cut_facts_tac prems, K (rewrite_goals_tac defs), EVERY' (map (dtac o inst_spec) insts), assume_tac]*} lemma - assumes asm: "even n" + assumes "even n" shows "P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" -apply(tactic {* induction_tac [@{thm even_def}, @{thm odd_def}] [@{thm asm}] - [@{cterm "P::nat\bool"}, @{cterm "Q::nat\bool"}] *}) +apply(tactic {* + let + val defs = [@{thm even_def}, @{thm odd_def}] + val insts = [@{cterm "P::nat\bool"}, @{cterm "Q::nat\bool"}] + in + induction_tac defs @{thms prems} insts + end *}) done -ML %linenosgray{*fun inductions rules defs preds Tss lthy1 = +text {* + While the generic proof is relatively simple, it is a bit harder to + set up the goals for the induction principles. +*} + + +ML %linenosgray{*fun inductions rules defs preds tyss lthy1 = let val Ps = replicate (length preds) "P" val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1 val thy = ProofContext.theory_of lthy2 - val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss - val newpreds = map Free (newprednames ~~ Tss') + val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss + val newpreds = map Free (newprednames ~~ tyss') val cnewpreds = map (cterm_of thy) newpreds val rules' = map (subst_free (preds ~~ newpreds)) rules - fun prove_induction ((pred, newpred), Ts) = + fun prove_induction ((pred, newpred), tys) = let - val zs = replicate (length Ts) "z" + val zs = replicate (length tys) "z" val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; - val newargs = map Free (newargnames ~~ Ts) + val newargs = map Free (newargnames ~~ tys) val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) val goal = Logic.list_implies @@ -158,26 +187,137 @@ |> singleton (ProofContext.export lthy3 lthy1) end in - map prove_induction (preds ~~ newpreds ~~ Tss) + map prove_induction (preds ~~ newpreds ~~ tyss) +end*} + +(* +ML {* + let + val rules = [@{term "even 0"}, + @{term "\n::nat. odd n \ even (Suc n)"}, + @{term "\n::nat. even n \ odd (Suc n)"}] + val defs = [@{thm even_def}, @{thm odd_def}] + val preds = [@{term "even::nat\bool"}, @{term "odd::nat\bool"}] + val tyss = [[@{typ "nat"}],[@{typ "nat"}]] + in + inductions rules defs preds tyss @{context} + end +*} +*) + +subsection {* Introduction Rules *} + +ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) +val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} + +ML{*fun subproof2 prem params2 prems2 = + SUBPROOF (fn {prems, ...} => + let + val prem' = prems MRS prem; + val prem'' = + case prop_of prem' of + _ $ (Const (@{const_name All}, _) $ _) => + prem' |> all_elims params2 + |> imp_elims prems2 + | _ => prem'; + in + rtac prem'' 1 + end)*} + +ML{*fun subproof1 rules preds i = + SUBPROOF (fn {params, prems, context = ctxt', ...} => + let + val (prems1, prems2) = chop (length prems - length rules) prems; + val (params1, params2) = chop (length params - length preds) params; + in + rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 + THEN + EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) + end)*} + +ML{* +fun introductions_tac defs rules preds i ctxt = + EVERY1 [ObjectLogic.rulify_tac, + K (rewrite_goals_tac defs), + REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), + subproof1 rules preds i ctxt]*} + +ML{*fun introductions rules preds defs lthy = +let + fun prove_intro (i, goal) = + Goal.prove lthy [] [] goal + (fn {context, ...} => introductions_tac defs rules preds i context) +in + map_index prove_intro rules end*} -ML {* Goal.prove *} -ML {* singleton *} -ML {* ProofContext.export *} +ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy = +let + val syns = map snd pred_specs + val pred_specs' = map fst pred_specs + val prednames = map fst pred_specs' + val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs' -text {* + val tyss = map (binder_types o fastype_of) preds + val (attrs, rules) = split_list rule_specs + + val (defs, lthy') = definitions rules preds prednames syns tyss lthy + val ind_rules = inductions rules defs preds tyss lthy' + val intro_rules = introductions rules preds defs lthy' -*} - -text {* - @{ML_chunk [display,gray] subproof1} - - @{ML_chunk [display,gray] subproof2} - - @{ML_chunk [display,gray] intro_rules} + val mut_name = space_implode "_" (map Binding.name_of prednames) + val case_names = map (Binding.name_of o fst) attrs +in + lthy' + |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => + ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) + |-> (fn intross => LocalTheory.note Thm.theoremK + ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) + |>> snd + ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => + ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), + [Attrib.internal (K (RuleCases.case_names case_names)), + Attrib.internal (K (RuleCases.consumes 1)), + Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) + (pred_specs ~~ ind_rules)) #>> maps snd) + |> snd +end*} -*} +ML{*fun read_specification' vars specs lthy = +let + val specs' = map (fn (a, s) => [(a, [s])]) specs + val ((varst, specst), _) = + Specification.read_specification vars specs' lthy + val specst' = map (apsnd the_single) specst +in + (varst, specst') +end*} + +ML{*fun add_inductive pred_specs rule_specs lthy = +let + val (pred_specs', rule_specs') = + read_specification' pred_specs rule_specs lthy +in + add_inductive_i pred_specs' rule_specs' lthy +end*} + +ML{*val spec_parser = + OuterParse.opt_target -- + OuterParse.fixes -- + Scan.optional + (OuterParse.$$$ "where" |-- + OuterParse.!!! + (OuterParse.enum1 "|" + (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} + +ML{*val specification = + spec_parser >> + (fn ((loc, pred_specs), rule_specs) => + Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*} + +ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" + OuterKeyword.thy_decl specification*} text {* Things to include at the end: @@ -191,5 +331,11 @@ *} +simple_inductive + Even and Odd +where + Even0: "Even 0" +| EvenS: "Odd n \ Even (Suc n)" +| OddS: "Even n \ Odd (Suc n)" end