tuned add_thmss;
authorwenzelm
Wed Jul 10 14:51:18 2002 +0200 (2002-07-10 ago)
changeset 133361bd21b082466
parent 13335 7995b3f4ca5e
child 13337 f75dfc606ac7
tuned add_thmss;
beginnings of locale predicates;
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Jul 10 14:50:08 2002 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Jul 10 14:51:18 2002 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4      ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
     1.5      theory -> theory * (bstring * thm list) list
     1.6    val add_thmss: string -> ((string * thm list) * context attribute list) list ->
     1.7 -    context * theory -> (context * theory) * thm list list
     1.8 +    theory * context -> (theory * context) * thm list list
     1.9    val setup: (theory -> theory) list
    1.10  end;
    1.11  
    1.12 @@ -414,9 +414,8 @@
    1.13  fun activate_elemss prep_facts = foldl_map (fn (ctxt, ((name, ps), raw_elems)) =>
    1.14    let
    1.15      val elems = map (prep_facts ctxt) raw_elems;
    1.16 -    val res = ((name, ps), elems);
    1.17 -    val (ctxt', facts) = apsnd flat (activate_elems res ctxt);
    1.18 -  in (ctxt', (res, facts)) end);
    1.19 +    val (ctxt', facts) = apsnd flat (activate_elems ((name, ps), map fst elems) ctxt);
    1.20 +  in (ctxt', (((name, ps), elems), facts)) end);
    1.21  
    1.22  in
    1.23  
    1.24 @@ -424,10 +423,6 @@
    1.25    let val (ctxt', (elemss', factss)) = apsnd split_list (activate_elemss prep_facts ctxt_elemss)
    1.26    in (ctxt', (elemss', flat factss)) end;
    1.27  
    1.28 -fun apply_facts name (ctxt, facts) =
    1.29 -  let val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((name, []), [Notes facts])])
    1.30 -  in (ctxt', map #2 facts') end;
    1.31 -
    1.32  end;
    1.33  
    1.34  
    1.35 @@ -517,34 +512,39 @@
    1.36  
    1.37  val norm_term = Envir.beta_norm oo Term.subst_atomic;
    1.38  
    1.39 -fun abstract_def eq =    (*assumes well-formedness according to ProofContext.cert_def*)
    1.40 +fun abstract_term eq =    (*assumes well-formedness according to ProofContext.cert_def*)
    1.41    let
    1.42      val body = Term.strip_all_body eq;
    1.43      val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
    1.44      val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
    1.45      val (f, xs) = Term.strip_comb lhs;
    1.46 -  in (Term.dest_Free f, Term.list_abs_free (map Term.dest_Free xs, rhs)) end;
    1.47 +    val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
    1.48 +  in (Term.dest_Free f, eq') end;
    1.49 +
    1.50 +fun abstract_thm sign eq =
    1.51 +  Thm.assume (Thm.cterm_of sign eq) |> Drule.gen_all |> Drule.abs_def;
    1.52  
    1.53 -fun bind_def ctxt (name, ps) ((xs, env), eq) =
    1.54 +fun bind_def ctxt (name, ps) ((xs, env, ths), eq) =
    1.55    let
    1.56 -    val ((y, T), b) = abstract_def eq;
    1.57 +    val ((y, T), b) = abstract_term eq;
    1.58      val b' = norm_term env b;
    1.59 +    val th = abstract_thm (ProofContext.sign_of ctxt) eq;
    1.60      fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
    1.61    in
    1.62      conditional (exists (equal y o #1) xs) (fn () =>
    1.63        err "Attempt to define previously specified variable");
    1.64      conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
    1.65        err "Attempt to redefine variable");
    1.66 -    (Term.add_frees (xs, b'), (Free (y, T), b') :: env)
    1.67 +    (Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths)
    1.68    end;
    1.69  
    1.70  fun eval_text _ _ _ (text, Fixes _) = text
    1.71 -  | eval_text _ _ do_text ((spec, (xs, env)), Assumes asms) =
    1.72 +  | eval_text _ _ do_text ((spec, (xs, env, defs)), Assumes asms) =
    1.73        let
    1.74          val ts = map (norm_term env) (flat (map (map #1 o #2) asms));
    1.75          val spec' = if do_text then spec @ ts else spec;
    1.76          val xs' = foldl Term.add_frees (xs, ts);
    1.77 -      in (spec', (xs', env)) end
    1.78 +      in (spec', (xs', env, defs)) end
    1.79    | eval_text ctxt id _ ((spec, binds), Defines defs) =
    1.80        (spec, foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
    1.81    | eval_text _ _ _ (text, Notes _) = text;
    1.82 @@ -623,7 +623,7 @@
    1.83      val parms = param_types (xs ~~ typing);
    1.84  
    1.85      val (text, elemss) =
    1.86 -      finish_elemss ctxt parms do_close do_text (([], ([], [])), raw_elemss ~~ proppss);
    1.87 +      finish_elemss ctxt parms do_close do_text (([], ([], [], [])), raw_elemss ~~ proppss);
    1.88    in ((parms, elemss, concl), text) end;
    1.89  
    1.90  in
    1.91 @@ -643,12 +643,12 @@
    1.92      raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
    1.93    else (name, atts);
    1.94  
    1.95 -fun prep_facts _ _ (Int elem) = elem
    1.96 -  | prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes
    1.97 -  | prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms)
    1.98 -  | prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs)
    1.99 -  | prep_facts get ctxt (Ext (Notes facts)) = Notes (facts |> map (fn (a, bs) =>
   1.100 -      (prep_name ctxt a, map (apfst (get ctxt)) bs)));
   1.101 +fun prep_facts _ _ (Int elem) = (elem, false)
   1.102 +  | prep_facts _ _ (Ext (Fixes fixes)) = (Fixes fixes, true)
   1.103 +  | prep_facts _ ctxt (Ext (Assumes asms)) = (Assumes (map (apfst (prep_name ctxt)) asms), true)
   1.104 +  | prep_facts _ ctxt (Ext (Defines defs)) = (Defines (map (apfst (prep_name ctxt)) defs), true)
   1.105 +  | prep_facts get ctxt (Ext (Notes facts)) = (Notes (facts |> map (fn (a, bs) =>
   1.106 +      (prep_name ctxt a, map (apfst (get ctxt)) bs))), true);
   1.107  
   1.108  in
   1.109  
   1.110 @@ -674,8 +674,10 @@
   1.111  
   1.112      val (import_ids, raw_import_elemss) = flatten ([], Expr import);
   1.113      val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
   1.114 -    val ((parms, all_elemss, concl), (spec, (xs, _))) = prep_elemss do_close do_text context
   1.115 -      fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
   1.116 +    val ((parms, all_elemss, concl), (spec, (xs, _, defs))) = prep_elemss do_close do_text
   1.117 +      context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
   1.118 +    val xs' = parms |> mapfilter (fn (p, _) =>
   1.119 +      (case assoc_string (xs, p) of None => None | Some T => Some (p, T)));
   1.120  
   1.121      val n = length raw_import_elemss;
   1.122      val (import_ctxt, (import_elemss, import_facts)) =
   1.123 @@ -684,7 +686,7 @@
   1.124        activate_facts prep_facts (import_ctxt, drop (n, all_elemss));
   1.125    in
   1.126      ((((import_ctxt, (import_elemss, import_facts)),
   1.127 -      (ctxt, (elemss, facts))), (xs, spec)), concl)
   1.128 +      (ctxt, (elemss, facts))), (xs', spec, defs)), concl)
   1.129    end;
   1.130  
   1.131  val gen_context = prep_context_statement intern_expr read_elemss get_facts;
   1.132 @@ -719,15 +721,17 @@
   1.133  
   1.134  
   1.135  
   1.136 -(** print locale **)
   1.137 +(** define locales **)
   1.138 +
   1.139 +(* print locale *)
   1.140  
   1.141  fun print_locale thy import body =
   1.142    let
   1.143      val sg = Theory.sign_of thy;
   1.144      val thy_ctxt = ProofContext.init thy;
   1.145 -    val (((_, (import_elemss, _)), (ctxt, (elemss, _))), (pred_xs, pred_ts)) =
   1.146 -      read_context true import body thy_ctxt;
   1.147 -    val all_elems = flat (map #2 (import_elemss @ elemss));
   1.148 +    val (((_, (import_elemss, _)), (ctxt, (elemss, _))), _) =
   1.149 +      read_context false import body thy_ctxt;
   1.150 +    val all_elems = map #1 (flat (map #2 (import_elemss @ elemss)));
   1.151  
   1.152      val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
   1.153      val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
   1.154 @@ -753,23 +757,12 @@
   1.155        | prt_elem (Assumes asms) = items "assumes" (map prt_asm asms)
   1.156        | prt_elem (Defines defs) = items "defines" (map prt_def defs)
   1.157        | prt_elem (Notes facts) = items "notes" (map prt_fact facts);
   1.158 -
   1.159 -    val prt_pred =
   1.160 -      if null pred_ts then Pretty.str ""
   1.161 -      else
   1.162 -        Library.foldr1 Logic.mk_conjunction pred_ts
   1.163 -        |> ObjectLogic.atomize_term sg
   1.164 -        |> curry Term.list_abs_free pred_xs
   1.165 -        |> prt_term;
   1.166    in
   1.167 -    [Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems),
   1.168 -      Pretty.big_list "predicate text:" [prt_pred]] |> Pretty.chunks |> Pretty.writeln
   1.169 +    Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems)
   1.170 +    |> Pretty.writeln
   1.171    end;
   1.172  
   1.173  
   1.174 -
   1.175 -(** define locales **)
   1.176 -
   1.177  (* store results *)
   1.178  
   1.179  local
   1.180 @@ -821,15 +814,44 @@
   1.181  val have_thmss = gen_have_thmss intern ProofContext.get_thms;
   1.182  val have_thmss_i = gen_have_thmss (K I) (K I);
   1.183  
   1.184 -fun add_thmss loc args (ctxt, thy) =
   1.185 +fun add_thmss loc args (thy, ctxt) =
   1.186    let
   1.187      val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
   1.188 -    val (ctxt', facts') = apply_facts loc (ctxt, args');
   1.189 -  in ((ctxt', thy |> put_facts loc args'), facts') end;
   1.190 +    val thy' = put_facts loc args' thy;
   1.191 +    val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((loc, []), [(Notes args', false)])]);
   1.192 +  in ((thy', ctxt'), map #2 facts') end;
   1.193  
   1.194  end;
   1.195  
   1.196  
   1.197 +(* predicate text *)
   1.198 +
   1.199 +val predN = suffix "_axioms";
   1.200 +
   1.201 +fun define_pred _ _ _ [] thy = thy
   1.202 +  | define_pred bname name xs ts thy =
   1.203 +      let
   1.204 +        val sign = Theory.sign_of thy;
   1.205 +
   1.206 +        val body = ObjectLogic.atomize_term sign (Library.foldr1 Logic.mk_conjunction ts);
   1.207 +        val bodyT = Term.fastype_of body;
   1.208 +        val predT = map #2 xs ---> bodyT;
   1.209 +
   1.210 +        val n = length xs;
   1.211 +        fun aprop_tr' c = (c, fn args =>
   1.212 +          if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
   1.213 +          else raise Match);
   1.214 +      in
   1.215 +        thy
   1.216 +        |> (if bodyT <> propT then I
   1.217 +            else Theory.add_trfuns ([], [], map aprop_tr' (NameSpace.accesses' (predN name)), []))
   1.218 +        |> Theory.add_consts_i [(predN bname, predT, Syntax.NoSyn)]
   1.219 +        |> PureThy.add_defs_i false [((Thm.def_name (predN bname),
   1.220 +            Logic.mk_equals (Term.list_comb (Const (predN name, predT), map Free xs), body)), [])]
   1.221 +        |> #1
   1.222 +      end;
   1.223 +
   1.224 +
   1.225  (* add_locale(_i) *)
   1.226  
   1.227  local
   1.228 @@ -842,21 +864,18 @@
   1.229        error ("Duplicate definition of locale " ^ quote name));
   1.230  
   1.231      val thy_ctxt = ProofContext.init thy;
   1.232 -    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))), (xs, spec)) =
   1.233 -      prep_ctxt true raw_import raw_body thy_ctxt;
   1.234 +    val (((import_ctxt, (import_elemss, _)), (body_ctxt, (body_elemss, _))),
   1.235 +      (pred_xs, pred_ts, defs)) = prep_ctxt true raw_import raw_body thy_ctxt;
   1.236  
   1.237      val import_parms = params_of import_elemss;
   1.238      val body_parms = params_of body_elemss;
   1.239      val all_parms = import_parms @ body_parms;
   1.240  
   1.241 -    (* FIXME define foo xs' == atomized spec *)
   1.242 -    val xs' = all_parms |> mapfilter (fn (p, _) =>
   1.243 -      (case assoc_string (xs, p) of None => None | Some T => Some (p, T)));
   1.244 -
   1.245      val import = prep_expr sign raw_import;
   1.246 -    val elems = flat (map snd body_elemss);
   1.247 +    val elems = map fst (flat (map snd body_elemss));
   1.248    in
   1.249      thy
   1.250 +    |> define_pred bname name pred_xs pred_ts
   1.251      |> declare_locale name
   1.252      |> put_locale name (make_locale import (map (fn e => (e, stamp ())) elems)
   1.253          (all_parms, map fst body_parms))