src/HOL/Import/replay.ML
changeset 41164 6854e9a40edc
parent 39557 fe5722fce758
child 41522 42d13d00ccfb
     1.1 --- a/src/HOL/Import/replay.ML	Wed Dec 15 15:01:34 2010 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Wed Dec 15 15:11:56 2010 +0100
     1.3 @@ -2,11 +2,9 @@
     1.4      Author:     Sebastian Skalberg (TU Muenchen)
     1.5  *)
     1.6  
     1.7 -structure Replay =
     1.8 +structure Replay =  (* FIXME proper signature *)
     1.9  struct
    1.10  
    1.11 -structure P = ProofKernel
    1.12 -
    1.13  open ProofKernel
    1.14  open ImportRecorder
    1.15  
    1.16 @@ -17,12 +15,12 @@
    1.17  fun replay_proof int_thms thyname thmname prf thy =
    1.18      let
    1.19          val _ = ImportRecorder.start_replay_proof thyname thmname 
    1.20 -        fun rp (PRefl tm) thy = P.REFL tm thy
    1.21 +        fun rp (PRefl tm) thy = ProofKernel.REFL tm thy
    1.22            | rp (PInstT(p,lambda)) thy =
    1.23              let
    1.24                  val (thy',th) = rp' p thy
    1.25              in
    1.26 -                P.INST_TYPE lambda th thy'
    1.27 +                ProofKernel.INST_TYPE lambda th thy'
    1.28              end
    1.29            | rp (PSubst(prfs,ctxt,prf)) thy =
    1.30              let
    1.31 @@ -34,52 +32,52 @@
    1.32                                             end) prfs (thy,[])
    1.33                  val (thy'',th) = rp' prf thy'
    1.34              in
    1.35 -                P.SUBST ths ctxt th thy''
    1.36 +                ProofKernel.SUBST ths ctxt th thy''
    1.37              end
    1.38            | rp (PAbs(prf,v)) thy =
    1.39              let
    1.40                  val (thy',th) = rp' prf thy
    1.41              in
    1.42 -                P.ABS v th thy'
    1.43 +                ProofKernel.ABS v th thy'
    1.44              end
    1.45            | rp (PDisch(prf,tm)) thy =
    1.46              let
    1.47                  val (thy',th) = rp' prf thy
    1.48              in
    1.49 -                P.DISCH tm th thy'
    1.50 +                ProofKernel.DISCH tm th thy'
    1.51              end
    1.52            | rp (PMp(prf1,prf2)) thy =
    1.53              let
    1.54                  val (thy1,th1) = rp' prf1 thy
    1.55                  val (thy2,th2) = rp' prf2 thy1
    1.56              in
    1.57 -                P.MP th1 th2 thy2
    1.58 +                ProofKernel.MP th1 th2 thy2
    1.59              end
    1.60 -          | rp (PHyp tm) thy = P.ASSUME tm thy
    1.61 +          | rp (PHyp tm) thy = ProofKernel.ASSUME tm thy
    1.62            | rp (PDef(seg,name,rhs)) thy =
    1.63 -            (case P.get_def seg name rhs thy of
    1.64 +            (case ProofKernel.get_def seg name rhs thy of
    1.65                   (thy',SOME res) => (thy',res)
    1.66                 | (thy',NONE) => 
    1.67                   if seg = thyname
    1.68 -                 then P.new_definition seg name rhs thy'
    1.69 +                 then ProofKernel.new_definition seg name rhs thy'
    1.70                   else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
    1.71 -          | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    1.72 +          | rp (POracle(tg,asl,c)) thy = (*ProofKernel.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    1.73            | rp (PSpec(prf,tm)) thy =
    1.74              let
    1.75                  val (thy',th) = rp' prf thy
    1.76              in
    1.77 -                P.SPEC tm th thy'
    1.78 +                ProofKernel.SPEC tm th thy'
    1.79              end
    1.80            | rp (PInst(prf,theta)) thy =
    1.81              let
    1.82                  val (thy',th) = rp' prf thy
    1.83              in
    1.84 -                P.INST theta th thy'
    1.85 +                ProofKernel.INST theta th thy'
    1.86              end
    1.87            | rp (PGen(prf,v)) thy =
    1.88              let
    1.89                  val (thy',th) = rp' prf thy
    1.90 -                val p = P.GEN v th thy'
    1.91 +                val p = ProofKernel.GEN v th thy'
    1.92              in
    1.93                  p
    1.94              end
    1.95 @@ -87,91 +85,91 @@
    1.96              let
    1.97                  val (thy',th) = rp' prf thy
    1.98              in
    1.99 -                P.GEN_ABS opt vl th thy'
   1.100 +                ProofKernel.GEN_ABS opt vl th thy'
   1.101              end
   1.102            | rp (PImpAS(prf1,prf2)) thy =
   1.103              let
   1.104                  val (thy1,th1) = rp' prf1 thy
   1.105                  val (thy2,th2) = rp' prf2 thy1
   1.106              in
   1.107 -                P.IMP_ANTISYM th1 th2 thy2
   1.108 +                ProofKernel.IMP_ANTISYM th1 th2 thy2
   1.109              end
   1.110            | rp (PSym prf) thy =
   1.111              let
   1.112                  val (thy1,th) = rp' prf thy
   1.113              in
   1.114 -                P.SYM th thy1
   1.115 +                ProofKernel.SYM th thy1
   1.116              end
   1.117            | rp (PTrans(prf1,prf2)) thy =
   1.118              let
   1.119                  val (thy1,th1) = rp' prf1 thy
   1.120                  val (thy2,th2) = rp' prf2 thy1
   1.121              in
   1.122 -                P.TRANS th1 th2 thy2
   1.123 +                ProofKernel.TRANS th1 th2 thy2
   1.124              end
   1.125            | rp (PComb(prf1,prf2)) thy =
   1.126              let
   1.127                  val (thy1,th1) = rp' prf1 thy
   1.128                  val (thy2,th2) = rp' prf2 thy1
   1.129              in
   1.130 -                P.COMB th1 th2 thy2
   1.131 +                ProofKernel.COMB th1 th2 thy2
   1.132              end
   1.133            | rp (PEqMp(prf1,prf2)) thy =
   1.134              let
   1.135                  val (thy1,th1) = rp' prf1 thy
   1.136                  val (thy2,th2) = rp' prf2 thy1
   1.137              in
   1.138 -                P.EQ_MP th1 th2 thy2
   1.139 +                ProofKernel.EQ_MP th1 th2 thy2
   1.140              end
   1.141            | rp (PEqImp prf) thy =
   1.142              let
   1.143                  val (thy',th) = rp' prf thy
   1.144              in
   1.145 -                P.EQ_IMP_RULE th thy'
   1.146 +                ProofKernel.EQ_IMP_RULE th thy'
   1.147              end
   1.148            | rp (PExists(prf,ex,wit)) thy =
   1.149              let
   1.150                  val (thy',th) = rp' prf thy
   1.151              in
   1.152 -                P.EXISTS ex wit th thy'
   1.153 +                ProofKernel.EXISTS ex wit th thy'
   1.154              end
   1.155            | rp (PChoose(v,prf1,prf2)) thy =
   1.156              let
   1.157                  val (thy1,th1) = rp' prf1 thy
   1.158                  val (thy2,th2) = rp' prf2 thy1
   1.159              in
   1.160 -                P.CHOOSE v th1 th2 thy2
   1.161 +                ProofKernel.CHOOSE v th1 th2 thy2
   1.162              end
   1.163            | rp (PConj(prf1,prf2)) thy =
   1.164              let
   1.165                  val (thy1,th1) = rp' prf1 thy
   1.166                  val (thy2,th2) = rp' prf2 thy1
   1.167              in
   1.168 -                P.CONJ th1 th2 thy2
   1.169 +                ProofKernel.CONJ th1 th2 thy2
   1.170              end
   1.171            | rp (PConjunct1 prf) thy =
   1.172              let
   1.173                  val (thy',th) = rp' prf thy
   1.174              in
   1.175 -                P.CONJUNCT1 th thy'
   1.176 +                ProofKernel.CONJUNCT1 th thy'
   1.177              end
   1.178            | rp (PConjunct2 prf) thy =
   1.179              let
   1.180                  val (thy',th) = rp' prf thy
   1.181              in
   1.182 -                P.CONJUNCT2 th thy'
   1.183 +                ProofKernel.CONJUNCT2 th thy'
   1.184              end
   1.185            | rp (PDisj1(prf,tm)) thy =
   1.186              let
   1.187                  val (thy',th) = rp' prf thy
   1.188              in
   1.189 -                P.DISJ1 th tm thy'
   1.190 +                ProofKernel.DISJ1 th tm thy'
   1.191              end
   1.192            | rp (PDisj2(prf,tm)) thy =
   1.193              let
   1.194                  val (thy',th) = rp' prf thy
   1.195              in
   1.196 -                P.DISJ2 tm th thy'
   1.197 +                ProofKernel.DISJ2 tm th thy'
   1.198              end
   1.199            | rp (PDisjCases(prf,prf1,prf2)) thy =
   1.200              let
   1.201 @@ -179,25 +177,25 @@
   1.202                  val (thy1,th1) = rp' prf1 thy'
   1.203                  val (thy2,th2) = rp' prf2 thy1
   1.204              in
   1.205 -                P.DISJ_CASES th th1 th2 thy2
   1.206 +                ProofKernel.DISJ_CASES th th1 th2 thy2
   1.207              end
   1.208            | rp (PNotI prf) thy =
   1.209              let
   1.210                  val (thy',th) = rp' prf thy
   1.211              in
   1.212 -                P.NOT_INTRO th thy'
   1.213 +                ProofKernel.NOT_INTRO th thy'
   1.214              end
   1.215            | rp (PNotE prf) thy =
   1.216              let
   1.217                  val (thy',th) = rp' prf thy
   1.218              in
   1.219 -                P.NOT_ELIM th thy'
   1.220 +                ProofKernel.NOT_ELIM th thy'
   1.221              end
   1.222            | rp (PContr(prf,tm)) thy =
   1.223              let
   1.224                  val (thy',th) = rp' prf thy
   1.225              in
   1.226 -                P.CCONTR tm th thy'
   1.227 +                ProofKernel.CCONTR tm th thy'
   1.228              end
   1.229            | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
   1.230            | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
   1.231 @@ -226,7 +224,7 @@
   1.232                                                | SOME th => (thy,th))
   1.233                                         else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
   1.234                                       | NONE => 
   1.235 -                                       (case P.get_thm thyname' thmname thy of
   1.236 +                                       (case ProofKernel.get_thm thyname' thmname thy of
   1.237                                              (thy',SOME res) => (thy',res)
   1.238                                            | (thy',NONE) => 
   1.239                                              if thyname' = thyname
   1.240 @@ -242,31 +240,31 @@
   1.241                                                          PTmSpec _ => (thy',th)
   1.242                                                        | PTyDef  _ => (thy',th)
   1.243                                                        | PTyIntro _ => (thy',th)
   1.244 -                                                      | _ => P.store_thm thyname' thmname th thy'
   1.245 +                                                      | _ => ProofKernel.store_thm thyname' thmname th thy'
   1.246                                                  end
   1.247                                              else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
   1.248                                  | NONE => raise ERR "rp'.PDisk" "Not enough information")
   1.249                    | PAxm(name,c) =>
   1.250 -                    (case P.get_axiom thyname name thy of
   1.251 +                    (case ProofKernel.get_axiom thyname name thy of
   1.252                              (thy',SOME res) => (thy',res)
   1.253 -                          | (thy',NONE) => P.new_axiom name c thy')
   1.254 +                          | (thy',NONE) => ProofKernel.new_axiom name c thy')
   1.255                    | PTmSpec(seg,names,prf') =>
   1.256                      let
   1.257                          val (thy',th) = rp' prf' thy
   1.258                      in
   1.259 -                        P.new_specification seg thmname names th thy'
   1.260 +                        ProofKernel.new_specification seg thmname names th thy'
   1.261                      end
   1.262                    | PTyDef(seg,name,prf') =>
   1.263                      let
   1.264                          val (thy',th) = rp' prf' thy
   1.265                      in
   1.266 -                        P.new_type_definition seg thmname name th thy'
   1.267 +                        ProofKernel.new_type_definition seg thmname name th thy'
   1.268                      end
   1.269                    | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
   1.270                      let
   1.271                          val (thy',th) = rp' prf' thy
   1.272                      in
   1.273 -                        P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   1.274 +                        ProofKernel.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   1.275                      end
   1.276                    | _ => rp pc thy
   1.277              end
   1.278 @@ -282,7 +280,7 @@
   1.279  fun setup_int_thms thyname thy =
   1.280      let
   1.281          val fname =
   1.282 -            case P.get_proof_dir thyname thy of
   1.283 +            case ProofKernel.get_proof_dir thyname thy of
   1.284                  SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
   1.285                | NONE => error "Cannot find proof files"
   1.286          val is = TextIO.openIn fname
   1.287 @@ -291,7 +289,7 @@
   1.288                  fun get_facts facts =
   1.289                      case TextIO.inputLine is of
   1.290                          NONE => (case facts of
   1.291 -                                   i::facts => (the (Int.fromString i),map P.protect_factname (rev facts))
   1.292 +                                   i::facts => (the (Int.fromString i),map ProofKernel.protect_factname (rev facts))
   1.293                                   | _ => raise ERR "replay_thm" "Bad facts.lst file")
   1.294                        | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   1.295              in
   1.296 @@ -349,9 +347,9 @@
   1.297            | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
   1.298              add_hol4_type_mapping thyname tycname true fulltyname thy
   1.299            | delta (Indexed_theorem (i, th)) thy = 
   1.300 -            (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)                   
   1.301 -          | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
   1.302 -          | delta (Dump s) thy = P.replay_add_dump s thy
   1.303 +            (Array.update (int_thms,i-1,SOME (ProofKernel.to_hol_thm (th_of thy th))); thy)                   
   1.304 +          | delta (Protect_varname (s,t)) thy = (ProofKernel.replay_protect_varname s t; thy)
   1.305 +          | delta (Dump s) thy = ProofKernel.replay_add_dump s thy
   1.306      in
   1.307          rps
   1.308      end