paulson@4349: (*  Title:      FOL/fologic.ML
paulson@4349:     Author:     Lawrence C Paulson
paulson@4349: 
paulson@4349: Abstract syntax operations for FOL.
paulson@4349: *)
paulson@4349: 
paulson@4349: signature FOLOGIC =
paulson@4349: sig
wenzelm@32449:   val oT: typ
wenzelm@32449:   val mk_Trueprop: term -> term
wenzelm@32449:   val dest_Trueprop: term -> term
wenzelm@32449:   val not: term
wenzelm@32449:   val conj: term
wenzelm@32449:   val disj: term
wenzelm@32449:   val imp: term
wenzelm@32449:   val iff: term
wenzelm@32449:   val mk_conj: term * term -> term
wenzelm@32449:   val mk_disj: term * term -> term
wenzelm@32449:   val mk_imp: term * term -> term
wenzelm@32449:   val dest_imp: term -> term * term
wenzelm@32449:   val dest_conj: term -> term list
wenzelm@32449:   val mk_iff: term * term -> term
wenzelm@32449:   val dest_iff: term -> term * term
wenzelm@32449:   val all_const: typ -> term
wenzelm@32449:   val mk_all: term * term -> term
wenzelm@32449:   val exists_const: typ -> term
wenzelm@32449:   val mk_exists: term * term -> term
wenzelm@32449:   val eq_const: typ -> term
wenzelm@32449:   val mk_eq: term * term -> term
wenzelm@32449:   val dest_eq: term -> term * term
paulson@9543:   val mk_binop: string -> term * term -> term
paulson@9543:   val mk_binrel: string -> term * term -> term
paulson@9543:   val dest_bin: string -> typ -> term -> term * term
paulson@4349: end;
paulson@4349: 
paulson@4349: 
paulson@4349: structure FOLogic: FOLOGIC =
paulson@4349: struct
paulson@4349: 
haftmann@38500: val oT = Type(@{type_name o},[]);
paulson@4349: 
haftmann@38500: val Trueprop = Const(@{const_name Trueprop}, oT-->propT);
paulson@4349: 
paulson@4349: fun mk_Trueprop P = Trueprop $ P;
paulson@4349: 
haftmann@38500: fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
paulson@4349:   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
paulson@4349: 
wenzelm@32449: 
wenzelm@32449: (* Logical constants *)
paulson@4349: 
haftmann@38500: val not = Const (@{const_name Not}, oT --> oT);
wenzelm@41310: val conj = Const(@{const_name conj}, [oT,oT]--->oT);
wenzelm@41310: val disj = Const(@{const_name disj}, [oT,oT]--->oT);
wenzelm@41310: val imp = Const(@{const_name imp}, [oT,oT]--->oT)
wenzelm@41310: val iff = Const(@{const_name iff}, [oT,oT]--->oT);
paulson@4349: 
wenzelm@7692: fun mk_conj (t1, t2) = conj $ t1 $ t2
wenzelm@7692: and mk_disj (t1, t2) = disj $ t1 $ t2
paulson@9543: and mk_imp (t1, t2) = imp $ t1 $ t2
paulson@9543: and mk_iff (t1, t2) = iff $ t1 $ t2;
wenzelm@7692: 
wenzelm@41310: fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B)
paulson@4466:   | dest_imp  t = raise TERM ("dest_imp", [t]);
paulson@4466: 
wenzelm@41310: fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t'
wenzelm@11668:   | dest_conj t = [t];
wenzelm@11668: 
wenzelm@41310: fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B)
paulson@9543:   | dest_iff  t = raise TERM ("dest_iff", [t]);
paulson@9543: 
wenzelm@41310: fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT);
paulson@4349: fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
paulson@4349: 
wenzelm@41310: fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
paulson@6140:   | dest_eq t = raise TERM ("dest_eq", [t])
paulson@6140: 
haftmann@38500: fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
wenzelm@44241: fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
paulson@4349: 
haftmann@38500: fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
wenzelm@44241: fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
paulson@4349: 
wenzelm@32449: 
paulson@9543: (* binary oprations and relations *)
paulson@9543: 
paulson@9543: fun mk_binop c (t, u) =
paulson@9543:   let val T = fastype_of t in
paulson@9543:     Const (c, [T, T] ---> T) $ t $ u
paulson@9543:   end;
paulson@9543: 
paulson@9543: fun mk_binrel c (t, u) =
paulson@9543:   let val T = fastype_of t in
paulson@9543:     Const (c, [T, T] ---> oT) $ t $ u
paulson@9543:   end;
paulson@9543: 
paulson@9543: fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
paulson@9543:       if c = c' andalso T = T' then (t, u)
paulson@9543:       else raise TERM ("dest_bin " ^ c, [tm])
paulson@9543:   | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
paulson@9543: 
paulson@4349: end;