# HG changeset patch # User wenzelm # Date 1131550012 -3600 # Node ID cb916659c89bcf92f62670c5a152c1b9d08d245e # Parent 51385f358b532bd1ae8efbbcfcd4bdf045d4fc11 moved datatype elem to element.ML; removed unused imports function; diff -r 51385f358b53 -r cb916659c89b src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Nov 09 16:26:51 2005 +0100 +++ b/src/Pure/Isar/locale.ML Wed Nov 09 16:26:52 2005 +0100 @@ -32,56 +32,44 @@ signature LOCALE = sig - type context (*= Proof.context*) - datatype ('typ, 'term, 'fact) elem = - Fixes of (string * 'typ option * mixfix option) list | - Constrains of (string * 'typ) list | - Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list | - Defines of ((string * Attrib.src list) * ('term * 'term list)) list | - Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list - type element (*= (string, string, thmref) elem*) - type element_i (*= (typ, term, thm list) elem*) datatype expr = Locale of string | Rename of expr * (string * mixfix option) option list | Merge of expr list val empty: expr - datatype 'a elem_expr = Elem of 'a | Expr of expr + datatype 'a element = Elem of 'a | Expr of expr (* Abstract interface to locales *) type locale val intern: theory -> xstring -> string val extern: theory -> string -> xstring val the_locale: theory -> string -> locale - val intern_attrib_elem: theory -> - ('typ, 'term, 'fact) elem -> ('typ, 'term, 'fact) elem - val intern_attrib_elem_expr: theory -> - ('typ, 'term, 'fact) elem elem_expr -> ('typ, 'term, 'fact) elem elem_expr (* Processing of locale statements *) - val read_context_statement: xstring option -> element elem_expr list -> - (string * (string list * string list)) list list -> context -> - string option * (cterm list * cterm list) * context * context * + val read_context_statement: xstring option -> Element.context element list -> + (string * (string list * string list)) list list -> ProofContext.context -> + string option * (cterm list * cterm list) * ProofContext.context * ProofContext.context * (term * (term list * term list)) list list - val cert_context_statement: string option -> element_i elem_expr list -> - (term * (term list * term list)) list list -> context -> - string option * (cterm list * cterm list) * context * context * + val cert_context_statement: string option -> Element.context_i element list -> + (term * (term list * term list)) list list -> ProofContext.context -> + string option * (cterm list * cterm list) * ProofContext.context * ProofContext.context * (term * (term list * term list)) list list (* Diagnostic functions *) val print_locales: theory -> unit - val print_locale: theory -> bool -> expr -> element list -> unit + val print_locale: theory -> bool -> expr -> Element.context list -> unit val print_global_registrations: bool -> string -> theory -> unit - val print_local_registrations': bool -> string -> context -> unit - val print_local_registrations: bool -> string -> context -> unit + val print_local_registrations': bool -> string -> ProofContext.context -> unit + val print_local_registrations: bool -> string -> ProofContext.context -> unit + + val add_locale_context: bool -> bstring -> expr -> Element.context list -> theory + -> (Element.context_i list * ProofContext.context) * theory + val add_locale_context_i: bool -> bstring -> expr -> Element.context_i list -> theory + -> (Element.context_i list * ProofContext.context) * theory + val add_locale: bool -> bstring -> expr -> Element.context list -> theory -> theory + val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory -> theory (* Storing results *) - val add_locale_context: bool -> bstring -> expr -> element list -> theory - -> (element_i list * ProofContext.context) * theory - val add_locale_context_i: bool -> bstring -> expr -> element_i list -> theory - -> (element_i list * ProofContext.context) * theory - val add_locale: bool -> bstring -> expr -> element list -> theory -> theory - val add_locale_i: bool -> bstring -> expr -> element_i list -> theory -> theory val smart_note_thmss: string -> string option -> ((bstring * theory attribute list) * (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list @@ -91,26 +79,27 @@ val note_thmss_i: string -> string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> theory -> (theory * ProofContext.context) * (bstring * thm list) list + val theorem: string -> Method.text option -> (thm list list -> theory -> theory) -> - string * Attrib.src list -> element elem_expr list -> + string * Attrib.src list -> Element.context element list -> ((string * Attrib.src list) * (string * (string list * string list)) list) list -> theory -> Proof.state val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) -> - string * theory attribute list -> element_i elem_expr list -> + string * theory attribute list -> Element.context_i element list -> ((string * theory attribute list) * (term * (term list * term list)) list) list -> theory -> Proof.state val theorem_in_locale: string -> Method.text option -> (thm list list -> thm list list -> theory -> theory) -> - xstring -> string * Attrib.src list -> element elem_expr list -> + xstring -> string * Attrib.src list -> Element.context element list -> ((string * Attrib.src list) * (string * (string list * string list)) list) list -> theory -> Proof.state val theorem_in_locale_i: string -> Method.text option -> (thm list list -> thm list list -> theory -> theory) -> - string -> string * Attrib.src list -> element_i elem_expr list -> + string -> string * Attrib.src list -> Element.context_i element list -> ((string * Attrib.src list) * (term * (term list * term list)) list) list -> theory -> Proof.state val smart_theorem: string -> xstring option -> - string * Attrib.src list -> element elem_expr list -> + string * Attrib.src list -> Element.context element list -> ((string * Attrib.src list) * (string * (string list * string list)) list) list -> theory -> Proof.state val interpretation: string * Attrib.src list -> expr -> string option list -> @@ -126,17 +115,7 @@ (** locale elements and expressions **) -type context = ProofContext.context; - -datatype ('typ, 'term, 'fact) elem = - Fixes of (string * 'typ option * mixfix option) list | - Constrains of (string * 'typ) list | - Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list | - Defines of ((string * Attrib.src list) * ('term * 'term list)) list | - Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list; - -type element = (string, string, thmref) elem; -type element_i = (typ, term, thm list) elem; +datatype ctxt = datatype Element.ctxt; datatype expr = Locale of string | @@ -145,9 +124,12 @@ val empty = Merge []; -datatype 'a elem_expr = +datatype 'a element = Elem of 'a | Expr of expr; +fun map_elem f (Elem e) = Elem (f e) + | map_elem _ (Expr e) = Expr e; + type witness = term * thm; (*hypothesis as fact*) type locale = {predicate: cterm list * witness list, @@ -161,7 +143,7 @@ (cf. [1], normalisation of locale expressions.) *) import: expr, (*dynamic import*) - elems: (element_i * stamp) list, (*static content*) + elems: (Element.context_i * stamp) list, (*static content*) params: ((string * typ) * mixfix option) list * string list, (*all/local params*) regs: ((string * string list) * (term * thm) list) list} @@ -177,99 +159,6 @@ -(** term and type instantiation, using symbol tables **) -(** functions for term instantiation beta-reduce the result - unless the instantiation table is empty (inst_tab_term) - or the instantiation has no effect (inst_tab_thm) **) - -(* instantiate TFrees *) - -fun tinst_tab_type tinst T = if Symtab.is_empty tinst - then T - else Term.map_type_tfree - (fn (v as (x, _)) => getOpt (Symtab.lookup tinst x, (TFree v))) T; - -fun tinst_tab_term tinst t = if Symtab.is_empty tinst - then t - else Term.map_term_types (tinst_tab_type tinst) t; - -fun tinst_tab_thm thy tinst thm = if Symtab.is_empty tinst - then thm - else let - val cert = Thm.cterm_of thy; - val certT = Thm.ctyp_of thy; - val {hyps, prop, ...} = Thm.rep_thm thm; - val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); - val tinst' = Symtab.dest tinst |> - List.filter (fn (a, _) => a mem_string tfrees); - in - if null tinst' then thm - else thm |> Drule.implies_intr_list (map cert hyps) - |> Drule.tvars_intr_list (map #1 tinst') - |> (fn (th, al) => th |> Thm.instantiate - ((map (fn (a, T) => (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) tinst'), - [])) - |> (fn th => Drule.implies_elim_list th - (map (Thm.assume o cert o tinst_tab_term tinst) hyps)) - end; - -(* instantiate TFrees and Frees *) - -fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst - then tinst_tab_term tinst - else (* instantiate terms and types simultaneously *) - let - fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T) - | instf (Free (x, T)) = (case Symtab.lookup inst x of - NONE => Free (x, tinst_tab_type tinst T) - | SOME t => t) - | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T) - | instf (b as Bound _) = b - | instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t) - | instf (s $ t) = instf s $ instf t - in Envir.beta_norm o instf end; - -fun inst_tab_thm thy (inst, tinst) thm = if Symtab.is_empty inst - then tinst_tab_thm thy tinst thm - else let - val cert = Thm.cterm_of thy; - val certT = Thm.ctyp_of thy; - val {hyps, prop, ...} = Thm.rep_thm thm; - (* type instantiations *) - val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); - val tinst' = Symtab.dest tinst |> - List.filter (fn (a, _) => a mem_string tfrees); - (* term instantiations; - note: lhss are type instantiated, because - type insts will be done first*) - val frees = foldr Term.add_term_frees [] (prop :: hyps); - val inst' = Symtab.dest inst |> - List.mapPartial (fn (a, t) => - get_first (fn (Free (x, T)) => - if a = x then SOME (Free (x, tinst_tab_type tinst T), t) - else NONE) frees); - in - if null tinst' andalso null inst' then tinst_tab_thm thy tinst thm - else thm |> Drule.implies_intr_list (map cert hyps) - |> Drule.tvars_intr_list (map #1 tinst') - |> (fn (th, al) => th |> Thm.instantiate - ((map (fn (a, T) => (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) tinst'), - [])) - |> Drule.forall_intr_list (map (cert o #1) inst') - |> Drule.forall_elim_list (map (cert o #2) inst') - |> Drule.fconv_rule (Thm.beta_conversion true) - |> (fn th => Drule.implies_elim_list th - (map (Thm.assume o cert o inst_tab_term (inst, tinst)) hyps)) - end; - - -fun inst_tab_att thy (inst as (_, tinst)) = - Args.map_values I (tinst_tab_type tinst) - (inst_tab_term inst) (inst_tab_thm thy inst); - -fun inst_tab_atts thy inst = map (inst_tab_att thy inst); - - (** management of registrations in theories and proof contexts **) structure Registrations : @@ -327,7 +216,8 @@ |> Symtab.make; in SOME (attn, map (fn (t, th) => - (inst_tab_term (inst', tinst') t, inst_tab_thm sign (inst', tinst') th)) thms) + (Element.inst_term (tinst', inst') t, + Element.inst_thm sign (tinst', inst') th)) thms) end) end; @@ -515,25 +405,9 @@ if id = id' then (id', thm :: thms) else (id', thms); in put_locale name {predicate = predicate, import = import, - elems = elems, params = params, regs = map add regs} thy + elems = elems, params = params, regs = map add regs} thy end; -(* import hierarchy - implementation could be more efficient, eg. by maintaining a database - of dependencies *) - -fun imports thy (upper, lower) = - let - fun imps (Locale name) low = (name = low) orelse - (case get_locale thy name of - NONE => false - | SOME {import, ...} => imps import low) - | imps (Rename (expr, _)) low = imps expr low - | imps (Merge es) low = exists (fn e => imps e low) es; - in - imps (Locale (intern thy upper)) (intern thy lower) - end; - (* printing of registrations *) @@ -602,145 +476,11 @@ (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); in raise ProofContext.CONTEXT (err_msg, ctxt) end; -(* Version for identifiers with axioms *) - fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); -(** primitives **) -(* map elements *) - -fun map_elem {name, var, typ, term, fact, attrib} = - fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => - let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end)) - | Constrains csts => Constrains (csts |> map (fn (x, T) => - let val (x', _) = var (x, SOME Syntax.NoSyn) in (x', typ T) end)) - | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => - ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) => - (term t, (map term ps, map term qs)))))) - | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => - ((name a, map attrib atts), (term t, map term ps)))) - | Notes facts => Notes (facts |> map (fn ((a, atts), bs) => - ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))); - -fun map_values typ term thm = map_elem - {name = I, var = I, typ = typ, term = term, fact = map thm, - attrib = Args.map_values I typ term thm}; - - -(* map attributes *) - -fun map_attrib_elem f = map_elem {name = I, var = I, typ = I, term = I, fact = I, attrib = f}; - -fun intern_attrib_elem thy = map_attrib_elem (Attrib.intern_src thy); - -fun intern_attrib_elem_expr thy (Elem elem) = Elem (intern_attrib_elem thy elem) - | intern_attrib_elem_expr _ (Expr expr) = Expr expr; - - -(* renaming *) - -(* ren maps names to (new) names and syntax; represented as association list *) - -fun rename_var ren (x, mx) = - case AList.lookup (op =) ren x of - NONE => (x, mx) - | SOME (x', NONE) => - (x', if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*) - | SOME (x', SOME mx') => - if mx = NONE then raise ERROR_MESSAGE - ("Attempt to change syntax of structure parameter " ^ quote x) - else (x', SOME mx'); (*change syntax*) - -fun rename ren x = - case AList.lookup (op =) ren x of - NONE => x - | SOME (x', _) => x'; (*ignore syntax*) - -fun rename_term ren (Free (x, T)) = Free (rename ren x, T) - | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u - | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t) - | rename_term _ a = a; - -fun rename_thm ren th = - let - val {thy, hyps, prop, maxidx, ...} = Thm.rep_thm th; - val cert = Thm.cterm_of thy; - val (xs, Ts) = Library.split_list (fold Term.add_frees (prop :: hyps) []); - val xs' = map (rename ren) xs; - fun cert_frees names = map (cert o Free) (names ~~ Ts); - fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts); - in - if xs = xs' then th - else - th - |> Drule.implies_intr_list (map cert hyps) - |> Drule.forall_intr_list (cert_frees xs) - |> Drule.forall_elim_list (cert_vars xs) - |> Thm.instantiate ([], cert_vars xs ~~ cert_frees xs') - |> (fn th' => Drule.implies_elim_list th' (map (Thm.assume o cert o rename_term ren) hyps)) - end; - -fun rename_elem ren = - map_values I (rename_term ren) (rename_thm ren) o - map_elem {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren}; - -fun rename_facts prfx = - map_elem {var = I, typ = I, term = I, fact = I, attrib = I, name = NameSpace.qualified prfx}; - - -(* type instantiation *) - -fun inst_type [] T = T - | inst_type env T = Term.map_type_tfree (fn v => AList.lookup (op =) env v |> the_default (TFree v)) T; - -fun inst_term [] t = t - | inst_term env t = Term.map_term_types (inst_type env) t; - -fun inst_thm _ [] th = th - | inst_thm ctxt env th = - let - val thy = ProofContext.theory_of ctxt; - val cert = Thm.cterm_of thy; - val certT = Thm.ctyp_of thy; - val {hyps, prop, maxidx, ...} = Thm.rep_thm th; - val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps); - val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env; - in - if null env' then th - else - th - |> Drule.implies_intr_list (map cert hyps) - |> Drule.tvars_intr_list (map (#1 o #1) env') - |> (fn (th', al) => th' |> - Thm.instantiate ((map (fn ((a, _), T) => - (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) env'), [])) - |> (fn th'' => Drule.implies_elim_list th'' - (map (Thm.assume o cert o inst_term env') hyps)) - end; - -fun inst_elem ctxt env = - map_values (inst_type env) (inst_term env) (inst_thm ctxt env); - - -(* term and type instantiation, variant using symbol tables *) - -(* instantiate TFrees *) - -fun tinst_tab_elem thy tinst = - map_values (tinst_tab_type tinst) (tinst_tab_term tinst) (tinst_tab_thm thy tinst); - -(* instantiate TFrees and Frees *) - -fun inst_tab_elem thy (inst as (_, tinst)) = - map_values (tinst_tab_type tinst) (inst_tab_term inst) (inst_tab_thm thy inst); - -fun inst_tab_elems thy inst ((n, ps), elems) = - ((n, map (inst_tab_term inst) ps), map (inst_tab_elem thy inst) elems); - - -(* protected thms *) +(** witnesses -- protected facts **) fun assume_protected thy t = (t, Goal.protect (Thm.assume (Thm.cterm_of thy t))); @@ -827,11 +567,6 @@ local -(* CB: OUTDATED unique_parms has the following type: - 'a -> - (('b * (('c * 'd) list * Symtab.key list)) * 'e) list -> - (('b * ('c * 'd) list) * 'e) list *) - fun unique_parms ctxt elemss = let val param_decls = @@ -844,8 +579,7 @@ | NONE => map (apfst (apfst (apsnd #1))) elemss) end; -fun unify_parms ctxt (fixed_parms : (string * typ) list) - (raw_parmss : (string * typ option) list list) = +fun unify_parms ctxt fixed_parms raw_parmss = let val thy = ProofContext.theory_of ctxt; val maxidx = length raw_parmss; @@ -855,17 +589,16 @@ fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); val parms = fixed_parms @ List.concat (map varify_parms idx_parmss); - fun unify T ((env, maxidx), U) = - Sign.typ_unify thy (U, T) (env, maxidx) + fun unify T U envir = Sign.typ_unify thy (U, T) envir handle Type.TUNIFY => - let val prt = Sign.string_of_typ thy - in raise TYPE ("unify_parms: failed to unify types " ^ - prt U ^ " and " ^ prt T, [U, T], []) - end - fun unify_list (envir, T :: Us) = Library.foldl (unify T) (envir, Us) - | unify_list (envir, []) = envir; - val (unifier, _) = Library.foldl unify_list - ((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); + let val prt = Sign.string_of_typ thy in + raise TYPE ("unify_parms: failed to unify types " ^ + prt U ^ " and " ^ prt T, [U, T], []) + end; + fun unify_list (T :: Us) = fold (unify T) Us + | unify_list [] = I; + val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_multi parms))) + (Vartab.empty, maxidx); val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct (eq_fst (op =)) parms); val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms')); @@ -874,8 +607,9 @@ foldr Term.add_typ_tfrees [] (List.mapPartial snd ps) |> List.mapPartial (fn (a, S) => let val T = Envir.norm_type unifier' (TVar ((a, i), S)) - in if T = TFree (a, S) then NONE else SOME ((a, S), T) end) - in map inst_parms idx_parmss end : ((string * sort) * typ) list list; + in if T = TFree (a, S) then NONE else SOME (a, T) end) + |> Symtab.make; + in map inst_parms idx_parmss end; in @@ -883,11 +617,13 @@ | unify_elemss _ [] [elems] = [elems] | unify_elemss ctxt fixed_parms elemss = let + val thy = ProofContext.theory_of ctxt; val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss); fun inst ((((name, ps), mode), elems), env) = - (((name, map (apsnd (Option.map (inst_type env))) ps), - map_mode (map (fn (t, th) => (inst_term env t, inst_thm ctxt env th))) mode), - map (inst_elem ctxt env) elems); + (((name, map (apsnd (Option.map (Element.instT_type env))) ps), + map_mode (map (fn (t, th) => + (Element.instT_term env t, Element.instT_thm thy env th))) mode), + map (Element.instT_ctxt thy env) elems); in map inst (elemss ~~ envs) end; (* like unify_elemss, but does not touch mode, additional @@ -897,11 +633,12 @@ | unify_elemss' _ [] [elems] [] = [elems] | unify_elemss' ctxt fixed_parms elemss c_parms = let - val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss @ map single c_parms); + val thy = ProofContext.theory_of ctxt; + val envs = + unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss @ map single c_parms); fun inst ((((name, ps), (ps', mode)), elems), env) = - (((name, map (apsnd (Option.map (inst_type env))) ps), - (ps', mode)), - map (inst_elem ctxt env) elems); + (((name, map (apsnd (Option.map (Element.instT_type env))) ps), (ps', mode)), + map (Element.instT_ctxt thy env) elems); in map inst (elemss ~~ (Library.take (length elemss, envs))) end; @@ -929,9 +666,6 @@ fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = let val thy = ProofContext.theory_of ctxt; - (* thy used for retrieval of locale info, - ctxt for error messages, parameter unification and instantiation - of axioms *) fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys | renaming (NONE :: xs) (y :: ys) = renaming xs ys @@ -940,12 +674,12 @@ commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs)); fun rename_parms top ren ((name, ps), (parms, mode)) = - let val ps' = map (rename ren) ps in + let val ps' = map (Element.rename ren) ps in (case duplicates ps' of [] => ((name, ps'), - if top then (map (rename ren) parms, + if top then (map (Element.rename ren) parms, map_mode (map (fn (t, th) => - (rename_term ren t, rename_thm ren th))) mode) + (Element.rename_term ren t, Element.rename_thm ren th))) mode) else (parms, mode)) | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')]) end; @@ -963,14 +697,14 @@ val [env] = unify_parms ctxt ps [map (apsnd SOME) ps'']; (* propagate parameter types, to keep them consistent *) val regs' = map (fn ((name, ps), ths) => - ((name, map (rename ren) ps), ths)) regs; + ((name, map (Element.rename ren) ps), ths)) regs; val new_regs = gen_rems (eq_fst (op =)) (regs', ids); val new_ids = map fst new_regs; val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids; val new_ths = new_regs |> map (fn (_, ths') => ths' |> map (fn (t, th) => - (t |> inst_term env |> rename_term ren, - th |> inst_thm ctxt env |> rename_thm ren |> satisfy_protected ths))); + (t |> Element.instT_term env |> Element.rename_term ren, + th |> Element.instT_thm thy env |> Element.rename_thm ren |> satisfy_protected ths))); val new_ids' = map (fn (id, ths) => (id, ([], Derived ths))) (new_ids ~~ new_ths); in @@ -1021,8 +755,7 @@ val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids'); val parms'' = distinct (List.concat (map (#2 o #1) ids'')); - val syn'' = syn' |> Symtab.dest |> map (rename_var ren) |> - Symtab.make; + val syn'' = syn' |> Symtab.dest |> map (Element.rename_var ren) |> Symtab.make; (* check for conflicting syntax? *) in (ids'', parms'', syn'') end | identify top (Merge es) = @@ -1037,7 +770,7 @@ es ([], [], Symtab.empty); - (* CB: enrich identifiers by parameter types and + (* CB: enrich identifiers by parameter types and the corresponding elements (with renamed parameters), also takes care of parameter syntax *) @@ -1049,9 +782,11 @@ map (fn x => (x, valOf (Symtab.lookup syn x))) xs; val (params', elems') = if null ren then ((ps', qs), map #1 elems) - else ((map (apfst (rename ren)) ps', map (rename ren) qs), - map (rename_elem ren o #1) elems); - val elems'' = map (rename_facts (space_implode "_" xs)) elems'; + else ((map (apfst (Element.rename ren)) ps', map (Element.rename ren) qs), + map (Element.rename_ctxt ren o #1) elems); + val elems'' = elems' |> map (Element.map_ctxt + {var = I, typ = I, term = I, fact = I, attrib = I, + name = NameSpace.qualified (space_implode "_" xs)}); in (((name, params'), axs), elems'') end; (* type constraint for renamed parameter with syntax *) @@ -1080,8 +815,8 @@ val {hyps, prop, ...} = Thm.rep_thm th; val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []); val [env] = unify_parms ctxt all_params [ps]; - val t' = inst_term env t; - val th' = inst_thm ctxt env th; + val t' = Element.instT_term env t; + val th' = Element.instT_thm thy env th; in (t', th') end; val final_elemss = map (fn ((id, mode), elems) => ((id, map_mode (map inst_th) mode), elems)) elemss'; @@ -1158,7 +893,8 @@ val elems = map (prep_facts ctxt) raw_elems; val (ctxt', res) = apsnd List.concat (activate_elems (((name, ps), mode), elems) ctxt); - val elems' = map (map_attrib_elem Args.closure) elems; + val elems' = elems |> map (Element.map_ctxt + {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure}); in ((((name, ps), elems'), res), ctxt') end); in @@ -1190,23 +926,8 @@ end; -(* register elements *) -(* not used -fun register_elems (((_, ps), (((name, ax_ps), axs), _)), ctxt) = - if name = "" then ctxt - else let val ps' = map (fn (n, SOME T) => Free (n, T)) ax_ps - val ctxt' = put_local_registration (name, ps') ("", []) ctxt - in foldl (fn (ax, ctxt) => - add_local_witness (name, ps') ax ctxt) ctxt' axs - end; - -fun register_elemss id_elemss ctxt = - foldl register_elems ctxt id_elemss; -*) - - -(** prepare context elements **) +(** prepare locale elements **) (* expressions *) @@ -1254,15 +975,15 @@ *) fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let - val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))] + val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))] in - ((ids', - merge_syntax ctxt ids' - (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes)) - handle Symtab.DUPS xs => err_in_locale ctxt - ("Conflicting syntax for parameters: " ^ commas_quote xs) + ((ids', + merge_syntax ctxt ids' + (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes)) + handle Symtab.DUPS xs => err_in_locale ctxt + ("Conflicting syntax for parameters: " ^ commas_quote xs) (map #1 ids')), - [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))]) + [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))]) end | flatten _ ((ids, syn), Elem elem) = ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)]) @@ -1306,8 +1027,6 @@ in -(* CB: only called by prep_elemss. *) - fun declare_elemss prep_parms fixed_params raw_elemss ctxt = let (* CB: fix of type bug of goal in target with context elements. @@ -1328,14 +1047,8 @@ local -(* CB: normalise Assumes and Defines wrt. previous definitions *) - val norm_term = Envir.beta_norm oo Term.subst_atomic; - -(* CB: following code (abstract_term, abstract_thm, bind_def) - used in eval_text for Defines elements. *) - fun abstract_term eq = (*assumes well-formedness according to ProofContext.cert_def*) let val body = Term.strip_all_body eq; @@ -1397,13 +1110,13 @@ | finish_derived _ _ (Derived _) (Constrains _) = NONE | finish_derived sign wits (Derived _) (Assumes asms) = asms |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], [])))) - |> Notes |> map_values I I (satisfy_protected wits) |> SOME + |> Notes |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME | finish_derived sign wits (Derived _) (Defines defs) = defs |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])])) - |> Notes |> map_values I I (satisfy_protected wits) |> SOME + |> Notes |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME | finish_derived _ wits _ (Notes facts) = (Notes facts) - |> map_values I I (satisfy_protected wits) |> SOME; + |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME; (* CB: for finish_elems (Ext) *) @@ -1560,14 +1273,13 @@ local fun prep_name ctxt name = - (* CB: reject qualified theorem names in locale declarations *) if NameSpace.is_qualified name then raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt) else name; fun prep_facts _ _ ctxt (Int elem) = - map_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem - | prep_facts get intern ctxt (Ext elem) = elem |> map_elem + Element.map_ctxt_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem + | prep_facts get intern ctxt (Ext elem) = elem |> Element.map_ctxt {var = I, typ = I, term = I, name = prep_name ctxt, fact = get ctxt, @@ -1650,54 +1362,16 @@ end; -(** define locales **) - (* print locale *) fun print_locale thy show_facts import body = let - val thy_ctxt = ProofContext.init thy; - val (((_, import_elemss), (ctxt, elemss, _)), _) = read_context import body thy_ctxt; + val (((_, import_elemss), (ctxt, elemss, _)), _) = + read_context import body (ProofContext.init thy); + val prt_elem = Element.pretty_ctxt ctxt; val all_elems = List.concat (map #2 (import_elemss @ elemss)); - - val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; - val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; - val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt; - val prt_atts = Args.pretty_attribs ctxt; - - fun prt_syn syn = - let val s = (case syn of NONE => "(structure)" | SOME mx => Syntax.string_of_mixfix mx) - in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end; - fun prt_fix (x, SOME T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: - prt_typ T :: Pretty.brk 1 :: prt_syn syn) - | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn); - fun prt_cst (x, T) = Pretty.block [Pretty.str (x ^ " ::"), prt_typ T]; - - fun prt_name name = Pretty.str (ProofContext.extern_thm ctxt name); - fun prt_name_atts (name, atts) = - if name = "" andalso null atts then [] - else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str ":"]))]; - - fun prt_asm (a, ts) = - Pretty.block (Pretty.breaks (prt_name_atts a @ map (prt_term o fst) ts)); - fun prt_def (a, (t, _)) = - Pretty.block (Pretty.breaks (prt_name_atts a @ [prt_term t])); - - fun prt_fact (ths, []) = map prt_thm ths - | prt_fact (ths, atts) = - Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: prt_atts atts; - fun prt_note (a, ths) = - Pretty.block (Pretty.breaks (List.concat (prt_name_atts a :: map prt_fact ths))); - - fun items _ [] = [] - | items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items " and" xs; - fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes) - | prt_elem (Constrains csts) = items "constrains" (map prt_cst csts) - | prt_elem (Assumes asms) = items "assumes" (map prt_asm asms) - | prt_elem (Defines defs) = items "defines" (map prt_def defs) - | prt_elem (Notes facts) = items "notes" (map prt_note facts); in - Pretty.big_list "context elements:" (all_elems + Pretty.big_list "locale elements:" (all_elems |> (if show_facts then I else filter (fn Notes _ => false | _ => true)) |> map (Pretty.chunks o prt_elem)) |> Pretty.writeln @@ -1768,14 +1442,14 @@ val parmvTs = map Type.varifyT parmTs; val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty; val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T)) - |> Symtab.make; + |> Symtab.make; (* replace parameter names in ids by instantiations *) val vinst = Symtab.make (parms ~~ vts); fun vinst_names ps = map (the o Symtab.lookup vinst) ps; val inst = Symtab.make (parms ~~ ts); val ids' = map (apsnd vinst_names) ids; val wits = List.concat (map (snd o valOf o get_global_registration thy) ids'); - in ((inst, tinst), wits) end; + in ((tinst, inst), wits) end; (* store instantiations of args for all registered interpretations @@ -1794,14 +1468,15 @@ fun activate (thy, (vts, ((prfx, atts2), _))) = let - val ((inst, tinst), prems) = collect_global_witnesses thy parms ids vts; - val args' = map (fn ((n, atts), [(ths, [])]) => + val (insts, prems) = collect_global_witnesses thy parms ids vts; + val inst_atts = + Args.map_values I (Element.instT_type (#1 insts)) + (Element.inst_term insts) (Element.inst_thm thy insts); + val args' = args |> map (fn ((n, atts), [(ths, [])]) => ((NameSpace.qualified prfx n, - map (Attrib.global_attribute_i thy) - (inst_tab_atts thy (inst, tinst) atts @ atts2)), + map (Attrib.global_attribute_i thy) (map inst_atts atts @ atts2)), [(map (Drule.standard o satisfy_protected prems o - inst_tab_thm thy (inst, tinst)) ths, [])])) - args; + Element.inst_thm thy insts) ths, [])])); in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end; in Library.foldl activate (thy, regs) end; @@ -1864,6 +1539,9 @@ end; + +(** define locales **) + (* predicate text *) (* CB: generate locale predicates and delta predicates *) @@ -1950,7 +1628,7 @@ fun change_elemss axioms elemss = (map (conclude_protected o #2) axioms, elemss) |> foldl_map (fn (axms, (id as ("", _), es)) => - foldl_map assumes_to_notes (axms, map (map_values I I (satisfy_protected axioms)) es) + foldl_map assumes_to_notes (axms, map (Element.map_ctxt_values I I (satisfy_protected axioms)) es) |> apsnd (pair id) | x => x) |> #2; @@ -2021,7 +1699,7 @@ else (thy, (elemss, ([], []))); val pred_ctxt = ProofContext.init pred_thy; - fun axiomify axioms elemss = + fun axiomify axioms elemss = (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let val ts = List.concat (List.mapPartial (fn (Assumes asms) => SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems); @@ -2064,6 +1742,9 @@ local +fun intern_attrib thy = map_elem (Element.map_ctxt + {name = I, var = I, typ = I, term = I, fact = I, attrib = Attrib.intern_src thy}); + fun global_goal prep_att = Proof.global_goal ProofDisplay.present_results prep_att ProofContext.bind_propp_schematic_i; @@ -2094,7 +1775,7 @@ |> ProofContext.add_view thy_ctxt locale_view; val locale_ctxt' = locale_ctxt |> ProofContext.add_view thy_ctxt locale_view; - + val stmt = map (apsnd (K []) o fst) concl ~~ propp; fun after_qed' results = @@ -2111,13 +1792,17 @@ in -val theorem = gen_theorem Attrib.global_attribute intern_attrib_elem_expr read_context_statement; +val theorem = gen_theorem Attrib.global_attribute intern_attrib read_context_statement; val theorem_i = gen_theorem (K I) (K I) cert_context_statement; -val theorem_in_locale = gen_theorem_in_locale intern Attrib.intern_src - intern_attrib_elem_expr read_context_statement false; -val theorem_in_locale_i = gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement false; -val theorem_in_locale_no_target = - gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement true; + +val theorem_in_locale = gen_theorem_in_locale intern Attrib.intern_src intern_attrib + read_context_statement false; + +val theorem_in_locale_i = gen_theorem_in_locale (K I) (K I) (K I) + cert_context_statement false; + +val theorem_in_locale_no_target = gen_theorem_in_locale (K I) (K I) (K I) + cert_context_statement true; fun smart_theorem kind NONE a [] concl = Proof.theorem kind NONE (K I) (SOME "") a concl o ProofContext.init @@ -2271,15 +1956,16 @@ (* defined params without user input *) val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T) | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs)); - fun add_def ((inst, tinst), (p, pT)) = + fun add_def (p, pT) inst = let val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of NONE => error ("Instance missing for parameter " ^ quote p) | SOME (Free (_, T), t) => (t, T); - val d = inst_tab_term (inst, tinst) t; - in (Symtab.update_new (p, d) inst, tinst) end; - val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given); - (* Note: inst and tinst contain no vars. *) + val d = Element.inst_term (tinst, inst) t; + in Symtab.update_new (p, d) inst end; + val inst = fold add_def not_given inst; + val insts = (tinst, inst); + (* Note: insts contain no vars. *) (** compute proof obligations **) @@ -2287,12 +1973,11 @@ val ids' = map (fn ((n, ps), (_, mode)) => ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) ids; (* instantiate ids and elements *) - val inst_elemss = map - (fn ((id, _), ((_, mode), elems)) => - inst_tab_elems thy (inst, tinst) (id, map (fn Int e => e) elems) - |> apfst (fn id => (id, map_mode (map (fn (t, th) => - (inst_tab_term (inst, tinst) t, inst_tab_thm thy (inst, tinst) th))) mode))) - (ids' ~~ all_elemss); + val inst_elemss = (ids' ~~ all_elemss) |> map (fn (((n, ps), _), ((_, mode), elems)) => + ((n, map (Element.inst_term insts) ps), + map (fn Int e => Element.inst_ctxt thy insts e) elems) + |> apfst (fn id => (id, map_mode (map (fn (t, th) => + (Element.inst_term insts t, Element.inst_thm thy insts th))) mode))); (* remove fragments already registered with theory or context *) val new_inst_elemss = List.filter (fn ((id, _), _) => @@ -2363,9 +2048,8 @@ | activate_id _ thy = thy; fun activate_reg (vts, ((prfx, atts2), _)) thy = let - val ((inst, tinst), wits) = - collect_global_witnesses thy fixed t_ids vts; - fun inst_parms ps = map + val (insts, wits) = collect_global_witnesses thy fixed t_ids vts; + fun inst_parms ps = map (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps; val disch = satisfy_protected wits; val new_elemss = List.filter (fn (((name, ps), _), _) => @@ -2379,8 +2063,7 @@ else thy |> put_global_registration (name, ps') (prfx, atts2) |> fold (fn (t, th) => fn thy => add_global_witness (name, ps') - (inst_tab_term (inst, tinst) t, - disch (inst_tab_thm thy (inst, tinst) th)) thy) thms + (Element.inst_term insts t, disch (Element.inst_thm thy insts th)) thy) thms end; fun activate_derived_id ((_, Assumed _), _) thy = thy @@ -2392,19 +2075,19 @@ else thy |> put_global_registration (name, ps') (prfx, atts2) |> fold (fn (t, th) => fn thy => add_global_witness (name, ps') - (inst_tab_term (inst, tinst) t, - disch (inst_tab_thm thy (inst, tinst) (satisfy th))) thy) ths + (Element.inst_term insts t, + disch (Element.inst_thm thy insts (satisfy th))) thy) ths end; fun activate_elem (Notes facts) thy = let val facts' = facts |> Attrib.map_facts (Attrib.global_attribute_i thy o - Args.map_values I (tinst_tab_type tinst) - (inst_tab_term (inst, tinst)) - (disch o inst_tab_thm thy (inst, tinst) o satisfy)) + Args.map_values I (Element.instT_type (#1 insts)) + (Element.inst_term insts) + (disch o Element.inst_thm thy insts o satisfy)) |> map (apfst (apsnd (fn a => a @ map (Attrib.global_attribute thy) atts2))) - |> map (apsnd (map (apfst (map (disch o inst_tab_thm thy (inst, tinst) o satisfy))))) + |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy))))) |> map (apfst (apfst (NameSpace.qualified prfx))) in fst (global_note_accesses_i (Drule.kind "") prfx facts' thy) @@ -2442,12 +2125,11 @@ fun interpretation (prfx, atts) expr insts thy = let - val thy_ctxt = ProofContext.init thy; val (propss, activate) = prep_global_registration (prfx, atts) expr insts thy; val kind = goal_name thy "interpretation" NONE propss; - fun after_qed results = activate (prep_result propss results); + val after_qed = activate o (prep_result propss); in - thy_ctxt + ProofContext.init thy |> Proof.theorem_i kind NONE after_qed NONE ("", []) (prep_propp propss) |> refine_protected end; @@ -2457,7 +2139,7 @@ val target = intern thy raw_target; val (propss, activate) = prep_registration_in_locale target expr thy; val kind = goal_name thy "interpretation" (SOME target) propss; - fun after_qed locale_results _ = activate (prep_result propss locale_results); + val after_qed = K (activate o prep_result propss); in thy |> theorem_in_locale_no_target kind NONE after_qed target ("", []) [] (prep_propp propss)