author wenzelm Sat Aug 05 14:52:58 2006 +0200 (2006-08-05 ago) changeset 20343 e093a54bf25e parent 20342 4392003fcbfa child 20344 d02b43ea722e
```     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.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.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.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