# HG changeset patch # User ballarin # Date 1117621850 -7200 # Node ID b59202511b8ab799ca4cd8372e91043c9de370b2 # Parent adb83939177f9db98d0c83f60b9d2948eb48f518 Locales: new element constrains, parameter renaming with syntax, experimental command instantiate withdrawn. diff -r adb83939177f -r b59202511b8a src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Wed Jun 01 12:30:49 2005 +0200 +++ b/src/Pure/Isar/isar_thy.ML Wed Jun 01 12:30:50 2005 +0200 @@ -47,8 +47,6 @@ val using_facts_i: (thm * Proof.context attribute list) list list -> ProofHistory.T -> ProofHistory.T val chain: ProofHistory.T -> ProofHistory.T - val instantiate_locale: (string * Attrib.src list) * string -> ProofHistory.T - -> ProofHistory.T val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T @@ -291,14 +289,6 @@ val chain = ProofHistory.apply Proof.chain; -(* locale instantiation *) - -fun instantiate_locale ((name, atts), loc) = - ProofHistory.apply (fn state => - Proof.instantiate_locale (loc, - (name, map (Attrib.local_attribute (Proof.theory_of state)) atts)) state); - - (* context *) val fix = ProofHistory.apply o Proof.fix; diff -r adb83939177f -r b59202511b8a src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Jun 01 12:30:49 2005 +0200 +++ b/src/Pure/Isar/locale.ML Wed Jun 01 12:30:50 2005 +0200 @@ -18,11 +18,19 @@ 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 @@ -78,8 +86,6 @@ 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) @@ -101,6 +107,7 @@ 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; @@ -303,7 +310,7 @@ 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; @@ -563,6 +570,8 @@ 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)))))) @@ -970,6 +979,7 @@ 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; @@ -1066,14 +1076,14 @@ local -fun prep_fixes prep_vars ctxt fixes = - let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes)) - in map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes) end; +fun prep_parms prep_vars ctxt parms = + let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T) => ([x], T)) parms)) + in map (fn ([x'], T') => (x', T')) vars end; in -fun read_fixes x = prep_fixes ProofContext.read_vars x; -fun cert_fixes x = prep_fixes ProofContext.cert_vars x; +fun read_parms x = prep_parms ProofContext.read_vars x; +fun cert_parms x = prep_parms ProofContext.cert_vars x; end; @@ -1124,17 +1134,27 @@ (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) = - (ctxt |> ProofContext.add_fixes (prep_fixes ctxt fixes), []) +fun declare_ext_elem prep_parms (ctxt, Fixes 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; @@ -1142,7 +1162,7 @@ (* 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 @@ -1156,7 +1176,7 @@ 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; @@ -1198,6 +1218,7 @@ (* 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); @@ -1235,6 +1256,8 @@ 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) = @@ -1270,7 +1293,7 @@ (* 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. *) @@ -1278,7 +1301,7 @@ 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 @@ -1311,8 +1334,8 @@ (* 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), - compute final form of context elements. *) + (fixes, constrains and notes in raw_elemss don't have an effect on + 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: @@ -1330,7 +1353,7 @@ 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 @@ -1339,8 +1362,8 @@ in -fun read_elemss x = prep_elemss read_fixes ProofContext.read_propp_schematic x; -fun cert_elemss x = prep_elemss cert_fixes ProofContext.cert_propp_schematic x; +fun read_elemss x = prep_elemss read_parms ProofContext.read_propp_schematic x; +fun cert_elemss x = prep_elemss cert_parms ProofContext.cert_propp_schematic x; end; @@ -1442,182 +1465,6 @@ 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 *) @@ -1639,6 +1486,7 @@ 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) = @@ -1659,6 +1507,7 @@ 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); @@ -2016,21 +1865,12 @@ (* 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) = @@ -2042,6 +1882,7 @@ (* 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 diff -r adb83939177f -r b59202511b8a src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Wed Jun 01 12:30:49 2005 +0200 +++ b/src/Pure/Isar/outer_parse.ML Wed Jun 01 12:30:50 2005 +0200 @@ -314,11 +314,14 @@ local val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K NONE || opt_mixfix >> SOME; -val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "includes"; +val loc_keyword = $$$ "fixes" || $$$ "constrains" || $$$ "assumes" || + $$$ "defines" || $$$ "notes" || $$$ "includes"; val loc_element = $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix >> triple1)) >> Locale.Fixes || + $$$ "constrains" |-- !!! (and_list1 (name -- ($$$ "::" |-- typ))) + >> Locale.Constrains || $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp)) >> Locale.Assumes || $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp')) diff -r adb83939177f -r b59202511b8a src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Jun 01 12:30:49 2005 +0200 +++ b/src/Pure/Isar/proof.ML Wed Jun 01 12:30:50 2005 +0200 @@ -68,8 +68,6 @@ (thm list * context attribute list) list) list -> state -> state val using_thmss: ((thmref * context attribute list) list) list -> state -> state val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state - val instantiate_locale: string * (string * context attribute list) -> state - -> state val fix: (string list * string option) list -> state -> state val fix_i: (string list * typ option) list -> state -> state val assm: ProofContext.exporter @@ -635,20 +633,6 @@ end; -(* locale instantiation *) - -fun instantiate_locale (loc_name, prfx_attribs) state = - let - val facts = if is_chain state then get_facts state else NONE; - in - state - |> assert_forward_or_chain - |> enter_forward - |> reset_facts - |> map_context (Locale.instantiate loc_name prfx_attribs facts) - end; - - (* fix *) fun gen_fix f xs state =