eliminated global prems;
authorwenzelm
Wed Jan 12 16:33:04 2011 +0100 (2011-01-12)
changeset 4152654b4686704af
parent 41525 a42cbf5b44c8
child 41527 924106faa45f
eliminated global prems;
src/CCL/Set.thy
src/CCL/Type.thy
src/CCL/Wfd.thy
src/CCL/ex/Stream.thy
src/CTT/CTT.thy
src/CTT/ex/Elimination.thy
src/Cube/Cube.thy
src/FOL/ex/Intro.thy
src/FOLP/ex/Foundation.thy
src/FOLP/ex/Intro.thy
src/ZF/Induct/Tree_Forest.thy
     1.1 --- a/src/CCL/Set.thy	Wed Jan 12 15:53:37 2011 +0100
     1.2 +++ b/src/CCL/Set.thy	Wed Jan 12 16:33:04 2011 +0100
     1.3 @@ -222,7 +222,7 @@
     1.4  proof -
     1.5    have "\<not> (EX x. x:A) \<Longrightarrow> A = {}"
     1.6      by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+
     1.7 -  with prems show ?thesis by blast
     1.8 +  with assms show ?thesis by blast
     1.9  qed
    1.10  
    1.11  
     2.1 --- a/src/CCL/Type.thy	Wed Jan 12 15:53:37 2011 +0100
     2.2 +++ b/src/CCL/Type.thy	Wed Jan 12 16:33:04 2011 +0100
     2.3 @@ -214,7 +214,7 @@
     2.4  
     2.5  subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *}
     2.6  
     2.7 -lemma NatM: "mono(%X. Unit+X)";
     2.8 +lemma NatM: "mono(%X. Unit+X)"
     2.9    apply (rule PlusM constM idM)+
    2.10    done
    2.11  
    2.12 @@ -358,7 +358,7 @@
    2.13    shows "t(a) : gfp(B)"
    2.14    apply (rule coinduct)
    2.15     apply (rule_tac P = "%x. EX y:A. x=t (y)" in CollectI)
    2.16 -   apply (blast intro!: prems)+
    2.17 +   apply (blast intro!: assms)+
    2.18    done
    2.19  
    2.20  lemma def_gfpI:
     3.1 --- a/src/CCL/Wfd.thy	Wed Jan 12 15:53:37 2011 +0100
     3.2 +++ b/src/CCL/Wfd.thy	Wed Jan 12 16:33:04 2011 +0100
     3.3 @@ -253,11 +253,11 @@
     3.4    shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
     3.5    apply (unfold letrec2_def)
     3.6    apply (rule SPLITB [THEN subst])
     3.7 -  apply (assumption | rule letrecT pairT splitT prems)+
     3.8 +  apply (assumption | rule letrecT pairT splitT assms)+
     3.9    apply (subst SPLITB)
    3.10 -  apply (assumption | rule ballI SubtypeI prems)+
    3.11 +  apply (assumption | rule ballI SubtypeI assms)+
    3.12    apply (rule SPLITB [THEN subst])
    3.13 -  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
    3.14 +  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
    3.15      erule bspec SubtypeE sym [THEN subst])+
    3.16    done
    3.17  
    3.18 @@ -275,11 +275,11 @@
    3.19    shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
    3.20    apply (unfold letrec3_def)
    3.21    apply (rule lem [THEN subst])
    3.22 -  apply (assumption | rule letrecT pairT splitT prems)+
    3.23 +  apply (assumption | rule letrecT pairT splitT assms)+
    3.24    apply (simp add: SPLITB)
    3.25 -  apply (assumption | rule ballI SubtypeI prems)+
    3.26 +  apply (assumption | rule ballI SubtypeI assms)+
    3.27    apply (rule lem [THEN subst])
    3.28 -  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
    3.29 +  apply (assumption | rule letrecT SubtypeI pairT splitT assms |
    3.30      erule bspec SubtypeE sym [THEN subst])+
    3.31    done
    3.32  
    3.33 @@ -520,7 +520,7 @@
    3.34    assumes "f ---> lam x. b(x)"
    3.35      and "b(a) ---> c"
    3.36    shows "f ` a ---> c"
    3.37 -  unfolding apply_def by (eval prems)
    3.38 +  unfolding apply_def by (eval assms)
    3.39  
    3.40  lemma letV:
    3.41    assumes 1: "t ---> a"
     4.1 --- a/src/CCL/ex/Stream.thy	Wed Jan 12 15:53:37 2011 +0100
     4.2 +++ b/src/CCL/ex/Stream.thy	Wed Jan 12 16:33:04 2011 +0100
     4.3 @@ -63,7 +63,7 @@
     4.4    shows "map(f,l@m) = map(f,l) @ map(f,m)"
     4.5    apply (tactic {* eq_coinduct3_tac @{context}
     4.6      "{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *})
     4.7 -  apply (blast intro: prems)
     4.8 +  apply (blast intro: assms)
     4.9    apply safe
    4.10    apply (drule ListsXH [THEN iffD1])
    4.11    apply (tactic "EQgen_tac @{context} [] 1")
    4.12 @@ -82,7 +82,7 @@
    4.13    shows "k @ l @ m = (k @ l) @ m"
    4.14    apply (tactic {* eq_coinduct3_tac @{context}
    4.15      "{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*})
    4.16 -  apply (blast intro: prems)
    4.17 +  apply (blast intro: assms)
    4.18    apply safe
    4.19    apply (drule ListsXH [THEN iffD1])
    4.20    apply (tactic "EQgen_tac @{context} [] 1")
    4.21 @@ -100,7 +100,7 @@
    4.22    shows "l @ m = l"
    4.23    apply (tactic {* eq_coinduct3_tac @{context}
    4.24      "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *})
    4.25 -  apply (blast intro: prems)
    4.26 +  apply (blast intro: assms)
    4.27    apply safe
    4.28    apply (drule IListsXH [THEN iffD1])
    4.29    apply (tactic "EQgen_tac @{context} [] 1")
     5.1 --- a/src/CTT/CTT.thy	Wed Jan 12 15:53:37 2011 +0100
     5.2 +++ b/src/CTT/CTT.thy	Wed Jan 12 16:33:04 2011 +0100
     5.3 @@ -319,7 +319,7 @@
     5.4      and "a: A"
     5.5      and "!!z. z: B(a) ==> c(z): C(z)"
     5.6    shows "c(p`a): C(p`a)"
     5.7 -apply (rule prems ProdE)+
     5.8 +apply (rule assms ProdE)+
     5.9  done
    5.10  
    5.11  
     6.1 --- a/src/CTT/ex/Elimination.thy	Wed Jan 12 15:53:37 2011 +0100
     6.2 +++ b/src/CTT/ex/Elimination.thy	Wed Jan 12 16:33:04 2011 +0100
     6.3 @@ -145,7 +145,7 @@
     6.4  apply (rule subst_eqtyparg)
     6.5  apply (rule comp_rls)
     6.6  apply (rule_tac [4] SumE_snd)
     6.7 -apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms prems}) *})
     6.8 +apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms assms}) *})
     6.9  done
    6.10  
    6.11  text "Axiom of choice.  Proof without fst, snd.  Harder still!"
     7.1 --- a/src/Cube/Cube.thy	Wed Jan 12 15:53:37 2011 +0100
     7.2 +++ b/src/Cube/Cube.thy	Wed Jan 12 16:33:04 2011 +0100
     7.3 @@ -76,11 +76,11 @@
     7.4  
     7.5  lemma imp_elim:
     7.6    assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P"
     7.7 -  shows "PROP P" by (rule app prems)+
     7.8 +  shows "PROP P" by (rule app assms)+
     7.9  
    7.10  lemma pi_elim:
    7.11    assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P"
    7.12 -  shows "PROP P" by (rule app prems)+
    7.13 +  shows "PROP P" by (rule app assms)+
    7.14  
    7.15  
    7.16  locale L2 =
     8.1 --- a/src/FOL/ex/Intro.thy	Wed Jan 12 15:53:37 2011 +0100
     8.2 +++ b/src/FOL/ex/Intro.thy	Wed Jan 12 16:33:04 2011 +0100
     8.3 @@ -76,7 +76,7 @@
     8.4    shows "~ P"
     8.5  apply (unfold not_def)
     8.6  apply (rule impI)
     8.7 -apply (rule prems)
     8.8 +apply (rule assms)
     8.9  apply assumption
    8.10  done
    8.11  
     9.1 --- a/src/FOLP/ex/Foundation.thy	Wed Jan 12 15:53:37 2011 +0100
     9.2 +++ b/src/FOLP/ex/Foundation.thy	Wed Jan 12 16:33:04 2011 +0100
     9.3 @@ -23,17 +23,17 @@
     9.4    assumes "p : A & B"
     9.5      and "!!x y. x : A ==> y : B ==> f(x, y) : C"
     9.6    shows "?p : C"
     9.7 -apply (rule prems)
     9.8 +apply (rule assms)
     9.9  apply (rule conjunct1)
    9.10 -apply (rule prems)
    9.11 +apply (rule assms)
    9.12  apply (rule conjunct2)
    9.13 -apply (rule prems)
    9.14 +apply (rule assms)
    9.15  done
    9.16  
    9.17  schematic_lemma
    9.18    assumes "!!A x. x : ~ ~A ==> cla(x) : A"
    9.19    shows "?p : B | ~B"
    9.20 -apply (rule prems)
    9.21 +apply (rule assms)
    9.22  apply (rule notI)
    9.23  apply (rule_tac P = "~B" in notE)
    9.24  apply (rule_tac [2] notI)
    9.25 @@ -51,7 +51,7 @@
    9.26  schematic_lemma
    9.27    assumes "!!A x. x : ~ ~A ==> cla(x) : A"
    9.28    shows "?p : B | ~B"
    9.29 -apply (rule prems)
    9.30 +apply (rule assms)
    9.31  apply (rule notI)
    9.32  apply (rule notE)
    9.33  apply (rule_tac [2] notI)
    9.34 @@ -68,11 +68,11 @@
    9.35      and "q : ~ ~A"
    9.36    shows "?p : A"
    9.37  apply (rule disjE)
    9.38 -apply (rule prems)
    9.39 +apply (rule assms)
    9.40  apply assumption
    9.41  apply (rule FalseE)
    9.42  apply (rule_tac P = "~A" in notE)
    9.43 -apply (rule prems)
    9.44 +apply (rule assms)
    9.45  apply assumption
    9.46  done
    9.47  
    9.48 @@ -84,7 +84,7 @@
    9.49    shows "?p : ALL z. G(z)|H(z)"
    9.50  apply (rule allI)
    9.51  apply (rule disjI1)
    9.52 -apply (rule prems [THEN spec])
    9.53 +apply (rule assms [THEN spec])
    9.54  done
    9.55  
    9.56  schematic_lemma "?p : ALL x. EX y. x=y"
    9.57 @@ -112,7 +112,7 @@
    9.58    assumes "p : (EX z. F(z)) & B"
    9.59    shows "?p : EX z. F(z) & B"
    9.60  apply (rule conjE)
    9.61 -apply (rule prems)
    9.62 +apply (rule assms)
    9.63  apply (rule exE)
    9.64  apply assumption
    9.65  apply (rule exI)
    10.1 --- a/src/FOLP/ex/Intro.thy	Wed Jan 12 15:53:37 2011 +0100
    10.2 +++ b/src/FOLP/ex/Intro.thy	Wed Jan 12 16:33:04 2011 +0100
    10.3 @@ -76,7 +76,7 @@
    10.4    shows "?p : ~ P"
    10.5  apply (unfold not_def)
    10.6  apply (rule impI)
    10.7 -apply (rule prems)
    10.8 +apply (rule assms)
    10.9  apply assumption
   10.10  done
   10.11  
    11.1 --- a/src/ZF/Induct/Tree_Forest.thy	Wed Jan 12 15:53:37 2011 +0100
    11.2 +++ b/src/ZF/Induct/Tree_Forest.thy	Wed Jan 12 16:33:04 2011 +0100
    11.3 @@ -176,7 +176,7 @@
    11.4    assumes "!!x. x \<in> A ==> h(x): B"
    11.5    shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
    11.6      and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
    11.7 -  using prems
    11.8 +  using assms
    11.9    by (induct rule: tree'induct forest'induct) simp_all
   11.10  
   11.11  text {*