author  wenzelm 
Mon, 19 Jul 1999 21:26:33 +0200  
changeset 7048  3535eec33c50 
parent 6796  c2e5cb8cd50d 
child 7331  aee8f76fe54c 
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 

22 
val concl = Logic.strip_imp_concl prop; 

23 
val env = [(name ^ "_prop", prop), (name ^ "_concl", concl)] @ 

24 
(case concl of Const ("Trueprop", _) $ t => [(name, t)]  _ => []); 

25 
in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end; 

6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset

26 

6796  27 
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

28 

9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset

29 

6796  30 
(* facts *) 
31 

32 
fun dddot_bind prop = 

33 
(case Logic.strip_imp_concl prop of 

34 
Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)] 

35 
 _ => []); 

36 

37 
fun facts _ [] = [] 

7048  38 
 facts name [prop] = dddot_bind prop 
39 
 facts name props = dddot_bind (Library.last_elem props); 

6796  40 

41 

6783
9cf9c17d9e35
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff
changeset

42 
end; 