Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
To: info-hol@ted.cs.uidaho.edu
Subject: Re: Parnas: "some theorems we should prove"
In-Reply-To: Your message of "Fri, 18 Jun 93 01:02:14 BST." <"swan.cl.cam.:266830:930618000222"@cl.cam.ac.uk>
Date: Mon, 21 Jun 93 18:16:41 +0100
From: Sara Kalvala <Sara.Kalvala@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:292530:930621171650"@cl.cam.ac.uk>


One more proof session for the "Parnas theorems", this time in
Isabelle. Most of them were done in a line or two, and were quite
easy. As you can see, they often entailed in an application of
"fast_tac". I hope I understood the problems correctly!

						- Sara

-----
|| THE INTRODUCTORY EXAMPLE
||
|| The first 2 theorems to be proved here are straightforward
|| arithmetic examples, so I used the Higher-Order Logic instantiation
|| of Isabelle. I have simplified the work somewhat by using natural
|| numbers rather than reals, as it shouldn't matter for these
|| cases. The proofs are "automatic". 
-----


prove_goal Arith.thy " x < 0 | x = 0 | 0 < x"
(fn _ => [resolve_tac [less_linear] 1]);

val cs = HOL_cs addSEs [less_anti_refl] addEs [less_anti_sym];

prove_goal Arith.thy
 "~ ((x < 0 & x = 0) | (x < 0 & 0 < x) | (0 < x & x = 0))"
(fn _ => [fast_tac cs 1]);


-----
|| Because the theorems to do with square root entail in reasoning
|| about partial functions, I have a quick-and-dirty typing theory for
|| square root and negation, based on ZF:
-----


val sqrt_theory = extend_theory Arith.thy "sqrt"
([],[],[],[],
[(["sqrt","minus"],"i=>i"),
 (["neg","non_neg"],"i")], None)
[("sqrt_dom", "x :non_neg ==> sqrt(x):non_neg"),
 ("minus_rl1", "x :neg ==> minus(x):non_neg"),
 ("minus_rl2", "x :non_neg ==> minus(x):neg")];

-----
|| With this theory, it is easy to prove the next two theorems:
-----

val sqrt_dom = get_axiom sqrt_theory "sqrt_dom";
val minus_rl1 = get_axiom sqrt_theory "minus_rl1";
val minus_rl2 = get_axiom sqrt_theory "minus_rl2";


prove_goal sqrt_theory "x :neg --> sqrt(minus(x)) : non_neg"
(fn _ => [resolve_tac [impI] 1,
	  resolve_tac [sqrt_dom] 1,
	  eresolve_tac [minus_rl1] 1]);

prove_goal sqrt_theory "x :non_neg --> sqrt(x) : non_neg"
(fn _ => [resolve_tac [impI] 1,
	  eresolve_tac [sqrt_dom] 1]);

-----
|| The possibility exists to extend ZF with rules as given in the
|| background paper by Beeson; this will probably be done soon.
-----

-----
|| ARRAY SEARCH EXAMPLE
||
|| The simple theorems are obtained automatically, using arithmetic
|| built on Higher-Order logic:
-----

prove_goal Arith.thy
"(? i . B(i) = x) | (! i . ((0 < i) & (i < Suc(N))) --> ~ (B(i) = x))"
(fn _ => [fast_tac cs 1]);

prove_goal Arith.thy
" ~ ((? i . ((0 < i) & (i < Suc(N))) & (B(i) = x)) &     \
\    (! i . ((0 < i) & (i < Suc(N))) --> ~ (B(i) = x)))"
(fn _ => [fast_tac cs 1]);


-----
|| PALINDROME EXAMPLE
||
|| As this example has to do with inclusion in a set, I thought I
|| would use the ZF logic. The arithmetic is not as highly supported
|| as in the Higher-Order Logic; my aim is to show that one can
|| develop lemmas as needed quite easily, such that full automation is
|| not really necessary to keep proofs simple.
-----

-----
|| The first theorem is trivial. I simplified the goal a bit because I
|| used natural numbers rather than integers.
-----

prove_goal Arith.thy
"(EX l:nat. (ALL i. (i : n #/ succ(succ(0))) \
\                      --> (A(l #+ i) = A(l #+ n #- 1 #- i)))) --> \
\ ~ ({l:nat. (ALL i. (i : n #/ succ(succ(0))) \
\                      --> (A(l #+ i) = A(l #+ n #- 1 #- i)))} <= 0)"
(fn _ => [fast_tac ZF_cs 1]);

-----
|| For the second one i needed a couple lemmas, both of which were
|| quite easy to prove.
-----

val not_empty =
(prove_goal Arith.thy "(EX x:y. P(x)) --> ~({x:y. P(x)} <= 0)"
(fn _ => [fast_tac ZF_cs 1])) RS mp;

val my_cs = ZF_cs addIs [nat_0I,nat_succI];

val div_1_2 =
prove_goal Arith.thy "succ(0) #/ succ(succ(0)) = 0"
(fn _ => [resolve_tac [quo_less] 1,
	  ALLGOALS (fast_tac my_cs)]);

-----
|| From these two lemmas and by an explicit instantiation I have:
-----

prove_goal Arith.thy
" ~ ({n :nat . (EX l. (ALL i. (i : n #/ succ(succ(0))) --> \
\     (A(l #+ i) = A(l #+ n #- 1 #- i))))} <= 0)"
(fn _ => [resolve_tac [not_empty] 1,
	  res_inst_tac [("x","succ(0)")] bexI 1,
	  SIMP_TAC (ZF_ss addrews [div_1_2]) 1,
	  fast_tac my_cs 1]);