author  paulson 
Wed, 03 Dec 1997 10:48:16 +0100  
changeset 4349  50403e5a44c0 
child 4466  305390f23734 
permissions  rwrr 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

1 
(* Title: FOL/fologic.ML 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

2 
ID: $Id$ 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

4 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

5 
Abstract syntax operations for FOL. 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

6 
*) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

7 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

8 
signature FOLOGIC = 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

9 
sig 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

10 
val oT: typ 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

11 
val mk_Trueprop: term > term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

12 
val dest_Trueprop: term > term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

13 
val conj: term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

14 
val disj: term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

15 
val imp: term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

16 
val eq_const: typ > term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

17 
val all_const: typ > term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

18 
val exists_const: typ > term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

19 
val mk_eq: term * term > term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

20 
val mk_all: term * term > term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

21 
val mk_exists: term * term > term 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

22 
end; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

23 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

24 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

25 
structure FOLogic: FOLOGIC = 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

26 
struct 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

27 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

28 
val oT = Type("o",[]); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

29 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

30 
val Trueprop = Const("Trueprop", oT>propT); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

31 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

32 
fun mk_Trueprop P = Trueprop $ P; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

33 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

34 
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

35 
 dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

36 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

37 
(** Logical constants **) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

38 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

39 
val conj = Const("op &", [oT,oT]>oT) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

40 
and disj = Const("op ", [oT,oT]>oT) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

41 
and imp = Const("op >", [oT,oT]>oT); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

42 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

43 
fun eq_const T = Const ("op =", [T, T] > oT); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

44 
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

45 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

46 
fun all_const T = Const ("All", [T > oT] > oT); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

47 
fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P)); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

48 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

49 
fun exists_const T = Const ("Ex", [T > oT] > oT); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

50 
fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P)); 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

51 

50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

52 
end; 