# HG changeset patch # User wenzelm # Date 1189969483 -7200 # Node ID 7acbb982fc771a874d59d29c9fc1b858e3818884 # Parent 98689b0e595684e9a0514d29803700c2d63a363b moved induct patterns to HOL/Induct/Common_Patterns.thy; diff -r 98689b0e5956 -r 7acbb982fc77 NEWS --- a/NEWS Sun Sep 16 20:25:43 2007 +0200 +++ b/NEWS Sun Sep 16 21:04:43 2007 +0200 @@ -446,75 +446,25 @@ Typically, the constant `partial_order.less' is created by a definition specification element in the context of locale partial_order. -* Provers/induct: improved internal context management to support -local fixes and defines on-the-fly. Thus explicit meta-level -connectives !! and ==> are rarely required anymore in inductive goals -(using object-logic connectives for this purpose has been long -obsolete anyway). The subsequent proof patterns illustrate advanced -techniques of natural induction; general datatypes and inductive sets -work analogously (see also src/HOL/Lambda for realistic examples). - -(1) This is how to ``strengthen'' an inductive goal wrt. certain -parameters: - - lemma - fixes n :: nat and x :: 'a - assumes a: "A n x" - shows "P n x" - using a -- {* make induct insert fact a *} - proof (induct n arbitrary: x) -- {* generalize goal to "!!x. A n x ==> P n x" *} - case 0 - show ?case sorry - next - case (Suc n) - note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *} - note `A (Suc n) x` -- {* induction premise, stemming from fact a *} - show ?case sorry - qed - -(2) This is how to perform induction over ``expressions of a certain -form'', using a locally defined inductive parameter n == "a x" -together with strengthening (the latter is usually required to get -sufficiently flexible induction hypotheses): - - lemma - fixes a :: "'a => nat" - assumes a: "A (a x)" - shows "P (a x)" - using a - proof (induct n == "a x" arbitrary: x) - ... - -See also HOL/Isar_examples/Puzzle.thy for an application of the this -particular technique. - -(3) This is how to perform existential reasoning ('obtains' or -'obtain') by induction, while avoiding explicit object-logic -encodings: - - lemma - fixes n :: nat - obtains x :: 'a where "P n x" and "Q n x" - proof (induct n arbitrary: thesis) - case 0 - obtain x where "P 0 x" and "Q 0 x" sorry - then show thesis by (rule 0) - next - case (Suc n) - obtain x where "P n x" and "Q n x" by (rule Suc.hyps) - obtain x where "P (Suc n) x" and "Q (Suc n) x" sorry - then show thesis by (rule Suc.prems) - qed - -Here the 'arbitrary: thesis' specification essentially modifies the -scope of the formal thesis parameter, in order to the get the whole -existence statement through the induction as expected. - -* Provers/induct: mutual induction rules are now specified as a list -of rule sharing the same induction cases. HOL packages usually -provide foo_bar.inducts for mutually defined items foo and bar -(e.g. inductive sets or datatypes). INCOMPATIBILITY, users need to -specify mutual induction rules differently, i.e. like this: +* Provers/induct: improved internal context management to support local +fixes and defines on-the-fly. Thus explicit meta-level connectives !! +and ==> are rarely required anymore in inductive goals (using +object-logic connectives for this purpose has been long obsolete +anyway). Common proof patterns are explained in +HOL/Induct/Common_Patterns.thy, see also HOL/Isar_examples/Puzzle.thy +and src/HOL/Lambda for realistic examples. + +* Provers/induct: improved handling of simultaneous goals. Instead of +introducing object-level conjunction, the statement is now split into +several conclusions, while the corresponding symbolic cases are nested +accordingly. INCOMPATIBILITY, proofs need to be structured explicitly, +see HOL/Induct/Common_Patterns.thy, for example. + +* Provers/induct: mutual induction rules are now specified as a list of +rule sharing the same induction cases. HOL packages usually provide +foo_bar.inducts for mutually defined items foo and bar (e.g. inductive +sets or datatypes). INCOMPATIBILITY, users need to specify mutual +induction rules differently, i.e. like this: (induct rule: foo_bar.inducts) (induct set: foo bar) @@ -523,75 +473,7 @@ The ML function ProjectRule.projections turns old-style rules into the new format. -* Provers/induct: improved handling of simultaneous goals. Instead of -introducing object-level conjunction, the statement is now split into -several conclusions, while the corresponding symbolic cases are -nested accordingly. INCOMPATIBILITY, proofs need to be structured -explicitly. For example: - - lemma - fixes n :: nat - shows "P n" and "Q n" - proof (induct n) - case 0 case 1 - show "P 0" sorry - next - case 0 case 2 - show "Q 0" sorry - next - case (Suc n) case 1 - note `P n` and `Q n` - show "P (Suc n)" sorry - next - case (Suc n) case 2 - note `P n` and `Q n` - show "Q (Suc n)" sorry - qed - -The split into subcases may be deferred as follows -- this is -particularly relevant for goal statements with local premises. - - lemma - fixes n :: nat - shows "A n ==> P n" and "B n ==> Q n" - proof (induct n) - case 0 - { - case 1 - note `A 0` - show "P 0" sorry - next - case 2 - note `B 0` - show "Q 0" sorry - } - next - case (Suc n) - note `A n ==> P n` and `B n ==> Q n` - { - case 1 - note `A (Suc n)` - show "P (Suc n)" sorry - next - case 2 - note `B (Suc n)` - show "Q (Suc n)" sorry - } - qed - -If simultaneous goals are to be used with mutual rules, the statement -needs to be structured carefully as a two-level conjunction, using -lists of propositions separated by 'and': - - lemma - shows "a : A ==> P1 a" - "a : A ==> P2 a" - and "b : B ==> Q1 b" - "b : B ==> Q2 b" - "b : B ==> Q3 b" - proof (induct set: A B) - -* Provers/induct: support coinduction as well. See +* Provers/induct: support coinduction as well. See src/HOL/Library/Coinductive_List.thy for various examples. * Attribute "symmetric" produces result with standardized schematic