Improvements to Isar/Locales: premises generated by "includes" elements
authorballarin
Tue Sep 30 15:13:02 2003 +0200 (2003-09-30)
changeset 14215ebf291f3b449
parent 14214 5369d671f100
child 14216 a15951091d5d
Improvements to Isar/Locales: premises generated by "includes" elements
changed. Bugfix "unify_frozen".
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 30 15:10:59 2003 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 30 15:13:02 2003 +0200
     1.3 @@ -1,15 +1,15 @@
     1.4  (*  Title:      Pure/Isar/locale.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Markus Wenzel, LMU/TU München
     1.7 +    Author:     Markus Wenzel, LMU/TU Muenchen
     1.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  
    1.10  Locales -- Isar proof contexts as meta-level predicates, with local
    1.11  syntax and implicit structures.
    1.12  
    1.13 -Draws some basic ideas from Florian Kammüller's original version of
    1.14 +Draws some basic ideas from Florian Kammueller's original version of
    1.15  locales, but uses the richer infrastructure of Isar instead of the raw
    1.16  meta-logic.  Furthermore, we provide structured import of contexts
    1.17 -(with merge and rename operations), well as type-inference of the
    1.18 +(with merge and rename operations), as well as type-inference of the
    1.19  signature parts, and predicate definitions of the specification text.
    1.20  *)
    1.21  
    1.22 @@ -58,6 +58,7 @@
    1.23      theory -> theory * (bstring * thm list) list
    1.24    val add_thmss: string -> ((string * thm list) * context attribute list) list ->
    1.25      theory * context -> (theory * context) * (string * thm list) list
    1.26 +  val prune_prems: theory -> thm -> thm
    1.27    val setup: (theory -> theory) list
    1.28  end;
    1.29  
    1.30 @@ -97,7 +98,6 @@
    1.31   {view = view, import = import, elems = elems, params = params}: locale;
    1.32  
    1.33  
    1.34 -
    1.35  (** theory data **)
    1.36  
    1.37  structure LocalesArgs =
    1.38 @@ -141,6 +141,185 @@
    1.39    | None => error ("Unknown locale " ^ quote name));
    1.40  
    1.41  
    1.42 +(* import hierarchy
    1.43 +   implementation could be more efficient, eg. by maintaining a database
    1.44 +   of dependencies *)
    1.45 +
    1.46 +fun imports thy (upper, lower) =
    1.47 +  let
    1.48 +    val sign = sign_of thy;
    1.49 +    fun imps (Locale name) low = (name = low) orelse
    1.50 +      (case get_locale thy name of
    1.51 +           None => false
    1.52 +         | Some {import, ...} => imps import low)
    1.53 +      | imps (Rename (expr, _)) low = imps expr low
    1.54 +      | imps (Merge es) low = exists (fn e => imps e low) es;
    1.55 +  in
    1.56 +    imps (Locale (intern sign upper)) (intern sign lower)
    1.57 +  end;
    1.58 +
    1.59 +(** Name suffix of internal delta predicates.
    1.60 +    These specify additional assumptions in a locale with import.
    1.61 +    Also name of theorem set with destruct rules for locale main
    1.62 +    predicates. **)
    1.63 +
    1.64 +val axiomsN = "axioms";
    1.65 +
    1.66 +local
    1.67 +
    1.68 +(* A trie-like structure is used to compute a cover of a normalised
    1.69 +   locale specification.  Entries of the trie will be identifiers:
    1.70 +   locale names with parameter lists. *)
    1.71 +
    1.72 +datatype 'a trie = Trie of ('a * 'a trie) list;
    1.73 +
    1.74 +(* Subsumption relation on identifiers *)
    1.75 +
    1.76 +fun subsumes thy ((name1, args1), (name2, args2)) =
    1.77 +  (name2 = "" andalso null args2) orelse
    1.78 +  ((name2 = name1 orelse imports thy (name1, name2)) andalso
    1.79 +    (args2 prefix args1));
    1.80 +
    1.81 +(* Insert into trie, wherever possible but avoiding branching *)
    1.82 +
    1.83 +fun insert_ident subs id (Trie trie) =
    1.84 +  let
    1.85 +    fun insert id [] = [(id, Trie [])]
    1.86 +      | insert id ((id', Trie t')::ts) =
    1.87 +          if subs (id, id')
    1.88 +          then if null ts
    1.89 +            then [(id', Trie (insert id t'))] (* avoid new branch *)
    1.90 +            else (id', Trie (insert id t'))::insert id ts
    1.91 +          else (id', Trie t')::insert id ts
    1.92 +  in Trie (insert id trie) end;
    1.93 +
    1.94 +(* List of leaves of a trie, removing duplicates *)
    1.95 +
    1.96 +fun leaves _ (Trie []) = []
    1.97 +  | leaves eq (Trie ((id, Trie [])::ts)) =
    1.98 +      gen_ins eq (id, leaves eq (Trie ts))
    1.99 +  | leaves eq (Trie ((id, ts')::ts)) =
   1.100 +      gen_merge_lists eq (leaves eq ts') (leaves eq (Trie ts));
   1.101 +
   1.102 +in 
   1.103 +
   1.104 +(* Prune premises: remove internal delta predicates.
   1.105 +
   1.106 +   Assumes no outer quanfifiers and no flex-flex pairs.
   1.107 +   May change names of TVars.
   1.108 +   Performs compress and close_derivation on result, if modified. *)
   1.109 +
   1.110 +fun prune_prems thy thm = let
   1.111 +  val sign = Theory.sign_of thy;
   1.112 +  fun analyse cprem =
   1.113 +    (* Returns None if head of premise is not a predicate defined by a locale,
   1.114 +       returns also None if locale has import but predicate is not *_axioms
   1.115 +       since this is a premise that wasn't generated by includes.  *)
   1.116 +    case Term.strip_comb (ObjectLogic.drop_judgment sign (term_of cprem)) of
   1.117 +	(Const (raw_name, T), args) => let
   1.118 +            val name = unsuffix ("_" ^ axiomsN) raw_name
   1.119 +              handle LIST _ => raw_name
   1.120 +          in case get_locale thy name of
   1.121 +		None => None
   1.122 +	      | Some {import, ...} =>
   1.123 +                  if name = raw_name andalso import <> empty
   1.124 +                  then None
   1.125 +                  else Some (((name, args), T), name = raw_name)
   1.126 +          end
   1.127 +      | _ => None;
   1.128 +  val TFrees = add_term_tfree_names (prop_of thm, []);
   1.129 +    (* Ignores TFrees in flex-flex pairs ! *)
   1.130 +  val (frozen, thaw) = Drule.freeze_thaw thm;
   1.131 +  val cprop = cprop_of frozen;
   1.132 +  val cprems = Drule.strip_imp_prems cprop;
   1.133 +  val analysis = map analyse cprems;
   1.134 +in
   1.135 +  if foldl (fn (b, None) => b | (b, Some (_, b')) => b andalso b')
   1.136 +           (true, analysis)
   1.137 +  then thm   (* No premise contains *_axioms predicate
   1.138 +                ==> no changes necessary. *)
   1.139 +  else let
   1.140 +    val ids = map (apsome fst) analysis;
   1.141 +    (* Analyse dependencies of locale premises: store in trie. *)
   1.142 +    fun subs ((x, _), (y, _)) = subsumes thy (x, y);
   1.143 +    val Trie depcs = foldl (fn (trie, None) => trie
   1.144 +			     | (trie, Some id) => insert_ident subs id trie)
   1.145 +			   (Trie [], ids);
   1.146 +    (* Assemble new theorem; new prems will be hyps.
   1.147 +       Axioms is an intermeditate list of locale axioms required to
   1.148 +       replace old premises by new ones. *)
   1.149 +    fun scan ((roots, thm, cprems', axioms), (cprem, id)) =
   1.150 +	  case id of
   1.151 +	      None => (roots, implies_elim thm (assume cprem),
   1.152 +		       cprems' @ [cprem], [])
   1.153 +					       (* Normal premise: keep *)
   1.154 +	    | Some id =>                       (* Locale premise *)
   1.155 +		let
   1.156 +		  fun elim_ax [] thm =  (* locale has no axioms *)
   1.157 +		      implies_elim thm (assume cprem)
   1.158 +		    | elim_ax axs thm = let
   1.159 +		    (* Eliminate first premise of thm, which is of the form
   1.160 +                       id.  Add hyp of the used axiom to thm. *)
   1.161 +		    val ax = the (assoc (axs, fst (fst id)))
   1.162 +	              handle _ => error ("Internal error in Locale.prune_\
   1.163 +                        \prems: axiom for premise" ^
   1.164 +                        fst (fst id) ^ " not found.");
   1.165 +		    val [ax_cprem] = Drule.strip_imp_prems (cprop_of ax)
   1.166 +		      handle _ => error ("Internal error in Locale.prune_\
   1.167 +                        \prems: exactly one premise in axiom expected.");
   1.168 +		    val ax_hyp = implies_elim ax (assume (ax_cprem))
   1.169 +		  in implies_elim thm ax_hyp
   1.170 +		  end
   1.171 +		in
   1.172 +		  if null roots
   1.173 +		  then (roots, elim_ax axioms thm, cprems', axioms)
   1.174 +					       (* Remaining premise: drop *)
   1.175 +		  else let
   1.176 +		      fun mk_cprem ((name, args), T) = cterm_of sign
   1.177 +                        (ObjectLogic.assert_propT sign
   1.178 +			  (Term.list_comb (Const (name, T), args)));
   1.179 +		      fun get_axs ((name, args), _) = let
   1.180 +			  val {view = (_, axioms), ...} = the_locale thy name;
   1.181 +			  fun inst ax =
   1.182 +			    let
   1.183 +			      val std = standard ax;
   1.184 +                              val (prem, concl) =
   1.185 +                                Logic.dest_implies (prop_of std);
   1.186 +			      val (Const (name2, _), _) = Term.strip_comb
   1.187 +				(ObjectLogic.drop_judgment sign concl);
   1.188 +                              val (_, vars) = Term.strip_comb
   1.189 +				(ObjectLogic.drop_judgment sign prem);
   1.190 +			      val cert = map (cterm_of sign);
   1.191 +			    in (unsuffix ("_" ^ axiomsN) name2
   1.192 +                                  handle LIST _ => name2,
   1.193 +			       cterm_instantiate (cert vars ~~ cert args) std)
   1.194 +			    end;
   1.195 +			in map inst axioms end;
   1.196 +		      val (id', trie) = hd roots;
   1.197 +		    in if id = id'
   1.198 +		      then                     (* Initial premise *)
   1.199 +			let
   1.200 +			  val lvs = leaves eq_fst (Trie [(id', trie)]);
   1.201 +			  val axioms' = flat (map get_axs lvs)
   1.202 +			in (tl roots, elim_ax axioms' thm,
   1.203 +                            cprems' @ map (mk_cprem) lvs, axioms')
   1.204 +			end
   1.205 +		      else (roots, elim_ax axioms thm, cprems', axioms)
   1.206 +					       (* Remaining premise: drop *)
   1.207 +		    end
   1.208 +		end;
   1.209 +    val (_, thm', cprems', _) =
   1.210 +      (foldl scan ((depcs, frozen, [], []), cprems ~~ ids));
   1.211 +    val thm'' = implies_intr_list cprems' thm';
   1.212 +  in
   1.213 +    fst (varifyT' TFrees (thaw thm''))
   1.214 +    |> Thm.compress |> Drule.close_derivation
   1.215 +  end
   1.216 +end;
   1.217 +
   1.218 +end (* local *)
   1.219 +
   1.220 +
   1.221  (* diagnostics *)
   1.222  
   1.223  fun err_in_locale ctxt msg ids =
   1.224 @@ -265,15 +444,17 @@
   1.225  
   1.226  fun unify_frozen ctxt maxidx Ts Us =
   1.227    let
   1.228 -    val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
   1.229 -    fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T)
   1.230 -          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   1.231 -      | unify (env, _) = env;
   1.232      fun paramify (i, None) = (i, None)
   1.233        | paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T));
   1.234  
   1.235      val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);
   1.236      val (maxidx'', Us') = foldl_map paramify (maxidx', Us);
   1.237 +    val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
   1.238 +
   1.239 +    fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T)
   1.240 +          handle Type.TUNIFY =>
   1.241 +            raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
   1.242 +      | unify (env, _) = env;
   1.243      val (unifier, _) = foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us');
   1.244      val Vs = map (apsome (Envir.norm_type unifier)) Us';
   1.245      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (mapfilter I Vs));
   1.246 @@ -323,7 +504,7 @@
   1.247        foldr Term.add_typ_tfrees (mapfilter snd ps, [])
   1.248        |> mapfilter (fn (a, S) =>
   1.249            let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   1.250 -          in if T = TFree (a, S) then None else Some ((a, S), T) end);
   1.251 +          in if T = TFree (a, S) then None else Some ((a, S), T) end)
   1.252    in map inst_parms idx_parmss end;
   1.253  
   1.254  in
   1.255 @@ -354,6 +535,8 @@
   1.256        end;
   1.257  
   1.258      fun identify ((ids, parms), Locale name) =
   1.259 +    (* CB: ids is list of pairs: locale name and list of parameter renamings,
   1.260 +       parms is accumulated list of parameters *)
   1.261            let
   1.262              val {import, params, ...} = the_locale thy name;
   1.263              val ps = map #1 (#1 params);
   1.264 @@ -510,12 +693,19 @@
   1.265  
   1.266  in
   1.267  
   1.268 +(* CB: only called by prep_elemss. *)
   1.269 +
   1.270  fun declare_elemss prep_fixes fixed_params raw_elemss ctxt =
   1.271    let
   1.272 +    (* CB: fix of type bug of goal in target with context elements.
   1.273 +       Parameters new in context elements must receive types that are
   1.274 +       distinct from types of parameters in target (fixed_params).  *)
   1.275 +    val ctxt_with_fixed =
   1.276 +      ProofContext.declare_terms (map Free fixed_params) ctxt;
   1.277      val int_elemss =
   1.278        raw_elemss
   1.279        |> mapfilter (fn (id, Int es) => Some (id, es) | _ => None)
   1.280 -      |> unify_elemss ctxt fixed_params;
   1.281 +      |> unify_elemss ctxt_with_fixed fixed_params;
   1.282      val (_, raw_elemss') =
   1.283        foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
   1.284          (int_elemss, raw_elemss);
   1.285 @@ -689,13 +879,24 @@
   1.286            apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr));
   1.287  
   1.288      val (import_ids, raw_import_elemss) = flatten ([], Expr import);
   1.289 +    (* CB: normalise "includes" among elements *)
   1.290      val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
   1.291      val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
   1.292        context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
   1.293 -
   1.294      val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
   1.295      val ((import_ctxt, axioms'), (import_elemss, _)) =
   1.296        activate_facts prep_facts ((context, axioms), ps);
   1.297 +
   1.298 +(* CB: testing *)
   1.299 +
   1.300 +val axioms' = if true (* null axioms *) then axioms' else
   1.301 +let val {view = (ax3_view, ax3_axioms), ...} =
   1.302 +  the_locale (ProofContext.theory_of context) "Type.ax3";
   1.303 +val ax_TrueFalse = Thm.assume (read_cterm (sign_of_thm (hd axioms))
   1.304 +  ("True <-> False", propT));
   1.305 +val {view = (ax4_view, ax4_axioms), ...} =
   1.306 +  the_locale (ProofContext.theory_of context) "Type.ax4";
   1.307 +in axioms' @ ax3_axioms @ [ax_TrueFalse] @ (tl ax4_axioms) end;
   1.308      val ((ctxt, _), (elemss, _)) =
   1.309        activate_facts prep_facts ((import_ctxt, axioms'), qs);
   1.310    in
   1.311 @@ -710,6 +911,7 @@
   1.312      val thy = ProofContext.theory_of ctxt;
   1.313      val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
   1.314      val ((view_statement, view_axioms), fixed_params, import) =
   1.315 +(* view_axioms are xxx.axioms of locale xxx *)
   1.316        (case locale of None => (([], []), [], empty)
   1.317        | Some name =>
   1.318            let val {view, params = (ps, _), ...} = the_locale thy name
   1.319 @@ -720,10 +922,29 @@
   1.320  
   1.321  in
   1.322  
   1.323 +(* CB
   1.324 +arguments are (see below): x->import, y->body (elements?), z->context
   1.325  fun read_context x y z = #1 (gen_context true [] [] x y [] z);
   1.326  fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
   1.327 +*)
   1.328 +fun read_context x y z = (warning "read_context\n"; #1 (gen_context true [] [] x y [] z));
   1.329 +fun cert_context x y z = (warning "cert_context\n"; #1 (gen_context_i true [] [] x y [] z));
   1.330 +
   1.331 +(* CB
   1.332  val read_context_statement = gen_statement intern gen_context;
   1.333  val cert_context_statement = gen_statement (K I) gen_context_i;
   1.334 +*)
   1.335 +
   1.336 +fun read_context_statement so cs xss ctxt =
   1.337 +let val (locale, view_statement, locale_ctxt, elems_ctxt, concl') =
   1.338 +  gen_statement intern gen_context so cs xss ctxt;
   1.339 +in (locale, view_statement, locale_ctxt, elems_ctxt, concl')
   1.340 +end;
   1.341 +fun cert_context_statement so cs xss ctxt =
   1.342 +let val (locale, view_statement, locale_ctxt, elems_ctxt, concl') =
   1.343 +  gen_statement (K I) gen_context_i so cs xss ctxt;
   1.344 +in (locale, view_statement, locale_ctxt, elems_ctxt, concl')  
   1.345 +end;
   1.346  
   1.347  end;
   1.348  
   1.349 @@ -837,7 +1058,6 @@
   1.350  local
   1.351  
   1.352  val introN = "intro";
   1.353 -val axiomsN = "axioms";
   1.354  
   1.355  fun atomize_spec sign ts =
   1.356    let
   1.357 @@ -979,6 +1199,7 @@
   1.358  in
   1.359  
   1.360  val add_locale = gen_add_locale read_context intern_expr;
   1.361 +
   1.362  val add_locale_i = gen_add_locale cert_context (K I);
   1.363  
   1.364  end;
     2.1 --- a/src/Pure/Isar/method.ML	Tue Sep 30 15:10:59 2003 +0200
     2.2 +++ b/src/Pure/Isar/method.ML	Tue Sep 30 15:13:02 2003 +0200
     2.3 @@ -674,7 +674,7 @@
     2.4  fun inst_args_var f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
     2.5  
     2.6  fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
     2.7 -  (fn (quant, s) => SIMPLE_METHOD' quant ( (*K (impose_hyps_tac ctxt) THEN' *) tac s))) src ctxt);
     2.8 +  (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt);
     2.9  
    2.10  fun goal_args args tac = goal_args' (Scan.lift args) tac;
    2.11  
     3.1 --- a/src/Pure/Isar/proof.ML	Tue Sep 30 15:10:59 2003 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Tue Sep 30 15:13:02 2003 +0200
     3.3 @@ -821,8 +821,13 @@
     3.4      val ts = flat tss;
     3.5      val locale_results = map (ProofContext.export_standard [] goal_ctxt locale_ctxt)
     3.6        (prep_result state ts raw_thm);
     3.7 +
     3.8 +    val locale_results' = map
     3.9 +      (Locale.prune_prems (ProofContext.theory_of locale_ctxt))
    3.10 +      locale_results;
    3.11 +
    3.12      val results = map (Drule.strip_shyps_warning o
    3.13 -      ProofContext.export_standard view locale_ctxt theory_ctxt) locale_results;
    3.14 +      ProofContext.export_standard view locale_ctxt theory_ctxt) locale_results';
    3.15  
    3.16      val (theory', results') =
    3.17        theory_of state
    3.18 @@ -830,7 +835,7 @@
    3.19          if length names <> length loc_attss then
    3.20            raise THEORY ("Bad number of locale attributes", [thy])
    3.21          else (thy, locale_ctxt)
    3.22 -          |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss)
    3.23 +          |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results') ~~ loc_attss)
    3.24            |> (fn ((thy', ctxt'), res) =>
    3.25              if name = "" andalso null loc_atts then thy'
    3.26              else (thy', ctxt')