author | wenzelm |
Sun, 11 Nov 2001 21:32:12 +0100 | |
changeset 12140 | a987beab002d |
parent 11764 | fd780dd6e0b4 |
child 12241 | c4a2a0686238 |
permissions | -rw-r--r-- |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/auto_bind.ML |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
8807 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
5 |
|
10359 | 6 |
Logic specific patterns and automatic term bindings. |
7675 | 7 |
|
8227 | 8 |
Note: the current implementation is not quite 'generic', but works |
10359 | 9 |
fine with common object-logics (HOL, FOL, ZF etc.). |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
10 |
*) |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
11 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
12 |
signature AUTO_BIND = |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
13 |
sig |
12140 | 14 |
val goal: Sign.sg -> term list -> (indexname * term option) list |
15 |
val facts: Sign.sg -> term list -> (indexname * term option) list |
|
9296 | 16 |
val thesisN: string |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
17 |
end; |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
18 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
19 |
structure AutoBind: AUTO_BIND = |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
20 |
struct |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
21 |
|
10359 | 22 |
(** bindings **) |
23 |
||
24 |
val thesisN = "thesis"; |
|
25 |
val thisN = "this"; |
|
26 |
||
11764 | 27 |
fun strip_judgment sg = ObjectLogic.drop_judgment sg o Logic.strip_assums_concl; |
28 |
||
29 |
fun statement_binds sg name prop = |
|
30 |
[((name, 0), Some (Term.list_abs (Logic.strip_params prop, strip_judgment sg prop)))]; |
|
10359 | 31 |
|
32 |
||
33 |
(* goal *) |
|
34 |
||
12140 | 35 |
fun goal sg props = statement_binds sg thesisN (Library.last_elem props); |
10359 | 36 |
|
37 |
||
38 |
(* facts *) |
|
39 |
||
11764 | 40 |
fun get_arg sg prop = |
41 |
(case strip_judgment sg prop of |
|
10808 | 42 |
_ $ t => Some (Term.list_abs (Logic.strip_params prop, t)) |
10359 | 43 |
| _ => None); |
44 |
||
12140 | 45 |
fun facts _ [] = [] |
46 |
| facts sg props = |
|
10359 | 47 |
let val prop = Library.last_elem props |
11764 | 48 |
in [(Syntax.dddot_indexname, get_arg sg prop)] @ statement_binds sg thisN prop end; |
10359 | 49 |
|
10808 | 50 |
|
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
51 |
end; |