48 |
48 |
49 |
49 |
50 (* Logical constants *) |
50 (* Logical constants *) |
51 |
51 |
52 val not = Const (@{const_name Not}, oT --> oT); |
52 val not = Const (@{const_name Not}, oT --> oT); |
53 val conj = Const(@{const_name "op &"}, [oT,oT]--->oT); |
53 val conj = Const(@{const_name conj}, [oT,oT]--->oT); |
54 val disj = Const(@{const_name "op |"}, [oT,oT]--->oT); |
54 val disj = Const(@{const_name disj}, [oT,oT]--->oT); |
55 val imp = Const(@{const_name "op -->"}, [oT,oT]--->oT) |
55 val imp = Const(@{const_name imp}, [oT,oT]--->oT) |
56 val iff = Const(@{const_name "op <->"}, [oT,oT]--->oT); |
56 val iff = Const(@{const_name iff}, [oT,oT]--->oT); |
57 |
57 |
58 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
58 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
59 and mk_disj (t1, t2) = disj $ t1 $ t2 |
59 and mk_disj (t1, t2) = disj $ t1 $ t2 |
60 and mk_imp (t1, t2) = imp $ t1 $ t2 |
60 and mk_imp (t1, t2) = imp $ t1 $ t2 |
61 and mk_iff (t1, t2) = iff $ t1 $ t2; |
61 and mk_iff (t1, t2) = iff $ t1 $ t2; |
62 |
62 |
63 fun dest_imp (Const(@{const_name "op -->"},_) $ A $ B) = (A, B) |
63 fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B) |
64 | dest_imp t = raise TERM ("dest_imp", [t]); |
64 | dest_imp t = raise TERM ("dest_imp", [t]); |
65 |
65 |
66 fun dest_conj (Const (@{const_name "op &"}, _) $ t $ t') = t :: dest_conj t' |
66 fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t' |
67 | dest_conj t = [t]; |
67 | dest_conj t = [t]; |
68 |
68 |
69 fun dest_iff (Const(@{const_name "op <->"},_) $ A $ B) = (A, B) |
69 fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B) |
70 | dest_iff t = raise TERM ("dest_iff", [t]); |
70 | dest_iff t = raise TERM ("dest_iff", [t]); |
71 |
71 |
72 fun eq_const T = Const (@{const_name "op ="}, [T, T] ---> oT); |
72 fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT); |
73 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
73 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
74 |
74 |
75 fun dest_eq (Const (@{const_name "op ="}, _) $ lhs $ rhs) = (lhs, rhs) |
75 fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs) |
76 | dest_eq t = raise TERM ("dest_eq", [t]) |
76 | dest_eq t = raise TERM ("dest_eq", [t]) |
77 |
77 |
78 fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT); |
78 fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT); |
79 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P)); |
79 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P)); |
80 |
80 |