tuned;
authorwenzelm
Thu Sep 27 15:42:08 2001 +0200 (2001-09-27)
changeset 11586d8a7f6318457
parent 11585 35a79fd062f7
child 11587 cf448586f26a
tuned;
src/HOL/ex/Antiquote.thy
src/HOL/ex/Multiquote.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/StringEx.thy
src/HOL/ex/mesontest2.thy
     1.1 --- a/src/HOL/ex/Antiquote.thy	Thu Sep 27 15:42:01 2001 +0200
     1.2 +++ b/src/HOL/ex/Antiquote.thy	Thu Sep 27 15:42:08 2001 +0200
     1.3 @@ -2,14 +2,17 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.7 -
     1.8 -Simple quote / antiquote example.
     1.9  *)
    1.10  
    1.11  header {* Antiquotations *}
    1.12  
    1.13  theory Antiquote = Main:
    1.14  
    1.15 +text {*
    1.16 +  A simple example on quote / antiquote in higher-order abstract
    1.17 +  syntax.
    1.18 +*}
    1.19 +
    1.20  syntax
    1.21    "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
    1.22  
    1.23 @@ -35,4 +38,3 @@
    1.24  term "Expr (\<lambda>env. f env + g env y + h a env z)"
    1.25  
    1.26  end
    1.27 -
     2.1 --- a/src/HOL/ex/Multiquote.thy	Thu Sep 27 15:42:01 2001 +0200
     2.2 +++ b/src/HOL/ex/Multiquote.thy	Thu Sep 27 15:42:08 2001 +0200
     2.3 @@ -2,15 +2,17 @@
     2.4      ID:         $Id$
     2.5      Author:     Markus Wenzel, TU Muenchen
     2.6      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.7 -
     2.8 -Multiple nested quotations and anti-quotations -- basically a
     2.9 -generalized version of de-Bruijn representation.
    2.10  *)
    2.11  
    2.12  header {* Multiple nested quotations and anti-quotations *}
    2.13  
    2.14  theory Multiquote = Main:
    2.15  
    2.16 +text {*
    2.17 +  Multiple nested quotations and anti-quotations -- basically a
    2.18 +  generalized version of de-Bruijn representation.
    2.19 +*}
    2.20 +
    2.21  syntax
    2.22    "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
    2.23    "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
     3.1 --- a/src/HOL/ex/NatSum.thy	Thu Sep 27 15:42:01 2001 +0200
     3.2 +++ b/src/HOL/ex/NatSum.thy	Thu Sep 27 15:42:08 2001 +0200
     3.3 @@ -36,7 +36,8 @@
     3.4  *}
     3.5  
     3.6  lemma sum_of_odd_squares:
     3.7 -  "#3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) = n * (#4 * n * n - #1)"
     3.8 +  "#3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) =
     3.9 +    n * (#4 * n * n - #1)"
    3.10    apply (induct n)
    3.11    txt {* This removes the @{term "-#1"} from the inductive step *}
    3.12     apply (case_tac [2] n)
    3.13 @@ -61,17 +62,20 @@
    3.14    \medskip The sum of the first @{term n} positive integers equals
    3.15    @{text "n (n + 1) / 2"}.*}
    3.16  
    3.17 -lemma sum_of_naturals: "#2 * setsum id (atMost n) = n * Suc n"
    3.18 +lemma sum_of_naturals:
    3.19 +    "#2 * setsum id (atMost n) = n * Suc n"
    3.20    apply (induct n)
    3.21     apply auto
    3.22    done
    3.23  
    3.24 -lemma sum_of_squares: "#6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)"
    3.25 +lemma sum_of_squares:
    3.26 +    "#6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)"
    3.27    apply (induct n)
    3.28     apply auto
    3.29    done
    3.30  
    3.31 -lemma sum_of_cubes: "#4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
    3.32 +lemma sum_of_cubes:
    3.33 +    "#4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n"
    3.34    apply (induct n)
    3.35     apply auto
    3.36    done
     4.1 --- a/src/HOL/ex/ROOT.ML	Thu Sep 27 15:42:01 2001 +0200
     4.2 +++ b/src/HOL/ex/ROOT.ML	Thu Sep 27 15:42:08 2001 +0200
     4.3 @@ -8,6 +8,20 @@
     4.4  time_use_thy "Recdefs";
     4.5  time_use_thy "Primrec";
     4.6  
     4.7 +setmp proofs 2 time_use_thy "Hilbert_Classical";
     4.8 +
     4.9 +(*advanced concrete syntax*)
    4.10 +time_use_thy "Tuple";
    4.11 +time_use_thy "Antiquote";
    4.12 +time_use_thy "Multiquote";
    4.13 +
    4.14 +(*basic use of extensible records*)
    4.15 +time_use_thy "MonoidGroup";
    4.16 +time_use_thy "Records";
    4.17 +
    4.18 +time_use_thy "StringEx";
    4.19 +time_use_thy "BinEx";
    4.20 +
    4.21  time_use_thy "NatSum";
    4.22  time_use     "cla.ML";
    4.23  time_use     "mesontest.ML";
    4.24 @@ -24,16 +38,4 @@
    4.25  time_use_thy "MT";
    4.26  time_use_thy "Tarski";
    4.27  
    4.28 -time_use_thy "StringEx";
    4.29 -time_use_thy "BinEx";
    4.30 -
    4.31  if_svc_enabled time_use_thy "svc_test";
    4.32 -
    4.33 -(*basic use of extensible records*)
    4.34 -time_use_thy "MonoidGroup";
    4.35 -time_use_thy "Records";
    4.36 -
    4.37 -(*advanced concrete syntax*)
    4.38 -time_use_thy "Tuple";
    4.39 -time_use_thy "Antiquote";
    4.40 -time_use_thy "Multiquote";
     5.1 --- a/src/HOL/ex/StringEx.thy	Thu Sep 27 15:42:01 2001 +0200
     5.2 +++ b/src/HOL/ex/StringEx.thy	Thu Sep 27 15:42:08 2001 +0200
     5.3 @@ -15,7 +15,8 @@
     5.4  lemma "''ABCD'' = ''ABCD''"
     5.5    by simp
     5.6  
     5.7 -lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq> ''ABCDEFGHIJKLMNOPQRSTUVWXY''"
     5.8 +lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq>
     5.9 +  ''ABCDEFGHIJKLMNOPQRSTUVWXY''"
    5.10    by simp
    5.11  
    5.12  lemma "set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}"
     6.1 --- a/src/HOL/ex/mesontest2.thy	Thu Sep 27 15:42:01 2001 +0200
     6.2 +++ b/src/HOL/ex/mesontest2.thy	Thu Sep 27 15:42:08 2001 +0200
     6.3 @@ -1,8 +1,7 @@
     6.4  
     6.5 -(*Theory Product_Type instead of HOL regards arguments as tuples.
     6.6 -  But theory Main would allow clashes with many other constants.*)
     6.7 +header {* Meson test cases *}
     6.8  
     6.9 -theory mesontest2 = Product_Type:
    6.10 +theory mesontest2 = Main:
    6.11  
    6.12  hide const inverse divide
    6.13