# HG changeset patch # User paulson # Date 864306716 -7200 # Node ID cdcc4d5602b671cae95b7d1577eac5dd5b7de8a8 # Parent 4f5ffefa77992abf6d5f74d699e1cc44ac50d97e Now the recdef induction rule variables are named u, v, ... diff -r 4f5ffefa7799 -r cdcc4d5602b6 TFL/tfl.sml --- a/TFL/tfl.sml Thu May 22 15:11:23 1997 +0200 +++ b/TFL/tfl.sml Thu May 22 15:11:56 1997 +0200 @@ -1,3 +1,11 @@ +(* Title: TFL/tfl + ID: $Id$ + Author: Konrad Slind, Cambridge University Computer Laboratory + Copyright 1997 University of Cambridge + +Main TFL functor +*) + functor TFL(structure Rules : Rules_sig structure Thry : Thry_sig structure Thms : Thms_sig @@ -54,25 +62,21 @@ * The next function is common to pattern-match translation and * proof of completeness of cases for the induction theorem. * - * "gvvariant" make variables that are guaranteed not to be in vlist and - * furthermore, are guaranteed not to be equal to each other. The names of - * the variables will start with "v" and end in a number. + * The curried function "gvvariant" returns a function to generate distinct + * variables that are guaranteed not to be in vlist. The names of + * the variables go u, v, ..., z, aa, ..., az, ... The returned + * function contains embedded refs! *---------------------------------------------------------------------------*) -local val counter = ref 0 -in fun gvvariant vlist = let val slist = ref (map (#Name o S.dest_var) vlist) - val mem = U.mem (curry (op=)) - val dummy = counter := 0 - fun pass str = - if (mem str (!slist)) - then ( counter := !counter + 1; - pass (U.concat"v" (Int.toString(!counter)))) - else (slist := str :: !slist; str) + val vname = ref "u" + fun new() = + if !vname mem_string (!slist) + then (vname := bump_string (!vname); new()) + else (slist := !vname :: !slist; !vname) in - fn ty => S.mk_var{Name=pass "v", Ty=ty} - end -end; + fn ty => Free(new(), ty) + end; (*--------------------------------------------------------------------------- diff -r 4f5ffefa7799 -r cdcc4d5602b6 src/HOL/ex/Primes.ML --- a/src/HOL/ex/Primes.ML Thu May 22 15:11:23 1997 +0200 +++ b/src/HOL/ex/Primes.ML Thu May 22 15:11:56 1997 +0200 @@ -88,7 +88,7 @@ (*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) goal thy "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"; -by (res_inst_tac [("v","m"),("v1.0","n")] gcd_induct 1); +by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1); by (case_tac "n=0" 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_less_divisor,zero_less_eq]))); @@ -112,7 +112,7 @@ (*Maximality: for all m,n,f naturals, if f divides m and f divides n then f divides gcd(m,n)*) goal thy "!!k. (f dvd m) & (f dvd n) --> f dvd gcd(m,n)"; -by (res_inst_tac [("v","m"),("v1.0","n")] gcd_induct 1); +by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1); by (case_tac "n=0" 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [dvd_mod, mod_less_divisor,