[Hol-developers] Soundness bug in Kananaskis-5 experimental kernel

[Peter V. H. <pal...@tr...>]

In the HOL4 Kananaskis-5 system with the experimental kernel (build
-expk) there is a soundness bug, specifically in the Term.inst
function in the experimental kernel.

Demonstration of bug:

-----------------------------------------------------------------
       HOL-4 [Kananaskis 5 (built Fri Jun 12 10:52:32 2009)]

       For introductory HOL help, type: help "hol";
-----------------------------------------------------------------

[loading theories and proof tools *************** ]
[closing file "/usr/local/hol/kananaskis-5/tools/end-init-boss.sml"]
- show_types := true;
> val it = () : unit
- val num = numSyntax.num;
> val num = ``:num`` : hol_type
- val K_DEF = combinTheory.K_DEF;
> val K_DEF = |- (K :'a -> 'b -> 'a) = (\(x :'a) (y :'b). x) : thm
- val tm = list_mk_abs([``x:'a``,``x:'b``], ``x:'a``);
> val tm = ``\(x :'a) (x :'b). x`` : term
- val th1 = REWR_CONV (SYM K_DEF) tm;
> val th1 = |- (\(x :'a) (x :'b). x) = (K :'a -> 'b -> 'a) : thm
- val th2 = INST_TYPE [beta |-> alpha] th1;
> val th2 = |- (\(x :'a) (x :'a). x) = (K :'a -> 'a -> 'a) : thm
- val th3 = INST_TYPE [alpha |-> num] th2;
> val th3 = |- (\(x :num) (x :num). x) = (K :num -> num -> num) : thm
- val th4 = AP_THM (AP_THM th3 ``2``) ``1``;
> val th4 = |- (\(x :num) (x :num). x) (2 :num) (1 :num) = K (2 :num) (1 :num)
     : thm
- val th5 = PURE_REWRITE_RULE [K_DEF] th4;
> val th5 =
    |- (\(x :num) (x :num). x) (2 :num) (1 :num) =
       (\(x :num) (y :num). x) (2 :num) (1 :num) : thm
- val th6 = BETA_RULE th5;
> val th6 = |- (1 :num) = (2 :num) : thm
-

The fallacy is in the calculation of INST_TYPE to produce th2.  The
variable x:'b is unified with the variable x:'a through the bug in
Term.inst.

I'll be checking in a bug fix shortly.

Peter

-- 
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)