Instantiated some rules to avoid problems with HO unification.
authorberghofe
Wed May 07 10:56:35 2008 +0200 (2008-05-07)
changeset 26793e36a92ff543e
parent 26792 f2d75fd23124
child 26794 354c3844dfde
Instantiated some rules to avoid problems with HO unification.
src/HOL/Induct/LList.thy
src/HOL/Inductive.thy
src/HOL/NumberTheory/EulerFermat.thy
     1.1 --- a/src/HOL/Induct/LList.thy	Wed May 07 10:56:34 2008 +0200
     1.2 +++ b/src/HOL/Induct/LList.thy	Wed May 07 10:56:35 2008 +0200
     1.3 @@ -566,7 +566,7 @@
     1.4  apply (drule imageI)
     1.5  apply (erule LList_equalityI, safe)
     1.6  apply (erule llist.cases, simp_all)
     1.7 -apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
     1.8 +apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ f])+
     1.9  apply assumption  
    1.10  done
    1.11  
    1.12 @@ -574,7 +574,7 @@
    1.13  apply (drule imageI)
    1.14  apply (erule LList_equalityI, safe)
    1.15  apply (erule llist.cases, simp_all)
    1.16 -apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
    1.17 +apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ "%x. x"])+
    1.18  apply assumption 
    1.19  done
    1.20  
     2.1 --- a/src/HOL/Inductive.thy	Wed May 07 10:56:34 2008 +0200
     2.2 +++ b/src/HOL/Inductive.thy	Wed May 07 10:56:35 2008 +0200
     2.3 @@ -112,8 +112,8 @@
     2.4    and P_f: "!!S. P S ==> P(f S)"
     2.5    and P_Union: "!!M. !S:M. P S ==> P(Union M)"
     2.6    shows "P(lfp f)"
     2.7 -  using assms unfolding Sup_set_def [symmetric]
     2.8 -  by (rule lfp_ordinal_induct) 
     2.9 +  using assms unfolding Sup_set_eq [symmetric]
    2.10 +  by (rule lfp_ordinal_induct [where P=P])
    2.11  
    2.12  
    2.13  text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
    2.14 @@ -215,7 +215,7 @@
    2.15  apply (rule Un_least [THEN Un_least])
    2.16  apply (rule subset_refl, assumption)
    2.17  apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
    2.18 -apply (rule monoD, assumption)
    2.19 +apply (rule monoD [where f=f], assumption)
    2.20  apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
    2.21  done
    2.22  
     3.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Wed May 07 10:56:34 2008 +0200
     3.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Wed May 07 10:56:35 2008 +0200
     3.3 @@ -162,7 +162,7 @@
     3.4  lemma RRset_gcd [rule_format]:
     3.5      "is_RRset A m ==> a \<in> A --> zgcd (a, m) = 1"
     3.6    apply (unfold is_RRset_def)
     3.7 -  apply (rule RsetR.induct, auto)
     3.8 +  apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd (a, m) = 1"], auto)
     3.9    done
    3.10  
    3.11  lemma RsetR_zmult_mono:
    3.12 @@ -219,7 +219,7 @@
    3.13    "1 < m ==>
    3.14      is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
    3.15    apply (unfold is_RRset_def)
    3.16 -  apply (rule RsetR.induct)
    3.17 +  apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"])
    3.18      apply (auto simp add: zcong_sym)
    3.19    done
    3.20