author | wenzelm |
Thu, 03 Aug 2000 18:43:35 +0200 | |
changeset 9512 | c30f6d0f81d2 |
parent 9464 | e290583864e4 |
child 10359 | 445e3b87f28b |
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 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
6 |
Automatic term bindings -- logic specific patterns. |
7675 | 7 |
|
8227 | 8 |
Note: the current implementation is not quite 'generic', but works |
9 |
fine with the more 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 |
7599 | 14 |
val goal: term -> (indexname * term option) list |
15 |
val facts: string -> term list -> (indexname * term option) list |
|
9296 | 16 |
val thesisN: string |
9464 | 17 |
val is_judgment: term -> bool |
8227 | 18 |
val add_judgment: bstring * string * mixfix -> theory -> theory |
19 |
val add_judgment_i: bstring * typ * mixfix -> theory -> theory |
|
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
20 |
end; |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
21 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
22 |
structure AutoBind: AUTO_BIND = |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
23 |
struct |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
24 |
|
7675 | 25 |
val thesisN = "thesis"; |
26 |
val thisN = "this"; |
|
6796 | 27 |
|
7675 | 28 |
|
8227 | 29 |
(** bindings **) |
30 |
||
8612 | 31 |
fun list_abs parms tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm); |
32 |
||
33 |
||
7675 | 34 |
(* goal *) |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
35 |
|
6796 | 36 |
fun statement_binds (name, prop) = |
37 |
let |
|
7331 | 38 |
val concl = Logic.strip_assums_concl prop; |
39 |
val parms = Logic.strip_params prop; |
|
40 |
||
8612 | 41 |
val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs parms concl)), |
42 |
(name, case concl of Const ("Trueprop", _) $ t => Some (list_abs parms t) | _ => None)]; |
|
7474 | 43 |
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
|
44 |
|
7675 | 45 |
fun goal prop = statement_binds (thesisN, prop); |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
46 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
47 |
|
6796 | 48 |
(* facts *) |
49 |
||
8612 | 50 |
fun get_subject prop = |
51 |
(case (Logic.strip_assums_concl prop) of |
|
52 |
Const ("Trueprop", _) $ (_ $ t) => Some (list_abs (Logic.strip_params prop) t) |
|
53 |
| _ => None); |
|
6796 | 54 |
|
55 |
fun facts _ [] = [] |
|
7452 | 56 |
| facts name props = |
57 |
let val prop = Library.last_elem props |
|
8612 | 58 |
in [(Syntax.dddot_indexname, get_subject prop)] @ statement_binds (thisN, prop) end; |
7675 | 59 |
|
60 |
||
9464 | 61 |
|
62 |
(** judgments **) |
|
7675 | 63 |
|
9464 | 64 |
fun is_judgment (Const ("Trueprop", _) $ _) = true |
65 |
| is_judgment _ = false; |
|
8227 | 66 |
|
67 |
||
9464 | 68 |
fun gen_add_judgment add (name, T, syn) thy = |
69 |
if name = "Trueprop" then |
|
70 |
thy |> PureThy.global_path |> add [(name, T, syn)] |> PureThy.local_path |
|
71 |
else error "Judgment name has to be \"Trueprop\""; |
|
8227 | 72 |
|
73 |
val add_judgment = gen_add_judgment Theory.add_consts; |
|
74 |
val add_judgment_i = gen_add_judgment Theory.add_consts_i; |
|
75 |
||
6796 | 76 |
|
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
77 |
end; |