src/Pure/Isar/method.ML
changeset 14174 f3cafd2929d5
parent 13650 31bd2a8cdbe2
child 14215 ebf291f3b449
     1.1 --- a/src/Pure/Isar/method.ML	Fri Aug 29 13:18:45 2003 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Aug 29 15:19:02 2003 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4    val frule: int -> thm list -> Proof.method
     1.5    val this: Proof.method
     1.6    val assumption: Proof.context -> Proof.method
     1.7 -  val impose_hyps_tac: Proof.context -> tactic
     1.8 +  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list -> thm -> int -> tactic
     1.9    val set_tactic: (Proof.context -> thm list -> tactic) -> unit
    1.10    val tactic: string -> Proof.context -> Proof.method
    1.11    exception METHOD_FAIL of (string * Position.T) * exn
    1.12 @@ -111,6 +111,10 @@
    1.13      -> Args.src -> Proof.context -> Proof.method
    1.14    val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
    1.15      -> ('a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
    1.16 +  val goal_args_ctxt: (Args.T list -> 'a * Args.T list) -> (Proof.context -> 'a -> int -> tactic)
    1.17 +    -> Args.src -> Proof.context -> Proof.method
    1.18 +  val goal_args_ctxt': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
    1.19 +    -> (Proof.context -> 'a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
    1.20    val setup: (theory -> theory) list
    1.21  end;
    1.22  
    1.23 @@ -322,23 +326,149 @@
    1.24  
    1.25  (* res_inst_tac etc. *)
    1.26  
    1.27 -(*robustify instantiation by imposing (part of) the present static context*)
    1.28 -val impose_hyps_tac =
    1.29 -  PRIMITIVE o Drule.impose_hyps o flat o map #1 o ProofContext.assumptions_of;
    1.30 +(* Reimplemented to support both static (Isar) and dynamic (proof state)
    1.31 +   context.  By Clemens Ballarin. *)
    1.32  
    1.33 -(*Note: insts refer to the implicit (!!) goal context; use at your own risk*)
    1.34 -fun gen_res_inst _ tac _ (quant, ([], thms)) =
    1.35 -      METHOD (fn facts => (quant (insert_tac facts THEN' tac thms)))
    1.36 -  | gen_res_inst tac _ ctxt (quant, (insts, [thm])) =
    1.37 -      METHOD (fn facts => (impose_hyps_tac ctxt THEN quant (insert_tac facts THEN' tac insts thm)))
    1.38 -  | gen_res_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
    1.39 +fun bires_inst_tac bires_flag ctxt insts thm =
    1.40 +  let
    1.41 +    val sign = ProofContext.sign_of ctxt;
    1.42 +    (* Separate type and term insts *)
    1.43 +    fun has_type_var ((x, _), _) = (case Symbol.explode x of
    1.44 +          "'"::cs => true | cs => false);
    1.45 +    val Tinsts = filter has_type_var insts;
    1.46 +    val tinsts = filter_out has_type_var insts;
    1.47 +    (* Tactic *)
    1.48 +    fun tac i st =
    1.49 +      let
    1.50 +        (* Preprocess state: extract environment information:
    1.51 +           - variables and their types
    1.52 +           - type variables and their sorts
    1.53 +           - parameters and their types *)
    1.54 +        val (types, sorts) = types_sorts st;
    1.55 +    (* Process type insts: Tinsts_env *)
    1.56 +    fun absent xi = error
    1.57 +	  ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
    1.58 +    val (rtypes, rsorts) = types_sorts thm;
    1.59 +    fun readT (xi, s) =
    1.60 +        let val S = case rsorts xi of Some S => S | None => absent xi;
    1.61 +            val T = Sign.read_typ (sign, sorts) s;
    1.62 +        in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T)
    1.63 +           else error
    1.64 +             ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
    1.65 +        end;
    1.66 +    val Tinsts_env = map readT Tinsts;
    1.67 +    (* Preprocess rule: extract vars and their types, apply Tinsts *)
    1.68 +    fun get_typ xi =
    1.69 +      (case rtypes xi of
    1.70 +           Some T => typ_subst_TVars Tinsts_env T
    1.71 +         | None => absent xi);
    1.72 +    val (xis, ss) = Library.split_list tinsts;
    1.73 +    val Ts = map get_typ xis;
    1.74 +	val (_, _, Bi, _) = dest_state(st,i)
    1.75 +	val params = Logic.strip_params Bi
    1.76 +			     (* params of subgoal i as string typ pairs *)
    1.77 +	val params = rev(Term.rename_wrt_term Bi params)
    1.78 +						 (* as they are printed *)
    1.79 +        fun types' (a, ~1) = (case assoc (params, a) of
    1.80 +                None => types (a, ~1)
    1.81 +              | some => some)
    1.82 +          | types' xi = types xi;
    1.83 +        val used = add_term_tvarnames
    1.84 +                  (prop_of st $ prop_of thm,[])
    1.85 +	val (ts, envT) =
    1.86 +	  ProofContext.read_termTs_env (types', sorts, used) ctxt (ss ~~ Ts);
    1.87 +	val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env);
    1.88 +	val cenv =
    1.89 +	  map
    1.90 +	    (fn (xi, t) =>
    1.91 +	      pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
    1.92 +	    (gen_distinct
    1.93 +	      (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
    1.94 +	      (xis ~~ ts));
    1.95 +	(* Lift and instantiate rule *)
    1.96 +	val {maxidx, ...} = rep_thm st;
    1.97 +	val paramTs = map #2 params
    1.98 +	and inc = maxidx+1
    1.99 +	fun liftvar (Var ((a,j), T)) =
   1.100 +	      Var((a, j+inc), paramTs ---> incr_tvar inc T)
   1.101 +	  | liftvar t = raise TERM("Variable expected", [t]);
   1.102 +	fun liftterm t = list_abs_free
   1.103 +	      (params, Logic.incr_indexes(paramTs,inc) t)
   1.104 +	fun liftpair (cv,ct) =
   1.105 +	      (cterm_fun liftvar cv, cterm_fun liftterm ct)
   1.106 +	fun lifttvar((a,i),ctyp) =
   1.107 +	    let val {T,sign} = rep_ctyp ctyp
   1.108 +	    in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
   1.109 +	val rule = Drule.instantiate
   1.110 +	      (map lifttvar cenvT, map liftpair cenv)
   1.111 +	      (lift_rule (st, i) thm)
   1.112 +      in
   1.113 +	if i > nprems_of st then no_tac st
   1.114 +	else st |>
   1.115 +	  compose_tac (bires_flag, rule, nprems_of thm) i
   1.116 +      end
   1.117 +	   handle TERM (msg,_)   => (warning msg; no_tac st)
   1.118 +		| THM  (msg,_,_) => (warning msg; no_tac st);
   1.119 +  in
   1.120 +    tac
   1.121 +  end;
   1.122  
   1.123 -val res_inst = gen_res_inst Tactic.res_inst_tac Tactic.resolve_tac;
   1.124 -val eres_inst = gen_res_inst Tactic.eres_inst_tac Tactic.eresolve_tac;
   1.125 -val dres_inst = gen_res_inst Tactic.dres_inst_tac Tactic.dresolve_tac;
   1.126 -val forw_inst = gen_res_inst Tactic.forw_inst_tac Tactic.forward_tac;
   1.127 -val cut_inst = gen_res_inst Tactic.cut_inst_tac Tactic.cut_rules_tac;
   1.128 +fun gen_inst _ tac _ (quant, ([], thms)) =
   1.129 +      METHOD (fn facts => quant (insert_tac facts THEN' tac thms))
   1.130 +  | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
   1.131 +      METHOD (fn facts =>
   1.132 +        quant (insert_tac facts THEN' inst_tac ctxt insts thm))
   1.133 +  | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
   1.134 +      
   1.135 +val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
   1.136 +
   1.137 +val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac;
   1.138 +
   1.139 +(* Preserve Var indexes of rl; increment revcut_rl instead.
   1.140 +   Copied from tactic.ML *)
   1.141 +fun make_elim_preserve rl =
   1.142 +  let val {maxidx,...} = rep_thm rl
   1.143 +      fun cvar xi = cterm_of (Theory.sign_of ProtoPure.thy) (Var(xi,propT));
   1.144 +      val revcut_rl' =
   1.145 +          instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   1.146 +                             (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   1.147 +      val arg = (false, rl, nprems_of rl)
   1.148 +      val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   1.149 +  in  th  end
   1.150 +  handle Bind => raise THM("make_elim_preserve", 1, [rl]);
   1.151  
   1.152 +val cut_inst_meth =
   1.153 +  gen_inst
   1.154 +    (fn ctxt => fn insts => fn thm =>
   1.155 +       bires_inst_tac false ctxt insts (make_elim_preserve thm))
   1.156 +    Tactic.cut_rules_tac;
   1.157 +
   1.158 +val dres_inst_meth =
   1.159 +  gen_inst
   1.160 +    (fn ctxt => fn insts => fn rule =>
   1.161 +       bires_inst_tac true ctxt insts (make_elim_preserve rule))
   1.162 +    Tactic.dresolve_tac;
   1.163 +
   1.164 +val forw_inst_meth =
   1.165 +  gen_inst
   1.166 +    (fn ctxt => fn insts => fn rule =>
   1.167 +       bires_inst_tac false ctxt insts (make_elim_preserve rule) THEN'
   1.168 +       assume_tac)
   1.169 +    Tactic.forward_tac;
   1.170 +
   1.171 +fun subgoal_tac ctxt sprop =
   1.172 +  DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl THEN'
   1.173 +  SUBGOAL (fn (prop, _) =>
   1.174 +    let val concl' = Logic.strip_assums_concl prop in
   1.175 +      if null (term_tvars concl') then ()
   1.176 +      else warning "Type variables in new subgoal: add a type constraint?";
   1.177 +      all_tac
   1.178 +  end);
   1.179 +
   1.180 +fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
   1.181 +
   1.182 +fun thin_tac ctxt s =
   1.183 +  bires_inst_tac true ctxt [(("V", 0), s)] thin_rl;
   1.184  
   1.185  (* simple Prolog interpreter *)
   1.186  
   1.187 @@ -536,13 +666,23 @@
   1.188  
   1.189  fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
   1.190  
   1.191 +val insts_var =
   1.192 +  Scan.optional
   1.193 +    (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   1.194 +      Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss;
   1.195 +
   1.196 +fun inst_args_var f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
   1.197  
   1.198  fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
   1.199 -  (fn (quant, s) => SIMPLE_METHOD' quant (K (impose_hyps_tac ctxt) THEN' tac s))) src ctxt);
   1.200 +  (fn (quant, s) => SIMPLE_METHOD' quant ( (*K (impose_hyps_tac ctxt) THEN' *) tac s))) src ctxt);
   1.201  
   1.202  fun goal_args args tac = goal_args' (Scan.lift args) tac;
   1.203  
   1.204 +fun goal_args_ctxt' args tac src ctxt =
   1.205 +  #2 (syntax (Args.goal_spec HEADGOAL -- args >>
   1.206 +  (fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt);
   1.207  
   1.208 +fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
   1.209  
   1.210  (** method text **)
   1.211  
   1.212 @@ -629,8 +769,8 @@
   1.213  
   1.214  (* misc tactic emulations *)
   1.215  
   1.216 -val subgoal_meth = goal_args (Scan.repeat1 Args.name) Tactic.subgoals_tac;
   1.217 -val thin_meth = goal_args Args.name Tactic.thin_tac;
   1.218 +val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac;
   1.219 +val thin_meth = goal_args_ctxt Args.name thin_tac;
   1.220  val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac;
   1.221  val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac;
   1.222  
   1.223 @@ -655,14 +795,14 @@
   1.224    ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
   1.225    ("this", no_args this, "apply current facts as rules"),
   1.226    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
   1.227 -  ("rule_tac", inst_args res_inst, "apply rule (dynamic instantiation!)"),
   1.228 -  ("erule_tac", inst_args eres_inst, "apply rule in elimination manner (dynamic instantiation!)"),
   1.229 -  ("drule_tac", inst_args dres_inst, "apply rule in destruct manner (dynamic instantiation!)"),
   1.230 -  ("frule_tac", inst_args forw_inst, "apply rule in forward manner (dynamic instantiation!)"),
   1.231 -  ("cut_tac", inst_args cut_inst, "cut rule (dynamic instantiation!)"),
   1.232 -  ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation!)"),
   1.233 -  ("thin_tac", thin_meth, "remove premise (dynamic instantiation!)"),
   1.234 -  ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation!)"),
   1.235 +  ("rule_tac", inst_args_var res_inst_meth, "apply rule (dynamic instantiation)"),
   1.236 +  ("erule_tac", inst_args_var eres_inst_meth, "apply rule in elimination manner (dynamic instantiation)"),
   1.237 +  ("drule_tac", inst_args_var dres_inst_meth, "apply rule in destruct manner (dynamic instantiation)"),
   1.238 +  ("frule_tac", inst_args_var forw_inst_meth, "apply rule in forward manner (dynamic instantiation)"),
   1.239 +  ("cut_tac", inst_args_var cut_inst_meth, "cut rule (dynamic instantiation)"),
   1.240 +  ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation)"),
   1.241 +  ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"),
   1.242 +  ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"),
   1.243    ("rotate_tac", rotate_meth, "rotate assumptions of goal"),
   1.244    ("prolog", thms_args prolog, "simple prolog interpreter"),
   1.245    ("tactic", simple_args Args.name tactic, "ML tactic as proof method")];