# HG changeset patch # User wenzelm # Date 1008717964 -3600 # Node ID 0c90e581379f22251bcf3609f0522cf36b1452ef # Parent 7319d384d0d3a6538d5c7da93416d8fc93c5a36a tuned; diff -r 7319d384d0d3 -r 0c90e581379f etc/settings --- 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 diff -r 7319d384d0d3 -r 0c90e581379f src/HOL/IMP/Compiler.thy --- 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 \ ((state\nat) \ (state\nat))set" syntax - "@stepa1" :: "[instr list,state,nat,state,nat] \ bool" + "_stepa1" :: "[instr list,state,nat,state,nat] \ bool" ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50) - "@stepa" :: "[instr list,state,nat,state,nat] \ bool" + "_stepa" :: "[instr list,state,nat,state,nat] \ bool" ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50) syntax (xsymbols) - "@stepa1" :: "[instr list,state,nat,state,nat] \ bool" + "_stepa1" :: "[instr list,state,nat,state,nat] \ bool" ("_ \ \_,_\/ -1\ \_,_\" [50,0,0,0,0] 50) - "@stepa" :: "[instr list,state,nat,state,nat] \ bool" + "_stepa" :: "[instr list,state,nat,state,nat] \ bool" ("_ \/ \_,_\/ -*\ \_,_\" [50,0,0,0,0] 50) translations diff -r 7319d384d0d3 -r 0c90e581379f src/HOL/IMP/Expr.thy --- 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 = (\n. i = f n \ (e,sigma) -a-> n)" +lemma [simp]: + "(Op1 f e,sigma) -a-> i = (\n. i = f n \ (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 = (\n0 n1. i = f n0 n1 \ (a1, sigma) -a-> n0 \ (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 - diff -r 7319d384d0d3 -r 0c90e581379f src/HOL/IMP/Hoare.thy --- 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 diff -r 7319d384d0d3 -r 0c90e581379f src/HOL/IMP/Natural.thy --- 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 \ state \ state) set" - "@evalc" :: "[com,state,state] \ bool" ("<_,_>/ -c-> _" [0,0,60] 60) +consts evalc :: "(com \ state \ state) set" +syntax "_evalc" :: "[com,state,state] \ bool" ("<_,_>/ -c-> _" [0,0,60] 60) syntax (xsymbols) - "@evalc" :: "[com,state,state] \ bool" ("\_,_\/ \\<^sub>c _" [0,0,60] 60) + "_evalc" :: "[com,state,state] \ bool" ("\_,_\/ \\<^sub>c _" [0,0,60] 60) text {* We write @{text "\c,s\ \\<^sub>c s'"} for \emph{Statement @{text c}, started diff -r 7319d384d0d3 -r 0c90e581379f src/HOL/IMP/Transition.thy --- 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] \ com option \ state" ("<_,_>") - "@angle2" :: "state \ com option \ state" ("<_>") + "_angle" :: "[com, state] \ com option \ state" ("<_,_>") + "_angle2" :: "state \ com option \ state" ("<_>") syntax (xsymbols) - "@angle" :: "[com, state] \ com option \ state" ("\_,_\") - "@angle2" :: "state \ com option \ state" ("\_\") + "_angle" :: "[com, state] \ com option \ state" ("\_,_\") + "_angle2" :: "state \ com option \ state" ("\_\") translations "\c,s\" == "(Some c, s)" @@ -44,19 +44,19 @@ iteration. *} syntax - "@evalc1" :: "[(com option\state),(com option\state)] \ bool" + "_evalc1" :: "[(com option\state),(com option\state)] \ bool" ("_ -1-> _" [60,60] 60) - "@evalcn" :: "[(com option\state),nat,(com option\state)] \ bool" + "_evalcn" :: "[(com option\state),nat,(com option\state)] \ bool" ("_ -_-> _" [60,60,60] 60) - "@evalc*" :: "[(com option\state),(com option\state)] \ bool" + "_evalc*" :: "[(com option\state),(com option\state)] \ bool" ("_ -*-> _" [60,60] 60) syntax (xsymbols) - "@evalc1" :: "[(com option\state),(com option\state)] \ bool" + "_evalc1" :: "[(com option\state),(com option\state)] \ bool" ("_ \\<^sub>1 _" [60,60] 61) - "@evalcn" :: "[(com option\state),nat,(com option\state)] \ bool" + "_evalcn" :: "[(com option\state),nat,(com option\state)] \ bool" ("_ -_\\<^sub>1 _" [60,60,60] 60) - "@evalc*" :: "[(com option\state),(com option\state)] \ bool" + "_evalc*" :: "[(com option\state),(com option\state)] \ bool" ("_ \\<^sub>1\<^sup>* _" [60,60] 60) translations diff -r 7319d384d0d3 -r 0c90e581379f src/HOL/IMP/document/root.tex --- 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} diff -r 7319d384d0d3 -r 0c90e581379f src/HOLCF/IMP/HoareEx.thy --- 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" diff -r 7319d384d0d3 -r 0c90e581379f src/HOLCF/IMP/document/root.tex --- 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} diff -r 7319d384d0d3 -r 0c90e581379f src/Pure/Isar/locale.ML --- 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;