added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
authorwenzelm
Fri May 14 19:53:36 2010 +0200 (2010-05-14 ago)
changeset 368834ed0d72def50
parent 36882 f33760bb8ca0
child 36932 dbd39471211c
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/proofterm.ML	Thu May 13 21:36:38 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Fri May 14 19:53:36 2010 +0200
     1.3 @@ -135,6 +135,8 @@
     1.4    val unconstrain_thm_proofs: bool Unsynchronized.ref
     1.5    val thm_proof: theory -> string -> sort list -> term list -> term ->
     1.6      (serial * proof_body future) list -> proof_body -> pthm * proof
     1.7 +  val unconstrain_thm_proof: theory -> sort list -> term ->
     1.8 +    (serial * proof_body future) list -> proof_body -> pthm * proof
     1.9    val get_name: term list -> term -> proof -> string
    1.10    val get_name_unconstrained: sort list -> term list -> term -> proof -> string
    1.11    val guess_name: proof -> string
    1.12 @@ -1400,16 +1402,14 @@
    1.13  
    1.14  fun unconstrainT_body thy constrs (PBody {oracles, thms, proof}) =
    1.15    PBody
    1.16 -   {oracles = oracles,  (* FIXME unconstrain (!?!) *)
    1.17 -    thms = thms,
    1.18 +   {oracles = oracles,  (* FIXME merge (!), unconstrain (!?!) *)
    1.19 +    thms = thms,  (* FIXME merge (!) *)
    1.20      proof = unconstrainT_prf thy constrs proof};
    1.21  
    1.22  
    1.23  (***** theorems *****)
    1.24  
    1.25 -val unconstrain_thm_proofs = Unsynchronized.ref false;
    1.26 -
    1.27 -fun thm_proof thy name shyps hyps concl promises body =
    1.28 +fun prepare_thm_proof do_unconstrain thy name shyps hyps concl promises body =
    1.29    let
    1.30      val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
    1.31      val prop = Logic.list_implies (hyps, concl);
    1.32 @@ -1418,13 +1418,16 @@
    1.33          if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
    1.34        map SOME (frees_of prop);
    1.35  
    1.36 -    val (postproc, ofclasses, prop1) =
    1.37 -      if ! unconstrain_thm_proofs then
    1.38 +    val (postproc, ofclasses, prop1, args1) =
    1.39 +      if do_unconstrain then
    1.40          let
    1.41            val ((atyp_map, constraints), prop1) = Logic.unconstrainT shyps prop;
    1.42            val postproc = unconstrainT_body thy (atyp_map, constraints);
    1.43 -        in (postproc, map (OfClass o fst) constraints, prop1) end
    1.44 -      else (I, [], prop);
    1.45 +          val args1 =
    1.46 +            (map o Option.map o Term.map_types o Term.map_atyps)
    1.47 +              (Type.strip_sorts o atyp_map) args;
    1.48 +        in (postproc, map (OfClass o fst) constraints, prop1, args1) end
    1.49 +      else (I, [], prop, args);
    1.50      val argsP = ofclasses @ map Hyp hyps;
    1.51  
    1.52      val proof0 =
    1.53 @@ -1442,9 +1445,21 @@
    1.54            else new_prf ()
    1.55        | _ => new_prf ());
    1.56      val head = PThm (i, ((name, prop1, NONE), body'));
    1.57 -  in
    1.58 -    ((i, (name, prop1, body')), proof_combP (proof_combt' (head, args), argsP))
    1.59 -  end;
    1.60 +  in ((i, (name, prop1, body')), head, args, argsP, args1) end;
    1.61 +
    1.62 +val unconstrain_thm_proofs = Unsynchronized.ref false;
    1.63 +
    1.64 +fun thm_proof thy name shyps hyps concl promises body =
    1.65 +  let val (pthm, head, args, argsP, _) =
    1.66 +    prepare_thm_proof (! unconstrain_thm_proofs) thy name shyps hyps concl promises body
    1.67 +  in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
    1.68 +
    1.69 +fun unconstrain_thm_proof thy shyps concl promises body =
    1.70 +  let
    1.71 +    val (pthm, head, _, _, args) =
    1.72 +      prepare_thm_proof true thy "" shyps [] concl promises body
    1.73 +  in (pthm, proof_combt' (head, args)) end;
    1.74 +
    1.75  
    1.76  fun get_name hyps prop prf =
    1.77    let val prop = Logic.list_implies (hyps, prop) in
     2.1 --- a/src/Pure/thm.ML	Thu May 13 21:36:38 2010 +0200
     2.2 +++ b/src/Pure/thm.ML	Fri May 14 19:53:36 2010 +0200
     2.3 @@ -1222,24 +1222,30 @@
     2.4        end;
     2.5  
     2.6  (*Internalize sort constraints of type variables*)
     2.7 -fun unconstrainT (thm as Thm (_, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
     2.8 +fun unconstrainT (thm as Thm (der, args)) =
     2.9    let
    2.10 +    val Deriv {promises, body} = der;
    2.11 +    val {thy_ref, shyps, hyps, tpairs, prop, ...} = args;
    2.12 +
    2.13      fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]);
    2.14 -
    2.15      val _ = null hyps orelse err "illegal hyps";
    2.16      val _ = null tpairs orelse err "unsolved flex-flex constraints";
    2.17      val tfrees = rev (Term.add_tfree_names prop []);
    2.18      val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
    2.19  
    2.20 -    val (_, prop') = Logic.unconstrainT shyps prop;
    2.21 +    val ps = map (apsnd (Future.map proof_body_of)) promises;
    2.22 +    val thy = Theory.deref thy_ref;
    2.23 +    val (pthm as (_, (_, prop', _)), proof) = Pt.unconstrain_thm_proof thy shyps prop ps body;
    2.24 +    val der' = make_deriv [] [] [pthm] proof;
    2.25 +    val _ = Theory.check_thy thy;
    2.26    in
    2.27 -    Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
    2.28 +    Thm (der',
    2.29       {thy_ref = thy_ref,
    2.30        tags = [],
    2.31        maxidx = maxidx_of_term prop',
    2.32        shyps = [[]],  (*potentially redundant*)
    2.33 -      hyps = hyps,
    2.34 -      tpairs = tpairs,
    2.35 +      hyps = [],
    2.36 +      tpairs = [],
    2.37        prop = prop'})
    2.38    end;
    2.39