src/HOL/Import/replay.ML
changeset 14516 a183dec876ab
child 14620 1be590fd2422
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Apr 02 17:37:45 2004 +0200
     1.3 @@ -0,0 +1,333 @@
     1.4 +structure Replay =
     1.5 +struct
     1.6 +
     1.7 +structure P = ProofKernel
     1.8 +
     1.9 +open ProofKernel
    1.10 +
    1.11 +exception REPLAY of string * string
    1.12 +fun ERR f mesg = REPLAY (f,mesg)
    1.13 +fun NY f = raise ERR f "NOT YET!"
    1.14 +
    1.15 +fun replay_proof int_thms thyname thmname prf thy =
    1.16 +    let
    1.17 +	fun rp (PRefl tm) thy = P.REFL tm thy
    1.18 +	  | rp (PInstT(p,lambda)) thy =
    1.19 +	    let
    1.20 +		val (thy',th) = rp' p thy
    1.21 +	    in
    1.22 +		P.INST_TYPE lambda th thy'
    1.23 +	    end
    1.24 +	  | rp (PSubst(prfs,ctxt,prf)) thy =
    1.25 +	    let
    1.26 +		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
    1.27 +					   let
    1.28 +					       val (thy',th) = rp' p thy
    1.29 +					   in
    1.30 +					       (thy',th::ths)
    1.31 +					   end) (prfs,(thy,[]))
    1.32 +		val (thy'',th) = rp' prf thy'
    1.33 +	    in
    1.34 +		P.SUBST ths ctxt th thy''
    1.35 +	    end
    1.36 +	  | rp (PAbs(prf,v)) thy =
    1.37 +	    let
    1.38 +		val (thy',th) = rp' prf thy
    1.39 +	    in
    1.40 +		P.ABS v th thy'
    1.41 +	    end
    1.42 +	  | rp (PDisch(prf,tm)) thy =
    1.43 +	    let
    1.44 +		val (thy',th) = rp' prf thy
    1.45 +	    in
    1.46 +		P.DISCH tm th thy'
    1.47 +	    end
    1.48 +	  | rp (PMp(prf1,prf2)) thy =
    1.49 +	    let
    1.50 +		val (thy1,th1) = rp' prf1 thy
    1.51 +		val (thy2,th2) = rp' prf2 thy1
    1.52 +	    in
    1.53 +		P.MP th1 th2 thy2
    1.54 +	    end
    1.55 +	  | rp (PHyp tm) thy = P.ASSUME tm thy
    1.56 +	  | rp (PDef(seg,name,rhs)) thy =
    1.57 +	    (case P.get_def seg name rhs thy of
    1.58 +		 (thy',Some res) => (thy',res)
    1.59 +	       | (thy',None) => 
    1.60 +		 if seg = thyname
    1.61 +		 then P.new_definition seg name rhs thy'
    1.62 +		 else raise ERR "replay_proof" "Too late for term definition")
    1.63 +	  | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    1.64 +	  | rp (PSpec(prf,tm)) thy =
    1.65 +	    let
    1.66 +		val (thy',th) = rp' prf thy
    1.67 +	    in
    1.68 +		P.SPEC tm th thy'
    1.69 +	    end
    1.70 +	  | rp (PInst(prf,theta)) thy =
    1.71 +	    let
    1.72 +		val (thy',th) = rp' prf thy
    1.73 +	    in
    1.74 +		P.INST theta th thy'
    1.75 +	    end
    1.76 +	  | rp (PGen(prf,v)) thy =
    1.77 +	    let
    1.78 +		val (thy',th) = rp' prf thy
    1.79 +	    in
    1.80 +		P.GEN v th thy'
    1.81 +	    end
    1.82 +	  | rp (PGenAbs(prf,opt,vl)) thy =
    1.83 +	    let
    1.84 +		val (thy',th) = rp' prf thy
    1.85 +	    in
    1.86 +		P.GEN_ABS opt vl th thy'
    1.87 +	    end
    1.88 +	  | rp (PImpAS(prf1,prf2)) thy =
    1.89 +	    let
    1.90 +		val (thy1,th1) = rp' prf1 thy
    1.91 +		val (thy2,th2) = rp' prf2 thy1
    1.92 +	    in
    1.93 +		P.IMP_ANTISYM th1 th2 thy2
    1.94 +	    end
    1.95 +	  | rp (PSym prf) thy =
    1.96 +	    let
    1.97 +		val (thy1,th) = rp' prf thy
    1.98 +	    in
    1.99 +		P.SYM th thy1
   1.100 +	    end
   1.101 +	  | rp (PTrans(prf1,prf2)) thy =
   1.102 +	    let
   1.103 +		val (thy1,th1) = rp' prf1 thy
   1.104 +		val (thy2,th2) = rp' prf2 thy1
   1.105 +	    in
   1.106 +		P.TRANS th1 th2 thy2
   1.107 +	    end
   1.108 +	  | rp (PComb(prf1,prf2)) thy =
   1.109 +	    let
   1.110 +		val (thy1,th1) = rp' prf1 thy
   1.111 +		val (thy2,th2) = rp' prf2 thy1
   1.112 +	    in
   1.113 +		P.COMB th1 th2 thy2
   1.114 +	    end
   1.115 +	  | rp (PEqMp(prf1,prf2)) thy =
   1.116 +	    let
   1.117 +		val (thy1,th1) = rp' prf1 thy
   1.118 +		val (thy2,th2) = rp' prf2 thy1
   1.119 +	    in
   1.120 +		P.EQ_MP th1 th2 thy2
   1.121 +	    end
   1.122 +	  | rp (PEqImp prf) thy =
   1.123 +	    let
   1.124 +		val (thy',th) = rp' prf thy
   1.125 +	    in
   1.126 +		P.EQ_IMP_RULE th thy'
   1.127 +	    end
   1.128 +	  | rp (PExists(prf,ex,wit)) thy =
   1.129 +	    let
   1.130 +		val (thy',th) = rp' prf thy
   1.131 +	    in
   1.132 +		P.EXISTS ex wit th thy'
   1.133 +	    end
   1.134 +	  | rp (PChoose(v,prf1,prf2)) thy =
   1.135 +	    let
   1.136 +		val (thy1,th1) = rp' prf1 thy
   1.137 +		val (thy2,th2) = rp' prf2 thy1
   1.138 +	    in
   1.139 +		P.CHOOSE v th1 th2 thy2
   1.140 +	    end
   1.141 +	  | rp (PConj(prf1,prf2)) thy =
   1.142 +	    let
   1.143 +		val (thy1,th1) = rp' prf1 thy
   1.144 +		val (thy2,th2) = rp' prf2 thy1
   1.145 +	    in
   1.146 +		P.CONJ th1 th2 thy2
   1.147 +	    end
   1.148 +	  | rp (PConjunct1 prf) thy =
   1.149 +	    let
   1.150 +		val (thy',th) = rp' prf thy
   1.151 +	    in
   1.152 +		P.CONJUNCT1 th thy'
   1.153 +	    end
   1.154 +	  | rp (PConjunct2 prf) thy =
   1.155 +	    let
   1.156 +		val (thy',th) = rp' prf thy
   1.157 +	    in
   1.158 +		P.CONJUNCT2 th thy'
   1.159 +	    end
   1.160 +	  | rp (PDisj1(prf,tm)) thy =
   1.161 +	    let
   1.162 +		val (thy',th) = rp' prf thy
   1.163 +	    in
   1.164 +		P.DISJ1 th tm thy'
   1.165 +	    end
   1.166 +	  | rp (PDisj2(prf,tm)) thy =
   1.167 +	    let
   1.168 +		val (thy',th) = rp' prf thy
   1.169 +	    in
   1.170 +		P.DISJ2 tm th thy'
   1.171 +	    end
   1.172 +	  | rp (PDisjCases(prf,prf1,prf2)) thy =
   1.173 +	    let
   1.174 +		val (thy',th)  = rp' prf  thy
   1.175 +		val (thy1,th1) = rp' prf1 thy'
   1.176 +		val (thy2,th2) = rp' prf2 thy1
   1.177 +	    in
   1.178 +		P.DISJ_CASES th th1 th2 thy2
   1.179 +	    end
   1.180 +	  | rp (PNotI prf) thy =
   1.181 +	    let
   1.182 +		val (thy',th) = rp' prf thy
   1.183 +	    in
   1.184 +		P.NOT_INTRO th thy'
   1.185 +	    end
   1.186 +	  | rp (PNotE prf) thy =
   1.187 +	    let
   1.188 +		val (thy',th) = rp' prf thy
   1.189 +	    in
   1.190 +		P.NOT_ELIM th thy'
   1.191 +	    end
   1.192 +	  | rp (PContr(prf,tm)) thy =
   1.193 +	    let
   1.194 +		val (thy',th) = rp' prf thy
   1.195 +	    in
   1.196 +		P.CCONTR tm th thy'
   1.197 +	    end
   1.198 +	  | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
   1.199 +	  | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
   1.200 +	  | rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)"
   1.201 +	  | rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)"
   1.202 +	  | rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?"
   1.203 +	and rp' p thy =
   1.204 +	    let
   1.205 +		val pc = content_of p
   1.206 +	    in
   1.207 +		case pc of
   1.208 +		    PDisk => (case disk_info_of p of
   1.209 +				  Some(thyname',thmname) =>
   1.210 +				  (case Int.fromString thmname of
   1.211 +				       SOME i =>
   1.212 +				       if thyname' = thyname
   1.213 +				       then
   1.214 +					   (case Array.sub(int_thms,i-1) of
   1.215 +						None =>
   1.216 +						let
   1.217 +						    val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
   1.218 +						    val _ = Array.update(int_thms,i-1,Some th)
   1.219 +						in
   1.220 +						    (thy',th)
   1.221 +						end
   1.222 +					      | Some th => (thy,th))
   1.223 +				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
   1.224 +				     | NONE => 
   1.225 +				       (case P.get_thm thyname' thmname thy of
   1.226 +					    (thy',Some res) => (thy',res)
   1.227 +					  | (thy',None) => 
   1.228 +					    if thyname' = thyname
   1.229 +					    then
   1.230 +						let
   1.231 +						    val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
   1.232 +						    val (f_opt,prf) = import_proof thyname' thmname thy'
   1.233 +						    val prf = prf thy'
   1.234 +						    val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
   1.235 +						in
   1.236 +						    case content_of prf of
   1.237 +							PTmSpec _ => (thy',th)
   1.238 +						      | PTyDef  _ => (thy',th)
   1.239 +						      | PTyIntro _ => (thy',th)
   1.240 +						      | _ => P.store_thm thyname' thmname th thy'
   1.241 +						end
   1.242 +					    else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
   1.243 +				| None => raise ERR "rp'.PDisk" "Not enough information")
   1.244 +		  | PAxm(name,c) =>
   1.245 +		    (case P.get_axiom thyname name thy of
   1.246 +			    (thy',Some res) => (thy',res)
   1.247 +			  | (thy',None) => P.new_axiom name c thy')
   1.248 +		  | PTmSpec(seg,names,prf') =>
   1.249 +		    let
   1.250 +			val (thy',th) = rp' prf' thy
   1.251 +		    in
   1.252 +			P.new_specification seg thmname names th thy'
   1.253 +		    end
   1.254 +		  | PTyDef(seg,name,prf') =>
   1.255 +		    let
   1.256 +			val (thy',th) = rp' prf' thy
   1.257 +		    in
   1.258 +			P.new_type_definition seg thmname name th thy'
   1.259 +		    end
   1.260 +		  | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
   1.261 +		    let
   1.262 +			val (thy',th) = rp' prf' thy
   1.263 +		    in
   1.264 +			P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   1.265 +		    end
   1.266 +		  | _ => rp pc thy
   1.267 +	    end
   1.268 +    in
   1.269 +	rp' prf thy handle e => (writeln "Exception in replay_proof"; print_exn e)
   1.270 +    end
   1.271 +
   1.272 +fun setup_int_thms thyname thy =
   1.273 +    let
   1.274 +	val is = TextIO.openIn(P.get_proof_dir thyname thy ^"/facts.lst")
   1.275 +	val (num_int_thms,facts) =
   1.276 +	    let
   1.277 +		fun get_facts facts =
   1.278 +		    case TextIO.inputLine is of
   1.279 +			"" => (case facts of
   1.280 +				   i::facts => (valOf (Int.fromString i),rev facts)
   1.281 +				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
   1.282 +		      | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   1.283 +	    in
   1.284 +		get_facts []
   1.285 +	    end
   1.286 +	val _ = TextIO.closeIn is
   1.287 +	val int_thms = Array.array(num_int_thms,None:thm option)
   1.288 +    in
   1.289 +	(int_thms,facts)
   1.290 +    end
   1.291 +
   1.292 +fun import_single_thm thyname int_thms thmname thy =
   1.293 +    let
   1.294 +	fun replay_fact (thmname,thy) =
   1.295 +	    let
   1.296 +		val _ = writeln ("Replaying " ^ thmname)
   1.297 +		val prf = mk_proof PDisk
   1.298 +		val _ = set_disk_info_of prf thyname thmname
   1.299 +	    in
   1.300 +		fst (replay_proof int_thms thyname thmname prf thy)
   1.301 +	    end
   1.302 +    in
   1.303 +	replay_fact (thmname,thy)
   1.304 +    end
   1.305 +
   1.306 +fun import_thms thyname int_thms thmnames thy =
   1.307 +    let
   1.308 +	fun replay_fact (thy,thmname) =
   1.309 +	    let
   1.310 +		val _ = writeln ("Replaying " ^ thmname)
   1.311 +		val prf = mk_proof PDisk
   1.312 +		val _ = set_disk_info_of prf thyname thmname
   1.313 +	    in
   1.314 +		fst (replay_proof int_thms thyname thmname prf thy)
   1.315 +	    end
   1.316 +	val res_thy = foldl replay_fact (thy,thmnames)
   1.317 +    in
   1.318 +	res_thy
   1.319 +    end
   1.320 +
   1.321 +fun import_thm thyname thmname thy =
   1.322 +    let
   1.323 +	val int_thms = fst (setup_int_thms thyname thy)
   1.324 +	fun replay_fact (thmname,thy) =
   1.325 +	    let
   1.326 +		val _ = writeln ("Replaying " ^ thmname)
   1.327 +		val prf = mk_proof PDisk
   1.328 +		val _ = set_disk_info_of prf thyname thmname
   1.329 +	    in
   1.330 +		fst (replay_proof int_thms thyname thmname prf thy)
   1.331 +	    end
   1.332 +    in
   1.333 +	replay_fact (thmname,thy)
   1.334 +    end
   1.335 +
   1.336 +end