author | wenzelm |
Fri, 03 Nov 2000 21:25:30 +0100 | |
changeset 10377 | 6b595f9ae37e |
parent 10359 | 445e3b87f28b |
child 10808 | cc4a3ed7e70b |
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 |
|
10359 | 6 |
Logic specific patterns and automatic term bindings. |
7675 | 7 |
|
8227 | 8 |
Note: the current implementation is not quite 'generic', but works |
10359 | 9 |
fine with 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 |
10359 | 14 |
val is_judgment: term -> bool |
10377 | 15 |
val atomic_judgment: theory -> string -> term |
10359 | 16 |
val add_judgment: bstring * string * mixfix -> theory -> theory |
17 |
val add_judgment_i: bstring * typ * mixfix -> theory -> theory |
|
7599 | 18 |
val goal: term -> (indexname * term option) list |
19 |
val facts: string -> term list -> (indexname * term option) list |
|
9296 | 20 |
val thesisN: string |
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
21 |
end; |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
22 |
|
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
23 |
structure AutoBind: AUTO_BIND = |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
24 |
struct |
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
25 |
|
9464 | 26 |
|
27 |
(** judgments **) |
|
7675 | 28 |
|
10377 | 29 |
val TruepropN = "Trueprop"; |
30 |
||
10359 | 31 |
fun strip_judgment prop = |
10377 | 32 |
(case Logic.strip_assums_concl prop of |
33 |
tm as (Const (c, _) $ t) => if c = TruepropN then t else tm |
|
34 |
| tm => tm); |
|
35 |
||
36 |
fun is_judgment (Const (c, _) $ _) = c = TruepropN |
|
37 |
| is_judgment _ = false; |
|
10359 | 38 |
|
10377 | 39 |
fun atomic_judgment thy x = |
40 |
let (*be robust wrt. low-level errors*) |
|
41 |
val aT = TFree ("'a", logicS); |
|
42 |
val T = |
|
43 |
if_none (Sign.const_type (Theory.sign_of thy) TruepropN) (aT --> propT) |
|
44 |
|> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S)); |
|
45 |
val U = Term.domain_type T handle Match => aT; |
|
46 |
in Const (TruepropN, T) $ Free (x, U) end; |
|
8227 | 47 |
|
48 |
||
9464 | 49 |
fun gen_add_judgment add (name, T, syn) thy = |
10377 | 50 |
if name = TruepropN then |
9464 | 51 |
thy |> PureThy.global_path |> add [(name, T, syn)] |> PureThy.local_path |
10377 | 52 |
else error ("Judgment name has to be " ^ quote TruepropN); |
8227 | 53 |
|
54 |
val add_judgment = gen_add_judgment Theory.add_consts; |
|
55 |
val add_judgment_i = gen_add_judgment Theory.add_consts_i; |
|
56 |
||
6796 | 57 |
|
10359 | 58 |
|
59 |
(** bindings **) |
|
60 |
||
61 |
val thesisN = "thesis"; |
|
62 |
val thisN = "this"; |
|
63 |
||
64 |
fun list_abs parms tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm); |
|
65 |
||
66 |
fun statement_binds name prop = |
|
67 |
[((name, 0), Some (list_abs (Logic.strip_params prop) (strip_judgment prop)))]; |
|
68 |
||
69 |
||
70 |
(* goal *) |
|
71 |
||
72 |
fun goal prop = statement_binds thesisN prop; |
|
73 |
||
74 |
||
75 |
(* facts *) |
|
76 |
||
77 |
fun get_arg prop = |
|
78 |
(case strip_judgment prop of |
|
79 |
_ $ t => Some (list_abs (Logic.strip_params prop) t) |
|
80 |
| _ => None); |
|
81 |
||
82 |
fun facts _ [] = [] |
|
83 |
| facts name props = |
|
84 |
let val prop = Library.last_elem props |
|
85 |
in [(Syntax.dddot_indexname, get_arg prop)] @ statement_binds thisN prop end; |
|
86 |
||
6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset
|
87 |
end; |