author  wenzelm 
Sat, 04 Sep 1999 21:05:01 +0200  
changeset 7474  43cedde6d52a 
parent 7452  c2289eabf706 
child 7599  40b7f7f51208 
permissions  rwrr 
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; 