wneuper/isa: comparison src/Pure/Isar/locale.ML

equal deleted inserted replaced

-:adb83939177f
+:b59202511b8a
 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
 In Stefano Berardi et al., Types for Proofs and Programs: International
 Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
 *)
+(* TODO:
+- beta-eta normalisation of interpretation parameters
+- no beta reduction of interpretation witnesses
+- mix of locales with and without open in activate_elems
+- dangling type frees in locales
+*)
 signature LOCALE =
 sig
 type 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
 datatype expr =
 Locale of string |
 theory -> theory * (bstring * thm list) list
 val add_thmss: string -> string -> ((string * thm list) * Attrib.src list) list ->
 theory * context -> (theory * context) * (string * thm list) list
 (* Locale interpretation *)
-val instantiate: string -> string * context attribute list
--> thm list option -> context -> context
 val prep_global_registration:
 string * Attrib.src list -> expr -> string option list -> theory ->
 theory * ((string * term list) * term list) list * (theory -> theory)
 val prep_local_registration:
 string * Attrib.src list -> expr -> string option list -> context ->
 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;
 datatype expr =
 in (Termtab.update ((t, (attn, [])), regs), sups') end
 | _ => (regs, []))
 end;
 (* add witness theorem to registration,
-only if instantiation is exact, otherwise excpetion Option raised *)
+only if instantiation is exact, otherwise exception Option raised *)
 fun add_witness ts thm regs =
 let
 val t = termify ts;
 val (x, thms) = valOf (Termtab.lookup (regs, t));
 in
 (* 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))))
 (* CB: turn remaining hyps into assumptions. *)
 |> Seq.single
 fun activate_elem _ ((ctxt, axs), Fixes fixes) =
 ((ctxt |> ProofContext.add_fixes fixes, axs), [])
+| activate_elem _ ((ctxt, axs), Constrains _) = ((ctxt, axs), [])
 | activate_elem _ ((ctxt, axs), Assumes asms) =
 let
 val asms' = map_attrib_specs (Attrib.context_attribute_i ctxt) asms;
 val ts = List.concat (map (map #1 o #2) asms');
 val (ps, qs) = splitAt (length ts, axs);
 (* parameters *)
 local
-fun prep_fixes prep_vars ctxt fixes =
+fun prep_parms prep_vars ctxt parms =
-let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes))
+let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T) => ([x], T)) parms))
-in map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes) end;
+in map (fn ([x'], T') => (x', T')) vars end;
 in
-fun read_fixes x = prep_fixes ProofContext.read_vars x;
+fun read_parms x = prep_parms ProofContext.read_vars x;
-fun cert_fixes x = prep_fixes ProofContext.cert_vars x;
+fun cert_parms x = prep_parms ProofContext.cert_vars x;
 end;
 (* propositions and bindings *)
 fun declare_int_elem (ctxt, Fixes fixes) =
 (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>
 (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), [])
 | declare_int_elem (ctxt, _) = (ctxt, []);
-fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =
+fun declare_ext_elem prep_parms (ctxt, Fixes fixes) =
-(ctxt |> ProofContext.add_fixes (prep_fixes ctxt fixes), [])
+let
+val parms = map (fn (x, T, _) => (x, T)) fixes;
+val parms' = prep_parms ctxt parms;
+val fixes' = map (fn ((x, T), (_, _, mx)) => (x, T, mx)) (parms' ~~ fixes);
+in (ctxt |> ProofContext.add_fixes fixes', []) end
+| declare_ext_elem prep_parms (ctxt, Constrains csts) =
+let
+val parms = map (fn (x, T) => (x, SOME T)) csts;
+val parms' = prep_parms ctxt parms;
+val ts = map (fn (x, SOME T) => Free (x, T)) parms';
+in (Library.fold ProofContext.declare_term ts ctxt, []) end
 | 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, []);
-fun declare_elems prep_fixes (ctxt, (((name, ps), _), elems)) =
+fun declare_elems prep_parms (ctxt, (((name, ps), _), elems)) =
 let val (ctxt', propps) =
 (case elems of
 Int es => foldl_map declare_int_elem (ctxt, es)
-| Ext e => foldl_map (declare_ext_elem prep_fixes) (ctxt, [e]))
+| Ext e => foldl_map (declare_ext_elem prep_parms) (ctxt, [e]))
 handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
 in (ctxt', propps) end;
 in
 (* CB: only called by prep_elemss. *)
-fun declare_elemss prep_fixes fixed_params raw_elemss ctxt =
+fun declare_elemss prep_parms fixed_params raw_elemss ctxt =
 let
 (* CB: fix of type bug of goal in target with context elements.
 Parameters new in context elements must receive types that are
 distinct from types of parameters in target (fixed_params).  *)
 val ctxt_with_fixed =
 |> List.mapPartial (fn (id, Int es) => SOME (id, es) | _ => NONE)
 |> unify_elemss ctxt_with_fixed fixed_params;
 val (_, raw_elemss') =
 foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
 (int_elemss, raw_elemss);
-in foldl_map (declare_elems prep_fixes) (ctxt, raw_elemss') end;
+in foldl_map (declare_elems prep_parms) (ctxt, raw_elemss') end;
 end;
 local
 end;
 (* CB: for finish_elems (Int and Ext) *)
 fun eval_text _ _ _ (text, Fixes _) = text
+| eval_text _ _ _ (text, Constrains _) = text
 | eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) =
 let
 val ts = List.concat (map (map #1 o #2) asms);
 val ts' = map (norm_term env) ts;
 val spec' =
 end;
 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
 (x, assoc_string (parms, x), mx)) fixes)
+| finish_ext_elem parms _ (Constrains csts, _) =
+Constrains (map (fn (x, _) => (x, valOf (assoc_string (parms, x)))) csts)
 | finish_ext_elem _ close (Assumes asms, propp) =
 close (Assumes (map #1 asms ~~ propp))
 | finish_ext_elem _ close (Defines defs, propp) =
 close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))
 | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
 end;
 (* CB: type inference and consistency checks for locales *)
-fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
+fun prep_elemss prep_parms prepp do_close context fixed_params raw_elemss raw_concl =
 let
 (* CB: contexts computed in the course of this function are discarded.
 They are used for type inference and consistency checks only. *)
 (* CB: fixed_params are the parameters (with types) of the target locale,
 empty list if there is no target. *)
 (* CB: raw_elemss are list of pairs consisting of identifiers and
 context elements, the latter marked as internal or external. *)
-val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
+val (raw_ctxt, raw_proppss) = declare_elemss prep_parms fixed_params raw_elemss context;
 (* CB: raw_ctxt is context with additional fixed variables derived from
 the fixes elements in raw_elemss,
 raw_proppss contains assumptions and definitions from the
 external elements in raw_elemss. *)
 val raw_propps = map List.concat raw_proppss;
 (map (ProofContext.default_type ctxt) xs);
 val parms = param_types (xs ~~ typing);
 (* CB: parms are the parameters from raw_elemss, with correct typing. *)
 (* CB: extract information from assumes and defines elements
-(fixes and notes in raw_elemss don't have an effect on text and elemss),
+(fixes, constrains and notes in raw_elemss don't have an effect on
-compute final form of context elements. *)
+text and elemss), compute final form of context elements. *)
 val (text, elemss) = finish_elemss ctxt parms do_close
 (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss);
 (* CB: text has the following structure:
 (((exts, exts'), (ints, ints')), (xs, env, defs))
 where
 is a free variable; substitutions represent defines elements and
 the rhs is normalised wrt. the previous env
 defs: theorems representing the substitutions from defines elements
 (thms are normalised wrt. env).
 elemss is an updated version of raw_elemss:
-- type info added to Fixes
+- type info added to Fixes and modified in Constrains
 - axiom and definition statement replaced by corresponding one
 from proppss in Assumes and Defines
 - Facts unchanged
 *)
 in ((parms, elemss, concl), text) end;
 in
-fun read_elemss x = prep_elemss read_fixes ProofContext.read_propp_schematic x;
+fun read_elemss x = prep_elemss read_parms ProofContext.read_propp_schematic x;
-fun cert_elemss x = prep_elemss cert_fixes ProofContext.cert_propp_schematic x;
+fun cert_elemss x = prep_elemss cert_parms ProofContext.cert_propp_schematic x;
 end;
 (* facts and attributes *)
 val cert_context_statement = gen_statement (K I) gen_context_i;
 end;
-(** CB: experimental instantiation mechanism **)
-fun instantiate loc_name (prfx, attribs) raw_inst ctxt =
-let
-val thy = ProofContext.theory_of ctxt;
-val sign = Theory.sign_of thy;
-val tsig = Sign.tsig_of sign;
-val cert = cterm_of sign;
-(** process the locale **)
-val {predicate = (_, axioms), params = (ps, _), ...} =
-the_locale thy (intern sign loc_name);
-val fixed_params = param_types (map #1 ps);
-val init = ProofContext.init thy;
-val (_, raw_elemss) = flatten (init, intern_expr sign)
-(([], Symtab.empty), Expr (Locale loc_name));
-val ((parms, all_elemss, concl),
-(spec as (_, (ints, _)), (xs, env, defs))) =
-read_elemss false (* do_close *) init
-fixed_params (* could also put [] here??? *) raw_elemss
-[] (* concl *);
-(** analyse the instantiation theorem inst **)
-val inst = case raw_inst of
-NONE => if null ints
-	  then NONE
-	  else error "Locale has assumptions but no chained fact was found"
-| SOME [] => if null ints
-	  then NONE
-	  else error "Locale has assumptions but no chained fact was found"
-| SOME [thm] => if null ints
-	  then (warning "Locale has no assumptions: fact ignored"; NONE)
-	  else SOME thm
-| SOME _ => error "Multiple facts are not allowed";
-val args = case inst of
-NONE => []
-| SOME thm => thm |> prop_of |> ObjectLogic.drop_judgment sign
-|> Term.strip_comb
-|>> (fn t as (Const (s, _)) => if (intern sign loc_name = s)
-then t
-else error ("Constant " ^ quote loc_name ^
-" expected but constant " ^ quote s ^ " was found")
-| t => error ("Constant " ^ quote loc_name ^ " expected \
-\but term " ^ quote (Sign.string_of_term sign t) ^
-" was found"))
-|> snd;
-val cargs = map cert args;
-(* process parameters: match their types with those of arguments *)
-val def_names = map (fn (Free (s, _), _) => s) env;
-val (defined, assumed) = List.partition
-(fn (s, _) => s mem def_names) fixed_params;
-val cassumed = map (cert o Free) assumed;
-val cdefined = map (cert o Free) defined;
-val param_types = map snd assumed;
-val v_param_types = map Type.varifyT param_types;
-val arg_types = map Term.fastype_of args;
-val Tenv = Library.foldl (Type.typ_match tsig)
-(Vartab.empty, v_param_types ~~ arg_types)
-handle UnequalLengths => error "Number of parameters does not \
-\match number of arguments of chained fact";
-(* get their sorts *)
-val tfrees = foldr Term.add_typ_tfrees [] param_types
-val Tenv' = map
-(fn ((a, i), (S, T)) => ((a, S), T))
-(Vartab.dest Tenv);
-(* process (internal) elements *)
-fun inst_type [] T = T
-| inst_type env T =
-Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T;
-fun inst_term [] t = t
-| inst_term env t = Term.map_term_types (inst_type env) t;
-(* parameters with argument types *)
-val cparams' = map (cterm_of sign o inst_term Tenv' o term_of) cassumed;
-val cdefined' = map (cert o inst_term Tenv' o term_of) cdefined;
-val cdefining = map (cert o inst_term Tenv' o snd) env;
-fun inst_thm _ [] th = th
-| inst_thm ctxt Tenv th =
-	  let
-	    val sign = ProofContext.sign_of ctxt;
-	    val cert = Thm.cterm_of sign;
-	    val certT = Thm.ctyp_of sign;
-	    val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
-	    val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
-	    val Tenv' = List.filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
-	  in
-	    if null Tenv' then th
-	    else
-	      th
-	      |> Drule.implies_intr_list (map cert hyps)
-	      |> Drule.tvars_intr_list (map (#1 o #1) Tenv')
-	      |> (fn (th', al) => th' |>
-		Thm.instantiate ((map (fn ((a, _), T) =>
-(certT (TVar (valOf (assoc (al, a)))), certT T)) Tenv'), []))
-	      |> (fn th'' => Drule.implies_elim_list th''
-		  (map (Thm.assume o cert o inst_term Tenv') hyps))
-	  end;
-val inst_type' = inst_type Tenv';
-val inst_term' = Term.subst_atomic
-(map (pairself term_of) ((cparams' @ cdefined') ~~ (cargs @ cdefining)))
-o inst_term Tenv';
-fun inst_thm' thm =
-let
-(* not all axs are normally applicable *)
-val hyps = #hyps (rep_thm thm);
-val ass = map (fn ax => (prop_of ax, ax)) axioms;
-val axs' = Library.foldl (fn (axs, hyp) =>
-(case gen_assoc (op aconv) (ass, hyp) of NONE => axs
-| SOME ax => axs @ [ax])) ([], hyps);
-val thm' = Drule.satisfy_hyps axs' thm;
-(* instantiate types *)
-val thm'' = inst_thm ctxt Tenv' thm';
-(* substitute arguments and discharge hypotheses *)
-val thm''' = case inst of
-NONE => thm''
-| SOME inst_thm => let
-		    val hyps = #hyps (rep_thm thm'');
-		    val th = thm'' |> implies_intr_hyps
-		      |> forall_intr_list (cparams' @ cdefined')
-		      |> forall_elim_list (cargs @ cdefining)
-		    (* th has premises of the form either inst_thm or x==x *)
-		    fun mk hyp = if Logic.is_equals hyp
-			  then hyp |> Logic.dest_equals |> snd |> cert
-				 |> reflexive
-			  else inst_thm
-in implies_elim_list th (map mk hyps)
-end;
-in thm''' end
-handle THM (msg, n, thms) => error ("Exception THM " ^
-string_of_int n ^ " raised\n" ^
-	  "Note: instantiate does not support old-style locales \
-\declared with (open)\n" ^ msg ^ "\n" ^
-	cat_lines (map string_of_thm thms));
-fun inst_elem (ctxt, (Ext _)) = ctxt
-| inst_elem (ctxt, (Int (Notes facts))) =
-(* instantiate fact *)
-let
-val facts = facts |> map_attrib_facts
-(Attrib.context_attribute_i ctxt o
-Args.map_values I inst_type' inst_term' inst_thm');
-val facts' =
-map (apsnd (map (apfst (map inst_thm')))) facts
-(* rename fact *)
-val facts'' = map (apfst (apfst (NameSpace.qualified prfx))) facts'
-(* add attributes *)
-val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts''
-in fst (ProofContext.note_thmss_i facts''' ctxt)
-end
-| inst_elem (ctxt, (Int _)) = ctxt;
-(* FIXME fold o fold *)
-fun inst_elems (ctxt, (id, elems)) = Library.foldl inst_elem (ctxt, elems);
-fun inst_elemss ctxt elemss = Library.foldl inst_elems (ctxt, elemss);
-(* main part *)
-val ctxt' = ProofContext.qualified_names ctxt;
-in ProofContext.restore_naming ctxt (inst_elemss ctxt' all_elemss) end;
 (** define locales **)
 (* print locale *)
 fun print_locale thy import body =
 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 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 ":"]))];
 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:" (map (Pretty.chunks o prt_elem) all_elems)
 local
 (* extract proof obligations (assms and defs) from elements *)
-(* check if defining equation has become t == t, these are dropped
-in extract_asms_elem, as they lead to trivial proof obligations *)
-(* currently disabled *)
-fun check_def (_, (def, _)) = SOME def;
-(*
-fun check_def (_, (def, _)) =
-if def |> Logic.dest_equals |> op aconv
-then NONE else SOME def;
-*)
 fun extract_asms_elem (ts, Fixes _) = ts
+| extract_asms_elem (ts, Constrains _) = ts
 | extract_asms_elem (ts, Assumes asms) =
 ts @ List.concat (map (fn (_, ams) => map (fn (t, _) => t) ams) asms)
 | extract_asms_elem (ts, Defines defs) =
-ts @ List.mapPartial check_def defs
+ts @ map (fn (_, (def, _)) => def) defs
 | extract_asms_elem (ts, Notes _) = ts;
 fun extract_asms_elems (id, elems) =
 (id, Library.foldl extract_asms_elem ([], elems));
 map extract_asms_elems elemss;
 (* activate instantiated facts in theory or context *)
 fun activate_facts_elem _ _ _ _ (thy_ctxt, Fixes _) = thy_ctxt
+| activate_facts_elem _ _ _ _ (thy_ctxt, Constrains _) = thy_ctxt
 | activate_facts_elem _ _ _ _ (thy_ctxt, Assumes _) = thy_ctxt
 | activate_facts_elem _ _ _ _ (thy_ctxt, Defines _) = thy_ctxt
 | activate_facts_elem note_thmss attrib
 disch (prfx, atts) (thy_ctxt, Notes facts) =
 let

changeset 16169	b59202511b8a
parent 16144	e339119f4261
child 16325	a6431098a929