81 @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"}, |
81 @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"}, |
82 @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}] |
82 @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}] |
83 val eo_preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
83 val eo_preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
84 val eo_prednames = [@{binding "even"}, @{binding "odd"}] |
84 val eo_prednames = [@{binding "even"}, @{binding "odd"}] |
85 val eo_syns = [NoSyn, NoSyn] |
85 val eo_syns = [NoSyn, NoSyn] |
86 val eo_arg_tyss = [[@{typ "nat"}],[@{typ "nat"}]] *} |
86 val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] *} |
87 |
87 |
88 |
88 |
89 ML{*val fresh_defs = [@{thm fresh_def}] |
89 ML{*val fresh_defs = [@{thm fresh_def}] |
90 val fresh_rules = |
90 val fresh_rules = |
91 [@{prop "\<And>a b. a\<noteq>b \<Longrightarrow> a\<sharp>Var b"}, |
91 [@{prop "\<And>a b. a\<noteq>b \<Longrightarrow> a\<sharp>Var b"}, |
101 |
101 |
102 |
102 |
103 subsection {* Definitions *} |
103 subsection {* Definitions *} |
104 |
104 |
105 text {* |
105 text {* |
106 First we have to produce for each predicate the definition, whose general form is |
106 We first have to produce for each predicate the definition, whose general form is |
107 |
107 |
108 @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
108 @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
109 |
109 |
110 and then ``register'' the definition inside a local theory. |
110 and then ``register'' the definition inside a local theory. |
111 To do the latter, we use the following wrapper for |
111 To do the latter, we use the following wrapper for |
122 end*} |
122 end*} |
123 |
123 |
124 text {* |
124 text {* |
125 It returns the definition (as a theorem) and the local theory in which this definition has |
125 It returns the definition (as a theorem) and the local theory in which this definition has |
126 been made. In Line 4, @{ML internalK in Thm} is a flag attached to the |
126 been made. In Line 4, @{ML internalK in Thm} is a flag attached to the |
127 theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}). |
127 theorem (others possibilities are the flags @{ML definitionK in Thm} and @{ML axiomK in Thm}). |
128 These flags just classify theorems and have no significant meaning, except |
128 These flags just classify theorems and have no significant meaning, except |
129 for tools that, for example, find theorems in the theorem database. We also |
129 for tools that, for example, find theorems in the theorem database. We also |
130 use @{ML empty_binding in Attrib} in Line 3, since the definition does |
130 use @{ML empty_binding in Attrib} in Line 3, since the definition does |
131 not need to have any theorem attributes. A testcase for this function is |
131 not need to have any theorem attributes. A testcase for this function is |
132 *} |
132 *} |
133 |
133 |
134 local_setup %gray {* fn lthy => |
134 local_setup %gray {* fn lthy => |
135 let |
135 let |
136 val arg = ((@{binding "MyTrue"}, NoSyn), @{term True}) |
136 val arg = ((@{binding "MyTrue"}, NoSyn), @{term True}) |
137 val (def, lthy') = make_defs arg lthy |
137 val (def, lthy') = make_defs arg lthy |
138 in |
138 in |
139 warning (str_of_thm_no_vars lthy' def); lthy' |
139 warning (str_of_thm_no_vars lthy' def); lthy' |
140 end *} |
140 end *} |
141 |
141 |
216 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"} |
216 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"} |
217 |
217 |
218 The second function for the definitions has to just iterate the function |
218 The second function for the definitions has to just iterate the function |
219 @{ML defs_aux} over all predicates. The argument @{text "preds"} is again |
219 @{ML defs_aux} over all predicates. The argument @{text "preds"} is again |
220 the the list of predicates as @{ML_type term}s; the argument @{text |
220 the the list of predicates as @{ML_type term}s; the argument @{text |
221 "prednames"} is the list of names of the predicates; @{text "arg_tyss"} is |
221 "prednames"} is the list of names of the predicates; @{text syns} are the |
|
222 syntax annotations for each predicate; @{text "arg_tyss"} is |
222 the list of argument-type-lists for each predicate. |
223 the list of argument-type-lists for each predicate. |
223 *} |
224 *} |
224 |
225 |
225 ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy = |
226 ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy = |
226 let |
227 let |
281 Recall that the proof of the induction principle |
282 Recall that the proof of the induction principle |
282 for @{text "even"} was: |
283 for @{text "even"} was: |
283 *} |
284 *} |
284 |
285 |
285 lemma manual_ind_prin: |
286 lemma manual_ind_prin: |
286 assumes prem: "even n" |
287 assumes prem: "even z" |
287 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
288 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z" |
288 apply(atomize (full)) |
289 apply(atomize (full)) |
289 apply(cut_tac prems) |
290 apply(cut_tac prem) |
290 apply(unfold even_def) |
291 apply(unfold even_def) |
291 apply(drule spec[where x=P]) |
292 apply(drule spec[where x=P]) |
292 apply(drule spec[where x=Q]) |
293 apply(drule spec[where x=Q]) |
293 apply(assumption) |
294 apply(assumption) |
294 done |
295 done |
368 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z" |
369 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z" |
369 apply(tactic {* test_tac @{thms prem} *}) |
370 apply(tactic {* test_tac @{thms prem} *}) |
370 done |
371 done |
371 |
372 |
372 text {* |
373 text {* |
|
374 This gives the theorem: |
|
375 |
|
376 \begin{isabelle} |
|
377 \isacommand{thm}~@{thm [source] automatic_ind_prin}\\ |
|
378 @{text "> "}~@{thm automatic_ind_prin} |
|
379 \end{isabelle} |
|
380 |
373 While the tactic for the induction principle is relatively simple, |
381 While the tactic for the induction principle is relatively simple, |
374 it is a bit harder to construct the goals from the introduction |
382 it is a bit harder to construct the goals from the introduction |
375 rules the user provides. In general we have to construct for each predicate |
383 rules the user provides. In general we have to construct for each predicate |
376 @{text "pred"} a goal of the form |
384 @{text "pred"} a goal of the form |
377 |
385 |
415 \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In |
423 \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In |
416 Line 5 we construct the terms corresponding to these variables. |
424 Line 5 we construct the terms corresponding to these variables. |
417 The variables are applied to the predicate in Line 7 (this corresponds |
425 The variables are applied to the predicate in Line 7 (this corresponds |
418 to the first premise @{text "pred zs"} of the induction principle). |
426 to the first premise @{text "pred zs"} of the induction principle). |
419 In Line 8 and 9, we first construct the term @{text "P zs"} |
427 In Line 8 and 9, we first construct the term @{text "P zs"} |
420 and then add the (substituded) introduction rules as premises. In case that |
428 and then add the (substituted) introduction rules as premises. In case that |
421 no introduction rules are given, the conclusion of this implication needs |
429 no introduction rules are given, the conclusion of this implication needs |
422 to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal |
430 to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal |
423 mechanism will fail. |
431 mechanism will fail. |
424 |
432 |
425 In Line 11 we set up the goal to be proved; in the next line we call the |
433 In Line 11 we set up the goal to be proved; in the next line we call the |
426 tactic for proving the induction principle. As mentioned before, this tactic |
434 tactic for proving the induction principle. As mentioned before, this tactic |
427 expects the definitions, the premise and the (certified) predicates with |
435 expects the definitions, the premise and the (certified) predicates with |
428 which the introduction rules have been substituted. The code in these two |
436 which the introduction rules have been substituted. The code in these two |
429 lines will return a theorem. However, it is a theorem |
437 lines will return a theorem. However, it is a theorem |
430 proved inside the local theory @{text "lthy'"}, where the variables @{text |
438 proved inside the local theory @{text "lthy'"}, where the variables @{text |
431 "zs"} are fixed, but free. By exporting this theorem from @{text |
439 "zs"} are fixed, but free (see Line 4). By exporting this theorem from @{text |
432 "lthy'"} (which contains the @{text "zs"} as free) to @{text |
440 "lthy'"} (which contains the @{text "zs"} as free) to @{text |
433 "lthy"} (which does not), we obtain the desired schematic variables @{text "?zs"}. |
441 "lthy"} (which does not), we obtain the desired schematic variables @{text "?zs"}. |
434 A testcase for this function is |
442 A testcase for this function is |
435 *} |
443 *} |
436 |
444 |
455 @{text [display] |
463 @{text [display] |
456 " \<lbrakk>even ?z; P 0; \<And>n. Q n \<Longrightarrow> P (Suc n); \<And>n. P n \<Longrightarrow> Q (Suc n)\<rbrakk> \<Longrightarrow> P ?z"} |
464 " \<lbrakk>even ?z; P 0; \<And>n. Q n \<Longrightarrow> P (Suc n); \<And>n. P n \<Longrightarrow> Q (Suc n)\<rbrakk> \<Longrightarrow> P ?z"} |
457 |
465 |
458 Note that the export from @{text lthy'} to @{text lthy} in Line 13 above |
466 Note that the export from @{text lthy'} to @{text lthy} in Line 13 above |
459 has turned the free, but fixed, @{text "z"} into a schematic |
467 has turned the free, but fixed, @{text "z"} into a schematic |
460 variable @{text "?z"}. The @{text "P"} and @{text "Q"} are not yet |
468 variable @{text "?z"}; the variables @{text "P"} and @{text "Q"} are not yet |
461 schematic. |
469 schematic. |
462 |
470 |
463 We still have to produce the new predicates with which the introduction |
471 We still have to produce the new predicates with which the introduction |
464 rules are substituted and iterate @{ML prove_induction} over all |
472 rules are substituted and iterate @{ML prove_induction} over all |
465 predicates. This is what the second function does: |
473 predicates. This is what the second function does: |
513 which prints out |
521 which prints out |
514 |
522 |
515 @{text [display] |
523 @{text [display] |
516 "> even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow> |
524 "> even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow> |
517 > (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z, |
525 > (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z, |
518 > odd ?z \<Longrightarrow> ?P1 0 |
526 > odd ?z \<Longrightarrow> ?P1 0 \<Longrightarrow> |
519 > \<Longrightarrow> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"} |
527 > (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"} |
520 |
528 |
521 Note that now both, the @{text "?Ps"} and the @{text "?zs"}, are schematic |
529 Note that now both, the @{text "?Ps"} and the @{text "?zs"}, are schematic |
522 variables. The numbers have been introduced by the pretty-printer and are |
530 variables. The numbers have been introduced by the pretty-printer and are |
523 not significant. |
531 not significant. |
524 |
532 |
573 |
581 |
574 @{ML_response_fake [display, gray] |
582 @{ML_response_fake [display, gray] |
575 "warning (str_of_thm_no_vars @{context} |
583 "warning (str_of_thm_no_vars @{context} |
576 (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))" |
584 (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))" |
577 "C"} |
585 "C"} |
578 *} |
586 |
579 |
587 We now look closely at the proof for the introduction rule |
580 ML {* prems_of *} |
588 |
581 ML {* Logic.strip_params *} |
589 \begin{isabelle} |
582 ML {* Logic.strip_assums_hyp *} |
590 @{term "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"} |
583 |
591 \end{isabelle} |
584 ML {* |
592 |
585 fun chop_print (params1, params2) (prems1, prems2) ctxt = |
593 *} |
586 let |
|
587 val _ = warning ((commas params1) ^ " | " ^ (commas params2)) |
|
588 val _ = warning ((commas (map (Syntax.string_of_term ctxt) prems1)) ^ " | " ^ |
|
589 (commas (map (Syntax.string_of_term ctxt) prems2))) |
|
590 in |
|
591 () |
|
592 end |
|
593 *} |
|
594 |
|
595 |
|
596 |
|
597 lemma intro1: |
|
598 shows "\<And>m. odd m \<Longrightarrow> even (Suc m)" |
|
599 apply(tactic {* ObjectLogic.rulify_tac 1 *}) |
|
600 apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *}) |
|
601 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *}) |
|
602 oops |
|
603 |
|
604 ML {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *} |
|
605 |
594 |
606 |
595 |
607 lemma fresh_App: |
596 lemma fresh_App: |
608 shows "\<And>a t s. \<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s" |
597 shows "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s" |
609 apply(tactic {* ObjectLogic.rulify_tac 1 *}) |
598 apply(tactic {* ObjectLogic.rulify_tac 1 *}) |
610 apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *}) |
599 apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *}) |
611 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *}) |
600 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *}) |
612 apply(tactic {* print_tac "" *}) |
601 apply(tactic {* print_tac "" *}) |
|
602 |
|
603 txt {* |
|
604 \begin{isabelle} |
|
605 @{subgoals} |
|
606 \end{isabelle} |
|
607 *} |
|
608 |
|
609 ML_prf {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *} |
|
610 |
613 apply(tactic {* SUBPROOF_test (fn {params, prems, ...} => |
611 apply(tactic {* SUBPROOF_test (fn {params, prems, ...} => |
614 let |
612 let |
615 val (prems1, prems2) = chop (length prems - length fresh_rules) prems |
613 val (prems1, prems2) = chop (length prems - length fresh_rules) prems |
616 val (params1, params2) = chop (length params - length fresh_preds) params |
614 val (params1, params2) = chop (length params - length fresh_preds) params |
617 in |
615 in |