author  wenzelm 
Sun, 30 Jul 2000 13:02:14 +0200  
changeset 9473  7d13a5ace928 
parent 7692  89bbce6f5c17 
child 9543  ce61d1c1a509 
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 

9473  12 
val atomic_Trueprop : string > term 
6140  13 
val dest_Trueprop : term > term 
14 
val conj : term 

15 
val disj : term 

16 
val imp : term 

7692  17 
val mk_conj : term * term > term 
18 
val mk_disj : term * term > term 

19 
val mk_imp : term * term > term 

6140  20 
val dest_imp : term > term*term 
21 
val all_const : typ > term 

22 
val mk_all : term * term > term 

23 
val exists_const : typ > term 

24 
val mk_exists : term * term > term 

25 
val eq_const : typ > term 

26 
val mk_eq : term * term > term 

27 
val dest_eq : term > term*term 

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

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

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

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

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

39 

9473  40 
fun atomic_Trueprop x = mk_Trueprop (Free (x, oT)); 
41 

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

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

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

44 

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

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

46 

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

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

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

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

50 

7692  51 
fun mk_conj (t1, t2) = conj $ t1 $ t2 
52 
and mk_disj (t1, t2) = disj $ t1 $ t2 

53 
and mk_imp (t1, t2) = imp $ t1 $ t2; 

54 

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

55 
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

56 
 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

57 

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

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

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

60 

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

63 

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

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

65 
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

66 

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

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

68 
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

69 

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

70 
end; 