# HG changeset patch # User Christian Urban # Date 1236735808 0 # Node ID 890fbfef6d6b3e9d8f3d20813ea871b437e6b2df # Parent 3f617d7a2691917d09637559d39e82129220b0b0 partially adapted to new antiquotation infrastructure 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 diff -r 3f617d7a2691 -r 890fbfef6d6b CookBook/Package/Ind_Prelims.thy --- a/CookBook/Package/Ind_Prelims.thy Tue Mar 10 13:20:46 2009 +0000 +++ b/CookBook/Package/Ind_Prelims.thy Wed Mar 11 01:43:28 2009 +0000 @@ -75,10 +75,10 @@ *} lemma %linenos trcl_induct: - assumes asm: "trcl R x y" + assumes "trcl R x y" shows "(\x. P x x) \ (\x y z. R x y \ P y z \ P x z) \ P x y" apply(atomize (full)) -apply(cut_tac asm) +apply(cut_tac prems) apply(unfold trcl_def) apply(drule spec[where x=P]) apply(assumption) @@ -212,11 +212,11 @@ *} simple_inductive - even\ and odd\ + even and odd where - even0: "even\ 0" -| evenS: "odd\ n \ even\ (Suc n)" -| oddS: "even\ n \ odd\ (Suc n)" + even0: "even 0" +| evenS: "odd n \ even (Suc n)" +| oddS: "even n \ odd (Suc n)" text {* Since the predicates @{term even} and @{term odd} are mutually inductive, each @@ -224,11 +224,11 @@ below @{text "P"} and @{text "Q"}). *} -definition "even \ +definition "even\ \ \n. \P Q. P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" -definition "odd \ +definition "odd\ \ \n. \P Q. P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ Q n" @@ -238,11 +238,11 @@ *} lemma even_induct: - 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(atomize (full)) -apply(cut_tac asm) +apply(cut_tac prems) apply(unfold even_def) apply(drule spec[where x=P]) apply(drule spec[where x=Q]) @@ -263,7 +263,7 @@ apply (unfold odd_def even_def) apply (rule allI impI)+ proof - - case (goal1 P) + case (goal1 P Q) have p1: "\P Q. P 0 \ (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ Q m" by fact have r1: "P 0" by fact @@ -303,10 +303,10 @@ *} lemma accpart_induct: - assumes asm: "accpart R x" + assumes "accpart R x" shows "(\x. (\y. R y x \ P y) \ P x) \ P x" apply(atomize (full)) -apply(cut_tac asm) +apply(cut_tac prems) apply(unfold accpart_def) apply(drule spec[where x=P]) apply(assumption) diff -r 3f617d7a2691 -r 890fbfef6d6b CookBook/Package/simple_inductive_package.ML --- a/CookBook/Package/simple_inductive_package.ML Tue Mar 10 13:20:46 2009 +0000 +++ b/CookBook/Package/simple_inductive_package.ML Wed Mar 11 01:43:28 2009 +0000 @@ -137,24 +137,25 @@ end) (* @end *) +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] + + (* @chunk intro_rules *) -fun INTROS rules parnames preds defs lthy1 = +fun introductions rules parnames preds defs lthy1 = let val (_, lthy2) = Variable.add_fixes parnames lthy1 fun prove_intro (i, goal) = Goal.prove lthy2 [] [] goal - (fn {context = ctxt, ...} => - EVERY1 - [ObjectLogic.rulify_tac, - K (rewrite_goals_tac defs), - REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), - subproof1 rules preds i ctxt]) - |> singleton (ProofContext.export lthy2 lthy1) + (fn {context, ...} => introductions_tac defs rules preds i context) + |> singleton (ProofContext.export lthy2 lthy1) in map_index prove_intro rules end - (* @end *) (* @chunk add_inductive_i *) @@ -163,7 +164,7 @@ val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params; val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds; val Tss = map (binder_types o fastype_of) preds'; - val (ass,rules) = split_list specs; + val (ass, rules) = split_list specs; (* FIXME: ass not used? *) val prednames = map (fst o fst) preds val syns = map snd preds @@ -173,7 +174,7 @@ val inducts = inductions rules defs parnames preds' Tss lthy1 - val intros = INTROS rules parnames preds' defs lthy1 + val intros = introductions rules parnames preds' defs lthy1 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); val case_names = map (Binding.name_of o fst o fst) specs diff -r 3f617d7a2691 -r 890fbfef6d6b CookBook/Recipes/Antiquotes.thy --- a/CookBook/Recipes/Antiquotes.thy Tue Mar 10 13:20:46 2009 +0000 +++ b/CookBook/Recipes/Antiquotes.thy Wed Mar 11 01:43:28 2009 +0000 @@ -36,15 +36,15 @@ *} +ML {* Pretty.str *} + ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt -fun output_ml src ctxt code_txt = +fun output_ml {source = src, context = ctxt, ...} code_txt = (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); - ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt - (space_explode "\n" code_txt)) + ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) -val _ = ThyOutput.add_commands - [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)]*} +val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} text {* @@ -53,13 +53,13 @@ is sent to the ML-compiler in the line 4 using the function @{ML ml_val}, which constructs the appropriate ML-expression. If the code is ``approved'' by the compiler, then the output function @{ML - "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the + "ThyOutput.output"} in the next line pretty prints the code. This function expects that the code is a list of strings where each string correspond to a line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)" for txt} - which produces this list according to linebreaks. There are a number of options for antiquotations - that are observed by @{ML ThyOutput.output_list} when printing the code (including - @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). + which produces this list according to linebreaks. There are a number of options + for antiquotations that are observed by @{ML ThyOutput.output} when printing the + code (including @{text "[display]"} and @{text "[quotes]"}). \begin{readmore} For more information about options of antiquotations see \rsccite{sec:antiq}). @@ -70,14 +70,12 @@ can improve the code above slightly by writing *} -ML%linenosgray{*fun output_ml src ctxt (code_txt,pos) = +ML%linenosgray{*fun output_ml {source = src, context = ctxt, ...} (code_txt,pos) = (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt); - ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt - (space_explode "\n" code_txt)) + ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) -val _ = ThyOutput.add_commands - [("ML_checked", ThyOutput.args - (Scan.lift (OuterParse.position Args.name)) output_ml)] *} +val _ = ThyOutput.antiquotation "ML_checked" + (Scan.lift (OuterParse.position Args.name)) output_ml *} text {* where in Lines 1 and 2 the positional information is properly treated. @@ -129,19 +127,16 @@ The rest of the code of the antiquotation is *} -ML{*fun output_ml_resp src ctxt ((code_txt,pat),pos) = +ML{*fun output_ml_resp {source = src, context = ctxt, ...} ((code_txt,pat),pos) = (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat)); let val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat) in - ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output + ThyOutput.output (map Pretty.str output) end) -val _ = ThyOutput.add_commands - [("ML_resp", - ThyOutput.args - (Scan.lift (OuterParse.position (Args.name -- Args.name))) - output_ml_resp)]*} +val _ = ThyOutput.antiquotation "ML_resp" + (Scan.lift (OuterParse.position (Args.name -- Args.name))) output_ml_resp*} text {* This extended antiquotation allows us to write diff -r 3f617d7a2691 -r 890fbfef6d6b CookBook/antiquote_setup.ML --- a/CookBook/antiquote_setup.ML Tue Mar 10 13:20:46 2009 +0000 +++ b/CookBook/antiquote_setup.ML Wed Mar 11 01:43:28 2009 +0000 @@ -48,9 +48,9 @@ val output_fn = Chunks.output_list (fn _ => fn s => Pretty.str s) (* checks and prints open expressions *) -fun output_ml src node = +fun output_ml () = let - fun output src ctxt ((txt,ovars),pos) = + fun output {state: Toplevel.state, source = src, context = ctxt} ((txt,ovars),pos) = (eval_fn ctxt pos (ml_val_open ovars txt); output_fn src ctxt (transform_cmts_str txt)) @@ -58,62 +58,63 @@ (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) []))) in - ThyOutput.args parser output src node + ThyOutput.antiquotation "ML" parser output end (* checks and prints types and structures *) -fun output_exp ml src node = +fun output_exp ml = let - fun output src ctxt (txt,pos) = + fun output {state: Toplevel.state, source = src, context = ctxt} (txt,pos) = (eval_fn ctxt pos (ml txt); output_fn src ctxt (string_explode "" txt)) in - ThyOutput.args single_arg output src node + ThyOutput.antiquotation "ML_type" single_arg output end (* checks and expression agains a result pattern *) -fun output_ml_response src node = +fun output_ml_response () = let - fun output src ctxt ((lhs,pat),pos) = + fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat),pos) = (eval_fn ctxt pos (ml_pat (lhs,pat)); output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))) in - ThyOutput.args two_args output src node + ThyOutput.antiquotation "ML_response" two_args output end (* checks the expressions, but does not check it against a result pattern *) -fun output_ml_response_fake src node = +fun output_ml_response_fake () = let - fun output src ctxt ((lhs,pat),pos) = + fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs, pat), pos) = (eval_fn ctxt pos (ml_val lhs); output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))) in - ThyOutput.args two_args output src node + ThyOutput.antiquotation "ML_response_fake" two_args output end (* just prints an expression and a result pattern *) -fun output_ml_response_fake_both src node = +fun output_ml_response_fake_both () = let - fun ouput src ctxt ((lhs,pat), _) = + fun ouput {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat), _) = output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)) in - ThyOutput.args two_args ouput src node + ThyOutput.antiquotation "ML_response_fake_both" two_args ouput end (* checks whether a file exists in the Isabelle distribution *) -fun check_file_exists src node = +fun check_file_exists () = let fun check txt = if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () else error ("Source file " ^ (quote txt) ^ " does not exist.") in - ThyOutput.args (Scan.lift Args.name) - (ThyOutput.output (fn _ => fn s => (check s; Pretty.str s))) src node + ThyOutput.antiquotation "ML_file" (Scan.lift Args.name) + (fn _ => fn s => (check s; ThyOutput.output [Pretty.str s])) end (* replaces the official subgoal antiquotation with one *) (* that is closer to the actual output *) -fun output_goals src node = +(* +fun output_goals {state = node, source: Args.src, context: Proof.context} _ = let fun subgoals 0 = "" | subgoals 1 = "goal (1 subgoal):" @@ -129,22 +130,22 @@ val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); val (As, B) = Logic.strip_horn prop; - val output = (case (length As) of + val output' = (case (length As) of 0 => goals | n => (Pretty.str (subgoals n))::goals) in - ThyOutput.args (Scan.succeed ()) - (Chunks.output (fn _ => fn _ => Pretty.chunks output)) src node + output end +*) + -val _ = ThyOutput.add_commands - [("ML", output_ml), - ("ML_file", check_file_exists), - ("ML_response", output_ml_response), - ("ML_response_fake", output_ml_response_fake), - ("ML_response_fake_both", output_ml_response_fake_both), - ("ML_struct", output_exp ml_struct), - ("ML_type", output_exp ml_type), - ("subgoals", output_goals)]; +val _ = output_ml (); +val _ = check_file_exists (); +val _ = output_ml_response (); +val _ = output_ml_response_fake (); +val _ = output_ml_response_fake_both (); +val _ = output_exp ml_struct; +val _ = output_exp ml_type; +(*val _ = output_goals*) end; diff -r 3f617d7a2691 -r 890fbfef6d6b CookBook/chunks.ML --- a/CookBook/chunks.ML Tue Mar 10 13:20:46 2009 +0000 +++ b/CookBook/chunks.ML Wed Mar 11 01:43:28 2009 +0000 @@ -139,7 +139,7 @@ || Scan.one not_eof >> ML_Lex.content_of)) #> fst; -fun output_chunk src ctxt name = +fun output_chunk {state: Toplevel.state, source = src, context = ctxt} name = let val toks = the_chunk (ProofContext.theory_of ctxt) name; val (spc, toks') = (case toks of @@ -164,7 +164,6 @@ output_list (fn _ => fn s => Pretty.str s) src ctxt end; -val _ = ThyOutput.add_commands - [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)]; +val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; end; diff -r 3f617d7a2691 -r 890fbfef6d6b cookbook.pdf Binary file cookbook.pdf has changed