src/Pure/Isar/rule_insts.ML
changeset 20343 e093a54bf25e
parent 20336 aac494583949
child 20487 6ac7a4fc32a0
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Aug 05 14:52:57 2006 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Aug 05 14:52:58 2006 +0200
     1.3 @@ -15,124 +15,152 @@
     1.4  struct
     1.5  
     1.6  
     1.7 -(** attributes **)
     1.8 -
     1.9 -(* read_instantiate: named instantiation of type and term variables *)
    1.10 +(** reading instantiations **)
    1.11  
    1.12  local
    1.13  
    1.14 -fun is_tvar (x, _) = (case Symbol.explode x of "'" :: _ => true | _ => false);
    1.15 +fun is_tvar (x, _) = String.isPrefix "'" x;
    1.16  
    1.17  fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi);
    1.18  
    1.19 -fun the_sort sorts xi = the (sorts xi)
    1.20 +fun the_sort tvars xi = the (AList.lookup (op =) tvars xi)
    1.21    handle Option.Option => error_var "No such type variable in theorem: " xi;
    1.22  
    1.23 -fun the_type types xi = the (types xi)
    1.24 +fun the_type vars xi = the (AList.lookup (op =) vars xi)
    1.25    handle Option.Option => error_var "No such variable in theorem: " xi;
    1.26  
    1.27 -fun unify_types thy types (xi, u) (unifier, maxidx) =
    1.28 +fun unify_vartypes thy vars (xi, u) (unifier, maxidx) =
    1.29    let
    1.30 -    val T = the_type types xi;
    1.31 +    val T = the_type vars xi;
    1.32      val U = Term.fastype_of u;
    1.33 -    val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
    1.34 +    val maxidx' = Term.maxidx_term u (Int.max (#2 xi, maxidx));
    1.35    in
    1.36      Sign.typ_unify thy (T, U) (unifier, maxidx')
    1.37        handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
    1.38    end;
    1.39  
    1.40 -fun typ_subst env = apsnd (Term.typ_subst_TVars env);
    1.41 -fun subst env = apsnd (Term.subst_TVars env);
    1.42 +fun instantiate inst =
    1.43 +  Term.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
    1.44 +  Envir.beta_norm;
    1.45  
    1.46 -fun instantiate thy envT env thm =
    1.47 +fun make_instT f v =
    1.48    let
    1.49 -    val (_, sorts) = Drule.types_sorts thm;
    1.50 -    fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T);
    1.51 -    fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t);
    1.52 -  in
    1.53 -    Drule.instantiate (map prepT (distinct (op =) envT),
    1.54 -      map prep (distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
    1.55 -  end;
    1.56 +    val T = TVar v;
    1.57 +    val T' = f T;
    1.58 +  in if T = T' then NONE else SOME (T, T') end;
    1.59 +
    1.60 +fun make_inst f v =
    1.61 +  let
    1.62 +    val t = Var v;
    1.63 +    val t' = f t;
    1.64 +  in if t aconv t' then NONE else SOME (t, t') end;
    1.65  
    1.66  in
    1.67  
    1.68 -fun read_instantiate mixed_insts (context, thm) =
    1.69 +fun read_insts ctxt mixed_insts (tvars, vars) =
    1.70    let
    1.71 -    val thy = Context.theory_of context;
    1.72 -    val ctxt = Context.proof_of context;
    1.73 +    val thy = ProofContext.theory_of ctxt;
    1.74 +    val cert = Thm.cterm_of thy;
    1.75 +    val certT = Thm.ctyp_of thy;
    1.76  
    1.77 -    val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts);
    1.78 +    val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
    1.79      val internal_insts = term_insts |> map_filter
    1.80        (fn (xi, Args.Term t) => SOME (xi, t)
    1.81 -      | (_, Args.Name _) => NONE
    1.82 -      | (xi, _) => error_var "Term argument expected for " xi);
    1.83 +        | (_, Args.Name _) => NONE
    1.84 +        | (xi, _) => error_var "Term argument expected for " xi);
    1.85      val external_insts = term_insts |> map_filter
    1.86        (fn (xi, Args.Name s) => SOME (xi, s) | _ => NONE);
    1.87  
    1.88  
    1.89 -    (* type instantiations *)
    1.90 -
    1.91 -    val sorts = #2 (Drule.types_sorts thm);
    1.92 +    (* mixed type instantiations *)
    1.93  
    1.94      fun readT (xi, arg) =
    1.95        let
    1.96 -        val S = the_sort sorts xi;
    1.97 +        val S = the_sort tvars xi;
    1.98          val T =
    1.99            (case arg of
   1.100              Args.Name s => ProofContext.read_typ ctxt s
   1.101            | Args.Typ T => T
   1.102            | _ => error_var "Type argument expected for " xi);
   1.103        in
   1.104 -        if Sign.of_sort thy (T, S) then (xi, T)
   1.105 +        if Sign.of_sort thy (T, S) then ((xi, S), T)
   1.106          else error_var "Incompatible sort for typ instantiation of " xi
   1.107        end;
   1.108  
   1.109 -    val type_insts' = map readT type_insts;
   1.110 -    val thm' = instantiate thy type_insts' [] thm;
   1.111 +    val type_insts1 = map readT type_insts;
   1.112 +    val instT1 = Term.instantiateT type_insts1;
   1.113 +    val vars1 = map (apsnd instT1) vars;
   1.114  
   1.115  
   1.116      (* internal term instantiations *)
   1.117  
   1.118 -    val types' = #1 (Drule.types_sorts thm');
   1.119 -    val unifier = map (apsnd snd) (Vartab.dest (#1
   1.120 -      (fold (unify_types thy types') internal_insts (Vartab.empty, 0))));
   1.121 -
   1.122 -    val type_insts'' = map (typ_subst unifier) type_insts';
   1.123 -    val internal_insts'' = map (subst unifier) internal_insts;
   1.124 -    val thm'' = instantiate thy unifier internal_insts'' thm';
   1.125 +    val instT2 = Envir.norm_type
   1.126 +      (#1 (fold (unify_vartypes thy vars1) internal_insts (Vartab.empty, 0)));
   1.127 +    val vars2 = map (apsnd instT2) vars1;
   1.128 +    val internal_insts2 = map (apsnd (map_term_types instT2)) internal_insts;
   1.129 +    val inst2 = instantiate internal_insts2;
   1.130  
   1.131  
   1.132      (* external term instantiations *)
   1.133  
   1.134 -    val types'' = #1 (Drule.types_sorts thm'');
   1.135 -
   1.136 -    val (xs, ss) = split_list external_insts;
   1.137 -    val Ts = map (the_type types'') xs;
   1.138 -    val (ts, inferred) = ProofContext.read_termTs ctxt (K false)
   1.139 -        (K NONE) (K NONE) (Drule.add_used thm'' []) (ss ~~ Ts);
   1.140 +    val (xs, strs) = split_list external_insts;
   1.141 +    val Ts = map (the_type vars2) xs;
   1.142 +    val (ts, inferred) =   (* FIXME polymorphic!? schematic vs. 'for' context!? *)
   1.143 +      ProofContext.read_termTs_schematic ctxt (K false) (K NONE) (K NONE) [] (strs ~~ Ts);
   1.144  
   1.145 -    val type_insts''' = map (typ_subst inferred) type_insts'';
   1.146 -    val internal_insts''' = map (subst inferred) internal_insts'';
   1.147 -
   1.148 -    val external_insts''' = xs ~~ ts;
   1.149 -    val term_insts''' = internal_insts''' @ external_insts''';
   1.150 -    val thm''' = instantiate thy inferred external_insts''' thm'';
   1.151 +    val instT3 = Term.typ_subst_TVars inferred;
   1.152 +    val vars3 = map (apsnd instT3) vars2;
   1.153 +    val internal_insts3 = map (apsnd (map_term_types instT3)) internal_insts2;
   1.154 +    val external_insts3 = xs ~~ ts;
   1.155 +    val inst3 = instantiate external_insts3;
   1.156  
   1.157  
   1.158 -    (* assign internalized values *)
   1.159 +    (* results *)
   1.160 +
   1.161 +    val type_insts3 = map (fn ((a, _), T) => (a, instT3 (instT2 T))) type_insts1;
   1.162 +    val term_insts3 = internal_insts3 @ external_insts3;
   1.163  
   1.164 -    val _ =
   1.165 +    val inst_tvars = map_filter (make_instT (instT3 o instT2 o instT1)) tvars;
   1.166 +    val inst_vars = map_filter (make_inst (inst3 o inst2)) vars3;
   1.167 +  in
   1.168 +    ((type_insts3, term_insts3),
   1.169 +      (map (pairself certT) inst_tvars, map (pairself cert) inst_vars))
   1.170 +  end;
   1.171 +
   1.172 +fun read_instantiate ctxt mixed_insts thm =
   1.173 +  let
   1.174 +    val ctxt' = ctxt |> Variable.declare_thm thm;
   1.175 +    val tvars = Drule.fold_terms Term.add_tvars thm [];
   1.176 +    val vars = Drule.fold_terms Term.add_vars thm [];
   1.177 +    val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars);
   1.178 +
   1.179 +    val _ = (*assign internalized values*)
   1.180        mixed_insts |> List.app (fn (arg, (xi, _)) =>
   1.181          if is_tvar xi then
   1.182 -          Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts''' xi)))) arg
   1.183 +          Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts xi)))) arg
   1.184          else
   1.185 -          Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts''' xi)))) arg);
   1.186 +          Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   1.187 +  in
   1.188 +    Drule.instantiate insts thm |> RuleCases.save thm
   1.189 +  end;
   1.190  
   1.191 -  in (context, thm''' |> RuleCases.save thm) end;
   1.192 +fun read_instantiate' ctxt (args, concl_args) thm =
   1.193 +  let
   1.194 +    fun zip_vars _ [] = []
   1.195 +      | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
   1.196 +      | zip_vars ((x, _) :: xs) ((arg, SOME t) :: rest) = (arg, (x, t)) :: zip_vars xs rest
   1.197 +      | zip_vars [] _ = error "More instantiations than variables in theorem";
   1.198 +    val insts =
   1.199 +      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
   1.200 +      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
   1.201 +  in read_instantiate ctxt insts thm end;
   1.202  
   1.203  end;
   1.204  
   1.205  
   1.206 +
   1.207 +(** attributes **)
   1.208 +
   1.209  (* where: named instantiation *)
   1.210  
   1.211  local
   1.212 @@ -147,26 +175,16 @@
   1.213  
   1.214  in
   1.215  
   1.216 -val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> read_instantiate);
   1.217 +val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args =>
   1.218 +  Thm.rule_attribute (fn context => read_instantiate (Context.proof_of context) args)));
   1.219  
   1.220  end;
   1.221  
   1.222  
   1.223 -(* of: positional instantiation (term arguments only) *)
   1.224 +(* of: positional instantiation (terms only) *)
   1.225  
   1.226  local
   1.227  
   1.228 -fun read_instantiate' (args, concl_args) (context, thm) =
   1.229 -  let
   1.230 -    fun zip_vars _ [] = []
   1.231 -      | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
   1.232 -      | zip_vars ((x, _) :: xs) ((arg, SOME t) :: rest) = (arg, (x, t)) :: zip_vars xs rest
   1.233 -      | zip_vars [] _ = error "More instantiations than variables in theorem";
   1.234 -    val insts =
   1.235 -      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
   1.236 -      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
   1.237 -  in read_instantiate insts (context, thm) end;
   1.238 -
   1.239  val value =
   1.240    Args.internal_term >> Args.Term ||
   1.241    Args.name >> Args.Name;
   1.242 @@ -180,7 +198,8 @@
   1.243  
   1.244  in
   1.245  
   1.246 -val of_att = Attrib.syntax (Scan.lift insts >> read_instantiate');
   1.247 +val of_att = Attrib.syntax (Scan.lift insts >> (fn args =>
   1.248 +  Thm.rule_attribute (fn context => read_instantiate' (Context.proof_of context) args)));
   1.249  
   1.250  end;
   1.251  
   1.252 @@ -189,7 +208,7 @@
   1.253  
   1.254  val _ = Context.add_setup (Attrib.add_attributes
   1.255   [("where", where_att, "named instantiation of theorem"),
   1.256 -  ("of", of_att, "rule applied to terms")]);
   1.257 +  ("of", of_att, "positional instantiation of theorem")]);
   1.258  
   1.259  
   1.260