improved handling of "that": insert into goal, only declare as Pure "intro";
authorwenzelm
Fri Nov 03 21:27:06 2000 +0100 (2000-11-03)
changeset 1037993630e0c5ae9
parent 10378 98c95ebf804f
child 10380 e5370304d893
improved handling of "that": insert into goal, only declare as Pure "intro";
eliminated functor;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Fri Nov 03 21:26:11 2000 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Fri Nov 03 21:27:06 2000 +0100
     1.3 @@ -12,18 +12,12 @@
     1.4    {
     1.5      fix thesis
     1.6      assume that: "!!x. P x ==> thesis"
     1.7 -    <chain_facts> have thesis <proof>
     1.8 +    <chain_facts> have thesis <proof (insert that)>
     1.9    }
    1.10 -  fix x assm(obtained) "P x"
    1.11 +  fix x assm (obtained) "P x"
    1.12  
    1.13  *)
    1.14  
    1.15 -signature OBTAIN_DATA =
    1.16 -sig
    1.17 -  val atomic_thesis: string -> term
    1.18 -  val that_atts: Proof.context attribute list
    1.19 -end;
    1.20 -
    1.21  signature OBTAIN =
    1.22  sig
    1.23    val obtain: ((string list * string option) * Comment.text) list
    1.24 @@ -34,7 +28,7 @@
    1.25        * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.26  end;
    1.27  
    1.28 -functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
    1.29 +structure Obtain: OBTAIN =
    1.30  struct
    1.31  
    1.32  
    1.33 @@ -58,7 +52,7 @@
    1.34        raise Proof.STATE ("Conclusion contains obtained parameters: " ^
    1.35          space_implode " " (map (Sign.string_of_term sign) bads), state)
    1.36      else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
    1.37 -      raise Proof.STATE ("Conclusion is not an object-logic judgment", state)
    1.38 +      raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
    1.39      else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    1.40    end;
    1.41  
    1.42 @@ -102,7 +96,7 @@
    1.43      val xs' = mapfilter occs_var xs;
    1.44      val parms = map (bind_skolem o Free) xs';
    1.45  
    1.46 -    val bound_thesis = bind_skolem (Data.atomic_thesis thesisN);
    1.47 +    val bound_thesis = bind_skolem (AutoBind.atomic_judgment (Proof.theory_of state) thesisN);
    1.48      val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
    1.49  
    1.50      fun export_obtained rule =
    1.51 @@ -118,16 +112,19 @@
    1.52      |> Proof.enter_forward
    1.53      |> Proof.begin_block
    1.54      |> Proof.fix_i [([thesisN], None)]
    1.55 -    |> Proof.assume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
    1.56 -    |> Proof.from_facts chain_facts
    1.57 -    |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
    1.58 +    |> Proof.assume_i [(thatN, [Method.intro_local], [(that_prop, ([], []))])]
    1.59 +    |> (fn state' =>
    1.60 +      state'
    1.61 +      |> Proof.from_facts chain_facts
    1.62 +      |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
    1.63 +      |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
    1.64    end;
    1.65  
    1.66  
    1.67 -val obtain = ProofHistory.apply o
    1.68 +val obtain = ProofHistory.applys o
    1.69    (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
    1.70  
    1.71 -val obtain_i = ProofHistory.apply o
    1.72 +val obtain_i = ProofHistory.applys o
    1.73    (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
    1.74  
    1.75