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 :: "tm list ⇒ tm list ⇒ fol fm list"
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)" |
  axiom_addimp:
                    "⊢ 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:
                    "⊢ concl 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)))"
  using axiom_addimp
  unfolding axiom_addimp_def
  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)))"
  using axiom_addimp
  unfolding axiom_addimp_def
  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 "equal_length l []"
  then show "equal_length [] l"
  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))"
  unfolding axiom_addimp_def
  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
  by (simp add: iffI)
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)
                           (axiom_addimp p (Imp(p,p))))
              (axiom_addimp 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                                            *)
(*         ------------------------------------------------ add_assum (p)    *)
(*                         |- p ==> q                                        *)
(* ------------------------------------------------------------------------- *)

fun add_assum p th = modusponens (axiom_addimp (concl th) p) th;

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

fun imp_add_assum p th =
  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
  modusponens (imp_add_assum p th2) th1
  end;

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

fun imp_insert q th =
  let val (p,r) = dest_imp(concl th) in
  imp_trans th (axiom_addimp r q)
  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
  imp_trans (axiom_addimp q p)
            (modusponens (axiom_distribimp p q r) th)
  end;

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

fun imp_trans_th p q r =
   imp_trans (axiom_addimp (Imp(q,r)) p)
             (axiom_distribimp p q r);

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

fun imp_add_concl r th =
  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)
            (imp_add_concl (Imp(p,r)) (axiom_addimp q p));

(* ------------------------------------------------------------------------- *)
(*  |- (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</