212 prep = (case prep1 of NONE => prep2 | _ => prep1)}; |
212 prep = (case prep1 of NONE => prep2 | _ => prep1)}; |
213 |
213 |
214 fun print _ _ = (); |
214 fun print _ _ = (); |
215 end); |
215 end); |
216 |
216 |
217 val _ = Context.add_setup [ExtractionData.init]; |
217 val _ = Context.add_setup ExtractionData.init; |
218 |
218 |
219 fun read_condeq thy = |
219 fun read_condeq thy = |
220 let val thy' = add_syntax thy |
220 let val thy' = add_syntax thy |
221 in fn s => |
221 in fn s => |
222 let val t = Logic.varify (term_of (read_cterm thy' (s, propT))) |
222 let val t = Logic.varify (term_of (read_cterm thy' (s, propT))) |
399 |
399 |
400 |
400 |
401 (** Pure setup **) |
401 (** Pure setup **) |
402 |
402 |
403 val _ = Context.add_setup |
403 val _ = Context.add_setup |
404 [add_types [("prop", ([], NONE))], |
404 (add_types [("prop", ([], NONE))] #> |
405 |
405 |
406 add_typeof_eqns |
406 add_typeof_eqns |
407 ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ |
407 ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ |
408 \ (typeof (PROP Q)) == (Type (TYPE('Q))) ==> \ |
408 \ (typeof (PROP Q)) == (Type (TYPE('Q))) ==> \ |
409 \ (typeof (PROP P ==> PROP Q)) == (Type (TYPE('Q)))", |
409 \ (typeof (PROP P ==> PROP Q)) == (Type (TYPE('Q)))", |
420 |
420 |
421 "(%x. typeof (PROP P (x))) == (%x. Type (TYPE('P))) ==> \ |
421 "(%x. typeof (PROP P (x))) == (%x. Type (TYPE('P))) ==> \ |
422 \ (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))", |
422 \ (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))", |
423 |
423 |
424 "(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==> \ |
424 "(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==> \ |
425 \ (typeof (f)) == (Type (TYPE('f)))"], |
425 \ (typeof (f)) == (Type (TYPE('f)))"] #> |
426 |
426 |
427 add_realizes_eqns |
427 add_realizes_eqns |
428 ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ |
428 ["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \ |
429 \ (realizes (r) (PROP P ==> PROP Q)) == \ |
429 \ (realizes (r) (PROP P ==> PROP Q)) == \ |
430 \ (PROP realizes (Null) (PROP P) ==> PROP realizes (r) (PROP Q))", |
430 \ (PROP realizes (Null) (PROP P) ==> PROP realizes (r) (PROP Q))", |
440 "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==> \ |
440 "(%x. typeof (PROP P (x))) == (%x. Type (TYPE(Null))) ==> \ |
441 \ (realizes (r) (!!x. PROP P (x))) == \ |
441 \ (realizes (r) (!!x. PROP P (x))) == \ |
442 \ (!!x. PROP realizes (Null) (PROP P (x)))", |
442 \ (!!x. PROP realizes (Null) (PROP P (x)))", |
443 |
443 |
444 "(realizes (r) (!!x. PROP P (x))) == \ |
444 "(realizes (r) (!!x. PROP P (x))) == \ |
445 \ (!!x. PROP realizes (r (x)) (PROP P (x)))"], |
445 \ (!!x. PROP realizes (r (x)) (PROP P (x)))"] #> |
446 |
446 |
447 Attrib.add_attributes |
447 Attrib.add_attributes |
448 [("extraction_expand", |
448 [("extraction_expand", |
449 (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute), |
449 (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute), |
450 "specify theorems / definitions to be expanded during extraction")]]; |
450 "specify theorems / definitions to be expanded during extraction")]); |
451 |
451 |
452 |
452 |
453 (**** extract program ****) |
453 (**** extract program ****) |
454 |
454 |
455 val dummyt = Const ("dummy", dummyT); |
455 val dummyt = Const ("dummy", dummyT); |