author | wenzelm |
Wed, 10 Jun 2015 14:46:31 +0200 | |
changeset 60414 | f25f2f2ba48c |
parent 60408 | 1fd46ced2fa8 |
child 60448 | 78f3c67bc35e |
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 |
Author: Markus Wenzel, TU Muenchen |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
3 |
|
17349 | 4 |
Automatic bindings of Isar text elements. |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
5 |
*) |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
6 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
7 |
signature AUTO_BIND = |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
8 |
sig |
9296 | 9 |
val thesisN: string |
17349 | 10 |
val thisN: string |
60414 | 11 |
val premsN: string |
21448 | 12 |
val assmsN: string |
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
13 |
val abs_params: term -> term -> term |
59970 | 14 |
val goal: Proof.context -> term list -> (indexname * term option) list |
15 |
val facts: Proof.context -> term list -> (indexname * term option) list |
|
60401 | 16 |
val no_facts: indexname list |
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 |
|
33386 | 19 |
structure Auto_Bind: AUTO_BIND = |
6783
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"; |
|
21448 | 26 |
val assmsN = "assms"; |
60414 | 27 |
val premsN = "prems"; |
10359 | 28 |
|
59970 | 29 |
fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl; |
11764 | 30 |
|
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
31 |
fun abs_params prop = fold_rev Term.abs (Logic.strip_params prop); |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
32 |
|
59970 | 33 |
fun statement_binds ctxt name prop = |
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
34 |
[((name, 0), SOME (abs_params prop (strip_judgment ctxt prop)))]; |
10359 | 35 |
|
36 |
||
37 |
(* goal *) |
|
38 |
||
59970 | 39 |
fun goal ctxt [prop] = statement_binds ctxt thesisN prop |
15531 | 40 |
| goal _ _ = [((thesisN, 0), NONE)]; |
10359 | 41 |
|
42 |
||
43 |
(* facts *) |
|
44 |
||
59970 | 45 |
fun get_arg ctxt prop = |
46 |
(case strip_judgment ctxt prop of |
|
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
47 |
_ $ t => SOME (abs_params prop t) |
15531 | 48 |
| _ => NONE); |
10359 | 49 |
|
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
50 |
fun facts ctxt props = |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
51 |
(case try List.last props of |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
52 |
NONE => [] |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
53 |
| SOME prop => |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60401
diff
changeset
|
54 |
[(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop); |
10359 | 55 |
|
60401 | 56 |
val no_facts = [Syntax_Ext.dddot_indexname, (thisN, 0)]; |
10808 | 57 |
|
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
58 |
end; |