Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: info-hol@edu.uidaho.cs.ted (Info-hol mailing list)
Subject: Re: Completeness proofs
In-Reply-To: Your message of Thu, 18 Feb 93 20:46:49 +0700. <9302181846.AA10379@elc.mth.uct.ac.za>
Date: Fri, 19 Feb 93 00:53:04 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.321:19.02.93.00.53.11"@cl.cam.ac.uk>


Gavan Tredoux writes:

> It struck me recently that nobody seems to have constructed any
> *completeness* proofs in HOL, of an embedded logics. Generally, metatheory
> has taken a back place to the practical issues surrounding the use of HOL in
> applied contexts -- where it is important to derive logics and then USE them
> rather than reason ABOUT them.

> Mounting a completeness proof would obviously involve formalizing the notion
> of proof. It would be interesting to formalize proof in the *sequent* style
> employed by HOL, within HOL itself. One way to do this is to use recursive
> type definitions to provide the *form* of proofs, equipped with a `meaning'
> function to deliver the proof in HOL itself (associate an abstract `rule'
> with a rule in the HOL logic itself).

Joakim von Wright is currently doing work in proof certification; as part of
this undertaking he has been formally defining in HOL the notion of a proof in
HOL itself (without of course aiming at a proof of completeness, or as far as I
know defining any semantic concepts). He may want to tell you more himself, but
he's currently away for a few days.

As an extremely trivial example of doing metalogical reasoning inside HOL, I
offer the following proof of the Deduction Theorem for propositional calculus,
which I did one evening about a year ago to try out the inductive definitions
package (well, it keeps me off the streets).

John.

%----------------------------------------------------------------------------%
% Simple example of recursive types & inductive definitions -                %
% proof system for propositional calculus                                    %
%----------------------------------------------------------------------------%

can unlink `LOGIC.th`;;

new_theory `LOGIC`;;

load_library `ind_defs`;;

let Term_def = define_type `Term_def` `Term = f | Var num | Imp Term Term`;;

let Not_def = new_definition(`Not_def`,
  "Not p = Imp p f");;

let Proves_rules,Proves_ind =
  let Proves = "Proves:(Term->bool) -> Term -> bool" in
  new_inductive_definition
        true `Proves_def` ("^Proves G t",[])
        [["(G:Term->bool) t"],"^Proves G t";
         [],"^Proves G (Imp p (Imp q p))";
         [],"^Proves G (Imp (Imp p (Imp q r)) (Imp (Imp p q) (Imp p r)))";
         [],"^Proves G (Imp (Not (Not p)) p)";
         ["^Proves G (Imp p q)"; "^Proves G p"],"^Proves G q"];;

let base = hd Proves_rules;;

let [ax1;ax2;ax3] = tl(butlast Proves_rules);;

let mpth = CONV_RULE LEFT_IMP_EXISTS_CONV (SPEC_ALL (last Proves_rules));;

let mp th1 th2 =  MATCH_MP mpth (CONJ th1 th2);;

let IMP_REFL = prove_thm(`IMP_REFL`,
  "!G p. G Proves (Imp p p)",
  let th1 = SPECL ["G:Term->bool"; "p:Term"; "Imp q p"; "p:Term"] ax2 in
  let th2 = SPECL ["G:Term->bool"; "p:Term"; "Imp q p"] ax1 in
  let th3 = mp th1 th2 in
  let th4 = SPECL ["G:Term->bool"; "p:Term"; "q:Term"] ax1 in
  let th5 = mp th3 th4 in
  MATCH_ACCEPT_TAC th5);;

let RULE_INDUCT_TAC = RULE_INDUCT_THEN Proves_ind ASSUME_TAC ASSUME_TAC;;

let CASES = derive_cases_thm (Proves_rules,Proves_ind);;

let MONOTONIC = prove_thm(`MONOTONIC`,
  "!G s t. G Proves t ==> (\x. G x \/ (x = s)) Proves t",
  REPEAT GEN_TAC THEN RULE_INDUCT_TAC THEN REWRITE_TAC Proves_rules THENL
   [MATCH_MP_TAC base THEN BETA_TAC THEN ASM_REWRITE_TAC[];
    MATCH_MP_TAC mpth THEN EXISTS_TAC "p:Term" THEN ASM_REWRITE_TAC[]]);;

let ADD_SUB_LEMMA = prove_thm(`ADD_SUB_LEMMA`,
  "!G:Term->bool. !s. ((\x. G x \/ (x = s)) = G) \/
         ((\x. (\x. G x \/ (x = s)) x /\ ~(x = s)) = G)",
  REPEAT GEN_TAC THEN BETA_TAC THEN
  CONV_TAC(ONCE_DEPTH_CONV(X_FUN_EQ_CONV "x:Term")) THEN BETA_TAC THEN
  ASM_CASES_TAC "(G:Term->bool) s" THENL
   [DISJ1_TAC; DISJ2_TAC] THEN
  GEN_TAC THEN ASM_CASES_TAC "x:Term = s" THEN ASM_REWRITE_TAC[]);;

let IMP_TRUE_LEMMA = prove_thm(`IMP_TRUE_LEMMA`,
  "!G s t. G Proves t ==> G Proves (Imp s t)",
  REPEAT GEN_TAC THEN DISCH_THEN(ACCEPT_TAC o mp
        (SPECL["G:Term->bool"; "t:Term"; "s:Term"] ax1)));;

let DEDUCTION = prove_thm(`DEDUCTION`,
  "!G s t. G Proves (Imp s t) = (\x. G x \/ (x = s)) Proves t",
  REPEAT GEN_TAC THEN EQ_TAC THENL
   [DISCH_TAC THEN MATCH_MP_TAC mpth THEN
    EXISTS_TAC "s:Term" THEN CONJ_TAC THENL
     [MATCH_MP_TAC MONOTONIC THEN POP_ASSUM ACCEPT_TAC;
      MATCH_MP_TAC base THEN BETA_TAC THEN REWRITE_TAC[]];
    DISJ_CASES_THEN2 SUBST1_TAC
     (CONV_TAC o RAND_CONV o RATOR_CONV o RAND_CONV o REWR_CONV o SYM)
     (SPECL ["G:Term->bool"; "s:Term"] ADD_SUB_LEMMA) THENL
     [MATCH_ACCEPT_TAC IMP_TRUE_LEMMA;
      SPEC_TAC("\x:Term. G x \/ (x = s)","G:Term->bool")]] THEN
  RULE_INDUCT_TAC THEN
  TRY(REPEAT GEN_TAC THEN MATCH_MP_TAC IMP_TRUE_LEMMA THEN
      REWRITE_TAC Proves_rules THEN NO_TAC) THENL
   [ASM_CASES_TAC "t:Term = s" THEN ASM_REWRITE_TAC[IMP_REFL] THEN
    MAP_EVERY MATCH_MP_TAC [IMP_TRUE_LEMMA; base] THEN BETA_TAC THEN
    ASM_REWRITE_TAC[];
    MATCH_MP_TAC mpth THEN EXISTS_TAC "Imp s p" THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC mpth THEN EXISTS_TAC "Imp s (Imp p q)" THEN
    ASM_REWRITE_TAC[ax2]]);;