# HG changeset patch # User paulson # Date 909834325 -3600 # Node ID 54276fba84202164be07f6eb05d4c36d66693b64 # Parent 95ac0bf10518896b443509b9c0bfefdfec952672 the Increasing operator diff -r 95ac0bf10518 -r 54276fba8420 src/HOL/UNITY/Constrains.ML --- a/src/HOL/UNITY/Constrains.ML Sat Oct 31 12:43:56 1998 +0100 +++ b/src/HOL/UNITY/Constrains.ML Sat Oct 31 12:45:25 1998 +0100 @@ -150,6 +150,27 @@ +(*** Increasing ***) + +Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def] + "Increasing f <= Increasing (length o f)"; +by Auto_tac; +by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1); +qed "Increasing_length"; + +Goalw [Increasing_def] + "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}"; +by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); +by (Blast_tac 1); +qed "Increasing_less"; + +Goalw [increasing_def, Increasing_def] + "F : increasing f ==> F : Increasing f"; +by (blast_tac (claset() addIs [stable_imp_Stable]) 1); +qed "increasing_imp_Increasing"; + + + (*** The Elimination Theorem. The "free" m has become universally quantified! Should the premise be !!m instead of ALL m ? Would make it harder to use in forward proof. ***) diff -r 95ac0bf10518 -r 54276fba8420 src/HOL/UNITY/Constrains.thy --- a/src/HOL/UNITY/Constrains.thy Sat Oct 31 12:43:56 1998 +0100 +++ b/src/HOL/UNITY/Constrains.thy Sat Oct 31 12:45:25 1998 +0100 @@ -23,4 +23,8 @@ Invariant :: "'a set => 'a program set" "Invariant A == {F. Init F <= A} Int Stable A" + (*Polymorphic in both states and the meaning of <= *) + Increasing :: "['a => 'b::{ord}] => 'a program set" + "Increasing f == INT z. Stable {s. z <= f s}" + end