summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 28 Jun 2002 20:01:09 +0200 | |

changeset 13258 | 8f394f266025 |

parent 13257 | 1b7104a1c0bd |

child 13259 | 01fa0c8dbc92 |

*** empty log message ***

doc-src/TutorialI/Overview/Isar0.thy | file | annotate | diff | comparison | revisions | |

doc-src/TutorialI/Overview/delete-verbatim | file | annotate | diff | comparison | revisions | |

doc-src/TutorialI/Overview/makeDemo | file | annotate | diff | comparison | revisions |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Overview/Isar0.thy Fri Jun 28 20:01:09 2002 +0200 @@ -0,0 +1,308 @@ +theory Isar0 = Main: + +(* +proof ::= "proof" [method] statement* "qed" + | "by" method +statement ::= "fix" variables + | "assume" proposition* + | ["then"] ("show" | "have") proposition proof +proposition ::= [label":"] string + +Typical skelton: + +proof +assume <assumptions> +have <formula1> -- intermediate result +: +have <formulan> -- intermediate result +show ?thesis -- the conclusion +end +*) + +lemma "A \<longrightarrow> A" +proof (rule impI) + assume A: "A" + show "A" by(rule A) +qed + +(* Operational reading: assume A - show A proves "A \<Longrightarrow> A", which rule impI +turns into the desired "A \<longrightarrow> A". Too much (operational) text *) + +(* 1st Principle: let "proof" select the rule automatically; based on the +goal and a predefined list of (introduction) rules. Here: impI is found +automatically: *) + +lemma "A \<longrightarrow> A" +proof + assume A: "A" + show "A" by(rule A) +qed + +(* Proof by assumption should be trivial. Method "." does just that (and a +bit more - see later). Thus naming of assumptions is often superfluous. *) + +lemma "A \<longrightarrow> A" +proof + assume "A" + have "A" . +qed + +(* To hide proofs by assumption, by(method) first applies method and then +tries to solve all remaining subgoals by assumption. *) + +lemma "A \<longrightarrow> A & A" +proof + assume A + show "A & A" by(rule conjI) +qed + +(* Proofs of the form by(rule <rule>) can be abbreviated to ".." if <rule> is +one of the predefined introduction rules (for user supplied rules see below). +Thus +*) + +lemma "A \<longrightarrow> A & A" +proof + assume A + show "A & A" .. +qed + +(* What happens: applies "conj" (first "."), then solves the two subgoals by +assumptions (second ".") *) + +(* Now: elimination *) + +lemma "A & B \<longrightarrow> B & A" +proof + assume AB: "A & B" + show "B & A" + proof (rule conjE[OF AB]) + assume A and B + show ?thesis .. --"thesis = statement in previous show" + qed +qed + +(* Again: too much text. + +Elimination rules are used to conclude new stuff from old. In Isar they are +triggered by propositions being fed INTO a proof block. Syntax: +from <previously proved propositions> show \<dots> +applies an elimination rule whose first premise matches one of the <previously proved propositions>. Thus: +*) + +lemma "A & B \<longrightarrow> B & A" +proof + assume AB: "A & B" + from AB show "B & A" + proof + assume A and B + show ?thesis .. + qed +qed + +(* +2nd principle: try to arrange sequence of propositions in a UNIX like +pipe, such that the proof of the next proposition uses the previous +one. The previous proposition can be referred to via "this". +This greatly reduces the need for explicit naming of propositions. +*) +lemma "A & B \<longrightarrow> B & A" +proof + assume "A & B" + from this show "B & A" + proof + assume A and B + show ?thesis .. + qed +qed + +(* Final simplification: "from this" = "thus". + +Alternative: pure forward reasoning: *) + +lemma "A & B --> B & A" +proof + assume ab: "A & B" + from ab have a: A .. + from ab have b: B .. + from b a show "B & A" .. +qed + +(* New: itermediate haves *) + +(* The predefined introduction and elimination rules include all the usual +natural deduction rules for propositional logic. Here is a longer example: *) + +lemma "~(A & B) \<longrightarrow> ~A | ~B" +proof + assume n: "~(A & B)" + show "~A | ~B" + proof (rule ccontr) + assume nn: "~(~ A | ~B)" + from n show False + proof + show "A & B" + proof + show A + proof (rule ccontr) + assume "~A" + have "\<not> A \<or> \<not> B" .. + from nn this show False .. + qed + next + show B + proof (rule ccontr) + assume "~B" + have "\<not> A \<or> \<not> B" .. + from nn this show False .. + qed + qed + qed + qed +qed; + +(* New: + +1. Multiple subgoals. When showing "A & B" we need to show both A and B. +Each subgoal is proved separately, in ANY order. The individual proofs are +separated by "next". + +2. "have" for proving an intermediate fact +*) + +subsection{*Becoming more concise*} + +(* Normally want to prove rules expressed with \<Longrightarrow>, not \<longrightarrow> *) + +lemma "\<lbrakk> A \<Longrightarrow> False \<rbrakk> \<Longrightarrow> \<not> A" +proof + assume "A \<Longrightarrow> False" A + thus False . +qed + +(* In this case the "proof" works on the "~A", thus selecting notI + +Now: avoid repeating formulae (which may be large). *) + +lemma "(large_formula \<Longrightarrow> False) \<Longrightarrow> ~ large_formula" + (is "(?P \<Longrightarrow> _) \<Longrightarrow> _") +proof + assume "?P \<Longrightarrow> False" ?P + thus False . +qed + +(* Even better: can state assumptions directly *) + +lemma assumes A: "large_formula \<Longrightarrow> False" + shows "~ large_formula" (is "~ ?P") +proof + assume ?P + from A show False . +qed; + + +(* Predicate calculus. Keyword fix introduces new local variables into a +proof. Corresponds to !! just like assume-show corresponds to \<Longrightarrow> *) + +lemma assumes P: "!x. P x" shows "!x. P(f x)" +proof --"allI" + fix x + from P show "P(f x)" .. --"allE" +qed + +lemma assumes Pf: "EX x. P (f x)" shows "EX y. P y" +proof - + from Pf show ?thesis + proof --"exE" + fix a + assume "P(f a)" + show ?thesis .. --"exI" + qed +qed + +text {* + Explicit $\exists$-elimination as seen above can become quite + cumbersome in practice. The derived Isar language element + ``\isakeyword{obtain}'' provides a more handsome way to do + generalized existence reasoning. +*} + +lemma assumes Pf: "EX x. P (f x)" shows "EX y. P y" +proof - + from Pf obtain a where "P (f a)" .. --"exE" + thus "EX y. P y" .. --"exI" +qed + +text {* + Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and + \isakeyword{assume} together with a soundness proof of the + elimination involved. Thus it behaves similar to any other forward + proof element. Also note that due to the nature of general existence + reasoning involved here, any result exported from the context of an + \isakeyword{obtain} statement may \emph{not} refer to the parameters + introduced there. +*} + +lemma assumes ex: "EX x. ALL y. P x y" shows "ALL y. EX x. P x y" +proof --"allI" + fix y + from ex obtain x where "ALL y. P x y" .. --"exE" + from this have "P x y" .. --"allE" + thus "EX x. P x y" .. --"exI" +qed + +(* some example with blast, if . and .. fail *) + +theorem "EX S. S ~: range (f :: 'a => 'a set)" +proof + let ?S = "{x. x ~: f x}" + show "?S ~: range f" + proof + assume "?S : range f" + then obtain y where fy: "?S = f y" .. + show False + proof (cases) + assume "y : ?S" + with fy show False by blast + next + assume "y ~: ?S" + with fy show False by blast + qed + qed +qed + +theorem "EX S. S ~: range (f :: 'a => 'a set)" +proof + let ?S = "{x. x ~: f x}" + show "?S ~: range f" + proof + assume "?S : range f" + then obtain y where eq: "?S = f y" .. + show False + proof (cases) + assume A: "y : ?S" + hence isin: "y : f y" by(simp add:eq) + from A have "y ~: f y" by simp + with isin show False by contradiction + next + assume A: "y ~: ?S" + hence notin: "y ~: f y" by(simp add:eq) + from A have "y : f y" by simp + with notin show False by contradiction + qed + qed +qed + +text {* + How much creativity is required? As it happens, Isabelle can prove + this theorem automatically using best-first search. Depth-first + search would diverge, but best-first search successfully navigates + through the large search space. The context of Isabelle's classical + prover contains rules for the relevant constructs of HOL's set + theory. +*} + +theorem "EX S. S ~: range (f :: 'a => 'a set)" + by best + +end

--- a/doc-src/TutorialI/Overview/delete-verbatim Fri Jun 28 19:51:40 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -#!/usr/bin/perl -w - -sub doit { - my ($file) = @_; - - open (FILE, $file) || die $!; - undef $/; $text = <FILE>; $/ = "\n"; - close FILE || die $!; - - $_ = $text; - - s/text_raw\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here - s/text\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here - s/\(\*<\*\)//sg; - s/\(\*>\*\)//sg; - - $result = $_; - - if ($text ne $result) { - print STDERR "fixing $file\n"; -# if (! -f "$file~~") { -# rename $file, "$file~~" || die $!; -# } - open (FILE, "> Demo/$file") || die $!; - print FILE $result; - close FILE || die $!; - } -} - - -foreach $file (@ARGV) { - eval { &doit($file); }; - if ($@) { print STDERR "*** doit $file: ", $@, "\n"; } -}

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Overview/makeDemo Fri Jun 28 20:01:09 2002 +0200 @@ -0,0 +1,34 @@ +#!/usr/bin/perl -w + +sub doit { + my ($file) = @_; + + open (FILE, $file) || die $!; + undef $/; $text = <FILE>; $/ = "\n"; + close FILE || die $!; + + $_ = $text; + + s/text_raw\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here + s/text\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here + s/\(\*<\*\)//sg; + s/\(\*>\*\)//sg; + + $result = $_; + + if ($text ne $result) { + print STDERR "fixing $file\n"; +# if (! -f "$file~~") { +# rename $file, "$file~~" || die $!; +# } + open (FILE, "> Demo/$file") || die $!; + print FILE $result; + close FILE || die $!; + } +} + + +foreach $file (@ARGV) { + eval { &doit($file); }; + if ($@) { print STDERR "*** doit $file: ", $@, "\n"; } +}