author  wenzelm 
Mon, 04 Oct 1999 21:35:26 +0200  
changeset 7692  89bbce6f5c17 
parent 6140  af32e2c3f77a 
child 9473  7d13a5ace928 
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 

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

18 
val mk_imp : term * term > term 

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

21 
val mk_all : term * term > term 

22 
val exists_const : typ > term 

23 
val mk_exists : term * term > term 

24 
val eq_const : typ > term 

25 
val mk_eq : term * term > term 

26 
val dest_eq : term > term*term 

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

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

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

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

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

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

41 

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

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

43 

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

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

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

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

47 

7692  48 
fun mk_conj (t1, t2) = conj $ t1 $ t2 
49 
and mk_disj (t1, t2) = disj $ t1 $ t2 

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

51 

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

52 
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

53 
 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

54 

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

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

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

57 

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

60 

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

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

62 
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

63 

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

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

65 
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

66 

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

67 
end; 