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

author | wenzelm |

Fri, 28 May 1999 13:30:59 +0200 | |

changeset 6746 | cf6ad8d22793 |

parent 6745 | 74e8f703f5f2 |

child 6747 | cee5adcc1f5c |

tuned formal comments;

--- a/src/HOL/Isar_examples/BasicLogic.thy Fri May 28 11:42:07 1999 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Fri May 28 13:30:59 1999 +0200 @@ -77,7 +77,7 @@ qed; -(* propositional proof (from 'Introduction to Isabelle') *) +text {* propositional proof (from 'Introduction to Isabelle') *}; lemma "P | P --> P"; proof; @@ -97,7 +97,7 @@ qed; -(* quantifier proof (from 'Introduction to Isabelle') *) +text {* quantifier proof (from 'Introduction to Isabelle') *}; lemma "(EX x. P(f(x))) --> (EX x. P(x))"; proof;

--- a/src/HOL/Isar_examples/Cantor.thy Fri May 28 11:42:07 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Fri May 28 13:30:59 1999 +0200 @@ -9,7 +9,7 @@ theory Cantor = Main:; -section "Example: Cantor's Theorem"; +section {* Example: Cantor's Theorem *}; text {* Cantor's Theorem states that every set has more subsets than it has

--- a/src/HOL/Isar_examples/ExprCompiler.thy Fri May 28 11:42:07 1999 +0200 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Fri May 28 13:30:59 1999 +0200 @@ -7,12 +7,10 @@ theory ExprCompiler = Main:; -title - "Correctness of a simple expression/stack-machine compiler --- an Isabelle/Isar demonstration" - "Markus Wenzel"; +title {* Correctness of a simple expression/stack-machine compiler *}; -section "Basics"; +section {* Basics *}; text {* First we define a type abbreviation for binary operations over some @@ -23,7 +21,7 @@ 'val binop = "'val => 'val => 'val"; -section "Machine"; +section {* Machine *}; text {* Next we model a simple stack machine, with three instructions. @@ -55,7 +53,7 @@ "execute instrs env == hd (exec instrs [] env)"; -section "Expressions"; +section {* Expressions *}; text {* We introduce a simple language of expressions: variables --- @@ -80,7 +78,7 @@ "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"; -section "Compiler"; +section {* Compiler *}; text {* So we are ready to define the compilation function of expressions to @@ -101,7 +99,6 @@ @{term "comp"}. We first establish some lemmas. *}; - lemma exec_append: "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs"); proof (induct ??P xs type: list); @@ -119,7 +116,6 @@ qed; qed; - lemma exec_comp: "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e"); proof (induct ??P e type: expr); @@ -133,7 +129,7 @@ qed; -text "Main theorem ahead."; +text {* Main theorem ahead. *}; theorem correctness: "execute (comp e) env = eval e env"; by (simp add: execute_def exec_comp);

--- a/src/HOL/Isar_examples/NatSum.thy Fri May 28 11:42:07 1999 +0200 +++ b/src/HOL/Isar_examples/NatSum.thy Fri May 28 13:30:59 1999 +0200 @@ -5,9 +5,9 @@ theory NatSum = Main:; -section "Summing natural numbers"; +section {* Summing natural numbers *}; -text "A summation operator: sum f (n+1) is the sum of all f(i), i=0...n."; +text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *}; consts sum :: "[nat => nat, nat] => nat"; @@ -20,9 +20,9 @@ (*theorems [simp] = add_assoc add_commute add_left_commute add_mult_distrib add_mult_distrib2;*) -subsection "The sum of the first n positive integers equals n(n+1)/2"; +subsection {* The sum of the first n positive integers equals n(n+1)/2 *}; -text "Emulate Isabelle proof script:"; +text {* Emulate Isabelle proof script: *}; (* Goal "2*sum (%i. i) (Suc n) = n*Suc(n)"; @@ -42,8 +42,8 @@ qed_with sum_of_naturals; -text "Proper Isabelle/Isar proof expressing the same reasoning (which - is apparently not the most natural one):"; +text {* Proper Isabelle/Isar proof expressing the same reasoning (which + is apparently not the most natural one): *}; theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n"; proof simp; @@ -55,9 +55,9 @@ qed; -subsection "The sum of the first n odd numbers equals n squared"; +subsection {* The sum of the first n odd numbers equals n squared *}; -text "First version: `proof-by-induction'"; +text {* First version: `proof-by-induction' *}; theorem sum_of_odds: "sum (%i. Suc (i + i)) n = n * n" (is "??P n"); proof (induct n); @@ -65,8 +65,8 @@ fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp); qed; -text "The second version tells more about what is going on during the -induction."; +text {* The second version tells more about what is going on during the +induction. *}; theorem sum_of_odds': "sum (%i. Suc (i + i)) n = n * n" (is "??P n"); proof (induct n);

--- a/src/HOL/Isar_examples/Peirce.thy Fri May 28 11:42:07 1999 +0200 +++ b/src/HOL/Isar_examples/Peirce.thy Fri May 28 13:30:59 1999 +0200 @@ -1,12 +1,11 @@ (* Title: HOL/Isar_examples/Peirce.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen - -Peirce's law: examples of classical proof. *) theory Peirce = Main:; +text {* Peirce's law: examples of classical proof. *}; theorem "((A --> B) --> A) --> A"; proof;

--- a/src/HOL/ex/Points.thy Fri May 28 11:42:07 1999 +0200 +++ b/src/HOL/ex/Points.thy Fri May 28 13:30:59 1999 +0200 @@ -5,11 +5,11 @@ theory Points = Main:; -title "Basic use of extensible records in HOL, including the famous points - and coloured points."; +title {* Basic use of extensible records in HOL, including the famous points + and coloured points. *}; -section "Points"; +section {* Points *}; record point = x :: nat @@ -42,14 +42,14 @@ consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)"; -subsection "Introducing concrete records and record schemes"; +subsection {* Introducing concrete records and record schemes *}; defs foo1_def: "foo1 == (| x = 1, y = 0 |)" foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)"; -subsection "Record selection and record update"; +subsection {* Record selection and record update *}; constdefs getX :: "('a::more) point_scheme => nat" @@ -58,13 +58,13 @@ "setX r n == r (| x := n |)"; -subsection "Some lemmas about records"; +subsection {* Some lemmas about records *}; -text "Note: any of these goals may be solved with a single - stroke of auto or force."; +text {* Note: any of these goals may be solved with a single + stroke of the auto or force proof method. *}; -text "basic simplifications"; +text {* basic simplifications *}; lemma "x (| x = m, y = n, ... = p |) = m"; by simp; @@ -73,7 +73,7 @@ by simp; -text "splitting quantifiers: the !!r is NECESSARY"; +text {* splitting quantifiers: the !!r is NECESSARY *}; lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"; proof record_split; @@ -92,7 +92,7 @@ qed; -text "equality of records"; +text {* equality of records *}; lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "??EQ --> _"); proof; @@ -101,14 +101,14 @@ qed; -text "concrete records are type instances of record schemes"; +text {* concrete records are type instances of record schemes *}; constdefs foo5 :: nat "foo5 == getX (| x = 1, y = 0 |)"; -text "manipulating the `...' (more) part"; +text {* manipulating the `...' (more) part *}; constdefs incX :: "('a::more) point_scheme => 'a point_scheme" @@ -121,7 +121,7 @@ qed; -text "alternative definition"; +text {* alternative definition *}; constdefs incX' :: "('a::more) point_scheme => 'a point_scheme" @@ -129,7 +129,7 @@ -section "coloured points: record extension"; +section {* coloured points: record extension *}; datatype colour = Red | Green | Blue; @@ -150,16 +150,16 @@ consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"; -text "functions on point schemes work for cpoints as well"; +text {* functions on point schemes work for cpoints as well *}; constdefs foo10 :: nat "foo10 == getX (| x = 2, y = 0, colour = Blue |)"; -subsection "Non-coercive structural subtyping"; +subsection {* Non-coercive structural subtyping *}; -text "foo11 has type cpoint, not type point --- Great!"; +text {* foo11 has type cpoint, not type point --- Great! *}; constdefs foo11 :: cpoint @@ -167,9 +167,9 @@ -section "Other features"; +section {* Other features *}; -text "field names contribute to record identity"; +text {* field names contribute to record identity *}; record point' = x' :: nat @@ -181,7 +181,7 @@ text {* Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid *}; -text "polymorphic records"; +text {* polymorphic records *}; record 'a point'' = point + content :: 'a; @@ -189,6 +189,6 @@ types cpoint'' = "colour point''"; -text "Have a lot of fun!"; +text {* Have a lot of fun! *}; end;