author | wenzelm |
Thu, 16 Feb 2006 18:25:58 +0100 | |
changeset 19075 | 12833c7e0fa6 |
parent 18605 | b971e113dee7 |
child 21448 | 09c953c07008 |
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 |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
4 |
|
17349 | 5 |
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
|
6 |
*) |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
7 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
8 |
signature AUTO_BIND = |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
9 |
sig |
17349 | 10 |
val rule_contextN: string |
9296 | 11 |
val thesisN: string |
17349 | 12 |
val thisN: string |
19075 | 13 |
val premsN: string |
17349 | 14 |
val goal: theory -> term list -> (indexname * term option) list |
15 |
val cases: theory -> term list -> (string * RuleCases.T option) list |
|
16 |
val facts: theory -> term list -> (indexname * term option) list |
|
17852 | 17 |
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
|
18 |
end; |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
19 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
20 |
structure AutoBind: AUTO_BIND = |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
21 |
struct |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
22 |
|
10359 | 23 |
(** bindings **) |
24 |
||
17349 | 25 |
val rule_contextN = "rule_context"; |
10359 | 26 |
val thesisN = "thesis"; |
27 |
val thisN = "this"; |
|
19075 | 28 |
val premsN = "prems"; |
10359 | 29 |
|
17349 | 30 |
fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl; |
11764 | 31 |
|
17349 | 32 |
fun statement_binds thy name prop = |
33 |
[((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))]; |
|
10359 | 34 |
|
35 |
||
36 |
(* goal *) |
|
37 |
||
17349 | 38 |
fun goal thy [prop] = statement_binds thy thesisN prop |
15531 | 39 |
| goal _ _ = [((thesisN, 0), NONE)]; |
10359 | 40 |
|
18605 | 41 |
fun cases thy [prop] = RuleCases.make_simple true (thy, prop) rule_contextN |
42 |
| cases _ _ = [(rule_contextN, NONE)]; |
|
17349 | 43 |
|
10359 | 44 |
|
45 |
(* facts *) |
|
46 |
||
17349 | 47 |
fun get_arg thy prop = |
48 |
(case strip_judgment thy prop of |
|
15531 | 49 |
_ $ t => SOME (Term.list_abs (Logic.strip_params prop, t)) |
50 |
| _ => NONE); |
|
10359 | 51 |
|
12140 | 52 |
fun facts _ [] = [] |
17349 | 53 |
| facts thy props = |
10359 | 54 |
let val prop = Library.last_elem props |
17349 | 55 |
in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end; |
10359 | 56 |
|
17852 | 57 |
val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)]; |
10808 | 58 |
|
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
59 |
end; |