src/Pure/proofterm.ML
changeset 33722 e588744f14da
parent 33522 737589bb9bb8
child 33955 fff6f11b1f09
     1.1 --- a/src/Pure/proofterm.ML	Mon Nov 16 21:56:32 2009 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Mon Nov 16 21:57:16 2009 +0100
     1.3 @@ -109,18 +109,20 @@
     1.4    val axm_proof: string -> term -> proof
     1.5    val oracle_proof: string -> term -> oracle * proof
     1.6    val promise_proof: theory -> serial -> term -> proof
     1.7 -  val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
     1.8 +  val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
     1.9    val thm_proof: theory -> string -> term list -> term ->
    1.10      (serial * proof_body future) list -> proof_body -> pthm * proof
    1.11    val get_name: term list -> term -> proof -> string
    1.12  
    1.13    (** rewriting on proof terms **)
    1.14    val add_prf_rrule: proof * proof -> theory -> theory
    1.15 -  val add_prf_rproc: (typ list -> proof -> proof option) -> theory -> theory
    1.16 +  val add_prf_rproc: (typ list -> proof -> (proof * proof) option) -> theory -> theory
    1.17 +  val no_skel: proof
    1.18 +  val normal_skel: proof
    1.19    val rewrite_proof: theory -> (proof * proof) list *
    1.20 -    (typ list -> proof -> proof option) list -> proof -> proof
    1.21 +    (typ list -> proof -> (proof * proof) option) list -> proof -> proof
    1.22    val rewrite_proof_notypes: (proof * proof) list *
    1.23 -    (typ list -> proof -> proof option) list -> proof -> proof
    1.24 +    (typ list -> proof -> (proof * proof) option) list -> proof -> proof
    1.25    val rew_proof: theory -> proof -> proof
    1.26  end
    1.27  
    1.28 @@ -1169,28 +1171,30 @@
    1.29  
    1.30  (**** rewriting on proof terms ****)
    1.31  
    1.32 -val skel0 = PBound 0;
    1.33 +val no_skel = PBound 0;
    1.34 +val normal_skel = Hyp (Var ((Name.uu, 0), propT));
    1.35  
    1.36  fun rewrite_prf tymatch (rules, procs) prf =
    1.37    let
    1.38 -    fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, skel0)
    1.39 -      | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, skel0)
    1.40 -      | rew Ts prf = (case get_first (fn r => r Ts prf) procs of
    1.41 -          SOME prf' => SOME (prf', skel0)
    1.42 -        | NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
    1.43 -            (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
    1.44 -               handle PMatch => NONE) (filter (could_unify prf o fst) rules));
    1.45 +    fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
    1.46 +      | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
    1.47 +      | rew Ts prf =
    1.48 +          (case get_first (fn r => r Ts prf) procs of
    1.49 +            NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
    1.50 +              (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
    1.51 +                 handle PMatch => NONE) (filter (could_unify prf o fst) rules)
    1.52 +          | some => some);
    1.53  
    1.54      fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) =
    1.55            if prf_loose_Pbvar1 prf' 0 then rew Ts prf
    1.56            else
    1.57              let val prf'' = incr_pboundvars (~1) 0 prf'
    1.58 -            in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
    1.59 +            in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
    1.60        | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) =
    1.61            if prf_loose_bvar1 prf' 0 then rew Ts prf
    1.62            else
    1.63              let val prf'' = incr_pboundvars 0 (~1) prf'
    1.64 -            in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
    1.65 +            in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
    1.66        | rew0 Ts prf = rew Ts prf;
    1.67  
    1.68      fun rew1 _ (Hyp (Var _)) _ = NONE
    1.69 @@ -1205,20 +1209,20 @@
    1.70      and rew2 Ts skel (prf % SOME t) = (case prf of
    1.71              Abst (_, _, body) =>
    1.72                let val prf' = prf_subst_bounds [t] body
    1.73 -              in SOME (the_default prf' (rew2 Ts skel0 prf')) end
    1.74 -          | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf of
    1.75 +              in SOME (the_default prf' (rew2 Ts no_skel prf')) end
    1.76 +          | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf of
    1.77                SOME prf' => SOME (prf' % SOME t)
    1.78              | NONE => NONE))
    1.79        | rew2 Ts skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
    1.80 -          (rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf)
    1.81 +          (rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf)
    1.82        | rew2 Ts skel (prf1 %% prf2) = (case prf1 of
    1.83              AbsP (_, _, body) =>
    1.84                let val prf' = prf_subst_pbounds [prf2] body
    1.85 -              in SOME (the_default prf' (rew2 Ts skel0 prf')) end
    1.86 +              in SOME (the_default prf' (rew2 Ts no_skel prf')) end
    1.87            | _ =>
    1.88              let val (skel1, skel2) = (case skel of
    1.89                  skel1 %% skel2 => (skel1, skel2)
    1.90 -              | _ => (skel0, skel0))
    1.91 +              | _ => (no_skel, no_skel))
    1.92              in case rew1 Ts skel1 prf1 of
    1.93                  SOME prf1' => (case rew1 Ts skel2 prf2 of
    1.94                      SOME prf2' => SOME (prf1' %% prf2')
    1.95 @@ -1228,16 +1232,16 @@
    1.96                    | NONE => NONE)
    1.97              end)
    1.98        | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts)
    1.99 -              (case skel of Abst (_, _, skel') => skel' | _ => skel0) prf of
   1.100 +              (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
   1.101              SOME prf' => SOME (Abst (s, T, prf'))
   1.102            | NONE => NONE)
   1.103        | rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts
   1.104 -              (case skel of AbsP (_, _, skel') => skel' | _ => skel0) prf of
   1.105 +              (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
   1.106              SOME prf' => SOME (AbsP (s, t, prf'))
   1.107            | NONE => NONE)
   1.108        | rew2 _ _ _ = NONE;
   1.109  
   1.110 -  in the_default prf (rew1 [] skel0 prf) end;
   1.111 +  in the_default prf (rew1 [] no_skel prf) end;
   1.112  
   1.113  fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
   1.114    Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
   1.115 @@ -1249,7 +1253,9 @@
   1.116  
   1.117  structure ProofData = Theory_Data
   1.118  (
   1.119 -  type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list;
   1.120 +  type T =
   1.121 +    (stamp * (proof * proof)) list *
   1.122 +    (stamp * (typ list -> proof -> (proof * proof) option)) list;
   1.123  
   1.124    val empty = ([], []);
   1.125    val extend = I;
   1.126 @@ -1277,27 +1283,26 @@
   1.127          | _ => false));
   1.128    in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
   1.129  
   1.130 -fun fulfill_proof _ [] body0 = body0
   1.131 -  | fulfill_proof thy ps body0 =
   1.132 -      let
   1.133 -        val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
   1.134 -        val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
   1.135 -        val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
   1.136 -        val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
   1.137 +fun fulfill_norm_proof thy ps body0 =
   1.138 +  let
   1.139 +    val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
   1.140 +    val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
   1.141 +    val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
   1.142 +    val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
   1.143  
   1.144 -        fun fill (Promise (i, prop, Ts)) =
   1.145 -            (case Inttab.lookup proofs i of
   1.146 -              NONE => NONE
   1.147 -            | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf))
   1.148 -          | fill _ = NONE;
   1.149 -        val (rules, procs) = get_data thy;
   1.150 -        val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
   1.151 -      in PBody {oracles = oracles, thms = thms, proof = proof} end;
   1.152 +    fun fill (Promise (i, prop, Ts)) =
   1.153 +          (case Inttab.lookup proofs i of
   1.154 +            NONE => NONE
   1.155 +          | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel))
   1.156 +      | fill _ = NONE;
   1.157 +    val (rules, procs) = get_data thy;
   1.158 +    val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
   1.159 +  in PBody {oracles = oracles, thms = thms, proof = proof} end;
   1.160  
   1.161  fun fulfill_proof_future _ [] body = Future.value body
   1.162    | fulfill_proof_future thy promises body =
   1.163        Future.fork_deps (map snd promises) (fn () =>
   1.164 -        fulfill_proof thy (map (apsnd Future.join) promises) body);
   1.165 +        fulfill_norm_proof thy (map (apsnd Future.join) promises) body);
   1.166  
   1.167  
   1.168  (***** theorems *****)