author nipkow Mon, 01 Jul 2002 16:43:50 +0200 changeset 13265 a8b5f0df6602 parent 13264 b698804db01a child 13266 2a6ad4357d72
*** empty log message ***
 doc-src/TutorialI/Overview/Isar0.thy file | annotate | diff | comparison | revisions
--- a/doc-src/TutorialI/Overview/Isar0.thy	Mon Jul 01 16:30:40 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,326 +0,0 @@
-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
-
-(* Finally, whole scripts may appear in the leaves of the proof tree,
-although this is best avoided. Here is a contrived example. *)
-
-lemma "A \<longrightarrow> (A \<longrightarrow>B) \<longrightarrow> B"
-proof
-  assume A: A
-  show "(A \<longrightarrow>B) \<longrightarrow> B"
-    apply(rule impI)
-    apply(erule impE)
-    apply(rule A)
-    apply assumption
-    done
-qed
-
-
-(* You may need to resort to this technique if an automatic step fails to
-prove the desired proposition. *)
-
-end