Theory FOL_Harrison

(*
FOL-Harrison - First-Order Logic According to Harrison

Authors: Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen

Acknowledgement: The SML code is based on the OCaml code accompanying John Harrison's
Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009
*)

chapter ‹FOL-Harrison›

theory FOL_Harrison
imports
Main
begin

section ‹Module Proven›

subsection ‹Syntax of first-order logic›

type_synonym id = String.literal

datatype tm = Var id | Fn id "tm list"

datatype 'a fm = Truth | Falsity | Atom 'a | Imp "'a fm" "'a fm" | Iff "'a fm" "'a fm" |
And "'a fm" "'a fm" | Or "'a fm" "'a fm" | Not "'a fm" | Exists id "'a fm" | Forall id "'a fm"

datatype fol = Rl id "tm list"

datatype "thm" = Thm (concl: "fol fm")

subsection ‹Definition of rules and axioms›

abbreviation (input) "fail_thm  Thm Truth"

definition fol_equal :: "fol fm  fol fm  bool"
where
"fol_equal p q  p = q"

definition zip_eq ::
where
"zip_eq l l'  map (λ(t, t'). Atom (Rl (STR ''='') [t, t'])) (zip l l')"

primrec occurs_in :: "id  tm  bool" and occurs_in_list :: "id  tm list  bool"
where
"occurs_in i (Var x) = (i = x)" |
"occurs_in i (Fn _ l) = occurs_in_list i l" |
"occurs_in_list _ [] = False" |
"occurs_in_list i (h # t) = (occurs_in i h  occurs_in_list i t)"

primrec free_in :: "id  fol fm  bool"
where
"free_in _ Truth = False" |
"free_in _ Falsity = False" |
"free_in i (Atom a) = (case a of Rl _ l  occurs_in_list i l)" |
"free_in i (Imp p q) = (free_in i p  free_in i q)" |
"free_in i (Iff p q) = (free_in i p  free_in i q)" |
"free_in i (And p q) = (free_in i p  free_in i q)" |
"free_in i (Or p q) = (free_in i p  free_in i q)" |
"free_in i (Not p) = free_in i p" |
"free_in i (Exists x p) = (i  x  free_in i p)" |
"free_in i (Forall x p) = (i  x  free_in i p)"

primrec equal_length :: "tm list  tm list  bool"
where
"equal_length l [] = (case l of []  True | _ # _  False)" |
"equal_length l (_ # r') = (case l of []  False | _ # l'  equal_length l' r')"

definition modusponens :: "thm  thm  thm"
where
"modusponens s s'  case concl s of Imp p q
let p' = concl s' in if fol_equal p p' then Thm q else fail_thm | _  fail_thm"

definition gen :: "id  thm  thm"
where
"gen x s  Thm (Forall x (concl s))"

definition axiom_addimp :: "fol fm  fol fm  thm"
where
"axiom_addimp p q  Thm (Imp p (Imp q p))"

definition axiom_distribimp :: "fol fm  fol fm  fol fm  thm"
where
"axiom_distribimp p q r  Thm (Imp (Imp p (Imp q r)) (Imp (Imp p q) (Imp p r )))"

definition axiom_doubleneg :: "fol fm  thm"
where
"axiom_doubleneg p  Thm (Imp (Imp (Imp p Falsity) Falsity) p)"

definition axiom_allimp :: "id  fol fm  fol fm  thm"
where
"axiom_allimp x p q  Thm (Imp (Forall x (Imp p q)) (Imp (Forall x p) (Forall x q)))"

definition axiom_impall :: "id  fol fm  thm"
where
"axiom_impall x p  if ¬ free_in x p then Thm (Imp p (Forall x p)) else fail_thm"

definition axiom_existseq :: "id  tm  thm"
where
"axiom_existseq x t  if ¬ occurs_in x t
then Thm (Exists x (Atom (Rl (STR ''='') [Var x, t]))) else fail_thm"

definition axiom_eqrefl :: "tm  thm"
where
"axiom_eqrefl t  Thm (Atom (Rl (STR ''='') [t, t]))"

definition axiom_funcong :: "id  tm list  tm list  thm"
where
"axiom_funcong i l l'  if equal_length l l'
then Thm (foldr Imp (zip_eq l l') (Atom (Rl (STR ''='') [Fn i l, Fn i l']))) else fail_thm"

definition axiom_predcong :: "id  tm list  tm list  thm"
where
"axiom_predcong i l l'  if equal_length l l'
then Thm (foldr Imp (zip_eq l l') (Imp (Atom (Rl i l)) (Atom (Rl i l')))) else fail_thm"

definition axiom_iffimp1 :: "fol fm  fol fm  thm"
where
"axiom_iffimp1 p q  Thm (Imp (Iff p q) (Imp p q))"

definition axiom_iffimp2 :: "fol fm  fol fm  thm"
where
"axiom_iffimp2 p q  Thm (Imp (Iff p q) (Imp q p))"

definition axiom_impiff :: "fol fm  fol fm  thm"
where
"axiom_impiff p q  Thm (Imp (Imp p q) (Imp (Imp q p) (Iff p q)))"

definition axiom_true :: "thm"
where
"axiom_true  Thm (Iff Truth (Imp Falsity Falsity))"

definition axiom_not :: "fol fm  thm"
where
"axiom_not p  Thm (Iff (Not p) (Imp p Falsity))"

definition axiom_and :: "fol fm  fol fm  thm"
where
"axiom_and p q  Thm (Iff (And p q) (Imp (Imp p (Imp q Falsity)) Falsity))"

definition axiom_or :: "fol fm  fol fm  thm"
where
"axiom_or p q  Thm (Iff (Or p q) (Not (And (Not p) (Not q))))"

definition axiom_exists :: "id  fol fm  thm"
where
"axiom_exists x p  Thm (Iff (Exists x p) (Not (Forall x (Not p))))"

subsection ‹Code generation for rules and axioms›

(* The following export_code's are only for inspection purposes *)

export_code
modusponens gen axiom_addimp axiom_distribimp axiom_doubleneg axiom_allimp axiom_impall
axiom_existseq axiom_eqrefl axiom_funcong axiom_predcong axiom_iffimp1 axiom_iffimp2
axiom_impiff axiom_true axiom_not axiom_and axiom_or axiom_exists concl
in SML module_name Proven

code_printing constant fol_equal  (SML) "_ = _" ― ‹More efficient›

export_code
modusponens gen axiom_addimp axiom_distribimp axiom_doubleneg axiom_allimp axiom_impall
axiom_existseq axiom_eqrefl axiom_funcong axiom_predcong axiom_iffimp1 axiom_iffimp2
axiom_impiff axiom_true axiom_not axiom_and axiom_or axiom_exists concl
in SML module_name Proven

code_printing constant fol_equal  (SML) ― ‹Delete›

export_code
modusponens gen axiom_addimp axiom_distribimp axiom_doubleneg axiom_allimp axiom_impall
axiom_existseq axiom_eqrefl axiom_funcong axiom_predcong axiom_iffimp1 axiom_iffimp2
axiom_impiff axiom_true axiom_not axiom_and axiom_or axiom_exists concl
in SML module_name Proven

subsection ‹Semantics of first-order logic›

definition length2 :: "tm list  bool"
where
"length2 l  case l of [_,_]  True | _  False"

primrec ― ‹Semantics of terms›
semantics_term :: "(id  'a)  (id  'a list  'a)  tm  'a" and
semantics_list :: "(id  'a)  (id  'a list  'a)  tm list  'a list"
where
"semantics_term e _ (Var x) = e x" |
"semantics_term e f (Fn i l) = f i (semantics_list e f l)" |
"semantics_list _ _ [] = []" |
"semantics_list e f (t # l) = semantics_term e f t # semantics_list e f l"

primrec ― ‹Semantics of formulas›
semantics :: "(id  'a)  (id  'a list  'a)  (id  'a list  bool)  fol fm  bool"
where
"semantics _ _ _ Truth = True" |
"semantics _ _ _ Falsity = False" |
"semantics e f g (Atom a) = (case a of Rl i l  if i = STR ''=''  length2 l
then (semantics_term e f (hd l) = semantics_term e f (hd (tl l)))
else g i (semantics_list e f l))" |
"semantics e f g (Imp p q) = (semantics e f g p  semantics e f g q)" |
"semantics e f g (Iff p q) = (semantics e f g p  semantics e f g q)" |
"semantics e f g (And p q) = (semantics e f g p  semantics e f g q)" |
"semantics e f g (Or p q) = (semantics e f g p  semantics e f g q)" |
"semantics e f g (Not p) = (¬ semantics e f g p)" |
"semantics e f g (Exists x p) = (v. semantics (e(x := v)) f g p)" |
"semantics e f g (Forall x p) = (v. semantics (e(x := v)) f g p)"

subsection ‹Definition of proof system›

inductive OK :: "fol fm  bool" (" _" 0)
where
modusponens:
" concl s   concl s'   concl (modusponens s s')" |
gen:
" concl s   concl (gen _ s)" |
" concl (axiom_addimp _ _)" |
axiom_distribimp:
" concl (axiom_distribimp _ _ _)" |
axiom_doubleneg:
" concl (axiom_doubleneg _)" |
axiom_allimp:
" concl (axiom_allimp _ _ _)" |
axiom_impall:
" concl (axiom_impall _ _)" |
axiom_existseq:
" concl (axiom_existseq _ _)" |
axiom_eqrefl:
" concl (axiom_eqrefl _)" |
axiom_funcong:
" concl (axiom_funcong _ _ _)" |
axiom_predcong:
" concl (axiom_predcong _ _ _)" |
axiom_iffimp1:
" concl (axiom_iffimp1 _ _)" |
axiom_iffimp2:
" concl (axiom_iffimp2 _ _)" |
axiom_impiff:
" concl (axiom_impiff _ _)" |
axiom_true:
|
axiom_not:
" concl (axiom_not _)" |
axiom_and:
" concl (axiom_and _ _)" |
axiom_or:
" concl (axiom_or _ _)" |
axiom_exists:
" concl (axiom_exists _ _)"

(* Example *)

proposition " Imp p p"
proof -
have 1: " concl (Thm (Imp (Imp p (Imp (Imp p p) p)) (Imp (Imp p (Imp p p)) (Imp p p))))"
using axiom_distribimp
unfolding axiom_distribimp_def
by simp

have 2: " concl (Thm (Imp p (Imp (Imp p p) p)))"
by simp

have 3: " concl (Thm (Imp (Imp p (Imp p p)) (Imp p p)))"
using 1 2 modusponens
unfolding modusponens_def fol_equal_def
by fastforce

have 4: " concl (Thm (Imp p (Imp p p)))"
by simp

have 5: " concl (Thm (Imp p p))"
using 3 4 modusponens
unfolding modusponens_def fol_equal_def
by fastforce

show ?thesis
using 5
by simp
qed

subsection ‹Soundness of proof system›

lemma map':
"¬ occurs_in x t  semantics_term e f t = semantics_term (e(x := v)) f t"
"¬ occurs_in_list x l  semantics_list e f l = semantics_list (e(x := v)) f l"
by (induct t and l rule: semantics_term.induct semantics_list.induct) simp_all

lemma map:
"¬ free_in x p  semantics e f g p  semantics (e(x := v)) f g p"
proof (induct p arbitrary: e)
fix e
show "¬ free_in x Truth  semantics e f g Truth  semantics (e(x := v)) f g Truth"
by simp
next
fix e
show "¬ free_in x Falsity  semantics e f g Falsity  semantics (e(x := v)) f g Falsity"
by simp
next
fix a e
show "¬ free_in x (Atom a)  semantics e f g (Atom a)  semantics (e(x := v)) f g (Atom a)"
proof (cases a)
fix i l
show "¬ free_in x (Atom a)  a = Rl i l
semantics e f g (Atom a)  semantics (e(x := v)) f g (Atom a)"
proof -
assume assm: "¬ free_in x (Atom a)" "a = Rl i l"
then have fresh: "¬ occurs_in_list x l"
by simp
show "semantics e f g (Atom a)  semantics (e(x := v)) f g (Atom a)"
proof cases
assume eq: "i = STR ''=''  length2 l"
then have "semantics e f g (Atom (Rl i l))
semantics_term e f (hd l) = semantics_term e f (hd (tl l))"
by simp
also have "...
semantics_term (e(x := v)) f (hd l) = semantics_term (e(x := v)) f (hd (tl l))"
using map'(1) fresh occurs_in_list.simps(2) eq list.case_eq_if list.collapse
unfolding length2_def
by metis
finally show ?thesis
using eq assm(2)
by simp
next
assume not_eq: "¬ (i = STR ''=''  length2 l)"
then have "semantics e f g (Atom (Rl i l))  g i (semantics_list e f l)"
by simp iprover
also have "...  g i (semantics_list (e(x := v)) f l)"
using map'(2) fresh
by metis
finally show ?thesis
using not_eq assm(2)
by simp iprover
qed
qed
qed
next
fix p1 p2 e
assume assm1: "¬ free_in x p1  semantics e f g p1  semantics (e(x := v)) f g p1" for e
assume assm2: "¬ free_in x p2  semantics e f g p2  semantics (e(x := v)) f g p2" for e
show "¬ free_in x (Imp p1 p2)
semantics e f g (Imp p1 p2)  semantics (e(x := v)) f g (Imp p1 p2)"
using assm1 assm2
by simp
next
fix p1 p2 e
assume assm1: "¬ free_in x p1  semantics e f g p1  semantics (e(x := v)) f g p1" for e
assume assm2: "¬ free_in x p2  semantics e f g p2  semantics (e(x := v)) f g p2" for e
show "¬ free_in x (Iff p1 p2)
semantics e f g (Iff p1 p2)  semantics (e(x := v)) f g (Iff p1 p2)"
using assm1 assm2
by simp
next
fix p1 p2 e
assume assm1: "¬ free_in x p1  semantics e f g p1  semantics (e(x := v)) f g p1" for e
assume assm2: "¬ free_in x p2  semantics e f g p2  semantics (e(x := v)) f g p2" for e
show "¬ free_in x (And p1 p2)
semantics e f g (And p1 p2)  semantics (e(x := v)) f g (And p1 p2)"
using assm1 assm2
by simp
next
fix p1 p2 e
assume assm1: "¬ free_in x p1  semantics e f g p1  semantics (e(x := v)) f g p1" for e
assume assm2: "¬ free_in x p2  semantics e f g p2  semantics (e(x := v)) f g p2" for e
show "¬ free_in x (Or p1 p2)
semantics e f g (Or p1 p2)  semantics (e(x := v)) f g (Or p1 p2)"
using assm1 assm2
by simp
next
fix p e
assume "¬ free_in x p  semantics e f g p  semantics (e(x := v)) f g p" for e
then show "¬ free_in x (Not p)  semantics e f g (Not p)  semantics (e(x := v)) f g (Not p)"
by simp
next
fix x1 p e
assume "¬ free_in x p  semantics e f g p  semantics (e(x := v)) f g p" for e
then show "¬ free_in x (Exists x1 p)
semantics e f g (Exists x1 p)  semantics (e(x := v)) f g (Exists x1 p)"
by simp (metis fun_upd_twist fun_upd_upd)
next
fix x1 p e
assume "¬ free_in x p  semantics e f g p  semantics (e(x := v)) f g p" for e
then show "¬ free_in x (Forall x1 p)
semantics e f g (Forall x1 p)  semantics (e(x := v)) f g (Forall x1 p)"
by simp (metis fun_upd_twist fun_upd_upd)
qed

lemma length2_equiv:
"length2 l  [hd l, hd (tl l)] = l"
proof -
have "length2 l  [hd l, hd (tl l)] = l"
unfolding length2_def
using list.case_eq_if list.exhaust_sel
by metis
then show ?thesis
unfolding length2_def
using list.case list.case_eq_if
by metis
qed

lemma equal_length_sym:
"equal_length l l'  equal_length l' l"
proof (induct l' arbitrary: l)
fix l
assume
then show
using equal_length.simps list.case_eq_if
by metis
next
fix l l' a
assume sym: "equal_length l l'  equal_length l' l" for l
assume "equal_length l (a # l')"
then show "equal_length (a # l') l"
using equal_length.simps list.case_eq_if list.collapse list.inject sym
by metis
qed

lemma equal_length2:
"equal_length l l'  length2 l  length2 l'"
proof -
assume assm: "equal_length l l'"
have "equal_length l [t, t']  length2 l" for t t'
unfolding length2_def
using equal_length.simps list.case_eq_if
by metis
moreover have "equal_length [t, t'] l'  length2 l'" for t t'
unfolding length2_def
using equal_length.simps list.case_eq_if equal_length_sym
by metis
ultimately show ?thesis
using assm length2_equiv
by metis
qed

lemma imp_chain_equiv:
"semantics e f g (foldr Imp l p)  (q  set l. semantics e f g q)  semantics e f g p"
using imp_conjL
by (induct l) simp_all

lemma imp_chain_zip_eq:
"equal_length l l'
semantics e f g (foldr Imp (zip_eq l l') p)
semantics_list e f l = semantics_list e f l'  semantics e f g p"
proof -
assume "equal_length l l'"
then have "(q  set (zip_eq l l'). semantics e f g q)
semantics_list e f l = semantics_list e f l'"
unfolding zip_eq_def
using length2_def
by (induct l l' rule: list_induct2') simp_all
then show ?thesis
using imp_chain_equiv
by iprover
qed

lemma funcong:
"equal_length l l'
semantics e f g (foldr Imp (zip_eq l l') (Atom (Rl (STR ''='') [Fn i l, Fn i l'])))"
proof -
assume assm: "equal_length l l'"
show ?thesis
proof cases
assume "semantics_list e f l = semantics_list e f l'"
then have "semantics e f g (Atom (Rl (STR ''='') [Fn i l, Fn i l']))"
using length2_def
by simp
then show ?thesis
using imp_chain_equiv
by iprover
next
assume "semantics_list e f l  semantics_list e f l'"
then show ?thesis
using assm imp_chain_zip_eq
by iprover
qed
qed

lemma predcong:
"equal_length l l'
semantics e f g (foldr Imp (zip_eq l l') (Imp (Atom (Rl i l)) (Atom (Rl i l'))))"
proof -
assume assm: "equal_length l l'"
show ?thesis
proof cases
assume eq: "i = STR ''=''  length2 l  length2 l'"
show ?thesis
proof cases
assume "semantics_list e f l = semantics_list e f l'"
then have "semantics_list e f [hd l, hd (tl l)] = semantics_list e f [hd l', hd (tl l')]"
using eq length2_equiv
by simp
then have "semantics e f g (Imp (Atom (Rl (STR ''='') l)) (Atom (Rl (STR ''='') l')))"
using eq
by simp
then show ?thesis
using eq imp_chain_equiv
by iprover
next
assume "semantics_list e f l  semantics_list e f l'"
then show ?thesis
using assm imp_chain_zip_eq
by iprover
qed
next
assume not_eq: "¬ (i = STR ''=''  length2 l  length2 l')"
show ?thesis
proof cases
assume "semantics_list e f l = semantics_list e f l'"
then have "semantics e f g (Imp (Atom (Rl i l)) (Atom (Rl i l')))"
using assm not_eq equal_length2
by simp iprover
then show ?thesis
using imp_chain_equiv
by iprover
next
assume "semantics_list e f l  semantics_list e f l'"
then show ?thesis
using assm imp_chain_zip_eq
by iprover
qed
qed
qed

theorem soundness:
" p  semantics e f g p"
proof (induct arbitrary: e rule: OK.induct)
fix e s s'
assume "semantics e f g (concl s)" "semantics e f g (concl s')" for e
then show "semantics e f g (concl (modusponens s s'))"
unfolding modusponens_def
proof (cases s)
fix r
assume "semantics e f g (concl s)" "semantics e f g (concl s')" "s = Thm r" for e
then show "semantics e f g (concl (case (concl s) of Imp p q
let p' = concl s' in if fol_equal p p' then Thm q else fail_thm | _  fail_thm))"
unfolding fol_equal_def
by (cases r) simp_all
qed
next
fix e x s
assume "semantics e f g (concl s)" for e
then show "semantics e f g (concl (gen x s))"
unfolding gen_def
by simp
next
fix e p q
show "semantics e f g (concl (axiom_addimp p q))"
by simp
next
fix e p q r
show "semantics e f g (concl (axiom_distribimp p q r))"
unfolding axiom_distribimp_def
by simp
next
fix e g p
show "semantics e f g (concl (axiom_doubleneg p))"
unfolding axiom_doubleneg_def
by simp
next
fix e x p q
show "semantics e f g (concl (axiom_allimp x p q))"
unfolding axiom_allimp_def
by simp
next
fix e x p
show "semantics e f g (concl (axiom_impall x p))"
unfolding axiom_impall_def
using map
by simp iprover
next
fix e x t
show "semantics e f g (concl (axiom_existseq x t))"
unfolding axiom_existseq_def
using map'(1) length2_def
by simp iprover
next
fix e t
show "semantics e f g (concl (axiom_eqrefl t))"
unfolding axiom_eqrefl_def
using length2_def
by simp
next
fix e i l l'
show "semantics e f g (concl (axiom_funcong i l l'))"
unfolding axiom_funcong_def
using funcong
by simp standard
next
fix e i l l'
show "semantics e f g (concl (axiom_predcong i l l'))"
unfolding axiom_predcong_def
using predcong
by simp standard
next
fix e p q
show "semantics e f g (concl (axiom_iffimp1 p q))"
unfolding axiom_iffimp1_def
by simp
next
fix e p q
show "semantics e f g (concl (axiom_iffimp2 p q))"
unfolding axiom_iffimp2_def
by simp
next
fix e p q
show "semantics e f g (concl (axiom_impiff p q))"
unfolding axiom_impiff_def
next
fix e
show "semantics e f g (concl (axiom_true))"
unfolding axiom_true_def
by simp
next
fix e p
show "semantics e f g (concl (axiom_not p))"
unfolding axiom_not_def
by simp
next
fix e p q
show "semantics e f g (concl (axiom_and p q))"
unfolding axiom_and_def
by simp
next
fix e p q
show "semantics e f g (concl (axiom_or p q))"
unfolding axiom_or_def
by simp
next
fix e x p
show "semantics e f g (concl (axiom_exists x p))"
unfolding axiom_exists_def
by simp
qed

corollary "¬ ( Falsity)"
using soundness
by fastforce

section ‹ML Code Reflection›

code_reflect
Proven
datatypes
fm = Falsity | Truth | Atom | Imp | Iff | And | Or | Not | Exists | Forall
and
tm = Var | Fn
and
fol = Rl
functions
modusponens gen axiom_addimp axiom_distribimp axiom_doubleneg axiom_allimp axiom_impall
axiom_existseq axiom_eqrefl axiom_funcong axiom_predcong axiom_iffimp1 axiom_iffimp2
axiom_impiff axiom_true axiom_not axiom_and axiom_or axiom_exists concl

ML open Proven

ML val print = writeln (* Should not add newline but only used for testing (see XXX label) *)

ML "format_simple.sml";

fun set_margin _ = ();

fun print_string x = print x;

fun open_box _ = ();

fun close_box () = ();

fun print_space () = print " ";

fun print_break _ _ = ();

fun open_hbox () = ();

fun print_flush () = ();

fun print_newline () = print "\n";

fun print_int n = print (Int.toString n);

fun open_hvbox _ = ();

ML "lib.sml";

(* ========================================================================= *)
(* Misc library functions to set up a nice environment.                      *)
(* ========================================================================= *)

fun str_ord s1 s2 =
case String.compare(s1,s2) of
EQUAL => 0    | GREATER => 1    | LESS  => ~1;

fun sip_ord (f1,a1) (f2,a2) =
case str_ord f1 f2 of
0 => if a1>a2 then 1 else ~1
| n => n
;

infix 6 lxor
infix 6 land

fun to_int_fun f = fn a => fn b => Word.toIntX (f ((Word.fromInt a),(Word.fromInt b) ) );

fun a lxor b = to_int_fun Word.xorb a b;
fun a land b = to_int_fun Word.andb a b;

fun list_hash elem_hash l=
let fun hash_code sval l =
case l of
[] => sval
| e::l' =>
let val e_hash = Word.fromInt (elem_hash e) in
hash_code (Word.+(Word.*(sval,0wx31),(e_hash))) l'
end
in
Word.toIntX(hash_code 0wx0 l)
end
;

fun str_hash str = list_hash Char.ord (String.explode str);

fun fst (x,_) = x;
fun snd (_,y) = y;

(* ========================================================================= *)
(* Misc library functions to set up a nice environment.                      *)
(* ========================================================================= *)

fun identity x = x;

(* ------------------------------------------------------------------------- *)
(* A useful idiom for "non contradictory" etc.                               *)
(* ------------------------------------------------------------------------- *)

fun non p x = not(p x);

(* ------------------------------------------------------------------------- *)
(* Kind of assertion checking.                                               *)
(* ------------------------------------------------------------------------- *)

fun check p x = if p(x) then x else raise Fail "check";

(* ------------------------------------------------------------------------- *)
(* Repetition of a function.                                                 *)
(* ------------------------------------------------------------------------- *)

fun funpow n f x =
if n < 1 then x
else funpow (n - 1) f (f x);

fun can f x = (f x; true) handle Fail _ => false;

fun repeat f x = repeat f (f x) handle Fail _ => x;

(* ------------------------------------------------------------------------- *)
(* Handy list operations.                                                    *)
(* ------------------------------------------------------------------------- *)

infix 6 --
fun m -- n = if m > n then [] else m::((m + 1) -- n);

fun map2 f l1 l2 =
case (l1,l2) of
([],[]) => []
| ((h1::t1),(h2::t2)) => let val h = f h1 h2 in h::(map2 f t1 t2) end
| _ => raise Fail "map2: length mismatch";

fun itlist f l b = List.foldr (fn (x,y) => f x y) b l;

fun end_itlist f l =
case l of
[]     => raise Fail "end_itlist"
| [x]    => x
| (h::t) => f h (end_itlist f t);

fun itlist2 f l1 l2 b =
case (l1,l2) of
([],[]) => b
| (h1::t1,h2::t2) => f h1 h2 (itlist2 f t1 t2 b)
| _ => raise Fail "itlist2";

fun zip l1 l2 =
case (l1,l2) of
([],[]) => []
| (h1::t1,h2::t2) => (h1,h2)::(zip t1 t2)
| _ => raise Fail "zip";

fun chop_list n l =
if n = 0 then ([],l) else
let val (m,l') = chop_list (n-1) (tl l) in ((hd l)::m,l') end
handle Fail _ => raise Fail "chop_list";

fun index x =
let fun ind n l =
case l of
[] => raise Fail "index"
| (h::t) => if x = h then n else ind (n + 1) t
in
ind 0
end;

fun unzip l =
case l of
[] => ([],[])
| (x,y)::t =>
let val (xs,ys) = unzip t in (x::xs,y::ys) end;

(* ------------------------------------------------------------------------- *)
(* Association lists.                                                        *)
(* ------------------------------------------------------------------------- *)

fun assoc a l =
case l of
(x,y)::t => if x = a then y else assoc a t
| [] => raise Fail "find";

(* ------------------------------------------------------------------------- *)
(* Merging of sorted lists (maintaining repetitions).                        *)
(* ------------------------------------------------------------------------- *)

fun merge ord l1 l2 =
case l1 of
[] => l2
| h1::t1 => case l2 of
[] => l1
| h2::t2 => if ord h1 h2 then h1::(merge ord t1 l2)
else h2::(merge ord l1 t2);

(* ------------------------------------------------------------------------- *)
(* Bottom-up mergesort.                                                      *)
(* ------------------------------------------------------------------------- *)

fun sort ord =
let fun mergepairs l1 l2 =
case (l1,l2) of
([s],[]) => s
| (l,[]) => mergepairs [] l
| (l,[s1]) => mergepairs (s1::l) []
| (l,(s1::s2::ss)) => mergepairs ((merge ord s1 s2)::l) ss in
fn l => if l = [] then [] else mergepairs [] (List.map (fn x => [x]) l)
end;

(* ------------------------------------------------------------------------- *)
(* Common measure predicates to use with "sort".                             *)
(* ------------------------------------------------------------------------- *)

fun increasing f x y = (f x) < (f y);

fun decreasing f x y = (f x) > (f y) ;

(* ------------------------------------------------------------------------- *)
(* Eliminate repetitions of adjacent elements, with and without counting.    *)
(* ------------------------------------------------------------------------- *)

fun uniq l =
case l of
x :: (t as y :: ys ) =>
let val t' = uniq t in
if x = y then t'
else
x :: t'
end
| _ => l;

fun tryfind f l =
case l of
[] => raise Fail "tryfind"
| (h::t) =>
((f h) handle Fail _ => tryfind f t);

(* ------------------------------------------------------------------------- *)
(* Set operations on ordered lists.                                          *)
(* ------------------------------------------------------------------------- *)

fun setify ord l=
let fun canonical lis =
case lis of
x::(rest as y::_) => ord x y < 0 andalso canonical rest
| _ => true in
if canonical l then l
else uniq (sort (fn x => fn y => ord x y <= 0) l)
end;

fun union ord s1 s2=
let fun union l1 l2 =
case (l1,l2) of
([],l2) => l2
| (l1,[]) => l1
| ((l1 as h1::t1),(l2 as h2::t2)) =>
if h1 = h2 then h1::(union t1 t2)
else if ord h1 h2 = ~1 then h1::(union t1 l2)
else h2::(union l1 t2) in
union (setify ord s1) (setify ord s2)
end;

fun union_str s1 s2 = union str_ord s1 s2;
fun union_sip p1 p2 = union sip_ord p1 p2;

fun subtract ord s1 s2=
let fun subtract l1 l2 =
case (l1,l2) of
([],l2) => []
| (l1,[]) => l1
| ((l1 as h1::t1),(l2 as h2::t2)) =>
if h1 = h2 then subtract t1 t2
else if ord h1 h2 = ~1 then h1::(subtract t1 l2)
else subtract l1 t2 in
subtract (setify ord s1) (setify ord s2)
end;

fun subtract_str s1 s2 = subtract str_ord s1 s2;

fun insert ord x s = union ord [x] s;

fun insert_str x s = insert str_ord x s;

(* ------------------------------------------------------------------------- *)
(* Union of a family of sets.                                                *)
(* ------------------------------------------------------------------------- *)

fun unions ord s =
let fun concat a b = a @ b in
setify ord (itlist concat s [])
end;

fun unions_str s = unions str_ord s;

(* ------------------------------------------------------------------------- *)
(* List membership. This does *not* assume the list is a set.                *)
(* ------------------------------------------------------------------------- *)

fun mem x lis =
case lis of
[] => false
| hd :: tl => hd = x orelse mem x tl;

(* ------------------------------------------------------------------------- *)
(* Timing; useful for documentation but not logically necessary.             *)
(* ------------------------------------------------------------------------- *)

fun time f x =
let val timer = Timer.startRealTimer()
val result = f x
val time = Timer.checkRealTimer timer
in (
(* XXX print_string ("CPU time (user): " ^ (Real.toString (Time.toReal time)));
print_newline(); *)
result
) end;

(* ------------------------------------------------------------------------- *)
(* Polymorphic finite partial functions via Patricia trees.                  *)
(*                                                                           *)
(* The point of this strange representation is that it is canonical (equal   *)
(* functions have the same encoding) yet reasonably efficient on average.    *)
(*                                                                           *)
(* Idea due to Diego Olivier Fernandez Pons (OCaml list, 2003/11/10).        *)
(* ------------------------------------------------------------------------- *)

datatype ('a,'b)func =
Empty
| Leaf of int * ('a*'b)list
| Branch of int * int * ('a,'b)func * ('a,'b)func;

(* ------------------------------------------------------------------------- *)
(* Undefined function.                                                       *)
(* ------------------------------------------------------------------------- *)

val undefined = Empty;

(* ------------------------------------------------------------------------- *)
(* In case of equality comparison worries, better use this.                  *)
(* ------------------------------------------------------------------------- *)

fun is_undefined f =
case f of
Empty => true
| _ => false;

(* ------------------------------------------------------------------------- *)
(* Operation analogous to "map" for lists.                                   *)
(* ------------------------------------------------------------------------- *)

local
fun map_list f l =
case l of
[] => []
| (x,y)::t => (x,f(y))::(map_list f t)
in
fun mapf f t =
case t of
Empty => Empty
| Leaf(h,l) => Leaf(h,map_list f l)
| Branch(p,b,l,r) => Branch(p,b,mapf f l,mapf f r)
end;

(* ------------------------------------------------------------------------- *)
(* Application.                                                              *)
(* ------------------------------------------------------------------------- *)

fun applyd ord hash f d x=
let fun apply_listd l d x =
case l of
(a,b)::t => if x = a then b else if ord x a > 0 then apply_listd t d x else d x
| [] => d x
val k = hash x
fun look t =
case t of
Leaf(h,l) =>
if (h = k) then
apply_listd l d x
else d x
| Branch(p,b,l,r) =>
if ((k lxor p) land (b - 1)) = 0 then
look (if k land b = 0 then l else r)
else d x
| _ => d x
in
look f
end
;

fun apply ord hash f = applyd ord hash f (fn x => raise Fail "apply");

fun apply_str f = apply str_ord str_hash f;

fun tryapplyd ord hash f a d = applyd ord hash f (fn x => d) a;

fun tryapplyd_str f a d = tryapplyd str_ord str_hash f a d;

fun tryapplyl ord hash f x = tryapplyd ord hash f x [];

fun defined ord hash f x = (apply ord hash f x; true) handle Fail _ => false;

fun defined_str f x = defined str_ord str_hash f x;

(* ------------------------------------------------------------------------- *)
(* Undefinition.                                                             *)
(* ------------------------------------------------------------------------- *)

local
fun undefine_list ord x l =
case l of
(ab as (a,b))::t =>
let val c = ord x a in
if c = 0 then
t
else if c < 0 then
l
else
let val t' = undefine_list ord x t in
ab::t'
end
end
| [] => []
in
fun undefine ord hash x =
let val k = hash x
fun und t =
case t of
Leaf(h,l) =>
if h=k then (
let val l' = undefine_list ord x l in
if l' = l then t
else if l' = [] then Empty
else Leaf(h,l')
end
) else t
| Branch(p,b,l,r) =>
if k land (b - 1) = p then (
if k land b = 0 then
let val l' = und l in
if l' = l then t
else (case l' of Empty => r | _ => Branch(p,b,l',r))
end
else
let val r' = und r in
if r' = r then t
else (case r' of Empty => l | _ => Branch(p,b,l,r'))
end
) else t
| _ => t
in
und
end
end;

fun undefine_str x t = undefine str_ord str_hash x t

(* ------------------------------------------------------------------------- *)
(* Redefinition and combination.                                             *)
(* ------------------------------------------------------------------------- *)

infix 6 |->

local
fun newbranch p1 t1 p2 t2 =
let val zp = p1 lxor p2
val b = zp land (~zp)
val p = p1 land (b - 1) in
if p1 land b = 0 then Branch(p,b,t1,t2)
else Branch(p,b,t2,t1)
end
fun define_list ord (xy as (x,y)) l =
case l of
(ab as (a,b))::t =>
let val c = ord x a in
if c = 0 then xy::t
else if c < 0 then xy::l
else ab::(define_list ord xy t)
end
| [] => [xy]
fun combine_list ord op' z l1 l2 =
case (l1,l2) of
([],_) => l2
| (_,[]) => l1
| ((xy1 as (x1,y1))::t1,(xy2 as (x2,y2))::t2) =>
let val c = ord x1 x2 in
if c < 0 then
xy1::(combine_list ord op' z t1 l2)
else if c > 0 then
xy2::(combine_list ord op' z l1 t2)
else
let val y = op' y1 y2
val l = combine_list ord op' z t1 t2 in
if z(y) then l else (x1,y)::l
end
end
in
fun (x |-> y) t ord hash =
let val k = hash x
fun upd t =
case t of
Empty => Leaf (k,[(x,y)])
| Leaf(h,l) =>
if h = k then Leaf(h,define_list ord (x,y) l)
else newbranch h t k (Leaf(k,[(x,y)]))
| Branch(p,b,l,r) =>
if k land (b - 1) <> p then newbranch p t k (Leaf(k,[(x,y)]))
else if k land b = 0 then Branch(p,b,upd l,r)
else Branch(p,b,l,upd r) in
upd t
end
fun combine ord op' z t1 t2 =
case (t1,t2) of
(Empty,_) => t2
| (_,Empty) => t1
| (Leaf(h1,l1),Leaf(h2,l2)) =>
if h1 = h2 then
let val l = combine_list ord op' z l1 l2 in
if l = [] then Empty else Leaf(h1,l)
end
else newbranch h1 t1 h2 t2
| ((lf as Leaf(k,lis)),(br as Branch(p,b,l,r))) =>
if k land (b - 1) = p then
if k land b = 0 then
(case combine ord op' z lf l of
Empty => r | l' => Branch(p,b,l',r))
else
(case combine ord op' z lf r of
Empty => l | r' => Branch(p,b,l,r'))
else
newbranch k lf p br
| ((br as Branch(p,b,l,r)),(lf as Leaf(k,lis))) =>
if k land (b - 1) = p then
if k land b = 0 then
(case combine ord op' z l lf of
Empty => r | l' => Branch(p,b,l',r))
else
(case combine ord op' z r lf of
Empty => l | r' => Branch(p,b,l,r'))
else
newbranch p br k lf
| (Branch(p1,b1,l1,r1),Branch(p2,b2,l2,r2)) =>
if b1 < b2 then
if p2 land (b1 - 1) <> p1 then newbranch p1 t1 p2 t2
else if p2 land b1 = 0 then
(case combine ord op' z l1 t2 of
Empty => r1 | l => Branch(p1,b1,l,r1))
else
(case combine ord op' z r1 t2 of
Empty => l1 | r => Branch(p1,b1,l1,r))
else if b2 < b1 then
if p1 land (b2 - 1) <> p2 then newbranch p1 t1 p2 t2
else if p1 land b2 = 0 then
(case combine ord op' z t1 l2 of
Empty => r2 | l => Branch(p2,b2,l,r2))
else
(case combine ord op' z t1 r2 of
Empty => l2 | r => Branch(p2,b2,l2,r))
else if p1 = p2 then
(case (combine ord op' z l1 l2,combine ord op' z r1 r2) of
(Empty,r) => r | (l,Empty) => l | (l,r) => Branch(p1,b1,l,r))
else
newbranch p1 t1 p2 t2
end ;

infix 6 |--> (* For strings *)

fun (x |--> y) t = (x |-> y) t str_ord str_hash;

(* ------------------------------------------------------------------------- *)
(* Special case of point function.                                           *)
(* ------------------------------------------------------------------------- *)

infix 6 |=>

fun x |=> y = (x |-> y) undefined;

infix 6 |==> (* For strings *)

fun x |==> y = (x |=> y) str_ord str_hash;

ML "intro.sml";

(* ========================================================================= *)
(* Simple algebraic expression example from the introductory chapter.        *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Lexical analysis.                                                         *)
(* ------------------------------------------------------------------------- *)

fun matches s =
let val chars = String.explode s in
fn c => mem c chars
end;

val space = matches " \t\n\r";
val punctuation = matches "()[]{},";
val symbolic = matches "~`!@#\$%^&*-+=|\\:;<>.?/";
val numeric = matches "0123456789";
val alphanumeric = matches
"abcdefghijklmnopqrstuvwxyz_'ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789";

fun lexwhile prop inp =
if inp <> [] andalso prop (List.hd inp) then
let val (tok,rest) = lexwhile prop (List.tl inp) in
((str (List.hd inp))^tok,rest)
end
else
("",inp);

fun lex inp =
case snd(lexwhile space inp) of
[] => []
| c::cs => let val prop = if alphanumeric(c) then alphanumeric
else if symbolic(c) then symbolic
else fn c => false
val (toktl,rest) = lexwhile prop cs in
((str c)^toktl)::lex rest
end;

(* ------------------------------------------------------------------------- *)
(* Generic function to impose lexing and exhaustion checking on a parser.    *)
(* ------------------------------------------------------------------------- *)

fun make_parser pfn s =
let val (expr,rest) = pfn (lex(String.explode s)) in
if rest = [] then expr else raise Fail "Unparsed input"
end;

ML "formulas.sml";

(* ========================================================================= *)
(* Polymorphic type of formulas with parser and printer.                     *)
(* ========================================================================= *)

fun fm_ord at_ord fm1 fm2 =
case (fm1,fm2) of
(Falsity,Falsity) => 0
| (Falsity,_) =>  1
| (_,Falsity) => ~1

| (Truth,Truth) => 0
| (Truth,_)  =>  1
| (_,Truth)  => ~1

| (Atom a, Atom b) => at_ord a b
| (Atom(_),_) => 1
| (_,Atom(_)) => ~1

| (Not a,Not b) => fm_ord at_ord a b
| (Not(_),_) => 1
| (_,Not(_)) => ~1

| (And(a1,a2),And(b1,b2)) => fm_pair_ord at_ord (a1,a2) (b1,b2)
| (And(_,_),_) =>  1
| (_,And(_,_)) => ~1

| (Or(a1,a2),Or(b1,b2)) => fm_pair_ord at_ord (a1,a2) (b1,b2)
| (Or(_,_),_) =>  1
| (_,Or(_,_)) => ~1

| (Imp(a1,a2),Imp(b1,b2)) => fm_pair_ord at_ord (a1,a2) (b1,b2)
| (Imp(_,_),_) =>  1
| (_,Imp(_,_)) => ~1

| (Iff(a1,a2),Iff(b1,b2)) => fm_pair_ord at_ord (a1,a2) (b1,b2)
| (Iff(_,_),_) =>  1
| (_,Iff(_,_)) => ~1

| (Forall(x1,a),Forall(x2,b)) => fm_quant_ord at_ord (x1,a) (x2,b)
| (Forall (_,_), _) => 1
| (_, Forall (_,_)) => ~1

| (Exists(x1,a),Exists(x2,b)) => fm_quant_ord at_ord (x1,a) (x2,b)
and fm_pair_ord at_ord (a1,a2) (b1,b2) =
case fm_ord at_ord a1 b1 of
0 => fm_ord at_ord a2 b2
|n => n
and fm_quant_ord at_ord (x1,a) (x2,b) =
case str_ord x1 x2 of
0 => fm_ord at_ord a b
|n => n
;

(* ------------------------------------------------------------------------- *)
(* General parsing of iterated infixes.                                      *)
(* ------------------------------------------------------------------------- *)

fun parse_ginfix opsym opupdate sof subparser inp =
let val (e1,inp1) = subparser inp in
if inp1 <> [] andalso List.hd inp1 = opsym then
parse_ginfix opsym opupdate (opupdate sof e1) subparser (List.tl inp1)
else (sof e1,inp1)
end;

fun parse_left_infix opsym opcon =
parse_ginfix opsym (fn f => fn e1 => fn e2 => opcon(f e1,e2)) (fn x => x);

fun parse_right_infix opsym opcon =
parse_ginfix opsym (fn f => fn e1 => fn e2 => f(opcon(e1,e2))) (fn x => x);

fun parse_list opsym =
parse_ginfix opsym (fn f => fn e1 => fn e2 => (f e1)@[e2]) (fn x => [x]);

(* ------------------------------------------------------------------------- *)
(* Other general parsing combinators.                                        *)
(* ------------------------------------------------------------------------- *)

fun papply f (ast,rest) = (f ast,rest);

fun nextin inp tok = inp <> [] andalso List.hd inp = tok;

fun parse_bracketed subparser cbra inp =
let val(ast,rest) = subparser inp in
if nextin rest cbra then (ast,List.tl rest)
else raise Fail "Closing bracket expected"
end;

(* ------------------------------------------------------------------------- *)
(* Parsing of formulas, parametrized by atom parser "pfn".                   *)
(* ------------------------------------------------------------------------- *)

fun parse_atomic_formula (ifn,afn) vs inp =
case inp of
[] => raise Fail "formula expected"
| "false"::rest => (Falsity,rest)
| "true"::rest => (Truth,rest)
| "("::rest => ( (ifn vs inp) handle Fail _ =>
parse_bracketed (parse_formula (ifn,afn) vs) ")" rest)
| "~"::rest => papply (fn p => Not p)
(parse_atomic_formula (ifn,afn) vs rest)
| "forall"::x::rest =>
parse_quant (ifn,afn) (x::vs) (fn (x,p) => Forall(x,p)) x rest
| "exists"::x::rest =>
parse_quant (ifn,afn) (x::vs) (fn (x,p) => Exists(x,p)) x rest
| _ => afn vs inp

and parse_quant (ifn,afn) vs qcon x inp =
case inp of
[] => raise Fail "Body of quantified term expected"
| y::rest =>
papply (fn fm => qcon(x,fm))
(if y = "." then parse_formula (ifn,afn) vs rest
else parse_quant (ifn,afn) (y::vs) qcon y rest)

and parse_formula (ifn,afn) vs inp =
parse_right_infix "<=>" (fn (p,q) => Iff(p,q))
(parse_right_infix "==>" (fn (p,q) => Imp(p,q))
(parse_right_infix "\\/" (fn (p,q) => Or(p,q))
(parse_right_infix "/\\" (fn (p,q) => And(p,q))
(parse_atomic_formula (ifn,afn) vs)))) inp;

(* ------------------------------------------------------------------------- *)
(* Printing of formulas, parametrized by atom printer.                       *)
(* ------------------------------------------------------------------------- *)

fun bracket p n f x y = (
(if p then print_string "(" else ());
open_box n; f x y; close_box();
(if p then print_string ")" else ())
);

fun strip_quant fm =
case fm of
Forall (x, (Forall (y, p))) =>
let val (xs, q) = strip_quant (Forall (y, p)) in
((x :: xs), q)
end
| Exists (x, (Exists (y, p))) =>
let val (xs, q) = strip_quant (Exists (y, p)) in
((x :: xs), q)
end
| Forall (x, p) =>
([x],p)
| Exists (x, p) =>
([x],p)
| _ =>
([], fm);

fun print_formula_aux pfn =
let fun print_formula pr fm =
case fm of
Falsity =>
print_string "false"
| Truth =>
print_string "true"
| Atom pargs =>
pfn pr pargs
| Not p =>
bracket (pr > 10) 1 (print_prefix 10) "~" p
| And (p, q) =>
bracket (pr > 8) 0 (print_infix 8 "/\\") p q
| Or (p, q) =>
bracket (pr > 6) 0 (print_infix 6 "\\/") p q
| Imp (p, q) =>
bracket (pr > 4) 0 (print_infix 4 "==>") p q
| Iff (p, q) =>
bracket (pr > 2) 0 (print_infix 2 "<=>") p q
| Forall (x, p) =>
bracket (pr > 0) 2 print_qnt "forall" (strip_quant fm)
| Exists (x, p) =>
bracket (pr > 0) 2 print_qnt "exists" (strip_quant fm)

and print_qnt qname (bvs, bod) = (
print_string qname;
List.app (fn v => (print_string " "; print_string v)) bvs;
print_string "."; print_space(); open_box 0;
print_formula 0 bod;
close_box()
)

and print_prefix newpr sym p = (
print_string sym ; print_formula (newpr + 1) p
)

and print_infix newpr sym p q = (
print_formula (newpr + 1) p ;
print_string (" "^sym); print_space();
print_formula newpr q
) in
print_formula 0
end
;

fun print_formula pfn fm = (print_formula_aux pfn fm; print_flush ());

fun print_qformula_aux pfn fm = (
open_box 0; print_string "<!";
open_box 0; print_formula_aux pfn fm; close_box();
print_string "!>"; close_box()
);

fun print_qformula pfn fm = (print_qformula_aux pfn fm; print_flush ());

fun mk_and p q = And (p, q)

fun mk_or p q = Or (p, q)

fun mk_imp p q = Imp (p, q)

fun mk_iff p q = Iff (p, q)

fun mk_forall x p = Forall (x, p)

fun mk_exists x p = Exists (x, p)

(* ------------------------------------------------------------------------- *)
(* Destructors.                                                              *)
(* ------------------------------------------------------------------------- *)

fun dest_iff fm =
case fm of Iff(p,q) => (p,q) | _ => raise Fail "dest_iff";

fun dest_and fm =
case fm of And(p,q) => (p,q) | _ => raise Fail "dest_and";

fun conjuncts fm =
case fm of And(p,q) => conjuncts p @ conjuncts q | _ => [fm];

fun dest_or fm =
case fm of Or(p,q) => (p,q) | _ => raise Fail "dest_or";

fun disjuncts fm =
case fm of Or(p,q) => disjuncts p @ disjuncts q | _ => [fm];

fun dest_imp fm =
case fm of Imp(p,q) => (p,q) | _ => raise Fail "dest_imp";

fun antecedent fm = fst (dest_imp fm);
fun consequent fm = snd (dest_imp fm);

(* ------------------------------------------------------------------------- *)
(* Apply a function to the atoms, otherwise keeping structure.               *)
(* ------------------------------------------------------------------------- *)

fun onatoms f fm =
case fm of
Atom a => f a
| Not(p) => Not(onatoms f p)
| And(p,q) => And(onatoms f p,onatoms f q)
| Or(p,q) => Or(onatoms f p,onatoms f q)
| Imp(p,q) => Imp(onatoms f p,onatoms f q)
| Iff(p,q) => Iff(onatoms f p,onatoms f q)
| Forall(x,p) => Forall(x,onatoms f p)
| Exists(x,p) => Exists(x,onatoms f p)
| _ => fm;

(* ------------------------------------------------------------------------- *)
(* Formula analog of list iterator "itlist".                                 *)
(* ------------------------------------------------------------------------- *)

fun overatoms f fm b =
case fm of
Atom(a) => f a b
| Not(p) => overatoms f p b
| And(p,q) => overatoms f p (overatoms f q b)
| Or(p,q)  => overatoms f p (overatoms f q b)
| Imp(p,q) => overatoms f p (overatoms f q b)
| Iff(p,q) => overatoms f p (overatoms f q b)
| Forall(x,p) => overatoms f p b
| Exists(x,p) => overatoms f p b
| _ => b;

(* ------------------------------------------------------------------------- *)
(* Special case of a union of the results of a function over the atoms.      *)
(* ------------------------------------------------------------------------- *)

fun atom_union ord f fm = setify ord (overatoms (fn h => fn t => f(h)@t) fm []);

fun atom_union_sip f fm = atom_union sip_ord f fm;

ML "prop.sml";

(* ========================================================================= *)
(* Basic stuff for propositional logic: datatype, parsing and printing.      *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Disjunctive normal form (DNF) via truth tables.                           *)
(* ------------------------------------------------------------------------- *)

fun list_conj l = if l = [] then Truth else end_itlist mk_and l;

ML "fol.sml";

(* ========================================================================= *)
(* Basic stuff for first order logic.                                        *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Terms.                                                                    *)
(* ------------------------------------------------------------------------- *)

fun t_ord t1 t2 =
case (t1,t2) of
(Var x1, Var x2 ) => str_ord x1 x2
| (Var _, _) => 1
| (_, Var _) => ~1
| (Fn(f1,tl1),Fn(f2,tl2)) =>
case str_ord f1 f2 of
0 => tl_ord tl1 tl2
|n => n
and tl_ord tl1 tl2 =
case (tl1,tl2) of
([],[]) => 0
| ([],_) => 1
| (_,[]) => ~1
| (t1::tl1',t2::tl2') =>
case t_ord t1 t2 of
0 => tl_ord tl1' tl2'
| n => n
;

fun t_hash t =
case t of
Var x => str_hash x
| Fn (f,tl) => Word.toIntX(Word.+(Word.*(0wx31,Word.fromInt(str_hash f)),
Word.fromInt(list_hash t_hash tl)))
;

infix 6 |---> (* For terms *)

fun (x |---> y) t = (x |-> y) t t_ord t_hash;

infix 6 |===> (* For terms *)
fun x |===> y = (x |=> y) t_ord t_hash;

fun apply_t f = apply t_ord t_hash f;

(* ------------------------------------------------------------------------- *)
(* Abbreviation for FOL formula.                                             *)
(* ------------------------------------------------------------------------- *)

fun fol_ord (r1 as Rl(s1,tl1)) (r2 as Rl(s2,tl2)) =
case str_ord s1 s2 of
0 => tl_ord tl1 tl2
| n => n
;

fun folfm_ord fm1 fm2 = fm_ord fol_ord fm1 fm2;

fun union_folfm s1 s2 = union folfm_ord s1 s2;

fun ftp_ord (fm1,t1) (fm2,t2) =
case folfm_ord fm1 fm2 of
0 => t_ord t1 t2
| n => n;

fun setify_ftp s = setify ftp_ord s;

(* ------------------------------------------------------------------------- *)
(* Special case of applying a subfunction to the top *terms*.                *)
(* ------------------------------------------------------------------------- *)

fun onformula f = onatoms(fn (Rl(p,a)) => Atom(Rl(p,List.map f a)));

(* ------------------------------------------------------------------------- *)
(* Parsing of terms.                                                         *)
(* ------------------------------------------------------------------------- *)

fun is_const_name s = List.all numeric (String.explode s) orelse s = "nil";

fun parse_atomic_term vs inp =
case inp of
[] => raise Fail "term expected"
| "("::rest => parse_bracketed (parse_term vs) ")" rest
| "-"::rest => papply (fn t => Fn("-",[t])) (parse_atomic_term vs rest)
| f::"("::")"::rest => (Fn(f,[]),rest)
| f::"("::rest =>
papply (fn args => Fn(f,args))
(parse_bracketed (parse_list "," (parse_term vs)) ")" rest)
| a::rest =>
((if is_const_name a andalso not(mem a vs) then Fn(a,[]) else Var a),rest)

and parse_term vs inp =
parse_right_infix "::" (fn (e1,e2) => Fn("::",[e1,e2]))
(parse_right_infix "+" (fn (e1,e2) => Fn("+",[e1,e2]))
(parse_left_infix "-" (fn (e1,e2) => Fn("-",[e1,e2]))
(parse_right_infix "*" (fn (e1,e2) => Fn("*",[e1,e2]))
(parse_left_infix "/" (fn (e1,e2) => Fn("/",[e1,e2]))
(parse_left_infix "^" (fn (e1,e2) => Fn("^",[e1,e2]))
(parse_atomic_term vs)))))) inp;

val parset = make_parser (parse_term []);

(* ------------------------------------------------------------------------- *)
(* Parsing of formulas.                                                      *)
(* ------------------------------------------------------------------------- *)

fun parse_infix_atom vs inp =
let val (tm,rest) = parse_term vs inp in
if List.exists (nextin rest) ["=", "<", "<=", ">", ">="] then
papply (fn tm' => Atom(Rl(List.hd rest,[tm,tm'])))
(parse_term vs (List.tl rest))
else raise Fail ""
end;

fun parse_atom vs inp =
(parse_infix_atom vs inp) handle Fail _ =>
case inp of
p::"("::")"::rest => (Atom(Rl(p,[])),rest)
| p::"("::rest =>
papply (fn args => Atom(Rl(p,args)))
(parse_bracketed (parse_list "," (parse_term vs)) ")" rest)
| p::rest =>
if p <> "(" then (Atom(Rl(p,[])),rest)
else raise Fail "parse_atom"
| _ => raise Fail "parse_atom";

val parse = make_parser
(parse_formula (parse_infix_atom,parse_atom) []);

(* ------------------------------------------------------------------------- *)
(* Set up parsing of quotations.                                             *)
(* ------------------------------------------------------------------------- *)

val default_parser = parse;
datatype default_parser_end = !>;
fun <! s !> = default_parser s;

val secondary_parser = parset;
datatype secondary_parser_end = |!>;
fun <!| s |!> = secondary_parser s;

(* ------------------------------------------------------------------------- *)
(* Printing of terms.                                                        *)
(* ------------------------------------------------------------------------- *)

fun print_term_aux prec fm =
case fm of
Var x => print_string x
| Fn("^",[tm1,tm2]) => print_infix_term_aux true prec 24 "^" tm1 tm2
| Fn("/",[tm1,tm2]) => print_infix_term_aux true prec 22 " /" tm1 tm2
| Fn("*",[tm1,tm2]) => print_infix_term_aux false prec 20 " *" tm1 tm2
| Fn("-",[tm1,tm2]) => print_infix_term_aux true prec 18 " -" tm1 tm2
| Fn("+",[tm1,tm2]) => print_infix_term_aux false prec 16 " +" tm1 tm2
| Fn("::",[tm1,tm2]) => print_infix_term_aux false prec 14 "::" tm1 tm2
| Fn(f,args) => print_fargs_aux f args

and print_fargs_aux f args = (
print_string f;
if args = [] then () else
(print_string "(";
open_box 0;
print_term_aux 0 (List.hd args); print_break 0 0;
List.app (fn t => (print_string ","; print_break 0 0 ; print_term_aux 0 t))
(List.tl args);
close_box ();
print_string ")")
)

and print_infix_term_aux isleft oldprec newprec sym p q = (
if oldprec > newprec then (print_string "("; open_box 0) else ();
print_term_aux (if isleft then newprec else newprec+1) p;
print_string sym;
print_break (if String.substring (sym, 0, 1) = " " then 1 else 0) 0;
print_term_aux (if isleft then newprec+1 else newprec) q;
if oldprec > newprec then (close_box (); print_string ")") else ()
);

fun print_term prec fm = (print_term_aux prec fm; print_flush ())
and print_fargs f args = (print_fargs_aux f args; print_flush ())
and print_infix_term isleft oldprec newprec sym p q = (print_infix_term_aux isleft oldprec newprec sym p q; print_flush ());

fun printert_aux tm = (
open_box 0; print_string "<!|";
open_box 0; print_term_aux 0 tm; close_box();
print_string "|!>"; close_box()
);

fun printert tm = (printert_aux tm; print_flush ());

(* ------------------------------------------------------------------------- *)
(* Printing of formulas.                                                     *)
(* ------------------------------------------------------------------------- *)

fun print_atom_aux prec (Rl (p, args)) =
if mem p ["=", "<", "<=", ">", ">="] andalso List.length args = 2 then
print_infix_term_aux false 12 12 (" " ^ p) (List.nth (args, 0)) (List.nth (args, 1))
else
print_fargs_aux p args;

fun print_atom prec rpa = (print_atom_aux prec rpa; print_flush ());

val print_fol_formula_aux = print_qformula_aux print_atom_aux;

fun print_fol_formula f = (print_fol_formula_aux f; print_flush ());

(* ------------------------------------------------------------------------- *)
(* Free variables in terms and formulas.                                     *)
(* ------------------------------------------------------------------------- *)

fun fvt tm =
case tm of
Var x => [x]
| Fn (f, args) =>
unions_str (List.map fvt args)
;

fun var fm =
case fm of
Falsity => []
| Truth => []
| Atom (Rl (p, args)) =>
unions str_ord (List.map fvt args)
| Not p => var p
| And (p, q) => union_str (var p) (var q)
| Or  (p, q) => union_str (var p) (var q)
| Imp (p, q) => union_str (var p) (var q)
| Iff (p, q) => union_str (var p) (var q)
| Forall (x, p) => insert_str x (var p)
| Exists (x, p) => insert_str x (var p)
;

fun fv fm =
case fm of
Falsity => []
| Truth => []
| Atom (Rl (p, args)) =>
unions_str (List.map fvt args)
| Not p => fv p
| And (p, q) => union_str (fv p) (fv q)
| Or  (p, q) => union_str (fv p) (fv q)
| Imp (p, q) => union_str (fv p) (fv q)
| Iff (p, q) => union_str (fv p) (fv q)
| Forall (x, p) => subtract_str (fv p) [x]
| Exists (x, p) => subtract_str (fv p) [x]
;

(* ------------------------------------------------------------------------- *)
(* Substitution within terms.                                                *)
(* ------------------------------------------------------------------------- *)

fun tsubst sfn tm =
case tm of
Var x => tryapplyd_str sfn x tm
| Fn(f,args) => Fn(f,List.map (tsubst sfn) args);

fun variant x vars =
if mem x vars then variant (x^"'") vars else x;

(* ------------------------------------------------------------------------- *)
(* Substitution in formulas, with variable renaming.                         *)
(* ------------------------------------------------------------------------- *)

fun subst subfn fm =
case fm of
Falsity => Falsity
| Truth => Truth
| Atom (Rl (p, args)) =>
Atom (Rl (p, List.map (tsubst subfn) args))
| Not p =>
Not (subst subfn p)
| And (p, q) =>
And (subst subfn p, subst subfn q)
| Or (p, q) =>
Or  (subst subfn p, subst subfn q)
| Imp (p, q) =>
Imp (subst subfn p, subst subfn q)
| Iff (p, q) =>
Iff (subst subfn p, subst subfn q)
| Forall (x, p) =>
substq subfn mk_forall x p
| Exists (x, p) =>
substq subfn mk_exists x p
and substq subfn quant x p =
let val x' =
if List.exists (fn y => mem x (fvt (tryapplyd_str subfn y (Var y))))
(subtract_str (fv p) [x]) then
variant x (fv (subst (undefine_str x subfn) p))
else x
in
quant x' (subst ((x |--> Var x') subfn) p)
end
;

ML "skolem.sml";

(* ========================================================================= *)
(* Prenex and Skolem normal forms.                                           *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Get the functions in a term and formula.                                  *)
(* ------------------------------------------------------------------------- *)

fun funcs tm =
case tm of
Var x => []
| Fn(f,args) => itlist (union_sip o funcs) args [(f,List.length args)];

fun functions fm =
atom_union_sip (fn (Rl(p,a)) => itlist (union_sip o funcs) a []) fm;

ML "unif.sml";

(* ========================================================================= *)
(* Unification for first order terms.                                        *)
(* ========================================================================= *)

fun istriv env x t =
case t of
Var y => y = x orelse defined_str env y andalso istriv env x (apply_str env y)
| Fn(f,args) => List.exists (istriv env x) args andalso raise Fail "cyclic";

(* ------------------------------------------------------------------------- *)
(* Main unification procedure                                                *)
(* ------------------------------------------------------------------------- *)

fun unify env eqs =
case eqs of
[] => env
| (Fn(f,fargs),Fn(g,gargs))::oth =>
if f = g andalso length fargs = length gargs
then unify env (zip fargs gargs @ oth)
else raise Fail "impossible unification"
| (Var x,t)::oth =>
if defined_str env x then unify env ((apply_str env x,t)::oth)
else unify (if istriv env x t then env else (x|-->t) env) oth
| (t,Var x)::oth =>
if defined_str env x then unify env ((apply_str env x,t)::oth)
else unify (if istriv env x t then env else (x|-->t) env) oth;

(* ------------------------------------------------------------------------- *)
(* Solve to obtain a single instantiation.                                   *)
(* ------------------------------------------------------------------------- *)

fun solve env =
let val env' = mapf (tsubst env) env in
if env' = env then env else solve env'
end;

(* ------------------------------------------------------------------------- *)
(* Unification reaching a final solved form (often this isn't needed).       *)
(* ------------------------------------------------------------------------- *)

fun fullunify eqs = solve (unify undefined eqs);

fun unify_and_apply eqs =
let val i = fullunify eqs
fun apply (t1,t2) = (tsubst i t1,tsubst i t2) in
map apply eqs
end;

ML "tableaux.sml";

(* ========================================================================= *)
(* Tableaux, seen as an optimized version of a Prawitz-like procedure.       *)
(* ========================================================================= *)

fun deepen f n =
((* XXX print_string "Searching with depth limit ";
print_int n; print_newline(); *) f n
)
handle Fail _ => deepen f (n + 1);

ML "resolution.sml";

(* ========================================================================= *)
(* Resolution.                                                               *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Matching of terms and literals.                                           *)
(* ------------------------------------------------------------------------- *)

fun term_match env eqs =
case eqs of
[] => env
| (Fn (f, fa), Fn(g, ga)) :: oth =>
if (f = g andalso List.length fa = List.length ga) then
term_match env (zip fa ga @ oth)
else raise Fail "term_match"
| (Var x, t) :: oth =>
if not (defined_str env x) then
term_match ((x |--> t) env) oth
else if apply_str env x = t then
term_match env oth
else
raise Fail "term_match"
| _ =>
raise Fail "term_match";

ML "equal.sml";

(* ========================================================================= *)
(* First order logic with equality.                                          *)
(* ========================================================================= *)

fun mk_eq s t = Atom(Rl("=",[s,t]));

fun dest_eq fm =
case fm of
Atom(Rl("=",[s,t])) => (s,t)
| _ => raise Fail "dest_eq: not an equation";

fun lhs eq = fst (dest_eq eq) and rhs eq = snd (dest_eq eq);

ML "order.sml";

(* ========================================================================= *)
(* Term orderings.                                                           *)
(* ========================================================================= *)

fun termsize tm =
case tm of
Var x => 1
| Fn(f,args) => itlist (fn t => fn n => termsize t + n) args 1;

ML "eqelim.sml";

(* ========================================================================= *)
(* Equality elimination including Brand transformation and relatives.        *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Replacement (substitution for non-variable) in term and literal.          *)
(* ------------------------------------------------------------------------- *)

fun replacet rfn tm =
apply_t rfn tm
handle Fail _ =>
case tm of
Fn(f,args) => Fn(f,List.map (replacet rfn) args)
| _ => tm;

ML "lcf.sml";

fun print_thm_aux th = (
open_box 0;
print_string "|-"; print_space();
open_box 0; print_formula_aux print_atom_aux (concl th); close_box();
close_box()
)

fun print_thm th = (print_thm_aux th; print_flush ())

ML "lcfprop.sml";

(* ========================================================================= *)
(* Propositional reasoning by derived rules atop the LCF core.               *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* |- p ==> p                                                                *)
(* ------------------------------------------------------------------------- *)

fun imp_refl p =
modusponens (modusponens (axiom_distribimp p (Imp(p,p)) p)

(* ------------------------------------------------------------------------- *)
(*                 |- p ==> p ==> q                                          *)
(*               -------------------- imp_unduplicate                        *)
(*                 |- p ==> q                                                *)
(* ------------------------------------------------------------------------- *)

fun imp_unduplicate th =
let val (p,pq) = dest_imp(concl th)
val q = consequent pq in
modusponens (modusponens (axiom_distribimp p p q) th) (imp_refl p)
end ;

(* ------------------------------------------------------------------------- *)
(* Some handy syntax operations.                                             *)
(* ------------------------------------------------------------------------- *)

fun negatef fm =
case fm of
Imp(p,Falsity) => p
| p => Imp(p,Falsity);

fun negativef fm =
case fm of
Imp(p,Falsity) => true
| _ => false;

(* ------------------------------------------------------------------------- *)
(*                           |- q                                            *)
(*                         |- p ==> q                                        *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(*                   |- q ==> r                                              *)
(*           |- (p ==> q) ==> (p ==> r)                                      *)
(* ------------------------------------------------------------------------- *)

let val (q,r) = dest_imp(concl th) in
modusponens (axiom_distribimp p q r) (add_assum p th)
end;

(* ------------------------------------------------------------------------- *)
(*            |- p ==> q              |- q ==> r                             *)
(*         ----------------------------------------- imp_trans               *)
(*                 |- p ==> r                                                *)
(* ------------------------------------------------------------------------- *)

fun imp_trans th1 th2 =
let val p = antecedent(concl th1) in
end;

(* ------------------------------------------------------------------------- *)
(*                 |- p ==> r                                                *)
(*         -------------------------- imp_insert q                           *)
(*              |- p ==> q ==> r                                             *)
(* ------------------------------------------------------------------------- *)

fun imp_insert q th =
let val (p,r) = dest_imp(concl th) in
end ;

(* ------------------------------------------------------------------------- *)
(*                 |- p ==> q ==> r                                          *)
(*              ---------------------- imp_swap                              *)
(*                 |- q ==> p ==> r                                          *)
(* ------------------------------------------------------------------------- *)

fun imp_swap th =
let val (p,qr) = dest_imp(concl th)
val (q,r) = dest_imp qr in
(modusponens (axiom_distribimp p q r) th)
end;

(* ------------------------------------------------------------------------- *)
(* |- (q ==> r) ==> (p ==> q) ==> (p ==> r)                                  *)
(* ------------------------------------------------------------------------- *)

fun imp_trans_th p q r =
(axiom_distribimp p q r);

(* ------------------------------------------------------------------------- *)
(*                 |- p ==> q                                                *)
(*          |- (q ==> r) ==> (p ==> r)                                       *)
(* ------------------------------------------------------------------------- *)

let val (p,q) = dest_imp(concl th) in
modusponens (imp_swap(imp_trans_th p q r)) th
end;

(* ------------------------------------------------------------------------- *)
(* |- (p ==> q ==> r) ==> (q ==> p ==> r)                                    *)
(* ------------------------------------------------------------------------- *)

fun imp_swap_th p q r =
imp_trans (axiom_distribimp p q r)

(* ------------------------------------------------------------------------- *)
(*  |- (p ==> q ==> r) ==> (s ==> t ==> u)                                   *)
(* -----------------------------------------                                 *)
(*  |- (q ==> p ==> r) ==> (t ==> s ==> u)                                   *)
(* ------------------------------------------------------------------------- *)

fun imp_swap2 th =
case concl th of
Imp(Imp(p,Imp(q,r)),Imp(s,Imp(t,u))) =>
imp_trans (imp_swap_th q p r) (imp_trans th (imp_swap_th s t u))
| _ => raise Fail "imp_swap2";

(* ------------------------------------------------------------------------- *)
(* If |- p ==> q ==> r and |- p ==> q then |- p ==> r.                       *)
(* ------------------------------------------------------------------------- *)

fun right_mp ith th =
imp_unduplicate(imp_trans th (imp_swap ith));

(* ------------------------------------------------------------------------- *)
(*                 |- p <=> q                                                *)
(*                ------------ iff_imp1                                      *)
(*                 |- p ==> q                                                *)
(* ------------------------------------------------------------------------- *)

fun iff_imp1 th =
let val (p,q) = dest_iff(concl th) in
modusponens (axiom_iffimp1 p q) th
end;

(* ------------------------------------------------------------------------- *)
(*                 |- p <=> q                                                *)
(*                ------------ iff_imp2                                      *)
(*                 |- q ==> p                                                *)
(* ------------------------------------------------------------------------- *)

fun iff_imp2 th =
let val (p,q) = dest_iff(concl th) in
modusponens (axiom_iffimp2 p q) th
end;

(* ------------------------------------------------------------------------- *)
(*         |- p ==> q      |- q ==> p                                        *)
(*        ---------------------------- imp_antisym                           *)
(*              |- p <=> q                                                   *)
(* ------------------------------------------------------------------------- *)

fun imp_antisym th1 th2 =
let val (p,q) = dest_imp(concl th1) in
modusponens (modusponens (axiom_impiff p q) th1) th2
end;

(* ------------------------------------------------------------------------- *)
(*         |- p ==> (q ==> false) ==> false                                  *)
(*       ----------------------------------- right_doubleneg                 *)
(*               |- p ==> q                                                  *)
(* ------------------------------------------------------------------------- *)

fun right_doubleneg th =
case concl th of
Imp(_,Imp(Imp(p,Falsity),Falsity)) => imp_trans th (axiom_doubleneg p)
| _ => raise Fail "right_doubleneg";

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(*         ------------------------------------------- ex_falso (p)          *)
(*                 |- false ==> p                                            *)
(* ------------------------------------------------------------------------- *)

fun ex_falso p = right_doubleneg(axiom_addimp Falsity (Imp(p,Falsity)));

(* ------------------------------------------------------------------------- *)
(*  |- p ==> q ==> r        |- r ==> s                                       *)
(* ------------------------------------ imp_trans2                           *)
(*      |- p ==> q ==> s                                                     *)
(* ------------------------------------------------------------------------- *)

fun imp_trans2 th1 th2 =
let val Imp(p,Imp(q,r)) = concl th1
val Imp(r',s) = concl th2
val th = imp_add_assum p (modusponens (imp_trans_th q r s) th2) in
modusponens th th1
end;

(* ------------------------------------------------------------------------- *)
(*         |- p ==> q1   ...   |- p ==> qn   |- q1 ==> ... ==> qn ==> r      *)
(*        --------------------------------------------------------------     *)
(*                             |- p ==> r                                    *)
(* ------------------------------------------------------------------------- *)

fun imp_trans_chain ths th =
itlist (fn a => fn b => imp_unduplicate (imp_trans a (imp_swap b)))
(List.rev(List.tl ths)) (imp_trans (List.hd ths) th);

(* ------------------------------------------------------------------------- *)
(* |- (q ==> false) ==> p ==> (p ==> q) ==> false                            *)
(* ------------------------------------------------------------------------- *)

fun imp_truefalse p q =
imp_trans (imp_trans_th p q Falsity) (imp_swap_th (Imp(p,q)) p Falsity);

(* ------------------------------------------------------------------------- *)
(*  |- (p' ==> p) ==> (q ==> q') ==> (p ==> q) ==> (p' ==> q')               *)
(* ------------------------------------------------------------------------- *)

fun imp_mono_th p p' q q' =
let val th1 = imp_trans_th (Imp(p,q)) (Imp(p',q)) (Imp(p',q'))
val th2 = imp_trans_th p' q q'
val th3 = imp_swap(imp_trans_th</