--- a/etc/settings Tue Dec 18 21:28:01 2001 +0100
+++ b/etc/settings Wed Dec 19 00:26:04 2001 +0100
@@ -14,7 +14,7 @@
# binaries. Do not invent new ML system names unless you know what
# you are doing. Only one of the sections below should be activated.
-# Poly/ML 3.x and 4.0 or later
+# Poly/ML 3.x, 4.0, 4.1, and 4.1.1
if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
#maybe a shrink-wrapped polyml-4.1.1 on x86-linux ...
ML_SYSTEM=polyml-4.1.1
@@ -120,7 +120,7 @@
[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
{ echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; }
-# Users may want to change this.
+# Users may want to override this.
ISABELLE_LOGIC=HOL
--- a/src/HOL/IMP/Compiler.thy Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOL/IMP/Compiler.thy Wed Dec 19 00:26:04 2001 +0100
@@ -19,15 +19,15 @@
consts stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
syntax
- "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
- "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
syntax (xsymbols)
- "@stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
("_ \<turnstile> \<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
- "@stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
("_ \<turnstile>/ \<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>" [50,0,0,0,0] 50)
translations
--- a/src/HOL/IMP/Expr.thy Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOL/IMP/Expr.thy Wed Dec 19 00:26:04 2001 +0100
@@ -6,7 +6,7 @@
header "Expressions"
-theory Expr = Datatype:
+theory Expr = Main:
text {*
Arithmetic expressions and Boolean expressions.
@@ -14,49 +14,46 @@
*}
subsection "Arithmetic expressions"
-typedecl loc
+typedecl loc
types
state = "loc => nat"
- n2n = "nat => nat"
- n2n2n = "nat => nat => nat"
datatype
aexp = N nat
| X loc
- | Op1 n2n aexp
- | Op2 n2n2n aexp aexp
+ | Op1 "nat => nat" aexp
+ | Op2 "nat => nat => nat" aexp aexp
subsection "Evaluation of arithmetic expressions"
consts evala :: "((aexp*state) * nat) set"
- "-a->" :: "[aexp*state,nat] => bool" (infixl 50)
+syntax "_evala" :: "[aexp*state,nat] => bool" (infixl "-a->" 50)
translations
"aesig -a-> n" == "(aesig,n) : evala"
inductive evala
- intros
+ intros
N: "(N(n),s) -a-> n"
X: "(X(x),s) -a-> s(x)"
Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
- Op2: "[| (e0,s) -a-> n0; (e1,s) -a-> n1 |]
+ Op2: "[| (e0,s) -a-> n0; (e1,s) -a-> n1 |]
==> (Op2 f e0 e1,s) -a-> f n0 n1"
lemmas [intro] = N X Op1 Op2
-types n2n2b = "[nat,nat] => bool"
subsection "Boolean expressions"
datatype
bexp = true
| false
- | ROp n2n2b aexp aexp
+ | ROp "nat => nat => bool" aexp aexp
| noti bexp
| andi bexp bexp (infixl 60)
| ori bexp bexp (infixl 60)
subsection "Evaluation of boolean expressions"
-consts evalb :: "((bexp*state) * bool)set"
- "-b->" :: "[bexp*state,bool] => bool" (infixl 50)
+consts evalb :: "((bexp*state) * bool)set"
+syntax "_evalb" :: "[bexp*state,bool] => bool" (infixl "-b->" 50)
translations
"besig -b-> b" == "(besig,b) : evalb"
@@ -66,12 +63,12 @@
intros
tru: "(true,s) -b-> True"
fls: "(false,s) -b-> False"
- ROp: "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |]
+ ROp: "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |]
==> (ROp f a0 a1,s) -b-> f n0 n1"
noti: "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
- andi: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
+ andi: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
==> (b0 andi b1,s) -b-> (w0 & w1)"
- ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
+ ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
==> (b0 ori b1,s) -b-> (w0 | w1)"
lemmas [intro] = tru fls ROp noti andi ori
@@ -98,56 +95,51 @@
lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
by (rule,cases set: evala) auto
-lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
+lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
by (rule,cases set: evala) auto
-lemma [simp]:
- "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
+lemma [simp]:
+ "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
by (rule,cases set: evala) auto
lemma [simp]:
- "(Op2 f a1 a2,sigma) -a-> i =
+ "(Op2 f a1 a2,sigma) -a-> i =
(\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
by (rule,cases set: evala) auto
-lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
+lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
by (rule,cases set: evalb) auto
lemma [simp]:
- "((false,sigma) -b-> w) = (w=False)"
+ "((false,sigma) -b-> w) = (w=False)"
by (rule,cases set: evalb) auto
lemma [simp]:
- "((ROp f a0 a1,sigma) -b-> w) =
- (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
+ "((ROp f a0 a1,sigma) -b-> w) =
+ (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
by (rule,cases set: evalb) auto
-lemma [simp]:
- "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
+lemma [simp]:
+ "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
+ by (rule,cases set: evalb) auto
+
+lemma [simp]:
+ "((b0 andi b1,sigma) -b-> w) =
+ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
by (rule,cases set: evalb) auto
lemma [simp]:
- "((b0 andi b1,sigma) -b-> w) =
- (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
- by (rule,cases set: evalb) auto
-
-lemma [simp]:
- "((b0 ori b1,sigma) -b-> w) =
- (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
+ "((b0 ori b1,sigma) -b-> w) =
+ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
by (rule,cases set: evalb) auto
-lemma aexp_iff [rule_format (no_asm)]:
- "!n. ((a,s) -a-> n) = (A a s = n)"
- apply (induct_tac "a")
- apply auto
- done
+lemma aexp_iff:
+ "!!n. ((a,s) -a-> n) = (A a s = n)"
+ by (induct a) auto
-lemma bexp_iff [rule_format (no_asm)]:
- "!w. ((b,s) -b-> w) = (B b s = w)"
- apply (induct_tac "b")
- apply (auto simp add: aexp_iff)
- done
+lemma bexp_iff:
+ "!!w. ((b,s) -b-> w) = (B b s = w)"
+ by (induct b) (auto simp add: aexp_iff)
end
-
--- a/src/HOL/IMP/Hoare.thy Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOL/IMP/Hoare.thy Wed Dec 19 00:26:04 2001 +0100
@@ -14,7 +14,7 @@
"|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
consts hoare :: "(assn * com * assn) set"
-syntax "@hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
+syntax "_hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
inductive hoare
--- a/src/HOL/IMP/Natural.thy Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOL/IMP/Natural.thy Wed Dec 19 00:26:04 2001 +0100
@@ -11,11 +11,11 @@
subsection "Execution of commands"
-consts evalc :: "(com \<times> state \<times> state) set"
- "@evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
+consts evalc :: "(com \<times> state \<times> state) set"
+syntax "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
syntax (xsymbols)
- "@evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
+ "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
text {*
We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
--- a/src/HOL/IMP/Transition.thy Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOL/IMP/Transition.thy Wed Dec 19 00:26:04 2001 +0100
@@ -28,12 +28,12 @@
@{text option} part in configurations:
*}
syntax
- "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
- "@angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
+ "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
+ "_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
syntax (xsymbols)
- "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
- "@angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
+ "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
+ "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
translations
"\<langle>c,s\<rangle>" == "(Some c, s)"
@@ -44,19 +44,19 @@
iteration.
*}
syntax
- "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
+ "_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
("_ -1-> _" [60,60] 60)
- "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
+ "_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
("_ -_-> _" [60,60,60] 60)
- "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
+ "_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
("_ -*-> _" [60,60] 60)
syntax (xsymbols)
- "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
+ "_evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
("_ \<longrightarrow>\<^sub>1 _" [60,60] 61)
- "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
+ "_evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60)
- "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
+ "_evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60)
translations
--- a/src/HOL/IMP/document/root.tex Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOL/IMP/document/root.tex Wed Dec 19 00:26:04 2001 +0100
@@ -1,22 +1,9 @@
\documentclass[a4wide]{article}
-\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also isabellesym.sty)
-%\usepackage{latexsym}
-%\usepackage{amssymb}
-%\usepackage[english]{babel}
-%\usepackage[latin1]{inputenc}
-%\usepackage[only,bigsqcap]{stmaryrd}
-%\usepackage{wasysym}
-%\usepackage{eufrak}
-
-% this should be the last package used
+\usepackage{graphicx,isabelle,isabellesym}
\usepackage{pdfsetup}
-% proper setup for best-style documents
\urlstyle{rm}
-%\isabellestyle{it}
\renewcommand{\isachardoublequote}{}
% pretty printing for the Com language
@@ -34,28 +21,29 @@
\begin{document}
-\title{IMP--A {\tt WHILE}-language and its Semantics}
-\author{Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, Gerwin Klein}
+\title{IMP --- A {\tt WHILE}-language and its Semantics}
+\author{Gerwin Klein, Heiko Loetzbeyer, Tobias Nipkow, Robert Sandner}
\maketitle
\parindent 0pt\parskip 0.5ex
\begin{abstract}\noindent
-The denotational, operational, and axiomatic semantics, a verification
-condition generator, and all the necessary soundness, completeness and
-equivalence proofs. Essentially a formalization of the first 100 pages
-of \cite{Winskel}.
-
-An eminently readable description of this theory is found in \cite{Nipkow}.
-
-A denotational semantics for IMP based on HOLCF is found in {\tt HOLCF/IMP}.
+ The denotational, operational, and axiomatic semantics, a verification
+ condition generator, and all the necessary soundness, completeness and
+ equivalence proofs. Essentially a formalization of the first 100 pages of
+ \cite{Winskel}.
+
+ An eminently readable description of this theory is found in \cite{Nipkow}.
+ See also HOLCF/IMP for a denotational semantics.
\end{abstract}
\tableofcontents
-\parindent 0pt\parskip 0.5ex
+\begin{center}
+ \includegraphics[scale=0.7]{session_graph}
+\end{center}
-% include generated text of all theories
+\parindent 0pt\parskip 0.5ex
\input{session}
\bibliographystyle{plain}
--- a/src/HOLCF/IMP/HoareEx.thy Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOLCF/IMP/HoareEx.thy Wed Dec 19 00:26:04 2001 +0100
@@ -9,9 +9,9 @@
theory HoareEx = Denotational:
text {*
- An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch \cite{MuellerNvOS99}.
- It demonstrates fixpoint reasoning by showing the correctness of the Hoare
- rule for while-loops.
+ An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
+ \cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing
+ the correctness of the Hoare rule for while-loops.
*}
types assn = "state => bool"
--- a/src/HOLCF/IMP/document/root.tex Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOLCF/IMP/document/root.tex Wed Dec 19 00:26:04 2001 +0100
@@ -1,24 +1,9 @@
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also isabellesym.sty)
-%\usepackage{latexsym}
-%\usepackage{amssymb}
-%\usepackage[english]{babel}
-%\usepackage[latin1]{inputenc}
-%\usepackage[only,bigsqcap]{stmaryrd}
-%\usepackage{wasysym}
-%\usepackage{eufrak}
-%\usepackage{textcomp}
-%\usepackage{marvosym}
-
-% this should be the last package used
\usepackage{pdfsetup}
-% proper setup for best-style documents
\urlstyle{rm}
-%\isabellestyle{it}
% pretty printing for the Com language
%\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}}
@@ -36,14 +21,12 @@
\begin{document}
\title{IMP in HOLCF}
-\author{Tobias Nipkow, Robert Sandner}
+\author{Tobias Nipkow and Robert Sandner}
\maketitle
\tableofcontents
\parindent 0pt\parskip 0.5ex
-
-% include generated text of all theories
\input{session}
\bibliographystyle{abbrv}
--- a/src/Pure/Isar/locale.ML Tue Dec 18 21:28:01 2001 +0100
+++ b/src/Pure/Isar/locale.ML Wed Dec 19 00:26:04 2001 +0100
@@ -253,7 +253,8 @@
fun unify_frozen ctxt maxidx Ts Us =
let
val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
- fun unify (env, (Some T, Some U)) = Type.unify tsig env (U, T)
+ fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T)
+ handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
| unify (env, _) = env;
fun paramify (i, None) = (i, None)
| paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T));
@@ -378,13 +379,13 @@
(* activate elements *)
-fun declare_fixes (s: string) fixes = (PolyML.print s; PolyML.print fixes;
+fun declare_fixes fixes =
ProofContext.add_syntax fixes o
- ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes));
+ ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes);
local
-fun activate_elem (Fixes fixes) = declare_fixes "activate_elem" fixes
+fun activate_elem (Fixes fixes) = declare_fixes fixes
| activate_elem (Assumes asms) =
#1 o ProofContext.assume_i ProofContext.export_assume asms o
ProofContext.fix_frees (flat (map (map #1 o #2) asms))
@@ -394,12 +395,18 @@
in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs) ctxt))
| activate_elem (Notes facts) = #1 o ProofContext.have_thmss facts;
-in
-
fun activate_elems ((name, ps), elems) = ProofContext.qualified (fn ctxt =>
foldl (fn (c, e) => activate_elem e c) (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) =>
err_in_locale ctxt msg [(name, map fst ps)]);
+in
+
+fun activate_facts prep_facts (ctxt, ((name, ps), raw_elems)) =
+ let
+ val elems = map (prep_facts ctxt) raw_elems;
+ val res = ((name, ps), elems);
+ in (ctxt |> activate_elems res, res) end;
+
end;
@@ -413,6 +420,20 @@
| intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs);
+(* attributes *)
+
+local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
+
+fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes)
+ | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms))
+ | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs))
+ | attribute attrib (Elem (Notes facts)) =
+ Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts))
+ | attribute _ (Expr expr) = Expr expr;
+
+end;
+
+
(* parameters *)
local
@@ -436,12 +457,12 @@
local
fun declare_int_elem i (ctxt, Fixes fixes) =
- (ctxt |> declare_fixes "declare_int_elem" (map (fn (x, T, mx) =>
+ (ctxt |> declare_fixes (map (fn (x, T, mx) =>
(x, apsome (Term.map_type_tfree (Type.param i)) T, mx)) fixes), [])
| declare_int_elem _ (ctxt, _) = (ctxt, []);
fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =
- (ctxt |> declare_fixes "declare_ext_elem" (prep_fixes ctxt fixes), [])
+ (ctxt |> declare_fixes (prep_fixes ctxt fixes), [])
| declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
| declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
| declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
@@ -450,7 +471,7 @@
let val (ctxt', propps) =
(case elems of
Int es => foldl_map (declare_int_elem i) (ctxt, es)
- | Ext es => foldl_map (declare_ext_elem prep_fixes) (ctxt, es))
+ | Ext e => foldl_map (declare_ext_elem prep_fixes) (ctxt, [e]))
handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
in ((ctxt', i + 1), propps) end;
@@ -477,7 +498,7 @@
val elems' =
(case elems of
Int es => map Int (#2 (hd (unify_elemss ctxt parms [((name, ps), es)])))
- | Ext es => map2 (finish_elem parms close) (es, propps));
+ | Ext e => [finish_elem parms close (e, hd propps)]);
val ps' = map (fn (x, _) => (x, assoc (parms, x))) ps;
in ((name, ps'), elems') end;
@@ -542,22 +563,7 @@
end;
-(* attributes *)
-
-local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
-
-fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes)
- | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms))
- | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs))
- | attribute attrib (Elem (Notes facts)) =
- Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts))
- | attribute _ (Expr expr) = Expr expr;
-
-end;
-
-
-
-(** prepare context statements: import + elements + conclusion **)
+(* full context statements: import + elements + conclusion *)
local
@@ -565,24 +571,19 @@
close fixed_params import elements raw_concl context =
let
val sign = ProofContext.sign_of context;
- fun flatten (Elem (Fixes fixes)) = [(("", map (rpair None o #1) fixes), Ext [Fixes fixes])]
- | flatten (Elem elem) = [(("", []), Ext [elem])]
+ fun flatten (Elem (Fixes fixes)) = [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]
+ | flatten (Elem elem) = [(("", []), Ext elem)]
| flatten (Expr expr) = map (apsnd Int) (flatten_expr context (prep_expr sign expr));
+ val activate = activate_facts prep_facts;
val raw_import_elemss = flatten (Expr import);
val raw_elemss = flat (map flatten elements);
val (parms, all_elemss, concl) =
prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
- fun activate_facts (ctxt, ((name, ps), raw_elems)) =
- let
- val elems = map (prep_facts ctxt) raw_elems;
- val res = ((name, ps), elems);
- in (ctxt |> activate_elems res, res) end;
-
val n = length raw_import_elemss;
- val (import_ctxt, import_elemss) = foldl_map activate_facts (context, take (n, all_elemss));
- val (ctxt, elemss) = foldl_map activate_facts (import_ctxt, drop (n, all_elemss));
+ val (import_ctxt, import_elemss) = foldl_map activate (context, take (n, all_elemss));
+ val (ctxt, elemss) = foldl_map activate (import_ctxt, drop (n, all_elemss));
in (((import_ctxt, import_elemss), (ctxt, elemss)), concl) end;
val gen_context = prep_context_statement intern_expr read_elemss get_facts;