author | wenzelm |
Sat, 04 Sep 1999 21:05:01 +0200 | |
changeset 7474 | 43cedde6d52a |
parent 7452 | c2289eabf706 |
child 7599 | 40b7f7f51208 |
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 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
5 |
Automatic term bindings -- logic specific patterns. |
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 |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
10 |
val goal: term -> (indexname * term) list |
6796 | 11 |
val facts: string -> term list -> (indexname * term) list |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
12 |
end; |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
13 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
14 |
structure AutoBind: AUTO_BIND = |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
15 |
struct |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
16 |
|
6796 | 17 |
|
18 |
(* goals *) |
|
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
19 |
|
6796 | 20 |
fun statement_binds (name, prop) = |
21 |
let |
|
7331 | 22 |
val concl = Logic.strip_assums_concl prop; |
23 |
val parms = Logic.strip_params prop; |
|
24 |
fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm); |
|
25 |
||
26 |
val env = [(name ^ "_prop", prop), (name ^ "_concl", list_abs concl)] @ |
|
27 |
(case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []); |
|
7474 | 28 |
in map (fn (s, t) => ((s, 0), t)) env end; |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
29 |
|
6796 | 30 |
fun goal prop = statement_binds ("thesis", prop); |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
31 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
32 |
|
6796 | 33 |
(* facts *) |
34 |
||
35 |
fun dddot_bind prop = |
|
36 |
(case Logic.strip_imp_concl prop of |
|
37 |
Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)] |
|
38 |
| _ => []); |
|
39 |
||
40 |
fun facts _ [] = [] |
|
7452 | 41 |
| facts name props = |
42 |
let val prop = Library.last_elem props |
|
43 |
in dddot_bind prop @ statement_binds ("this", prop) end; |
|
6796 | 44 |
|
45 |
||
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
46 |
end; |