equal
deleted
inserted
replaced
|
1 (* Title: Eisbach.thy |
|
2 Author: Daniel Matichuk, NICTA/UNSW |
|
3 |
|
4 Main entry point for Eisbach proof method language. |
|
5 *) |
|
6 |
|
7 theory Eisbach |
|
8 imports Pure |
|
9 keywords |
|
10 "method" :: thy_decl and |
|
11 "concl" |
|
12 "prems" (* FIXME conflict with "prems" in Isar, which is presently dormant *) |
|
13 "declares" |
|
14 "methods" |
|
15 "\<bar>" "\<Rightarrow>" |
|
16 "uses" |
|
17 begin |
|
18 |
|
19 ML_file "parse_tools.ML" |
|
20 ML_file "eisbach_rule_insts.ML" |
|
21 ML_file "method_closure.ML" |
|
22 ML_file "match_method.ML" |
|
23 ML_file "eisbach_antiquotations.ML" |
|
24 |
|
25 (* FIXME reform Isabelle/Pure attributes to make this work by default *) |
|
26 attribute_setup THEN = |
|
27 \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm >> (fn (i, B) => |
|
28 Method_Closure.free_aware_rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close> |
|
29 "resolution with rule" |
|
30 |
|
31 attribute_setup OF = |
|
32 \<open>Attrib.thms >> (fn Bs => |
|
33 Method_Closure.free_aware_rule_attribute Bs (fn _ => fn A => A OF Bs))\<close> |
|
34 "rule resolved with facts" |
|
35 |
|
36 attribute_setup rotated = |
|
37 \<open>Scan.lift (Scan.optional Parse.int 1 >> (fn n => |
|
38 Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close> |
|
39 "rotated theorem premises" |
|
40 |
|
41 method solves methods m = \<open>m; fail\<close> |
|
42 |
|
43 end |