author  paulson 
Tue, 23 Dec 1997 11:39:03 +0100  
changeset 4466  305390f23734 
parent 4349  50403e5a44c0 
child 6140  af32e2c3f77a 
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 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4349
diff
changeset

13 
val dest_imp : term > term*term 
4349
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

23 
end; 
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 

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

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

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

28 

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

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

30 

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

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

32 

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

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

34 

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

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

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

37 

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

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

39 

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

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

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

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

43 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4349
diff
changeset

44 
fun dest_imp (Const("op >",_) $ A $ B) = (A, B) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4349
diff
changeset

45 
 dest_imp t = raise TERM ("dest_imp", [t]); 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4349
diff
changeset

46 

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

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

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

49 

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

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

51 
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

52 

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

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

54 
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

55 

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

56 
end; 