examples/sigma/variableScript.sml

57 (* "variant" number; initially this will be zero, but when   *)
83 (* We define Index v as the "variant" number attached to the base. *)
123 (* itself is also considered to be a (null) variant of itself.     *)
127 (* An easy way to make a variant is to take an existing variable   *)
128 (* and add an integer to its "variant" number.                     *)
172 (* We would like to be able to test if a variable is a variant of  *)
323 (* We need to be able to detect when a variable is a variant of        *)
324 (* another variable, and when it is the *minimum* such variant,        *)
331 (* Here finally is the definition of the variant function. *)
332 (* "variant x s" is a string with x as its prefix, but     *)
333 (* with some number appended to x.  This variant is        *)
335 (* such variant (with the least index appended).           *)
371 val variant =
374          {name    = "variant",
375           consts  = [{const_name = "variant", fixity = NONE (*700*)}],
382 (* variant =
385        (variant x s IN variant_set x (SUC (CARD s)) /\
386        ~(variant x s IN s)) /\
389          Index (variant x s) <= Index z) : thm
402     ���!x s. FINITE s ==> (variant x s) IN (variant_set x (SUC(CARD s)))���,
404     THEN IMP_RES_THEN REWRITE_THM variant
410     ���!x s. FINITE s ==> ~(variant x s IN s)���,
413     THEN IMP_RES_THEN REWRITE_THM variant
420                      (Index(variant x s)) <= (Index y)���,
423     THEN IMP_RES_TAC variant
430     ���!x s t. FINITE s /\ t SUBSET s ==> ~(variant x s IN t)���,
439     ���!x s. FINITE s ==> (variant x s) is_variant x���,
448 (* Now we wish to express the variant definition more simply,   *)
449 (* by just saying that the variant selected is just a variant,  *)
450 (* without referring to any variant-sets.                       *)
457               ((variant x s) is_variant x /\ ~((variant x s) IN s))
459                      (Index (variant x s) <= Index z)���,
462     THEN IMP_RES_THEN REWRITE_THM variant
489                      (Index(variant x s) <= Index y)���,
497     ���!x s. FINITE s ==> (variant x s) is_variant x���,
508 (* Now we need to prove that the variant function as defined above *)
511 (* 1. the variant is a real variant of the original variable;      *)
513 (* 2. the variant is not a member of the exclusion list; and       *)
515 (* 3. the variant is the minimum such variant, as reckoned by      *)
522     ���!x s. FINITE s ==> (Base (variant x s) = Base x)���,
530     ���!x s. FINITE s ==> Index x <= Index (variant x s)���,
539     ���!x. variant x EMPTY = x���,
580     ���!x s. FINITE s /\ (x IN s) ==> ~(x = variant x s)���,
593     ���!x s. FINITE s /\ (x IN s) ==> ~(Index x = Index (variant x s))���,
602     ���!x k s. FINITE s ==> (variant (mk_variant x k) s) is_variant x���,
612     ���!x s. FINITE s ==> ~(variant (mk_variant x 1) s = x)���,
630               (variant x s = (if x IN s then variant (mk_variant x 1) s  else  x))���,
664    ���!x s. FINITE s /\ ~(x IN s) ==> (variant x s = x)���,
674    ���!x s. FINITE s ==> (variant x (s DELETE x) = x)���,
685       FINITE s /\ (x IN s) ==> (variant x s = variant (mk_variant x 1) s)���,
708                (let x' = variant x s in
718                   (CONS (variant x (SL xs' UNION s)) xs')))���;
727          (CONS (variant x s) (variants xs ((variant x s) INSERT s))))���,
781    THEN FIRST_ASSUM (MP_TAC o SPEC ���(variant x' s) INSERT s���)