src/FOL/fologic.ML
changeset 69593 3dda49e08b9d
parent 44241 7943b69f0188
equal deleted inserted replaced
69592:a80d8ec6c998 69593:3dda49e08b9d
    35 
    35 
    36 
    36 
    37 structure FOLogic: FOLOGIC =
    37 structure FOLogic: FOLOGIC =
    38 struct
    38 struct
    39 
    39 
    40 val oT = Type(@{type_name o},[]);
    40 val oT = Type(\<^type_name>\<open>o\<close>,[]);
    41 
    41 
    42 val Trueprop = Const(@{const_name Trueprop}, oT-->propT);
    42 val Trueprop = Const(\<^const_name>\<open>Trueprop\<close>, oT-->propT);
    43 
    43 
    44 fun mk_Trueprop P = Trueprop $ P;
    44 fun mk_Trueprop P = Trueprop $ P;
    45 
    45 
    46 fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
    46 fun dest_Trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ P) = P
    47   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    47   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    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>\<open>Not\<close>, oT --> oT);
    53 val conj = Const(@{const_name conj}, [oT,oT]--->oT);
    53 val conj = Const(\<^const_name>\<open>conj\<close>, [oT,oT]--->oT);
    54 val disj = Const(@{const_name disj}, [oT,oT]--->oT);
    54 val disj = Const(\<^const_name>\<open>disj\<close>, [oT,oT]--->oT);
    55 val imp = Const(@{const_name imp}, [oT,oT]--->oT)
    55 val imp = Const(\<^const_name>\<open>imp\<close>, [oT,oT]--->oT)
    56 val iff = Const(@{const_name iff}, [oT,oT]--->oT);
    56 val iff = Const(\<^const_name>\<open>iff\<close>, [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 imp},_) $ A $ B) = (A, B)
    63 fun dest_imp (Const(\<^const_name>\<open>imp\<close>,_) $ 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 conj}, _) $ t $ t') = t :: dest_conj t'
    66 fun dest_conj (Const (\<^const_name>\<open>conj\<close>, _) $ 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 iff},_) $ A $ B) = (A, B)
    69 fun dest_iff (Const(\<^const_name>\<open>iff\<close>,_) $ 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 eq}, [T, T] ---> oT);
    72 fun eq_const T = Const (\<^const_name>\<open>eq\<close>, [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 eq}, _) $ lhs $ rhs) = (lhs, rhs)
    75 fun dest_eq (Const (\<^const_name>\<open>eq\<close>, _) $ 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>\<open>All\<close>, [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 
    81 fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
    81 fun exists_const T = Const (\<^const_name>\<open>Ex\<close>, [T --> oT] ---> oT);
    82 fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
    82 fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
    83 
    83 
    84 
    84 
    85 (* binary oprations and relations *)
    85 (* binary oprations and relations *)
    86 
    86