src/Pure/Isar/obtain.ML
changeset 17111 d2ea9c974570
parent 17034 b4d9b87c102e
child 17357 ee2bdca144c7
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Aug 18 11:17:45 2005 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Aug 18 11:17:46 2005 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  signature OBTAIN =
     1.5  sig
     1.6    val obtain: (string list * string option) list ->
     1.7 -    ((string * Proof.context attribute list) * (string * (string list * string list)) list) list
     1.8 +    ((string * Attrib.src list) * (string * (string list * string list)) list) list
     1.9      -> (Proof.context -> string * (string * thm list) list -> unit) *
    1.10        (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    1.11    val obtain_i: (string list * typ option) list ->
    1.12 @@ -37,8 +37,8 @@
    1.13  
    1.14  fun export_obtain state parms rule _ cprops thm =
    1.15    let
    1.16 -    val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    1.17 -    val cparms = map (Thm.cterm_of sign) parms;
    1.18 +    val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
    1.19 +    val cparms = map (Thm.cterm_of thy) parms;
    1.20  
    1.21      val thm' = thm
    1.22        |> Drule.implies_intr_goals cprops
    1.23 @@ -52,7 +52,7 @@
    1.24      if not (null bads) then
    1.25        raise Proof.STATE ("Conclusion contains obtained parameters: " ^
    1.26          space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
    1.27 -    else if not (ObjectLogic.is_judgment sign (Logic.strip_assums_concl prop)) then
    1.28 +    else if not (ObjectLogic.is_judgment thy (Logic.strip_assums_concl prop)) then
    1.29        raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
    1.30      else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    1.31    end;
    1.32 @@ -63,12 +63,11 @@
    1.33  
    1.34  val thatN = "that";
    1.35  
    1.36 -fun gen_obtain prep_vars prep_propp raw_vars raw_asms print state =
    1.37 +fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms print state =
    1.38    let
    1.39      val _ = Proof.assert_forward_or_chain state;
    1.40      val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    1.41      val thy = Proof.theory_of state;
    1.42 -    val sign = Theory.sign_of thy;
    1.43  
    1.44      (*obtain vars*)
    1.45      val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars);
    1.46 @@ -78,14 +77,14 @@
    1.47      (*obtain asms*)
    1.48      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    1.49      val asm_props = List.concat (map (map fst) proppss);
    1.50 -    val asms = map fst raw_asms ~~ proppss;
    1.51 +    val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
    1.52  
    1.53      val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
    1.54  
    1.55      (*obtain statements*)
    1.56      val thesisN = Term.variant xs AutoBind.thesisN;
    1.57      val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN];
    1.58 -    val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment sign thesisN);
    1.59 +    val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment thy thesisN);
    1.60      val bound_thesis_raw as (bound_thesis_name, _) =
    1.61        Term.dest_Free (bind_thesis (Free (thesisN, propT)));
    1.62      val bound_thesis_var =
    1.63 @@ -106,25 +105,25 @@
    1.64        Logic.list_rename_params ([AutoBind.thesisN],
    1.65          Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
    1.66  
    1.67 -    fun after_qed _ st = st
    1.68 -      |> Method.local_qed false NONE print
    1.69 -      |> Seq.map (fn st' => st'
    1.70 +    fun after_qed _ =
    1.71 +      Proof.local_qed false NONE print
    1.72 +      #> Seq.map (fn st => st
    1.73          |> Proof.fix_i vars
    1.74 -        |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
    1.75 +        |> Proof.assm_i (export_obtain state parms (Proof.the_fact st)) asms);
    1.76    in
    1.77      state
    1.78      |> Proof.enter_forward
    1.79      |> Proof.have_i (K Seq.single) true [(("", []), [(obtain_prop, ([], []))])]
    1.80 -    |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
    1.81 +    |> Proof.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
    1.82      |> Proof.fix_i [([thesisN], NONE)]
    1.83      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
    1.84      |> `Proof.the_facts
    1.85      ||> Proof.from_facts chain_facts
    1.86      ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
    1.87 -    |-> (fn facts => Method.refine (Method.Basic (K (Method.insert facts))))
    1.88 +    |-> (fn facts => Proof.refine (Method.Basic (K (Method.insert facts))))
    1.89    end;
    1.90  
    1.91 -val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
    1.92 -val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp;
    1.93 +val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;
    1.94 +val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
    1.95  
    1.96  end;