per

(* ========================================================================= *)
(* Fixed and compilable minimal canonical LCF core (LCF-style kernel)        *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* AST: Terms and first-order formulas (the core syntax tree).               *)
(* ------------------------------------------------------------------------- *)

type term =
  | Var of string
  | Fn of string * term list

type formula =
  | False
  | True
  | Atom of string * term list
  | Not of formula
  | And of formula * formula
  | Or of formula * formula
  | Imp of formula * formula
  | Iff of formula * formula
  | Forall of string * formula
  | Exists of string * formula

(* ------------------------------------------------------------------------- *)
(* Helper functions used by the kernel (must be in scope for the module).    *)
(* ------------------------------------------------------------------------- *)

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

let rec occurs_in s t =
  s = t ||
  match t with
  | Var _ -> false
  | Fn(_, args) -> List.exists (occurs_in s) args

let rec free_in t fm =
  match fm with
  | False | True -> false
  | Atom(_, args) -> List.exists (occurs_in t) args
  | Not p -> free_in t p
  | And(p, q) | Or(p, q) | Imp(p, q) | Iff(p, q) -> free_in t p || free_in t q
  | Forall(y, p) | Exists(y, p) -> not (occurs_in (Var y) t) && free_in t p

(* ------------------------------------------------------------------------- *)
(* LCF kernel signature (thm is abstract).                                   *)
(* ------------------------------------------------------------------------- *)

module type Proofsystem = sig
  type thm
  val modusponens : thm -> thm -> thm
  val gen : string -> thm -> thm
  (* Axioms (core logical axioms of the LCF-style system) *)
  val axiom_addimp : formula -> formula -> thm
  val axiom_distribimp : formula -> formula -> formula -> thm
  val axiom_doubleneg : formula -> thm
  val axiom_allimp : string -> formula -> formula -> thm
  val axiom_impall : string -> formula -> thm
  val axiom_existseq : string -> term -> thm
  val axiom_eqrefl : term -> thm
  val axiom_funcong : string -> term list -> term list -> thm
  val axiom_predcong : string -> term list -> term list -> thm
  val axiom_iffimp1 : formula -> formula -> thm
  val axiom_iffimp2 : formula -> formula -> thm
  val axiom_impiff : formula -> formula -> thm
  val axiom_true : thm
  val axiom_not : formula -> thm
  val axiom_and : formula -> formula -> thm
  val axiom_or : formula -> formula -> thm
  val axiom_exists : string -> formula -> thm
  val concl : thm -> formula
end

(* ------------------------------------------------------------------------- *)
(* Concrete implementation of the trusted kernel (thm = formula).            *)
(* ------------------------------------------------------------------------- *)

module Proven : Proofsystem = struct
  type thm = formula

  let modusponens pq p =
    match pq with
    | Imp(p', q) when p = p' -> q
    | _ -> failwith "modusponens"

  let gen x p = Forall(x, p)

  let axiom_addimp p q = Imp(p, Imp(q, p))
  let axiom_distribimp p q r =
    Imp(Imp(p, Imp(q, r)), Imp(Imp(p, q), Imp(p, r)))
  let axiom_doubleneg p = Imp(Imp(Imp(p, False), False), p)
  let axiom_allimp x p q =
    Imp(Forall(x, Imp(p, q)), Imp(Forall(x, p), Forall(x, q)))
  let axiom_impall x p =
    if not (free_in (Var x) p) then Imp(p, Forall(x, p))
    else failwith "axiom_impall: variable free in formula"
  let axiom_existseq x t =
    if not (occurs_in (Var x) t) then Exists(x, mk_eq (Var x) t)
    else failwith "axiom_existseq: variable free in term"
  let axiom_eqrefl t = mk_eq t t
  let axiom_funcong f lefts rights =
    List.fold_right2 (fun s t p -> Imp(mk_eq s t, p)) lefts rights
      (mk_eq (Fn(f, lefts)) (Fn(f, rights)))
  let axiom_predcong p lefts rights =
    List.fold_right2 (fun s t p -> Imp(mk_eq s t, p)) lefts rights
      (Imp(Atom(p, lefts), Atom(p, rights)))
  let axiom_iffimp1 p q = Imp(Iff(p, q), Imp(p, q))
  let axiom_iffimp2 p q = Imp(Iff(p, q), Imp(q, p))
  let axiom_impiff p q =
    Imp(Imp(p, q), Imp(Imp(q, p), Iff(p, q)))
  let axiom_true = Iff(True, Imp(False, False))
  let axiom_not p = Iff(Not p, Imp(p, False))
  let axiom_and p q =
    Iff(And(p, q), Imp(Imp(p, Imp(q, False)), False))
  let axiom_or p q =
    Iff(Or(p, q), Not(And(Not p, Not q)))
  let axiom_exists x p =
    Iff(Exists(x, p), Not(Forall(x, Not p)))

  let concl c = c
end