src/Pure/Tools/rule_insts.ML
changeset 59825 9fb7661651ad
parent 59805 a162f779925a
child 59827 04e569577c18
equal deleted inserted replaced
59819:dbec7f33093d 59825:9fb7661651ad
    12   val of_rule: Proof.context -> string option list * string option list ->
    12   val of_rule: Proof.context -> string option list * string option list ->
    13     (binding * string option * mixfix) list -> thm -> thm
    13     (binding * string option * mixfix) list -> thm -> thm
    14   val read_instantiate: Proof.context ->
    14   val read_instantiate: Proof.context ->
    15     ((indexname * Position.T) * string) list -> string list -> thm -> thm
    15     ((indexname * Position.T) * string) list -> string list -> thm -> thm
    16   val schematic: bool Config.T
    16   val schematic: bool Config.T
       
    17   val goal_context: int -> thm -> Proof.context -> (string * typ) list * Proof.context
    17   val res_inst_tac: Proof.context ->
    18   val res_inst_tac: Proof.context ->
    18     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
    19     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
    19     int -> tactic
    20     int -> tactic
    20   val eres_inst_tac: Proof.context ->
    21   val eres_inst_tac: Proof.context ->
    21     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
    22     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
    99 fun read_insts thm mixed_insts ctxt =
   100 fun read_insts thm mixed_insts ctxt =
   100   let
   101   let
   101     val (type_insts, term_insts) =
   102     val (type_insts, term_insts) =
   102       List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) mixed_insts;
   103       List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) mixed_insts;
   103 
   104 
       
   105     (*thm context*)
       
   106     val ctxt1 = Variable.declare_thm thm ctxt;
   104     val tvars = Thm.fold_terms Term.add_tvars thm [];
   107     val tvars = Thm.fold_terms Term.add_tvars thm [];
   105     val vars = Thm.fold_terms Term.add_vars thm [];
   108     val vars = Thm.fold_terms Term.add_vars thm [];
   106 
   109 
   107     (*explicit type instantiations*)
   110     (*explicit type instantiations*)
   108     val instT1 = Term_Subst.instantiateT (map (read_type ctxt tvars) type_insts);
   111     val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);
   109     val vars1 = map (apsnd instT1) vars;
   112     val vars1 = map (apsnd instT1) vars;
   110 
   113 
   111     (*term instantiations*)
   114     (*term instantiations*)
   112     val (xs, ss) = split_list term_insts;
   115     val (xs, ss) = split_list term_insts;
   113     val Ts = map (the_type vars1) xs;
   116     val Ts = map (the_type vars1) xs;
   114     val ((ts, inferred), ctxt') = read_terms ss Ts ctxt;
   117     val ((ts, inferred), ctxt2) = read_terms ss Ts ctxt1;
   115 
   118 
   116     (*implicit type instantiations*)
   119     (*implicit type instantiations*)
   117     val instT2 = Term_Subst.instantiateT inferred;
   120     val instT2 = Term_Subst.instantiateT inferred;
   118     val vars2 = map (apsnd instT2) vars1;
   121     val vars2 = map (apsnd instT2) vars1;
   119     val inst2 =
   122     val inst2 =
   120       Term_Subst.instantiate ([], map2 (fn (xi, _) => fn t => ((xi, Term.fastype_of t), t)) xs ts)
   123       Term_Subst.instantiate ([], map2 (fn (xi, _) => fn t => ((xi, Term.fastype_of t), t)) xs ts)
   121       #> Envir.beta_norm;
   124       #> Envir.beta_norm;
   122 
   125 
   123     val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
   126     val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
   124     val inst_vars = map_filter (make_inst inst2) vars2;
   127     val inst_vars = map_filter (make_inst inst2) vars2;
   125   in ((inst_tvars, inst_vars), ctxt') end;
   128   in ((inst_tvars, inst_vars), ctxt2) end;
   126 
   129 
   127 end;
   130 end;
   128 
   131 
   129 
   132 
   130 
   133 
   131 (** forward rules **)
   134 (** forward rules **)
   132 
   135 
   133 fun where_rule ctxt mixed_insts fixes thm =
   136 fun where_rule ctxt mixed_insts fixes thm =
   134   let
   137   let
   135     val ctxt' = ctxt
   138     val ctxt' = ctxt |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
   136       |> Variable.declare_thm thm
       
   137       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
       
   138     val ((inst_tvars, inst_vars), ctxt'') = read_insts thm mixed_insts ctxt';
   139     val ((inst_tvars, inst_vars), ctxt'') = read_insts thm mixed_insts ctxt';
   139   in
   140   in
   140     thm
   141     thm
   141     |> Drule.instantiate_normalize
   142     |> Drule.instantiate_normalize
   142       (map (apply2 (Thm.ctyp_of ctxt'') o apfst TVar) inst_tvars,
   143       (map (apply2 (Thm.ctyp_of ctxt'') o apfst TVar) inst_tvars,
   197 
   198 
   198 
   199 
   199 
   200 
   200 (** tactics **)
   201 (** tactics **)
   201 
   202 
       
   203 (* goal context *)
       
   204 
   202 val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
   205 val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
   203 
   206 
   204 (* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
   207 fun goal_context i st ctxt =
   205 
   208   let
   206 fun bires_inst_tac bires_flag ctxt mixed_insts fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
   209     val goal = Thm.term_of (Thm.cprem_of st i);
   207   let
       
   208     (* goal parameters *)
       
   209 
       
   210     val goal = Thm.term_of cgoal;
       
   211     val params =
   210     val params =
   212       Logic.strip_params goal
   211       Logic.strip_params goal
   213       (*as they are printed: bound variables with the same name are renamed*)
   212       (*as they are printed: bound variables with the same name are renamed*)
   214       |> Term.rename_wrt_term goal
   213       |> Term.rename_wrt_term goal
   215       |> rev;
   214       |> rev;
   216     val (param_names, param_ctxt) = ctxt
   215     val (param_names, param_ctxt) = ctxt
   217       |> Variable.declare_thm thm
       
   218       |> Thm.fold_terms Variable.declare_constraints st
   216       |> Thm.fold_terms Variable.declare_constraints st
   219       |> Variable.improper_fixes
   217       |> Variable.improper_fixes
   220       |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params)
   218       |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params)
   221       ||> Variable.restore_proper_fixes ctxt
   219       ||> Variable.restore_proper_fixes ctxt
   222       ||> Config.get ctxt schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
   220       ||> Config.get ctxt schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
   223     val paramTs = map #2 params;
   221     val paramTs = map #2 params;
       
   222   in (param_names ~~ paramTs, param_ctxt) end;
       
   223 
       
   224 
       
   225 (* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
       
   226 
       
   227 fun bires_inst_tac bires_flag ctxt mixed_insts fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
       
   228   let
       
   229     (* goal context *)
       
   230 
       
   231     val (params, param_ctxt) = goal_context i st ctxt;
       
   232     val paramTs = map #2 params;
   224 
   233 
   225 
   234 
   226     (* local fixes *)
   235     (* local fixes *)
   227 
   236 
   228     val fixes_ctxt = param_ctxt
   237     val fixes_ctxt = param_ctxt
   238 
   247 
   239 
   248 
   240     (* lift and instantiate rule *)
   249     (* lift and instantiate rule *)
   241 
   250 
   242     val inc = Thm.maxidx_of st + 1;
   251     val inc = Thm.maxidx_of st + 1;
   243     fun lift_var ((a, j), T) =
   252     val lift_type = Logic.incr_tvar inc;
   244       Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T);
   253     fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T);
   245     fun lift_term t =
   254     fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t);
   246       fold_rev Term.absfree (param_names ~~ paramTs)
       
   247         (Logic.incr_indexes (fixed, paramTs, inc) t);
       
   248 
   255 
   249     val inst_tvars' = inst_tvars
   256     val inst_tvars' = inst_tvars
   250       |> map (apply2 (Thm.ctyp_of inst_ctxt o Logic.incr_tvar inc) o apfst TVar);
   257       |> map (apply2 (Thm.ctyp_of inst_ctxt o lift_type) o apfst TVar);
   251     val inst_vars' = inst_vars
   258     val inst_vars' = inst_vars
   252       |> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t));
   259       |> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t));
   253 
   260 
   254     val thm' =
   261     val thm' = Thm.lift_rule cgoal thm
   255       Drule.instantiate_normalize (inst_tvars', inst_vars')
   262       |> Drule.instantiate_normalize (inst_tvars', inst_vars')
   256         (Thm.lift_rule cgoal thm)
       
   257       |> singleton (Variable.export inst_ctxt param_ctxt);
   263       |> singleton (Variable.export inst_ctxt param_ctxt);
   258   in
   264   in
   259     compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i
   265     compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i
   260   end) i st;
   266   end) i st;
   261 
   267