Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 21 Jun 1993 15:07:42 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02353; Mon, 21 Jun 93 06:53:54 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA02348; Mon, 21 Jun 93 06:53:42 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 21 Jun 1993 14:52:35 +0100 To: shaw@cs.ucdavis.edu (Rob Shaw) Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk Subject: Re: CASES vs. INDUCT In-Reply-To: Your message of "Sun, 20 Jun 93 21:38:46 PDT." <9306210438.AA13884@toadflax.cs.ucdavis.edu> Date: Mon, 21 Jun 93 14:52:30 +0100 From: Tom Melham Message-Id: <"swan.cl.cam.:251130:930621135240"@cl.cam.ac.uk> Rob Shaw asks about case analsis vs induction: > If I have a type without recursive constructor: > ... > and I need to prove something like > > (2) ! t:Thing. P t You can do either cases analysis OR induction here. Since there are no recursive constructors, they amount to pretty much the same thing. For example, #let ty = define_type `ty` `ty = C1 | C2 num | C3 num num`;; ty = ... #let ind = prove_induction_thm ty;; ind = |- !P. P C1 /\ (!n. P(C2 n)) /\ (!n0 n1. P(C3 n0 n1)) ==> (!t. P t) #let cases = prove_cases_thm ind;; cases = |- !t. (t = C1) \/ (?n. t = C2 n) \/ (?n0 n1. t = C3 n0 n1) Now, suppose we have the goal: #g "!t:ty. P [t]";; "!t. P[t]" () : void Then induction gives the following: #expand (INDUCT_THEN ind (K ALL_TAC));; OK.. 3 subgoals "!n0 n1. P[C3 n0 n1]" "!n. P[C2 n]" "P[C1]" () : void Backing up... #b();; "!t. P[t]" () : void A (roughly) similar effect can be gotten by a case analysis: #e(GEN_TAC THEN STRUCT_CASES_TAC (SPEC "t:ty" cases));; OK.. 3 subgoals "P[C3 n0 n1]" "P[C2 n]" "P[C1]" () : void Notice that the variables n,n0,n1 do not get universally quantified. If we wanted exactly the same effect, we could do: #let CASES_TAC cases (A,g) = let x,body = dest_forall g in let xv = genvar (type_of x) in % in case x free in A % let sthm = SPEC xv cases in let fvs = \t. subtract (frees t) (frees g) in % in case g has frees % let stac (A,g) = MAP_EVERY (\t. SPEC_TAC (t,t)) (fvs g) (A,g) in EVERY [X_GEN_TAC xv; REPEAT_TCL STRIP_THM_THEN SUBST1_TAC sthm; stac] (A,g);; CASES_TAC = - : thm_tactic #g "!t:ty.P[t]";; "!t. P[t]" () : void #expand (CASES_TAC cases);; 3 subgoals "!n1 n0. P[C3 n0 n1]" "!n. P[C2 n]" "P[C1]" () : void The resulting tactic may, however, not generalize the variables in the *same order* as induction... Tom