author  paulson 
Tue, 19 Jan 1999 11:16:39 +0100  
changeset 6140  af32e2c3f77a 
parent 4466  305390f23734 
child 7692  89bbce6f5c17 
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 
6140  10 
val oT : typ 
11 
val mk_Trueprop : term > term 

12 
val dest_Trueprop : term > term 

13 
val conj : term 

14 
val disj : term 

15 
val imp : term 

16 
val dest_imp : term > term*term 

17 
val all_const : typ > term 

18 
val mk_all : term * term > term 

19 
val exists_const : typ > term 

20 
val mk_exists : term * term > term 

21 
val eq_const : typ > term 

22 
val mk_eq : term * term > term 

23 
val dest_eq : term > term*term 

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

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

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

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

28 
struct 
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 oT = Type("o",[]); 
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 
val Trueprop = Const("Trueprop", oT>propT); 
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 mk_Trueprop P = Trueprop $ P; 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

35 

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

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

37 
 dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); 
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 
(** Logical constants **) 
50403e5a44c0
Instantiated the onepointrule quantifier simpprocs for FOL
paulson
parents:
diff
changeset

40 

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

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

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

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

44 

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

45 
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

46 
 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

47 

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

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

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

50 

6140  51 
fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs) 
52 
 dest_eq t = raise TERM ("dest_eq", [t]) 

53 

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

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

55 
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

56 

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

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

58 
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

59 

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

60 
end; 