345 in bind_thm(name, thm) end; |
345 in bind_thm(name, thm) end; |
346 |
346 |
347 end; |
347 end; |
348 |
348 |
349 |
349 |
350 |
350 (*Thus, assignments to the references claset and simpset are recorded |
351 (*** Setting up the classical reasoner and simplifier ***) |
351 with theory "HOL". These files cannot be loaded directly in ROOT.ML.*) |
352 |
352 use "hologic.ML"; |
353 |
353 use "cladata.ML"; |
354 (** Applying HypsubstFun to generate hyp_subst_tac **) |
354 use "simpdata.ML"; |
355 section "Classical Reasoner"; |
|
356 |
|
357 structure Hypsubst_Data = |
|
358 struct |
|
359 structure Simplifier = Simplifier |
|
360 (*Take apart an equality judgement; otherwise raise Match!*) |
|
361 fun dest_eq (Const("Trueprop",_) $ (Const("op =",_) $ t $ u)) = (t,u); |
|
362 val eq_reflection = eq_reflection |
|
363 val imp_intr = impI |
|
364 val rev_mp = rev_mp |
|
365 val subst = subst |
|
366 val sym = sym |
|
367 end; |
|
368 |
|
369 structure Hypsubst = HypsubstFun(Hypsubst_Data); |
|
370 open Hypsubst; |
|
371 |
|
372 (*** Applying ClassicalFun to create a classical prover ***) |
|
373 structure Classical_Data = |
|
374 struct |
|
375 val sizef = size_of_thm |
|
376 val mp = mp |
|
377 val not_elim = notE |
|
378 val classical = classical |
|
379 val hyp_subst_tacs=[hyp_subst_tac] |
|
380 end; |
|
381 |
|
382 structure Classical = ClassicalFun(Classical_Data); |
|
383 open Classical; |
|
384 |
|
385 (*Propositional rules*) |
|
386 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] |
|
387 addSEs [conjE,disjE,impCE,FalseE,iffE]; |
|
388 |
|
389 (*Quantifier rules*) |
|
390 val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] |
|
391 addSEs [exE,ex1E] addEs [allE]; |
|
392 |
|
393 exception CS_DATA of claset; |
|
394 |
|
395 let fun merge [] = CS_DATA empty_cs |
|
396 | merge cs = let val cs = map (fn CS_DATA x => x) cs; |
|
397 in CS_DATA (foldl merge_cs (hd cs, tl cs)) end; |
|
398 |
|
399 fun put (CS_DATA cs) = claset := cs; |
|
400 |
|
401 fun get () = CS_DATA (!claset); |
|
402 in add_thydata "HOL" |
|
403 ("claset", ThyMethods {merge = merge, put = put, get = get}) |
|
404 end; |
|
405 |
|
406 claset := HOL_cs; |
|
407 |
|
408 section "Simplifier"; |
|
409 |
|
410 use "simpdata.ML"; |
|
411 simpset := HOL_ss; |
|
412 |
|
413 |
|
414 (** Install simpsets and datatypes in theory structure **) |
|
415 exception SS_DATA of simpset; |
|
416 |
|
417 let fun merge [] = SS_DATA empty_ss |
|
418 | merge ss = let val ss = map (fn SS_DATA x => x) ss; |
|
419 in SS_DATA (foldl merge_ss (hd ss, tl ss)) end; |
|
420 |
|
421 fun put (SS_DATA ss) = simpset := ss; |
|
422 |
|
423 fun get () = SS_DATA (!simpset); |
|
424 in add_thydata "HOL" |
|
425 ("simpset", ThyMethods {merge = merge, put = put, get = get}) |
|
426 end; |
|
427 |
|
428 type dtype_info = {case_const:term, case_rewrites:thm list, |
|
429 constructors:term list, nchotomy:thm, case_cong:thm}; |
|
430 |
|
431 exception DT_DATA of (string * dtype_info) list; |
|
432 val datatypes = ref [] : (string * dtype_info) list ref; |
|
433 |
|
434 let fun merge [] = DT_DATA [] |
|
435 | merge ds = |
|
436 let val ds = map (fn DT_DATA x => x) ds; |
|
437 in DT_DATA (foldl (gen_union eq_fst) (hd ds, tl ds)) end; |
|
438 |
|
439 fun put (DT_DATA ds) = datatypes := ds; |
|
440 |
|
441 fun get () = DT_DATA (!datatypes); |
|
442 in add_thydata "HOL" |
|
443 ("datatypes", ThyMethods {merge = merge, put = put, get = get}) |
|
444 end; |
|
445 |
|
446 |
|
447 add_thy_reader_file "thy_data.ML"; |
|