tuned;
authorwenzelm
Wed Dec 19 00:26:04 2001 +0100 (2001-12-19)
changeset 125460c90e581379f
parent 12545 7319d384d0d3
child 12547 46d21c784c07
tuned;
etc/settings
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Expr.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Natural.thy
src/HOL/IMP/Transition.thy
src/HOL/IMP/document/root.tex
src/HOLCF/IMP/HoareEx.thy
src/HOLCF/IMP/document/root.tex
src/Pure/Isar/locale.ML
     1.1 --- a/etc/settings	Tue Dec 18 21:28:01 2001 +0100
     1.2 +++ b/etc/settings	Wed Dec 19 00:26:04 2001 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  # binaries.  Do not invent new ML system names unless you know what
     1.5  # you are doing.  Only one of the sections below should be activated.
     1.6  
     1.7 -# Poly/ML 3.x and 4.0 or later
     1.8 +# Poly/ML 3.x, 4.0, 4.1, and 4.1.1
     1.9  if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
    1.10    #maybe a shrink-wrapped polyml-4.1.1 on x86-linux ...
    1.11    ML_SYSTEM=polyml-4.1.1
    1.12 @@ -120,7 +120,7 @@
    1.13  [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
    1.14    { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
    1.15  
    1.16 -# Users may want to change this.
    1.17 +# Users may want to override this.
    1.18  ISABELLE_LOGIC=HOL
    1.19  
    1.20  
     2.1 --- a/src/HOL/IMP/Compiler.thy	Tue Dec 18 21:28:01 2001 +0100
     2.2 +++ b/src/HOL/IMP/Compiler.thy	Wed Dec 19 00:26:04 2001 +0100
     2.3 @@ -19,15 +19,15 @@
     2.4  consts  stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
     2.5  
     2.6  syntax
     2.7 -  "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
     2.8 +  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
     2.9                 ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
    2.10 -  "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.11 +  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.12                 ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
    2.13  
    2.14  syntax (xsymbols)
    2.15 -  "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.16 +  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.17                 ("_ \<turnstile> \<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
    2.18 -  "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.19 +  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    2.20                 ("_ \<turnstile>/ \<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
    2.21  
    2.22  translations  
     3.1 --- a/src/HOL/IMP/Expr.thy	Tue Dec 18 21:28:01 2001 +0100
     3.2 +++ b/src/HOL/IMP/Expr.thy	Wed Dec 19 00:26:04 2001 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  
     3.5  header "Expressions"
     3.6  
     3.7 -theory Expr = Datatype:
     3.8 +theory Expr = Main:
     3.9  
    3.10  text {*
    3.11    Arithmetic expressions and Boolean expressions.
    3.12 @@ -14,49 +14,46 @@
    3.13  *}
    3.14  
    3.15  subsection "Arithmetic expressions"
    3.16 -typedecl loc 
    3.17 +typedecl loc
    3.18  
    3.19  types
    3.20    state = "loc => nat"
    3.21 -  n2n = "nat => nat"
    3.22 -  n2n2n = "nat => nat => nat"
    3.23  
    3.24  datatype
    3.25    aexp = N nat
    3.26         | X loc
    3.27 -       | Op1 n2n aexp
    3.28 -       | Op2 n2n2n aexp aexp
    3.29 +       | Op1 "nat => nat" aexp
    3.30 +       | Op2 "nat => nat => nat" aexp aexp
    3.31  
    3.32  subsection "Evaluation of arithmetic expressions"
    3.33  consts  evala    :: "((aexp*state) * nat) set"
    3.34 -       "-a->"    :: "[aexp*state,nat] => bool"         (infixl 50)
    3.35 +syntax "_evala"  :: "[aexp*state,nat] => bool"         (infixl "-a->" 50)
    3.36  translations
    3.37      "aesig -a-> n" == "(aesig,n) : evala"
    3.38  inductive evala
    3.39 -  intros 
    3.40 +  intros
    3.41    N:   "(N(n),s) -a-> n"
    3.42    X:   "(X(x),s) -a-> s(x)"
    3.43    Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
    3.44 -  Op2: "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |] 
    3.45 +  Op2: "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |]
    3.46          ==> (Op2 f e0 e1,s) -a-> f n0 n1"
    3.47  
    3.48  lemmas [intro] = N X Op1 Op2
    3.49  
    3.50 -types n2n2b = "[nat,nat] => bool"
    3.51  
    3.52  subsection "Boolean expressions"
    3.53  
    3.54  datatype
    3.55    bexp = true
    3.56         | false
    3.57 -       | ROp  n2n2b aexp aexp
    3.58 +       | ROp  "nat => nat => bool" aexp aexp
    3.59         | noti bexp
    3.60         | andi bexp bexp         (infixl 60)
    3.61         | ori  bexp bexp         (infixl 60)
    3.62  
    3.63  subsection "Evaluation of boolean expressions"
    3.64 -consts evalb    :: "((bexp*state) * bool)set"       
    3.65 -       "-b->"   :: "[bexp*state,bool] => bool"         (infixl 50)
    3.66 +consts evalb    :: "((bexp*state) * bool)set"
    3.67 +syntax "_evalb" :: "[bexp*state,bool] => bool"         (infixl "-b->" 50)
    3.68  
    3.69  translations
    3.70      "besig -b-> b" == "(besig,b) : evalb"
    3.71 @@ -66,12 +63,12 @@
    3.72    intros
    3.73    tru:   "(true,s) -b-> True"
    3.74    fls:   "(false,s) -b-> False"
    3.75 -  ROp:   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] 
    3.76 +  ROp:   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |]
    3.77            ==> (ROp f a0 a1,s) -b-> f n0 n1"
    3.78    noti:  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
    3.79 -  andi:  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
    3.80 +  andi:  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
    3.81            ==> (b0 andi b1,s) -b-> (w0 & w1)"
    3.82 -  ori:   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
    3.83 +  ori:   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
    3.84            ==> (b0 ori b1,s) -b-> (w0 | w1)"
    3.85  
    3.86  lemmas [intro] = tru fls ROp noti andi ori
    3.87 @@ -98,56 +95,51 @@
    3.88  lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
    3.89    by (rule,cases set: evala) auto
    3.90  
    3.91 -lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)" 
    3.92 +lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
    3.93    by (rule,cases set: evala) auto
    3.94  
    3.95 -lemma	[simp]: 
    3.96 -  "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)" 
    3.97 +lemma   [simp]:
    3.98 +  "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
    3.99    by (rule,cases set: evala) auto
   3.100  
   3.101  lemma [simp]:
   3.102 -  "(Op2 f a1 a2,sigma) -a-> i = 
   3.103 +  "(Op2 f a1 a2,sigma) -a-> i =
   3.104    (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
   3.105    by (rule,cases set: evala) auto
   3.106  
   3.107 -lemma [simp]: "((true,sigma) -b-> w) = (w=True)" 
   3.108 +lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
   3.109    by (rule,cases set: evalb) auto
   3.110  
   3.111  lemma [simp]:
   3.112 -  "((false,sigma) -b-> w) = (w=False)" 
   3.113 +  "((false,sigma) -b-> w) = (w=False)"
   3.114    by (rule,cases set: evalb) auto
   3.115  
   3.116  lemma [simp]:
   3.117 -  "((ROp f a0 a1,sigma) -b-> w) =   
   3.118 -  (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))" 
   3.119 +  "((ROp f a0 a1,sigma) -b-> w) =
   3.120 +  (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
   3.121    by (rule,cases set: evalb) auto
   3.122  
   3.123 -lemma [simp]:  
   3.124 -  "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))" 
   3.125 +lemma [simp]:
   3.126 +  "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
   3.127 +  by (rule,cases set: evalb) auto
   3.128 +
   3.129 +lemma [simp]:
   3.130 +  "((b0 andi b1,sigma) -b-> w) =
   3.131 +  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
   3.132    by (rule,cases set: evalb) auto
   3.133  
   3.134  lemma [simp]:
   3.135 -  "((b0 andi b1,sigma) -b-> w) =   
   3.136 -  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))" 
   3.137 -  by (rule,cases set: evalb) auto
   3.138 -
   3.139 -lemma [simp]:  
   3.140 -  "((b0 ori b1,sigma) -b-> w) =   
   3.141 -  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))" 
   3.142 +  "((b0 ori b1,sigma) -b-> w) =
   3.143 +  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
   3.144    by (rule,cases set: evalb) auto
   3.145  
   3.146  
   3.147 -lemma aexp_iff [rule_format (no_asm)]: 
   3.148 -  "!n. ((a,s) -a-> n) = (A a s = n)"
   3.149 -  apply (induct_tac "a")
   3.150 -  apply auto
   3.151 -  done
   3.152 +lemma aexp_iff:
   3.153 +  "!!n. ((a,s) -a-> n) = (A a s = n)"
   3.154 +  by (induct a) auto
   3.155  
   3.156 -lemma bexp_iff [rule_format (no_asm)]: 
   3.157 -  "!w. ((b,s) -b-> w) = (B b s = w)"
   3.158 -  apply (induct_tac "b")
   3.159 -  apply (auto simp add: aexp_iff)
   3.160 -  done
   3.161 +lemma bexp_iff:
   3.162 +  "!!w. ((b,s) -b-> w) = (B b s = w)"
   3.163 +  by (induct b) (auto simp add: aexp_iff)
   3.164  
   3.165  end
   3.166 -
     4.1 --- a/src/HOL/IMP/Hoare.thy	Tue Dec 18 21:28:01 2001 +0100
     4.2 +++ b/src/HOL/IMP/Hoare.thy	Wed Dec 19 00:26:04 2001 +0100
     4.3 @@ -14,7 +14,7 @@
     4.4            "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
     4.5  
     4.6  consts hoare :: "(assn * com * assn) set"
     4.7 -syntax "@hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
     4.8 +syntax "_hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
     4.9  translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
    4.10  
    4.11  inductive hoare
     5.1 --- a/src/HOL/IMP/Natural.thy	Tue Dec 18 21:28:01 2001 +0100
     5.2 +++ b/src/HOL/IMP/Natural.thy	Wed Dec 19 00:26:04 2001 +0100
     5.3 @@ -11,11 +11,11 @@
     5.4  
     5.5  subsection "Execution of commands"
     5.6  
     5.7 -consts  evalc  :: "(com \<times> state \<times> state) set" 
     5.8 -        "@evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
     5.9 +consts  evalc   :: "(com \<times> state \<times> state) set" 
    5.10 +syntax "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
    5.11  
    5.12  syntax (xsymbols)
    5.13 -  "@evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
    5.14 +  "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
    5.15  
    5.16  text {*
    5.17    We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started 
     6.1 --- a/src/HOL/IMP/Transition.thy	Tue Dec 18 21:28:01 2001 +0100
     6.2 +++ b/src/HOL/IMP/Transition.thy	Wed Dec 19 00:26:04 2001 +0100
     6.3 @@ -28,12 +28,12 @@
     6.4    @{text option} part in configurations:
     6.5  *}
     6.6  syntax
     6.7 -  "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
     6.8 -  "@angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
     6.9 +  "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
    6.10 +  "_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
    6.11  
    6.12  syntax (xsymbols)
    6.13 -  "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
    6.14 -  "@angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
    6.15 +  "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
    6.16 +  "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
    6.17  
    6.18  translations
    6.19    "\<langle>c,s\<rangle>" == "(Some c, s)"
    6.20 @@ -44,19 +44,19 @@
    6.21    iteration.
    6.22  *}
    6.23  syntax
    6.24 -  "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    6.25 +  "_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    6.26      ("_ -1-> _" [60,60] 60)
    6.27 -  "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    6.28 +  "_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    6.29      ("_ -_-> _" [60,60,60] 60)
    6.30 -  "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    6.31 +  "_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    6.32      ("_ -*-> _" [60,60] 60)
    6.33  
    6.34  syntax (xsymbols)
    6.35 -  "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    6.36 +  "_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    6.37      ("_ \<longrightarrow>\<^sub>1 _" [60,60] 61)
    6.38 -  "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    6.39 +  "_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
    6.40      ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60)
    6.41 -  "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    6.42 +  "_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
    6.43      ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60)
    6.44  
    6.45  translations
     7.1 --- a/src/HOL/IMP/document/root.tex	Tue Dec 18 21:28:01 2001 +0100
     7.2 +++ b/src/HOL/IMP/document/root.tex	Wed Dec 19 00:26:04 2001 +0100
     7.3 @@ -1,22 +1,9 @@
     7.4  
     7.5  \documentclass[a4wide]{article}
     7.6 -\usepackage{isabelle,isabellesym}
     7.7 -
     7.8 -% further packages required for unusual symbols (see also isabellesym.sty)
     7.9 -%\usepackage{latexsym}
    7.10 -%\usepackage{amssymb}
    7.11 -%\usepackage[english]{babel}
    7.12 -%\usepackage[latin1]{inputenc}
    7.13 -%\usepackage[only,bigsqcap]{stmaryrd}
    7.14 -%\usepackage{wasysym}
    7.15 -%\usepackage{eufrak}
    7.16 -
    7.17 -% this should be the last package used
    7.18 +\usepackage{graphicx,isabelle,isabellesym}
    7.19  \usepackage{pdfsetup}
    7.20  
    7.21 -% proper setup for best-style documents
    7.22  \urlstyle{rm}
    7.23 -%\isabellestyle{it}
    7.24  \renewcommand{\isachardoublequote}{}
    7.25  
    7.26  % pretty printing for the Com language
    7.27 @@ -34,28 +21,29 @@
    7.28  
    7.29  \begin{document}
    7.30  
    7.31 -\title{IMP--A {\tt WHILE}-language and its Semantics}
    7.32 -\author{Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, Gerwin Klein}
    7.33 +\title{IMP --- A {\tt WHILE}-language and its Semantics}
    7.34 +\author{Gerwin Klein, Heiko Loetzbeyer, Tobias Nipkow, Robert Sandner}
    7.35  \maketitle
    7.36  
    7.37  \parindent 0pt\parskip 0.5ex
    7.38  
    7.39  \begin{abstract}\noindent
    7.40 -The denotational, operational, and axiomatic semantics, a verification
    7.41 -condition generator, and all the necessary soundness, completeness and
    7.42 -equivalence proofs. Essentially a formalization of the first 100 pages
    7.43 -of \cite{Winskel}.
    7.44 -
    7.45 -An eminently readable description of this theory is found in \cite{Nipkow}.
    7.46 -
    7.47 -A denotational semantics for IMP based on HOLCF is found in {\tt HOLCF/IMP}.
    7.48 +  The denotational, operational, and axiomatic semantics, a verification
    7.49 +  condition generator, and all the necessary soundness, completeness and
    7.50 +  equivalence proofs. Essentially a formalization of the first 100 pages of
    7.51 +  \cite{Winskel}.
    7.52 +  
    7.53 +  An eminently readable description of this theory is found in \cite{Nipkow}.
    7.54 +  See also HOLCF/IMP for a denotational semantics.
    7.55  \end{abstract}
    7.56  
    7.57  \tableofcontents
    7.58  
    7.59 -\parindent 0pt\parskip 0.5ex
    7.60 +\begin{center}
    7.61 +  \includegraphics[scale=0.7]{session_graph}
    7.62 +\end{center}
    7.63  
    7.64 -% include generated text of all theories
    7.65 +\parindent 0pt\parskip 0.5ex
    7.66  \input{session}
    7.67  
    7.68  \bibliographystyle{plain}
     8.1 --- a/src/HOLCF/IMP/HoareEx.thy	Tue Dec 18 21:28:01 2001 +0100
     8.2 +++ b/src/HOLCF/IMP/HoareEx.thy	Wed Dec 19 00:26:04 2001 +0100
     8.3 @@ -9,9 +9,9 @@
     8.4  theory HoareEx = Denotational:
     8.5  
     8.6  text {*
     8.7 -  An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch \cite{MuellerNvOS99}.
     8.8 -  It demonstrates fixpoint reasoning by showing the correctness of the Hoare
     8.9 -  rule for while-loops.
    8.10 +  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
    8.11 +  \cite{MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
    8.12 +  the correctness of the Hoare rule for while-loops.
    8.13  *}
    8.14  
    8.15  types assn = "state => bool"
     9.1 --- a/src/HOLCF/IMP/document/root.tex	Tue Dec 18 21:28:01 2001 +0100
     9.2 +++ b/src/HOLCF/IMP/document/root.tex	Wed Dec 19 00:26:04 2001 +0100
     9.3 @@ -1,24 +1,9 @@
     9.4  
     9.5  \documentclass[11pt,a4paper]{article}
     9.6  \usepackage{isabelle,isabellesym}
     9.7 -
     9.8 -% further packages required for unusual symbols (see also isabellesym.sty)
     9.9 -%\usepackage{latexsym}
    9.10 -%\usepackage{amssymb}
    9.11 -%\usepackage[english]{babel}
    9.12 -%\usepackage[latin1]{inputenc}
    9.13 -%\usepackage[only,bigsqcap]{stmaryrd}
    9.14 -%\usepackage{wasysym}
    9.15 -%\usepackage{eufrak}
    9.16 -%\usepackage{textcomp}
    9.17 -%\usepackage{marvosym}
    9.18 -
    9.19 -% this should be the last package used
    9.20  \usepackage{pdfsetup}
    9.21  
    9.22 -% proper setup for best-style documents
    9.23  \urlstyle{rm}
    9.24 -%\isabellestyle{it}
    9.25  
    9.26  % pretty printing for the Com language
    9.27  %\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
    9.28 @@ -36,14 +21,12 @@
    9.29  \begin{document}
    9.30  
    9.31  \title{IMP in HOLCF}
    9.32 -\author{Tobias Nipkow, Robert Sandner}
    9.33 +\author{Tobias Nipkow and Robert Sandner}
    9.34  \maketitle
    9.35  
    9.36  \tableofcontents
    9.37  
    9.38  \parindent 0pt\parskip 0.5ex
    9.39 -
    9.40 -% include generated text of all theories
    9.41  \input{session}
    9.42  
    9.43  \bibliographystyle{abbrv}
    10.1 --- a/src/Pure/Isar/locale.ML	Tue Dec 18 21:28:01 2001 +0100
    10.2 +++ b/src/Pure/Isar/locale.ML	Wed Dec 19 00:26:04 2001 +0100
    10.3 @@ -253,7 +253,8 @@
    10.4  fun unify_frozen ctxt maxidx Ts Us =
    10.5    let
    10.6      val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
    10.7 -    fun unify (env, (Some T, Some U)) = Type.unify tsig env (U, T)
    10.8 +    fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T)
    10.9 +          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   10.10        | unify (env, _) = env;
   10.11      fun paramify (i, None) = (i, None)
   10.12        | paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T));
   10.13 @@ -378,13 +379,13 @@
   10.14  
   10.15  (* activate elements *)
   10.16  
   10.17 -fun declare_fixes (s: string) fixes = (PolyML.print s; PolyML.print fixes;
   10.18 +fun declare_fixes fixes =
   10.19    ProofContext.add_syntax fixes o
   10.20 -  ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes));
   10.21 +  ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes);
   10.22  
   10.23  local
   10.24  
   10.25 -fun activate_elem (Fixes fixes) = declare_fixes "activate_elem" fixes
   10.26 +fun activate_elem (Fixes fixes) = declare_fixes fixes
   10.27    | activate_elem (Assumes asms) =
   10.28        #1 o ProofContext.assume_i ProofContext.export_assume asms o
   10.29        ProofContext.fix_frees (flat (map (map #1 o #2) asms))
   10.30 @@ -394,12 +395,18 @@
   10.31          in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs) ctxt))
   10.32    | activate_elem (Notes facts) = #1 o ProofContext.have_thmss facts;
   10.33  
   10.34 -in
   10.35 -
   10.36  fun activate_elems ((name, ps), elems) = ProofContext.qualified (fn ctxt =>
   10.37    foldl (fn (c, e) => activate_elem e c) (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) =>
   10.38      err_in_locale ctxt msg [(name, map fst ps)]);
   10.39  
   10.40 +in
   10.41 +
   10.42 +fun activate_facts prep_facts (ctxt, ((name, ps), raw_elems)) =
   10.43 +  let
   10.44 +    val elems = map (prep_facts ctxt) raw_elems;
   10.45 +    val res = ((name, ps), elems);
   10.46 +  in (ctxt |> activate_elems res, res) end;
   10.47 +
   10.48  end;
   10.49  
   10.50  
   10.51 @@ -413,6 +420,20 @@
   10.52    | intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs);
   10.53  
   10.54  
   10.55 +(* attributes *)
   10.56 +
   10.57 +local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
   10.58 +
   10.59 +fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes)
   10.60 +  | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms))
   10.61 +  | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs))
   10.62 +  | attribute attrib (Elem (Notes facts)) =
   10.63 +      Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts))
   10.64 +  | attribute _ (Expr expr) = Expr expr;
   10.65 +
   10.66 +end;
   10.67 +
   10.68 +
   10.69  (* parameters *)
   10.70  
   10.71  local
   10.72 @@ -436,12 +457,12 @@
   10.73  local
   10.74  
   10.75  fun declare_int_elem i (ctxt, Fixes fixes) =
   10.76 -      (ctxt |> declare_fixes "declare_int_elem" (map (fn (x, T, mx) =>
   10.77 +      (ctxt |> declare_fixes (map (fn (x, T, mx) =>
   10.78          (x, apsome (Term.map_type_tfree (Type.param i)) T, mx)) fixes), [])
   10.79    | declare_int_elem _ (ctxt, _) = (ctxt, []);
   10.80  
   10.81  fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =
   10.82 -      (ctxt |> declare_fixes "declare_ext_elem" (prep_fixes ctxt fixes), [])
   10.83 +      (ctxt |> declare_fixes (prep_fixes ctxt fixes), [])
   10.84    | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
   10.85    | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
   10.86    | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
   10.87 @@ -450,7 +471,7 @@
   10.88    let val (ctxt', propps) =
   10.89      (case elems of
   10.90        Int es => foldl_map (declare_int_elem i) (ctxt, es)
   10.91 -    | Ext es => foldl_map (declare_ext_elem prep_fixes) (ctxt, es))
   10.92 +    | Ext e => foldl_map (declare_ext_elem prep_fixes) (ctxt, [e]))
   10.93      handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
   10.94    in ((ctxt', i + 1), propps) end;
   10.95  
   10.96 @@ -477,7 +498,7 @@
   10.97      val elems' =
   10.98        (case elems of
   10.99          Int es => map Int (#2 (hd (unify_elemss ctxt parms [((name, ps), es)])))
  10.100 -      | Ext es => map2 (finish_elem parms close) (es, propps));
  10.101 +      | Ext e => [finish_elem parms close (e, hd propps)]);
  10.102      val ps' = map (fn (x, _) => (x, assoc (parms, x))) ps;
  10.103    in ((name, ps'), elems') end;
  10.104  
  10.105 @@ -542,22 +563,7 @@
  10.106  end;
  10.107  
  10.108  
  10.109 -(* attributes *)
  10.110 -
  10.111 -local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
  10.112 -
  10.113 -fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes)
  10.114 -  | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms))
  10.115 -  | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs))
  10.116 -  | attribute attrib (Elem (Notes facts)) =
  10.117 -      Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts))
  10.118 -  | attribute _ (Expr expr) = Expr expr;
  10.119 -
  10.120 -end;
  10.121 -
  10.122 -
  10.123 -
  10.124 -(** prepare context statements: import + elements + conclusion **)
  10.125 +(* full context statements: import + elements + conclusion *)
  10.126  
  10.127  local
  10.128  
  10.129 @@ -565,24 +571,19 @@
  10.130      close fixed_params import elements raw_concl context =
  10.131    let
  10.132      val sign = ProofContext.sign_of context;
  10.133 -    fun flatten (Elem (Fixes fixes)) = [(("", map (rpair None o #1) fixes), Ext [Fixes fixes])]
  10.134 -      | flatten (Elem elem) = [(("", []), Ext [elem])]
  10.135 +    fun flatten (Elem (Fixes fixes)) = [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]
  10.136 +      | flatten (Elem elem) = [(("", []), Ext elem)]
  10.137        | flatten (Expr expr) = map (apsnd Int) (flatten_expr context (prep_expr sign expr));
  10.138 +    val activate = activate_facts prep_facts;
  10.139  
  10.140      val raw_import_elemss = flatten (Expr import);
  10.141      val raw_elemss = flat (map flatten elements);
  10.142      val (parms, all_elemss, concl) =
  10.143        prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
  10.144  
  10.145 -    fun activate_facts (ctxt, ((name, ps), raw_elems)) =
  10.146 -      let
  10.147 -        val elems = map (prep_facts ctxt) raw_elems;
  10.148 -        val res = ((name, ps), elems);
  10.149 -      in (ctxt |> activate_elems res, res) end;
  10.150 -
  10.151      val n = length raw_import_elemss;
  10.152 -    val (import_ctxt, import_elemss) = foldl_map activate_facts (context, take (n, all_elemss));
  10.153 -    val (ctxt, elemss) = foldl_map activate_facts (import_ctxt, drop (n, all_elemss));
  10.154 +    val (import_ctxt, import_elemss) = foldl_map activate (context, take (n, all_elemss));
  10.155 +    val (ctxt, elemss) = foldl_map activate (import_ctxt, drop (n, all_elemss));
  10.156    in (((import_ctxt, import_elemss), (ctxt, elemss)), concl) end;
  10.157  
  10.158  val gen_context = prep_context_statement intern_expr read_elemss get_facts;