ObtainFun;
authorwenzelm
Wed Jan 05 11:45:01 2000 +0100 (2000-01-05)
changeset 809462b45a2e6ecb
parent 8093 d5eb246c94ec
child 8095 497a9240acf3
ObtainFun;
prepare vars / asms / pats only once;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Jan 05 11:43:37 2000 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jan 05 11:45:01 2000 +0100
     1.3 @@ -2,8 +2,8 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -The 'obtain' language element -- achieves (eliminated) existential
     1.8 -quantification at proof command level.
     1.9 +The 'obtain' language element -- eliminated existential quantification
    1.10 +at the level of proof texts.
    1.11  
    1.12  The common case:
    1.13  
    1.14 @@ -32,94 +32,118 @@
    1.15      proof succeed
    1.16        fix x
    1.17        assume antecedent: G x
    1.18 -      def thesis == ?thesis_prop x
    1.19 +      def thesis == C x
    1.20        presume that: !!a. P a ==> thesis
    1.21        from goal_facts show thesis <proof>
    1.22      next
    1.23        fix a
    1.24        assume P a
    1.25  
    1.26 +TODO:
    1.27 +  - bind terms for goal as well (done?);
    1.28 +  - improve block structure (admit subsequent occurences of 'next') (no?);
    1.29 +  - handle general case (easy??);
    1.30 +*)
    1.31  
    1.32 -TODO:
    1.33 -  - handle general case;
    1.34 -*)
    1.35 +signature OBTAIN_DATA =
    1.36 +sig
    1.37 +  val that_atts: Proof.context attribute list
    1.38 +end;
    1.39  
    1.40  signature OBTAIN =
    1.41  sig
    1.42 -  val obtain: (string list * string option) list
    1.43 -    -> (string * Proof.context attribute list * (string * (string list * string list)) list) list
    1.44 -    -> Proof.state -> Proof.state Seq.seq
    1.45 -  val obtain_i: (string list * typ option) list
    1.46 -    -> (string * Proof.context attribute list * (term * (term list * term list)) list) list
    1.47 -    -> Proof.state -> Proof.state Seq.seq
    1.48 +  val obtain: ((string list * string option) * Comment.text) list
    1.49 +    * ((string * Args.src list * (string * (string list * string list)) list)
    1.50 +      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.51 +  val obtain_i: ((string list * typ option) * Comment.text) list
    1.52 +    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
    1.53 +      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.54  end;
    1.55  
    1.56 -structure Obtain: OBTAIN =
    1.57 +functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
    1.58  struct
    1.59  
    1.60 +
    1.61 +(** obtain(_i) **)
    1.62 +
    1.63  val thatN = "that";
    1.64  
    1.65 -fun gen_obtain prep_typ prep_prop fix assume raw_vars raw_asms state =
    1.66 +fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
    1.67    let
    1.68 +    (*thesis*)
    1.69      val (prop, (goal_facts, goal)) = Proof.get_goal (Proof.assert_backward state);
    1.70  
    1.71 -    val parms = Logic.strip_params prop;
    1.72 -    val hyps = Logic.strip_assums_hyp prop;
    1.73 -    val concl = Logic.strip_assums_concl prop;
    1.74 +    val parms = Logic.strip_params prop;        (* FIXME unused *)
    1.75      val _ =
    1.76        if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state);
    1.77 -
    1.78 +    val hyps = Logic.strip_assums_hyp prop;     (* FIXME unused *)
    1.79 +    val concl = Logic.strip_assums_concl prop;
    1.80      val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
    1.81  
    1.82 -
    1.83 -    fun fix_vars (ctxt, (xs, raw_T)) =
    1.84 -      let
    1.85 -        val T = apsome (prep_typ ctxt) raw_T;
    1.86 -        val ctxt' = ProofContext.fix_i [(xs, T)] ctxt;
    1.87 -      in (ctxt', map (ProofContext.cert_skolem ctxt') xs) end;
    1.88 +    (*vars*)
    1.89 +    val (vars_ctxt, vars) =
    1.90 +      foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
    1.91 +    val xs = flat (map fst vars);
    1.92  
    1.93 -    fun prep_asm (ctxt, (_, _, raw_propps)) =
    1.94 -      let val ts = map (prep_prop ctxt) (map fst raw_propps);
    1.95 -      in (ctxt |> ProofContext.declare_terms ts, ts) end;
    1.96 +    (*asms*)
    1.97 +    fun prep_asm (ctxt, (name, src, raw_propps)) =
    1.98 +      let
    1.99 +        val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
   1.100 +        val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
   1.101 +      in (ctxt', (name, atts, propps)) end;
   1.102  
   1.103 -    val (fix_ctxt, skolems) = apsnd flat (foldl_map fix_vars (Proof.context_of state, raw_vars));
   1.104 -    val (asms_ctxt, asms) = apsnd flat (foldl_map prep_asm (fix_ctxt, raw_asms));
   1.105 -    val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
   1.106 +    val (asms_ctxt, asms) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
   1.107 +    val asm_props = flat (map (map fst o #3) asms);
   1.108 +    val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
   1.109  
   1.110 +    (*that_prop*)
   1.111      fun find_free x t =
   1.112        (case Proof.find_free t x of Some (Free a) => Some a | _ => None);
   1.113 -    fun find_skolem x = Library.get_first (find_free x) asms;
   1.114 -    val skolemTs = mapfilter find_skolem skolems;
   1.115 -
   1.116 +    fun occs_var x = Library.get_first (find_free x) asm_props;
   1.117      val that_prop =
   1.118 -      Logic.list_rename_params (map (Syntax.dest_skolem o #1) skolemTs,
   1.119 -        Term.list_all_free (skolemTs, Logic.list_implies (asms, atomic_thesis)));
   1.120 -
   1.121 -    val presume_stateq =
   1.122 -      state
   1.123 -      |> Method.proof (Some (Method.Basic (K Method.succeed)))
   1.124 -      |> Seq.map (fn st => st
   1.125 -        |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
   1.126 -        |> Proof.presume_i [(thatN, [], [(that_prop, ([], []))])]);
   1.127 +      Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, atomic_thesis));
   1.128  
   1.129      fun after_qed st =
   1.130        st
   1.131        |> Proof.next_block
   1.132 -      |> fix raw_vars           (*prepared twice!*)
   1.133 -      |> assume raw_asms        (*prepared twice!*)
   1.134 +      |> Proof.fix_i vars
   1.135 +      |> Proof.assume_i asms
   1.136        |> Seq.single;
   1.137    in
   1.138 -    presume_stateq
   1.139 +    state
   1.140 +    |> Method.proof (Some (Method.Basic (K Method.succeed)))
   1.141      |> Seq.map (fn st => st
   1.142 +      |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
   1.143 +      |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
   1.144        |> Proof.from_facts goal_facts
   1.145 -      |> Proof.show_i after_qed "" [] (atomic_thesis, ([], []))
   1.146 -      |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts st)))))
   1.147 -    |> Seq.flat
   1.148 +      |> Proof.show_i after_qed "" [] (atomic_thesis, ([], [])))
   1.149    end;
   1.150  
   1.151  
   1.152 -val obtain = gen_obtain ProofContext.read_typ ProofContext.read_prop Proof.fix Proof.assume;
   1.153 -val obtain_i = gen_obtain ProofContext.cert_typ ProofContext.cert_prop Proof.fix_i Proof.assume_i;
   1.154 +val obtain = ProofHistory.applys o
   1.155 +  (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
   1.156 +
   1.157 +val obtain_i = ProofHistory.applys o
   1.158 +  (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
   1.159 +
   1.160 +
   1.161 +
   1.162 +(** outer syntax **)
   1.163 +
   1.164 +local structure P = OuterParse and K = OuterSyntax.Keyword in
   1.165 +
   1.166 +val obtainP =
   1.167 +  OuterSyntax.command "obtain" "proof text-level existential quantifier"
   1.168 +    K.prf_asm_goal
   1.169 +    (Scan.optional
   1.170 +      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
   1.171 +        --| P.$$$ "in") [] --
   1.172 +      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
   1.173 +    >> (Toplevel.print oo (Toplevel.proof o obtain)));
   1.174 +
   1.175 +val _ = OuterSyntax.add_parsers [obtainP];
   1.176 +
   1.177 +end;
   1.178  
   1.179  
   1.180  end;