some rationalizing of res_inst_tac
authorpaulson
Mon Jan 24 12:40:52 2005 +0100 (2005-01-24)
changeset 154536318e634e6cc
parent 15452 e2a721567f67
child 15454 4b339d3907a0
some rationalizing of res_inst_tac
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Fri Jan 21 18:00:18 2005 +0100
     1.2 +++ b/src/Pure/tactic.ML	Mon Jan 24 12:40:52 2005 +0100
     1.3 @@ -215,12 +215,28 @@
     1.4    let val (_, _, Bi, _) = dest_state (st, i)
     1.5    in rename_wrt_term Bi (Logic.strip_params Bi) end;
     1.6  
     1.7 +(*params of subgoal i as they are printed*)
     1.8 +fun params_of_state st i =
     1.9 +  let val (_, _, Bi, _) = dest_state(st,i)
    1.10 +      val params = Logic.strip_params Bi
    1.11 +  in rev(rename_wrt_term Bi params) end;
    1.12 +  
    1.13 +(*read instantiations with respect to subgoal i of proof state st*)
    1.14 +fun read_insts_in_state (st, i, sinsts, rule) =
    1.15 +	let val {sign,...} = rep_thm st
    1.16 +	    and params = params_of_state st i
    1.17 +	    and rts = types_sorts rule and (types,sorts) = types_sorts st
    1.18 +	    fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
    1.19 +	      | types'(ixn) = types ixn;
    1.20 +	    val used = add_term_tvarnames
    1.21 +	                  (prop_of st $ prop_of rule,[])
    1.22 +	in read_insts sign rts (types',sorts) used sinsts end;
    1.23 +
    1.24  (*Lift and instantiate a rule wrt the given state and subgoal number *)
    1.25  fun lift_inst_rule' (st, i, sinsts, rule) =
    1.26 -let val {maxidx,sign,...} = rep_thm st
    1.27 -    val (_, _, Bi, _) = dest_state(st,i)
    1.28 -    val params = Logic.strip_params Bi          (*params of subgoal i*)
    1.29 -    val params = rev(rename_wrt_term Bi params) (*as they are printed*)
    1.30 +let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule)
    1.31 +    and {maxidx,...} = rep_thm st
    1.32 +    and params = params_of_state st i
    1.33      val paramTs = map #2 params
    1.34      and inc = maxidx+1
    1.35      fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
    1.36 @@ -232,12 +248,6 @@
    1.37      fun lifttvar((a,i),ctyp) =
    1.38          let val {T,sign} = rep_ctyp ctyp
    1.39          in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
    1.40 -    val rts = types_sorts rule and (types,sorts) = types_sorts st
    1.41 -    fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
    1.42 -      | types'(ixn) = types ixn;
    1.43 -    val used = add_term_tvarnames
    1.44 -                  (prop_of st $ prop_of rule,[])
    1.45 -    val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
    1.46  in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
    1.47                       (lift_rule (st,i) rule)
    1.48  end;
    1.49 @@ -262,9 +272,7 @@
    1.50  *)
    1.51  fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
    1.52  let val {maxidx,sign,...} = rep_thm st
    1.53 -    val (_, _, Bi, _) = dest_state(st,i)
    1.54 -    val params = Logic.strip_params Bi          (*params of subgoal i*)
    1.55 -    val paramTs = map #2 params
    1.56 +    val paramTs = map #2 (params_of_state st i)
    1.57      and inc = maxidx+1
    1.58      fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
    1.59      (*lift only Var, not term, which must be lifted already*)