author | blanchet |
Fri, 01 Aug 2014 14:43:57 +0200 | |
changeset 57743 | 0af2d5dfb0ac |
parent 46219 | 426ed18eba43 |
child 59970 | e9f73d87d904 |
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 |
21448 | 11 |
val assmsN: string |
17349 | 12 |
val goal: theory -> term list -> (indexname * term option) list |
13 |
val facts: theory -> term list -> (indexname * term option) list |
|
17852 | 14 |
val no_facts: (indexname * term option) list |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
15 |
end; |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
16 |
|
33386 | 17 |
structure Auto_Bind: AUTO_BIND = |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
18 |
struct |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
19 |
|
10359 | 20 |
(** bindings **) |
21 |
||
22 |
val thesisN = "thesis"; |
|
23 |
val thisN = "this"; |
|
21448 | 24 |
val assmsN = "assms"; |
10359 | 25 |
|
35625 | 26 |
fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl; |
11764 | 27 |
|
17349 | 28 |
fun statement_binds thy name prop = |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42288
diff
changeset
|
29 |
[((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment thy prop)))]; |
10359 | 30 |
|
31 |
||
32 |
(* goal *) |
|
33 |
||
17349 | 34 |
fun goal thy [prop] = statement_binds thy thesisN prop |
15531 | 35 |
| goal _ _ = [((thesisN, 0), NONE)]; |
10359 | 36 |
|
37 |
||
38 |
(* facts *) |
|
39 |
||
17349 | 40 |
fun get_arg thy prop = |
41 |
(case strip_judgment thy prop of |
|
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42288
diff
changeset
|
42 |
_ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t) |
15531 | 43 |
| _ => NONE); |
10359 | 44 |
|
12140 | 45 |
fun facts _ [] = [] |
17349 | 46 |
| facts thy props = |
41489
8e2b8649507d
standardized split_last/last_elem towards List.last;
wenzelm
parents:
35625
diff
changeset
|
47 |
let val prop = List.last props |
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
41489
diff
changeset
|
48 |
in [(Syntax_Ext.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end; |
10359 | 49 |
|
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
41489
diff
changeset
|
50 |
val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)]; |
10808 | 51 |
|
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
52 |
end; |