1.1 --- a/src/Pure/proofterm.ML	Tue Jun 01 10:55:38 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue Jun 01 11:01:16 2010 +0200
     1.3 @@ -58,6 +58,8 @@
     1.4    val strip_combt: proof -> proof * term option list
     1.5    val strip_combP: proof -> proof * proof list
     1.6    val strip_thm: proof_body -> proof_body
     1.7 +  val map_proof_same: term Same.operation -> typ Same.operation
     1.8 +    -> (typ * class -> proof) -> proof Same.operation
     1.9    val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
    1.10    val map_proof_types_same: typ Same.operation -> proof Same.operation
    1.11    val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
    1.12 @@ -80,7 +82,9 @@
    1.13  
    1.14    (** proof terms for specific inference rules **)
    1.15    val implies_intr_proof: term -> proof -> proof
    1.16 +  val implies_intr_proof': term -> proof -> proof
    1.17    val forall_intr_proof: term -> string -> proof -> proof
    1.18 +  val forall_intr_proof': term -> proof -> proof
    1.19    val varify_proof: term -> (string * sort) list -> proof -> proof
    1.20    val legacy_freezeT: term -> proof -> proof
    1.21    val rotate_proof: term list -> term -> int -> proof -> proof
    1.22 @@ -121,13 +125,13 @@
    1.23  
    1.24    (** rewriting on proof terms **)
    1.25    val add_prf_rrule: proof * proof -> theory -> theory
    1.26 -  val add_prf_rproc: (typ list -> proof -> (proof * proof) option) -> theory -> theory
    1.27 +  val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory
    1.28    val no_skel: proof
    1.29    val normal_skel: proof
    1.30    val rewrite_proof: theory -> (proof * proof) list *
    1.31 -    (typ list -> proof -> (proof * proof) option) list -> proof -> proof
    1.32 +    (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
    1.33    val rewrite_proof_notypes: (proof * proof) list *
    1.34 -    (typ list -> proof -> (proof * proof) option) list -> proof -> proof
    1.35 +    (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
    1.36    val rew_proof: theory -> proof -> proof
    1.37  
    1.38    val promise_proof: theory -> serial -> term -> proof
    1.39 @@ -618,7 +622,7 @@
    1.40  
    1.41  (***** implication introduction *****)
    1.42  
    1.43 -fun implies_intr_proof h prf =
    1.44 +fun gen_implies_intr_proof f h prf =
    1.45    let
    1.46      fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME
    1.47        | abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
    1.48 @@ -630,14 +634,21 @@
    1.49        | abshyp _ _ = raise Same.SAME
    1.50      and abshyph i prf = (abshyp i prf handle Same.SAME => prf);
    1.51    in
    1.52 -    AbsP ("H", NONE (*h*), abshyph 0 prf)
    1.53 +    AbsP ("H", f h, abshyph 0 prf)
    1.54    end;
    1.55  
    1.56 +val implies_intr_proof = gen_implies_intr_proof (K NONE);
    1.57 +val implies_intr_proof' = gen_implies_intr_proof SOME;
    1.58 +
    1.59  
    1.60  (***** forall introduction *****)
    1.61  
    1.62  fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf);
    1.63  
    1.64 +fun forall_intr_proof' t prf =
    1.65 +  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    1.66 +  in Abst (a, SOME T, prf_abstract_over t prf) end;
    1.67 +
    1.68  
    1.69  (***** varify *****)
    1.70  
    1.71 @@ -1105,7 +1116,7 @@
    1.72  
    1.73  fun flt (i: int) = filter (fn n => n < i);
    1.74  
    1.75 -fun fomatch Ts tymatch j =
    1.76 +fun fomatch Ts tymatch j instsp p =
    1.77    let
    1.78      fun mtch (instsp as (tyinsts, insts)) = fn
    1.79          (Var (ixn, T), t)  =>
    1.80 @@ -1120,7 +1131,7 @@
    1.81        | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
    1.82        | (Bound i, Bound j) => if i=j then instsp else raise PMatch
    1.83        | _ => raise PMatch
    1.84 -  in mtch end;
    1.85 +  in mtch instsp (pairself Envir.beta_eta_contract p) end;
    1.86  
    1.87  fun match_proof Ts tymatch =
    1.88    let
    1.89 @@ -1253,72 +1264,72 @@
    1.90  
    1.91  fun rewrite_prf tymatch (rules, procs) prf =
    1.92    let
    1.93 -    fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
    1.94 -      | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
    1.95 -      | rew Ts prf =
    1.96 -          (case get_first (fn r => r Ts prf) procs of
    1.97 +    fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
    1.98 +      | rew _ _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
    1.99 +      | rew Ts hs prf =
   1.100 +          (case get_first (fn r => r Ts hs prf) procs of
   1.101              NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
   1.102                (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
   1.103                   handle PMatch => NONE) (filter (could_unify prf o fst) rules)
   1.104            | some => some);
   1.105  
   1.106 -    fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) =
   1.107 -          if prf_loose_Pbvar1 prf' 0 then rew Ts prf
   1.108 +    fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) =
   1.109 +          if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf
   1.110            else
   1.111              let val prf'' = incr_pboundvars (~1) 0 prf'
   1.112 -            in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
   1.113 -      | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) =
   1.114 -          if prf_loose_bvar1 prf' 0 then rew Ts prf
   1.115 +            in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
   1.116 +      | rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) =
   1.117 +          if prf_loose_bvar1 prf' 0 then rew Ts hs prf
   1.118            else
   1.119              let val prf'' = incr_pboundvars 0 (~1) prf'
   1.120 -            in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
   1.121 -      | rew0 Ts prf = rew Ts prf;
   1.122 +            in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
   1.123 +      | rew0 Ts hs prf = rew Ts hs prf;
   1.124  
   1.125 -    fun rew1 _ (Hyp (Var _)) _ = NONE
   1.126 -      | rew1 Ts skel prf = (case rew2 Ts skel prf of
   1.127 -          SOME prf1 => (case rew0 Ts prf1 of
   1.128 -              SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts skel' prf2))
   1.129 +    fun rew1 _ _ (Hyp (Var _)) _ = NONE
   1.130 +      | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of
   1.131 +          SOME prf1 => (case rew0 Ts hs prf1 of
   1.132 +              SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
   1.133              | NONE => SOME prf1)
   1.134 -        | NONE => (case rew0 Ts prf of
   1.135 -              SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts skel' prf1))
   1.136 +        | NONE => (case rew0 Ts hs prf of
   1.137 +              SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
   1.138              | NONE => NONE))
   1.139  
   1.140 -    and rew2 Ts skel (prf % SOME t) = (case prf of
   1.141 +    and rew2 Ts hs skel (prf % SOME t) = (case prf of
   1.142              Abst (_, _, body) =>
   1.143                let val prf' = prf_subst_bounds [t] body
   1.144 -              in SOME (the_default prf' (rew2 Ts no_skel prf')) end
   1.145 -          | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf of
   1.146 +              in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
   1.147 +          | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
   1.148                SOME prf' => SOME (prf' % SOME t)
   1.149              | NONE => NONE))
   1.150 -      | rew2 Ts skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
   1.151 -          (rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf)
   1.152 -      | rew2 Ts skel (prf1 %% prf2) = (case prf1 of
   1.153 +      | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
   1.154 +          (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf)
   1.155 +      | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of
   1.156              AbsP (_, _, body) =>
   1.157                let val prf' = prf_subst_pbounds [prf2] body
   1.158 -              in SOME (the_default prf' (rew2 Ts no_skel prf')) end
   1.159 +              in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
   1.160            | _ =>
   1.161              let val (skel1, skel2) = (case skel of
   1.162                  skel1 %% skel2 => (skel1, skel2)
   1.163                | _ => (no_skel, no_skel))
   1.164 -            in case rew1 Ts skel1 prf1 of
   1.165 -                SOME prf1' => (case rew1 Ts skel2 prf2 of
   1.166 +            in case rew1 Ts hs skel1 prf1 of
   1.167 +                SOME prf1' => (case rew1 Ts hs skel2 prf2 of
   1.168                      SOME prf2' => SOME (prf1' %% prf2')
   1.169                    | NONE => SOME (prf1' %% prf2))
   1.170 -              | NONE => (case rew1 Ts skel2 prf2 of
   1.171 +              | NONE => (case rew1 Ts hs skel2 prf2 of
   1.172                      SOME prf2' => SOME (prf1 %% prf2')
   1.173                    | NONE => NONE)
   1.174              end)
   1.175 -      | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts)
   1.176 +      | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs
   1.177                (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
   1.178              SOME prf' => SOME (Abst (s, T, prf'))
   1.179            | NONE => NONE)
   1.180 -      | rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts
   1.181 +      | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs)
   1.182                (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
   1.183              SOME prf' => SOME (AbsP (s, t, prf'))
   1.184            | NONE => NONE)
   1.185 -      | rew2 _ _ _ = NONE;
   1.186 +      | rew2 _ _ _ _ = NONE;
   1.187  
   1.188 -  in the_default prf (rew1 [] no_skel prf) end;
   1.189 +  in the_default prf (rew1 [] [] no_skel prf) end;
   1.190  
   1.191  fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
   1.192    Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
   1.193 @@ -1332,7 +1343,7 @@
   1.194  (
   1.195    type T =
   1.196      (stamp * (proof * proof)) list *
   1.197 -    (stamp * (typ list -> proof -> (proof * proof) option)) list;
   1.198 +    (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list;
   1.199  
   1.200    val empty = ([], []);
   1.201    val extend = I;
   1.202 @@ -1373,7 +1384,7 @@
   1.203            | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel))
   1.204        | fill _ = NONE;
   1.205      val (rules, procs) = get_data thy;
   1.206 -    val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
   1.207 +    val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
   1.208    in PBody {oracles = oracles, thms = thms, proof = proof} end;
   1.209  
   1.210  fun fulfill_proof_future _ [] postproc body = Future.value (postproc body)
   1.211 @@ -1421,12 +1432,13 @@
   1.212      val (postproc, ofclasses, prop1, args1) =
   1.213        if do_unconstrain then
   1.214          let
   1.215 -          val ((atyp_map, constraints), prop1) = Logic.unconstrainT shyps prop;
   1.216 +          val ((atyp_map, constraints, outer_constraints), prop1) =
   1.217 +            Logic.unconstrainT shyps prop;
   1.218            val postproc = unconstrainT_body thy (atyp_map, constraints);
   1.219            val args1 =
   1.220              (map o Option.map o Term.map_types o Term.map_atyps)
   1.221                (Type.strip_sorts o atyp_map) args;
   1.222 -        in (postproc, map (OfClass o fst) constraints, prop1, args1) end
   1.223 +        in (postproc, map OfClass outer_constraints, prop1, args1) end
   1.224        else (I, [], prop, args);
   1.225      val argsP = ofclasses @ map Hyp hyps;
   1.226  
   1.227 @@ -1447,7 +1459,7 @@
   1.228      val head = PThm (i, ((name, prop1, NONE), body'));
   1.229    in ((i, (name, prop1, body')), head, args, argsP, args1) end;
   1.230  
   1.231 -val unconstrain_thm_proofs = Unsynchronized.ref false;
   1.232 +val unconstrain_thm_proofs = Unsynchronized.ref true;
   1.233  
   1.234  fun thm_proof thy name shyps hyps concl promises body =
   1.235    let val (pthm, head, args, argsP, _) =