author | blanchet |
Wed, 11 Jun 2014 19:32:12 +0200 | |
changeset 57221 | d82c22eb9bea |
parent 44241 | 7943b69f0188 |
child 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
1 |
(* Title: FOL/fologic.ML |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
3 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
4 |
Abstract syntax operations for FOL. |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
5 |
*) |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
6 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
7 |
signature FOLOGIC = |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
8 |
sig |
32449 | 9 |
val oT: typ |
10 |
val mk_Trueprop: term -> term |
|
11 |
val dest_Trueprop: term -> term |
|
12 |
val not: term |
|
13 |
val conj: term |
|
14 |
val disj: term |
|
15 |
val imp: term |
|
16 |
val iff: term |
|
17 |
val mk_conj: term * term -> term |
|
18 |
val mk_disj: term * term -> term |
|
19 |
val mk_imp: term * term -> term |
|
20 |
val dest_imp: term -> term * term |
|
21 |
val dest_conj: term -> term list |
|
22 |
val mk_iff: term * term -> term |
|
23 |
val dest_iff: term -> term * term |
|
24 |
val all_const: typ -> term |
|
25 |
val mk_all: term * term -> term |
|
26 |
val exists_const: typ -> term |
|
27 |
val mk_exists: term * term -> term |
|
28 |
val eq_const: typ -> term |
|
29 |
val mk_eq: term * term -> term |
|
30 |
val dest_eq: term -> term * term |
|
9543 | 31 |
val mk_binop: string -> term * term -> term |
32 |
val mk_binrel: string -> term * term -> term |
|
33 |
val dest_bin: string -> typ -> term -> term * term |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
34 |
end; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
35 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
36 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
37 |
structure FOLogic: FOLOGIC = |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
38 |
struct |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
39 |
|
38500 | 40 |
val oT = Type(@{type_name o},[]); |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
41 |
|
38500 | 42 |
val Trueprop = Const(@{const_name Trueprop}, oT-->propT); |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
43 |
|
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
44 |
fun mk_Trueprop P = Trueprop $ P; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
45 |
|
38500 | 46 |
fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
47 |
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
48 |
|
32449 | 49 |
|
50 |
(* Logical constants *) |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
51 |
|
38500 | 52 |
val not = Const (@{const_name Not}, oT --> oT); |
41310 | 53 |
val conj = Const(@{const_name conj}, [oT,oT]--->oT); |
54 |
val disj = Const(@{const_name disj}, [oT,oT]--->oT); |
|
55 |
val imp = Const(@{const_name imp}, [oT,oT]--->oT) |
|
56 |
val iff = Const(@{const_name iff}, [oT,oT]--->oT); |
|
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
57 |
|
7692 | 58 |
fun mk_conj (t1, t2) = conj $ t1 $ t2 |
59 |
and mk_disj (t1, t2) = disj $ t1 $ t2 |
|
9543 | 60 |
and mk_imp (t1, t2) = imp $ t1 $ t2 |
61 |
and mk_iff (t1, t2) = iff $ t1 $ t2; |
|
7692 | 62 |
|
41310 | 63 |
fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B) |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4349
diff
changeset
|
64 |
| 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
|
65 |
|
41310 | 66 |
fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t' |
11668 | 67 |
| dest_conj t = [t]; |
68 |
||
41310 | 69 |
fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B) |
9543 | 70 |
| dest_iff t = raise TERM ("dest_iff", [t]); |
71 |
||
41310 | 72 |
fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT); |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
73 |
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
74 |
|
41310 | 75 |
fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs) |
6140 | 76 |
| dest_eq t = raise TERM ("dest_eq", [t]) |
77 |
||
38500 | 78 |
fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT); |
44241 | 79 |
fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P; |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
80 |
|
38500 | 81 |
fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT); |
44241 | 82 |
fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P; |
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
83 |
|
32449 | 84 |
|
9543 | 85 |
(* binary oprations and relations *) |
86 |
||
87 |
fun mk_binop c (t, u) = |
|
88 |
let val T = fastype_of t in |
|
89 |
Const (c, [T, T] ---> T) $ t $ u |
|
90 |
end; |
|
91 |
||
92 |
fun mk_binrel c (t, u) = |
|
93 |
let val T = fastype_of t in |
|
94 |
Const (c, [T, T] ---> oT) $ t $ u |
|
95 |
end; |
|
96 |
||
97 |
fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) = |
|
98 |
if c = c' andalso T = T' then (t, u) |
|
99 |
else raise TERM ("dest_bin " ^ c, [tm]) |
|
100 |
| dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]); |
|
101 |
||
4349
50403e5a44c0
Instantiated the one-point-rule quantifier simpprocs for FOL
paulson
parents:
diff
changeset
|
102 |
end; |