src/HOL/UNITY/Constrains.ML
changeset 6704 5febcf428342
parent 6672 8542c6dda828
child 6739 66e4118eead9
equal deleted inserted replaced
6703:8103c1fb092d 6704:5febcf428342
   199 
   199 
   200 
   200 
   201 (*** Increasing ***)
   201 (*** Increasing ***)
   202 
   202 
   203 Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
   203 Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
   204      "Increasing f <= Increasing (length o f)";
   204      "mono g ==> Increasing f <= Increasing (g o f)";
   205 by Auto_tac;
   205 by Auto_tac;
   206 by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1);
   206 by (blast_tac (claset() addIs [monoD, order_trans]) 1);
   207 qed "Increasing_size";
   207 qed "mono_Increasing_o";
   208 
   208 
   209 Goalw [Increasing_def]
   209 Goalw [Increasing_def]
   210      "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}";
   210      "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}";
   211 by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
   211 by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
   212 by (Blast_tac 1);
   212 by (Blast_tac 1);
   214 
   214 
   215 Goalw [increasing_def, Increasing_def]
   215 Goalw [increasing_def, Increasing_def]
   216      "F : increasing f ==> F : Increasing f";
   216      "F : increasing f ==> F : Increasing f";
   217 by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
   217 by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
   218 qed "increasing_imp_Increasing";
   218 qed "increasing_imp_Increasing";
   219 
       
   220 
   219 
   221 
   220 
   222 (*** The Elimination Theorem.  The "free" m has become universally quantified!
   221 (*** The Elimination Theorem.  The "free" m has become universally quantified!
   223      Should the premise be !!m instead of ALL m ?  Would make it harder to use
   222      Should the premise be !!m instead of ALL m ?  Would make it harder to use
   224      in forward proof. ***)
   223      in forward proof. ***)