src/Pure/tactic.ML
changeset 16425 2427be27cc60
parent 16325 a6431098a929
child 16666 9a987b59ecab
     1.1 --- a/src/Pure/tactic.ML	Fri Jun 17 18:33:05 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Fri Jun 17 18:33:08 2005 +0200
     1.3 @@ -111,15 +111,15 @@
     1.4    val simplify: bool -> thm list -> thm -> thm
     1.5    val conjunction_tac: tactic
     1.6    val smart_conjunction_tac: int -> tactic
     1.7 -  val prove_multi_plain: Sign.sg -> string list -> term list -> term list ->
     1.8 +  val prove_multi_plain: theory -> string list -> term list -> term list ->
     1.9      (thm list -> tactic) -> thm list
    1.10 -  val prove_multi: Sign.sg -> string list -> term list -> term list ->
    1.11 +  val prove_multi: theory -> string list -> term list -> term list ->
    1.12      (thm list -> tactic) -> thm list
    1.13 -  val prove_multi_standard: Sign.sg -> string list -> term list -> term list ->
    1.14 +  val prove_multi_standard: theory -> string list -> term list -> term list ->
    1.15      (thm list -> tactic) -> thm list
    1.16 -  val prove_plain: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.17 -  val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.18 -  val prove_standard: Sign.sg -> string list -> term list -> term ->
    1.19 +  val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.20 +  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.21 +  val prove_standard: theory -> string list -> term list -> term ->
    1.22      (thm list -> tactic) -> thm
    1.23    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
    1.24                            int -> tactic
    1.25 @@ -237,16 +237,16 @@
    1.26    let val (_, _, Bi, _) = dest_state(st,i)
    1.27        val params = Logic.strip_params Bi
    1.28    in rev(rename_wrt_term Bi params) end;
    1.29 -  
    1.30 +
    1.31  (*read instantiations with respect to subgoal i of proof state st*)
    1.32  fun read_insts_in_state (st, i, sinsts, rule) =
    1.33 -	let val {sign,...} = rep_thm st
    1.34 -	    and params = params_of_state st i
    1.35 -	    and rts = types_sorts rule and (types,sorts) = types_sorts st
    1.36 -	    fun types'(a,~1) = (case assoc(params,a) of NONE => types(a,~1) | sm => sm)
    1.37 -	      | types'(ixn) = types ixn;
    1.38 -	    val used = Drule.add_used rule (Drule.add_used st []);
    1.39 -	in read_insts sign rts (types',sorts) used sinsts end;
    1.40 +  let val thy = Thm.theory_of_thm st
    1.41 +      and params = params_of_state st i
    1.42 +      and rts = types_sorts rule and (types,sorts) = types_sorts st
    1.43 +      fun types'(a, ~1) = (case assoc_string (params, a) of NONE => types (a, ~1) | sm => sm)
    1.44 +        | types' ixn = types ixn;
    1.45 +      val used = Drule.add_used rule (Drule.add_used st []);
    1.46 +  in read_insts thy rts (types',sorts) used sinsts end;
    1.47  
    1.48  (*Lift and instantiate a rule wrt the given state and subgoal number *)
    1.49  fun lift_inst_rule' (st, i, sinsts, rule) =
    1.50 @@ -285,15 +285,15 @@
    1.51      i.e. Tinsts is not applied to insts.
    1.52  *)
    1.53  fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
    1.54 -let val {maxidx,sign,...} = rep_thm st
    1.55 +let val {maxidx,thy,...} = rep_thm st
    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*)
    1.60 -    fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
    1.61 +    fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
    1.62      fun liftTpair (((a, i), S), T) =
    1.63 -      (ctyp_of sign (TVar ((a, i + inc), S)),
    1.64 -       ctyp_of sign (incr_tvar inc T))
    1.65 +      (ctyp_of thy (TVar ((a, i + inc), S)),
    1.66 +       ctyp_of thy (incr_tvar inc T))
    1.67  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    1.68                       (lift_rule (st,i) rule)
    1.69  end;
    1.70 @@ -338,7 +338,7 @@
    1.71    increment revcut_rl instead.*)
    1.72  fun make_elim_preserve rl =
    1.73    let val {maxidx,...} = rep_thm rl
    1.74 -      fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT));
    1.75 +      fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
    1.76        val revcut_rl' =
    1.77            instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
    1.78                               (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
    1.79 @@ -596,11 +596,11 @@
    1.80  fun rename_params_tac xs i =
    1.81    case Library.find_first (not o Syntax.is_identifier) xs of
    1.82        SOME x => error ("Not an identifier: " ^ x)
    1.83 -    | NONE => 
    1.84 +    | NONE =>
    1.85         (if !Logic.auto_rename
    1.86 -	 then (warning "Resetting Logic.auto_rename";
    1.87 -	     Logic.auto_rename := false)
    1.88 -	else (); PRIMITIVE (rename_params_rule (xs, i)));
    1.89 +         then (warning "Resetting Logic.auto_rename";
    1.90 +             Logic.auto_rename := false)
    1.91 +        else (); PRIMITIVE (rename_params_rule (xs, i)));
    1.92  
    1.93  fun rename_tac str i =
    1.94    let val cs = Symbol.explode str in
    1.95 @@ -652,7 +652,7 @@
    1.96      (fn st =>
    1.97        compose_tac (false, Drule.incr_indexes_wrt [] [] [] [st] Drule.conj_intr_thm, 2) i st)
    1.98    | _ => no_tac);
    1.99 -  
   1.100 +
   1.101  val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
   1.102  
   1.103  fun smart_conjunction_tac 0 = assume_tac 1
   1.104 @@ -662,7 +662,7 @@
   1.105  
   1.106  (** minimal goal interface for programmed proofs *)
   1.107  
   1.108 -fun gen_prove_multi finish_thm sign xs asms props tac =
   1.109 +fun gen_prove_multi finish_thm thy xs asms props tac =
   1.110    let
   1.111      val prop = Logic.mk_conjunction_list props;
   1.112      val statement = Logic.list_implies (asms, prop);
   1.113 @@ -673,9 +673,9 @@
   1.114  
   1.115      fun err msg = raise ERROR_MESSAGE
   1.116        (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
   1.117 -        Sign.string_of_term sign (Term.list_all_free (params, statement)));
   1.118 +        Sign.string_of_term thy (Term.list_all_free (params, statement)));
   1.119  
   1.120 -    fun cert_safe t = Thm.cterm_of sign (Envir.beta_norm t)
   1.121 +    fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
   1.122        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
   1.123  
   1.124      val _ = cert_safe statement;
   1.125 @@ -696,8 +696,8 @@
   1.126  
   1.127      val raw_result = goal' RS Drule.rev_triv_goal;
   1.128      val prop' = prop_of raw_result;
   1.129 -    val _ = conditional (not (Pattern.matches (Sign.tsig_of sign) (prop, prop'))) (fn () =>
   1.130 -      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop'));
   1.131 +    val _ = conditional (not (Pattern.matches (Sign.tsig_of thy) (prop, prop'))) (fn () =>
   1.132 +      err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
   1.133    in
   1.134      Drule.conj_elim_precise (length props) raw_result
   1.135      |> map (fn res => res
   1.136 @@ -706,18 +706,18 @@
   1.137        |> finish_thm fixed_tfrees)
   1.138    end;
   1.139  
   1.140 -fun prove_multi_plain sign xs asms prop tac =
   1.141 -  gen_prove_multi (K norm_hhf_plain) sign xs asms prop tac;
   1.142 -fun prove_multi sign xs asms prop tac =
   1.143 +fun prove_multi_plain thy xs asms prop tac =
   1.144 +  gen_prove_multi (K norm_hhf_plain) thy xs asms prop tac;
   1.145 +fun prove_multi thy xs asms prop tac =
   1.146    gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o
   1.147        (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
   1.148 -    sign xs asms prop tac;
   1.149 -fun prove_multi_standard sign xs asms prop tac =
   1.150 -  map Drule.standard (prove_multi sign xs asms prop tac);
   1.151 +    thy xs asms prop tac;
   1.152 +fun prove_multi_standard thy xs asms prop tac =
   1.153 +  map Drule.standard (prove_multi thy xs asms prop tac);
   1.154  
   1.155 -fun prove_plain sign xs asms prop tac = hd (prove_multi_plain sign xs asms [prop] tac);
   1.156 -fun prove sign xs asms prop tac = hd (prove_multi sign xs asms [prop] tac);
   1.157 -fun prove_standard sign xs asms prop tac = Drule.standard (prove sign xs asms prop tac);
   1.158 +fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac);
   1.159 +fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
   1.160 +fun prove_standard thy xs asms prop tac = Drule.standard (prove thy xs asms prop tac);
   1.161  
   1.162  end;
   1.163