src/Pure/Isar/proof.ML
changeset 16450 66667013ca6e
parent 16169 b59202511b8a
child 16539 60adb8b28377
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Jun 17 18:33:34 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Jun 17 18:33:35 2005 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    val init_state: theory -> state
     1.5    val context_of: state -> context
     1.6    val theory_of: state -> theory
     1.7 -  val sign_of: state -> Sign.sg
     1.8 +  val sign_of: state -> theory    (*obsolete*)
     1.9    val map_context: (context -> context) -> state -> state
    1.10    val warn_extra_tfrees: state -> state -> state
    1.11    val put_thms: string * thm list -> state -> state
    1.12 @@ -49,8 +49,7 @@
    1.13    val level: state -> int
    1.14    type method
    1.15    val method: (thm list -> tactic) -> method
    1.16 -  val method_cases:
    1.17 -    (thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq) -> method
    1.18 +  val method_cases: (thm list -> RuleCases.tactic) -> method
    1.19    val refine: (context -> method) -> state -> state Seq.seq
    1.20    val refine_end: (context -> method) -> state -> state Seq.seq
    1.21    val match_bind: (string list * string) list -> state -> state
    1.22 @@ -154,9 +153,9 @@
    1.23  
    1.24  fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _),
    1.25          locale_spec = NONE, ...}) = s ^ (if a = "" then "" else " " ^ a)
    1.26 -  | kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _),
    1.27 +  | kind_name thy (Theorem {kind = s, theory_spec = ((a, _), _),
    1.28          locale_spec = SOME (name, _), ...}) =
    1.29 -      s ^ " (in " ^ Locale.extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
    1.30 +      s ^ " (in " ^ Locale.extern thy name ^ ")" ^ (if a = "" then "" else " " ^ a)
    1.31    | kind_name _ (Show _) = "show"
    1.32    | kind_name _ (Have _) = "have";
    1.33  
    1.34 @@ -218,7 +217,7 @@
    1.35  
    1.36  fun context_of (State (Node {context, ...}, _)) = context;
    1.37  val theory_of = ProofContext.theory_of o context_of;
    1.38 -val sign_of = ProofContext.sign_of o context_of;
    1.39 +val sign_of = theory_of;
    1.40  
    1.41  fun map_context f = map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
    1.42  
    1.43 @@ -412,7 +411,7 @@
    1.44      fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
    1.45        pretty_facts "using " ctxt
    1.46          (if mode <> Backward orelse null goal_facts then NONE else SOME goal_facts) @
    1.47 -      [Pretty.str ("goal (" ^ kind_name (sign_of state) kind ^ prt_names names ^
    1.48 +      [Pretty.str ("goal (" ^ kind_name (theory_of state) kind ^ prt_names names ^
    1.49            levels_up (i div 2) ^ subgoals (Thm.nprems_of thm) ^ "):")] @
    1.50        pretty_goals_local ctxt begin_goal (true, ! show_main_goal) (! Display.goals_limit) thm;
    1.51  
    1.52 @@ -442,8 +441,7 @@
    1.53  
    1.54  (* datatype method *)
    1.55  
    1.56 -datatype method =
    1.57 -  Method of thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq;
    1.58 +datatype method = Method of thm list -> RuleCases.tactic;
    1.59  
    1.60  fun method tac = Method (fn facts => fn st => Seq.map (rpair []) (tac facts st));
    1.61  val method_cases = Method;
    1.62 @@ -459,11 +457,11 @@
    1.63  fun no_goal_cases st = map (rpair NONE) (goals st);
    1.64  
    1.65  fun goal_cases st =
    1.66 -  RuleCases.make true NONE (Thm.sign_of_thm st, Thm.prop_of st) (goals st);
    1.67 +  RuleCases.make true NONE (Thm.theory_of_thm st, Thm.prop_of st) (goals st);
    1.68  
    1.69 -fun check_sign sg state =
    1.70 -  if Sign.subsig (sg, sign_of state) then state
    1.71 -  else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
    1.72 +fun check_theory thy state =
    1.73 +  if subthy (thy, theory_of state) then state
    1.74 +  else raise STATE ("Bad theory of method result: " ^ Context.str_of_thy thy, state);
    1.75  
    1.76  fun gen_refine current_context meth_fun state =
    1.77    let
    1.78 @@ -472,7 +470,7 @@
    1.79    in
    1.80      meth facts st |> Seq.map (fn (st', meth_cases) =>
    1.81        state
    1.82 -      |> check_sign (Thm.sign_of_thm st')
    1.83 +      |> check_theory (Thm.theory_of_thm st')
    1.84        |> map_goal
    1.85            (ProofContext.add_cases (no_goal_cases st @ goal_cases st' @ meth_cases))
    1.86            (K ((result, (facts, st')), x)))
    1.87 @@ -541,8 +539,8 @@
    1.88          (pretty_goals_local ctxt "" (true, !show_main_goal) (! Display.goals_limit) raw_th @
    1.89            [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
    1.90  
    1.91 -    val {hyps, sign, ...} = Thm.rep_thm raw_th;
    1.92 -    val tsig = Sign.tsig_of sign;
    1.93 +    val {hyps, thy, ...} = Thm.rep_thm raw_th;
    1.94 +    val tsig = Sign.tsig_of thy;
    1.95      val casms = List.concat (map #1 (ProofContext.assumptions_of (context_of state)));
    1.96      val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
    1.97  
    1.98 @@ -735,13 +733,13 @@
    1.99        |> enter_forward
   1.100        |> opt_block
   1.101        |> map_context_result (fn ctxt => prepp (ctxt, raw_propp));
   1.102 -    val sign' = sign_of state';
   1.103 +    val thy' = theory_of state';
   1.104  
   1.105      val AfterQed (after_local, after_global) = after_qed;
   1.106      val after_qed' = AfterQed (after_local o map_context gen_binds, after_global);
   1.107  
   1.108      val props = List.concat propss;
   1.109 -    val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props);
   1.110 +    val cprop = Thm.cterm_of thy' (Logic.mk_conjunction_list props);
   1.111      val goal = Drule.mk_triv_goal cprop;
   1.112  
   1.113      val tvars = foldr Term.add_term_tvars [] props;
   1.114 @@ -758,7 +756,7 @@
   1.115      |> put_goal (SOME (((kind, names, propss), ([], goal)), (after_qed', pr)))
   1.116      |> map_context (ProofContext.add_cases
   1.117       (if length props = 1 then
   1.118 -      RuleCases.make true NONE (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
   1.119 +      RuleCases.make true NONE (Thm.theory_of_thm goal, Thm.prop_of goal) [rule_contextN]
   1.120        else [(rule_contextN, NONE)]))
   1.121      |> auto_bind_goal props
   1.122      |> (if is_chain state then use_facts else reset_facts)
   1.123 @@ -863,7 +861,7 @@
   1.124        | _ => err_malformed "finish_local" state);
   1.125    in
   1.126      conditional pr (fn () => print_result goal_ctxt
   1.127 -      (kind_name (sign_of state) kind, names ~~ Library.unflat tss results));
   1.128 +      (kind_name (theory_of state) kind, names ~~ Library.unflat tss results));
   1.129      outer_state
   1.130      |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts)
   1.131      |> (fn st => Seq.map (fn res =>