--- a/src/HOL/Bali/AxCompl.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/AxCompl.thy Thu Sep 22 23:56:15 2005 +0200
@@ -451,9 +451,9 @@
proof -
from eval_e wt_e da_e wf normal_s1
have "nrm C \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approxE') rules
+ by (cases rule: da_good_approxE') iprover
with da_ps show ?thesis
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
qed
}
ultimately show ?thesis
@@ -845,7 +845,7 @@
show ?thesis
by (rule eval_type_soundE)
qed
- ultimately show ?thesis by rules
+ ultimately show ?thesis by iprover
qed
qed
next
@@ -1528,7 +1528,7 @@
proof -
from eval_t type_ok wf
obtain n where evaln: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
- by (rule eval_to_evaln [elim_format]) rules
+ by (rule eval_to_evaln [elim_format]) iprover
from valid have
valid_expanded:
"\<forall>n Y s Z. P Y s Z \<longrightarrow> type_ok G t s
--- a/src/HOL/Bali/AxSound.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/AxSound.thy Thu Sep 22 23:56:15 2005 +0200
@@ -192,7 +192,7 @@
from evaln have "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
by (rule evaln_eval)
from this wt da wf elim show P
- by (rule da_good_approxE') rules+
+ by (rule da_good_approxE') iprover+
qed
lemma validI:
@@ -336,7 +336,7 @@
proof -
from evaln have "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by (rule evaln_eval)
from this hyps show ?thesis
- by (rule dom_locals_eval_mono_elim) rules+
+ by (rule dom_locals_eval_mono_elim) iprover+
qed
@@ -616,7 +616,7 @@
proof -
from eval_e1 wt_e1 da_e1 wf True
have "nrm E1 \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approx_evalnE) rules
+ by (cases rule: da_good_approx_evalnE) iprover
with da_e2 show ?thesis
by (rule da_weakenE)
qed
@@ -944,7 +944,7 @@
obtain E2 where
da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1))
\<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
- by (rule da_e2_BinOp [elim_format]) rules
+ by (rule da_e2_BinOp [elim_format]) iprover
from wt_e2 wt_Skip obtain T2
where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
\<turnstile>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<Colon>T2"
@@ -957,7 +957,7 @@
case False
note ve=validE [OF valid_e2,OF Q' valid_A conf_s1 eval_e2]
with False show ?thesis
- by rules
+ by iprover
qed
with v have "R \<lfloor>v\<rfloor>\<^sub>e s2 Z"
by simp
@@ -1068,7 +1068,7 @@
proof -
from eval_var wt_var da_var wf True
have "nrm V \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approx_evalnE) rules
+ by (cases rule: da_good_approx_evalnE) iprover
with da_e show ?thesis
by (rule da_weakenE)
qed
@@ -1079,7 +1079,7 @@
case False
note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
with False show ?thesis
- by rules
+ by iprover
qed
with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
by simp
@@ -1120,7 +1120,7 @@
case False
note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
with False show ?thesis
- by rules
+ by iprover
qed
with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
by simp
@@ -1213,7 +1213,7 @@
case False
with valid_then_else P' valid_A conf_s1 eval_then_else
show ?thesis
- by (cases rule: validE) rules+
+ by (cases rule: validE) iprover+
qed
moreover
from eval wt da conf_s0 wf
@@ -1308,7 +1308,7 @@
proof -
from evaln_e wt_e da_e wf True
have "nrm C \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approx_evalnE) rules
+ by (cases rule: da_good_approx_evalnE) iprover
with da_args show ?thesis
by (rule da_weakenE)
qed
@@ -1328,7 +1328,7 @@
case False
with valid_args Q valid_A conf_s1 evaln_args
obtain "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" "s2\<Colon>\<preceq>(G,L)"
- by (cases rule: validE) rules+
+ by (cases rule: validE) iprover+
moreover
from False evaln_args have "s2=s1"
by auto
@@ -1413,7 +1413,7 @@
proof -
from evaln_e wt_e da_e wf normal_s1
have "nrm C \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approx_evalnE) rules
+ by (cases rule: da_good_approx_evalnE) iprover
with da_args show ?thesis
by (rule da_weakenE)
qed
@@ -1545,7 +1545,7 @@
,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
\<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
res: "Result \<in> nrm M'"
- by (rule wf_mdeclE) rules
+ by (rule wf_mdeclE) iprover
from da_body is_static_eq L' have
"\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr>
\<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
@@ -1594,7 +1594,7 @@
"\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3'))
\<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
using da
- by (rules intro: da.Body assigned.select_convs)
+ by (iprover intro: da.Body assigned.select_convs)
from _ this [simplified]
show ?thesis
by (rule da.Methd [simplified,elim_format])
@@ -1602,12 +1602,12 @@
qed
from valid_methd R' valid_A conf_s3' evaln_methd wt_methd da_methd
have "(set_lvars l .; S) \<lfloor>v\<rfloor>\<^sub>e s4 Z"
- by (cases rule: validE) rules+
+ by (cases rule: validE) iprover+
with s5 l show ?thesis
by simp
qed
qed
- with conf_s5 show ?thesis by rules
+ with conf_s5 show ?thesis by iprover
qed
qed
next
@@ -1755,7 +1755,7 @@
proof -
from eval_e wt_e da_e wf True
have "nrm E1 \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approx_evalnE) rules
+ by (cases rule: da_good_approx_evalnE) iprover
with da_es show ?thesis
by (rule da_weakenE)
qed
@@ -1766,7 +1766,7 @@
case False
with valid_es Q' valid_A conf_s1 eval_es
show ?thesis
- by (cases rule: validE) rules+
+ by (cases rule: validE) iprover+
qed
with v have "R \<lfloor>v\<rfloor>\<^sub>l s2 Z"
by simp
@@ -1904,7 +1904,7 @@
proof -
from eval_c1 wt_c1 da_c1 wf True
have "nrm C1 \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approx_evalnE) rules
+ by (cases rule: da_good_approx_evalnE) iprover
with da_c2 show ?thesis
by (rule da_weakenE)
qed
@@ -1915,7 +1915,7 @@
case False
from valid_c2 Q valid_A conf_s1 eval_c2 False
show ?thesis
- by (cases rule: validE) rules+
+ by (cases rule: validE) iprover+
qed
moreover
from eval wt da conf_s0 wf
@@ -1992,7 +1992,7 @@
case False
with valid_then_else P' valid_A conf_s1 eval_then_else
show ?thesis
- by (cases rule: validE) rules+
+ by (cases rule: validE) iprover+
qed
moreover
from eval wt da conf_s0 wf
--- a/src/HOL/Bali/Decl.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/Decl.thy Thu Sep 22 23:56:15 2005 +0200
@@ -80,7 +80,7 @@
have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
by (auto simp add: less_acc_def split add: acc_modi.split)
with prems show ?thesis
- by (unfold le_acc_def) rules
+ by (unfold le_acc_def) iprover
qed
next
show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
--- a/src/HOL/Bali/DefiniteAssignment.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Thu Sep 22 23:56:15 2005 +0200
@@ -1350,18 +1350,18 @@
from da
show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
proof (induct)
- case Skip thus ?case by (rules intro: da.Skip)
+ case Skip thus ?case by (iprover intro: da.Skip)
next
- case Expr thus ?case by (rules intro: da.Expr)
+ case Expr thus ?case by (iprover intro: da.Expr)
next
case (Lab A B C Env c l B')
have "PROP ?Hyp Env B \<langle>c\<rangle>" .
moreover
have B': "B \<subseteq> B'" .
ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
- by rules
+ by iprover
then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'"
- by (rules intro: da.Lab)
+ by (iprover intro: da.Lab)
thus ?case ..
next
case (Comp A B C1 C2 Env c1 c2 B')
@@ -1370,7 +1370,7 @@
moreover
have B': "B \<subseteq> B'" .
ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
- by rules
+ by iprover
with da_c1 B'
have
"nrm C1 \<subseteq> nrm C1'"
@@ -1378,9 +1378,9 @@
moreover
have "PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>" .
ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
- by rules
+ by iprover
with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'"
- by (rules intro: da.Comp)
+ by (iprover intro: da.Comp)
thus ?case ..
next
case (If A B C1 C2 E Env c1 c2 e B')
@@ -1389,7 +1389,7 @@
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain C1' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
@@ -1400,7 +1400,7 @@
moreover
have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle>" by (rule If.hyps)
ultimately
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain C2' where "Env\<turnstile> (B' \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
@@ -1410,11 +1410,11 @@
moreover
have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle>" by (rule If.hyps)
ultimately
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
ultimately
obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'"
- by (rules intro: da.If)
+ by (iprover intro: da.If)
thus ?case ..
next
case (Loop A B C E Env c e l B')
@@ -1423,7 +1423,7 @@
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain C' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
@@ -1434,11 +1434,11 @@
moreover
have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle>" by (rule Loop.hyps)
ultimately
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
ultimately
obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'"
- by (rules intro: da.Loop )
+ by (iprover intro: da.Loop )
thus ?case ..
next
case (Jmp A B Env jump B')
@@ -1453,12 +1453,12 @@
| Cont l \<Rightarrow> \<lambda>k. UNIV
| Ret \<Rightarrow> \<lambda>k. UNIV)"
- by rules
+ by iprover
ultimately have "Env\<turnstile> B' \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A'"
by (rule da.Jmp)
thus ?case ..
next
- case Throw thus ?case by (rules intro: da.Throw )
+ case Throw thus ?case by (iprover intro: da.Throw )
next
case (Try A B C C1 C2 Env c1 c2 vn B')
have B': "B \<subseteq> B'" .
@@ -1466,7 +1466,7 @@
proof -
have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain C2' where
@@ -1478,11 +1478,11 @@
(B \<union> {VName vn}) \<langle>c2\<rangle>"
by (rule Try.hyps)
ultimately
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
ultimately
obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'"
- by (rules intro: da.Try )
+ by (iprover intro: da.Try )
thus ?case ..
next
case (Fin A B C1 C2 Env c1 c2 B')
@@ -1491,33 +1491,33 @@
proof -
have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain C2' where "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
proof -
have "PROP ?Hyp Env B \<langle>c2\<rangle>" by (rule Fin.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
ultimately
obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'"
- by (rules intro: da.Fin )
+ by (iprover intro: da.Fin )
thus ?case ..
next
- case Init thus ?case by (rules intro: da.Init)
+ case Init thus ?case by (iprover intro: da.Init)
next
- case NewC thus ?case by (rules intro: da.NewC)
+ case NewC thus ?case by (iprover intro: da.NewC)
next
- case NewA thus ?case by (rules intro: da.NewA)
+ case NewA thus ?case by (iprover intro: da.NewA)
next
- case Cast thus ?case by (rules intro: da.Cast)
+ case Cast thus ?case by (iprover intro: da.Cast)
next
- case Inst thus ?case by (rules intro: da.Inst)
+ case Inst thus ?case by (iprover intro: da.Inst)
next
- case Lit thus ?case by (rules intro: da.Lit)
+ case Lit thus ?case by (iprover intro: da.Lit)
next
- case UnOp thus ?case by (rules intro: da.UnOp)
+ case UnOp thus ?case by (iprover intro: da.UnOp)
next
case (CondAnd A B E1 E2 Env e1 e2 B')
have B': "B \<subseteq> B'" .
@@ -1525,7 +1525,7 @@
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain E2' where "Env\<turnstile> B' \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
@@ -1534,11 +1534,11 @@
by blast
moreover
have "PROP ?Hyp Env (B \<union> assigns_if True e1) \<langle>e2\<rangle>" by (rule CondAnd.hyps)
- ultimately show ?thesis using that by rules
+ ultimately show ?thesis using that by iprover
qed
ultimately
obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'"
- by (rules intro: da.CondAnd)
+ by (iprover intro: da.CondAnd)
thus ?case ..
next
case (CondOr A B E1 E2 Env e1 e2 B')
@@ -1547,7 +1547,7 @@
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain E2' where "Env\<turnstile> B' \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
@@ -1556,11 +1556,11 @@
by blast
moreover
have "PROP ?Hyp Env (B \<union> assigns_if False e1) \<langle>e2\<rangle>" by (rule CondOr.hyps)
- ultimately show ?thesis using that by rules
+ ultimately show ?thesis using that by iprover
qed
ultimately
obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A'"
- by (rules intro: da.CondOr)
+ by (iprover intro: da.CondOr)
thus ?case ..
next
case (BinOp A B E1 Env binop e1 e2 B')
@@ -1569,7 +1569,7 @@
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
@@ -1580,35 +1580,35 @@
by (rule da_monotone [THEN conjE])
moreover
have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule BinOp.hyps)
- ultimately show ?thesis using that by rules
+ ultimately show ?thesis using that by iprover
qed
ultimately
have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A'"
- using BinOp.hyps by (rules intro: da.BinOp)
+ using BinOp.hyps by (iprover intro: da.BinOp)
thus ?case ..
next
case (Super B Env B')
have B': "B \<subseteq> B'" .
with Super.hyps have "This \<in> B' "
by auto
- thus ?case by (rules intro: da.Super)
+ thus ?case by (iprover intro: da.Super)
next
case (AccLVar A B Env vn B')
have "vn \<in> B" .
moreover
have "B \<subseteq> B'" .
ultimately have "vn \<in> B'" by auto
- thus ?case by (rules intro: da.AccLVar)
+ thus ?case by (iprover intro: da.AccLVar)
next
- case Acc thus ?case by (rules intro: da.Acc)
+ case Acc thus ?case by (iprover intro: da.Acc)
next
case (AssLVar A B E Env e vn B')
have B': "B \<subseteq> B'" .
then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
- by (rule AssLVar.hyps [elim_format]) rules
+ by (rule AssLVar.hyps [elim_format]) iprover
then obtain A' where
"Env\<turnstile> B' \<guillemotright>\<langle>LVar vn:=e\<rangle>\<guillemotright> A'"
- by (rules intro: da.AssLVar)
+ by (iprover intro: da.AssLVar)
thus ?case ..
next
case (Ass A B Env V e v B')
@@ -1619,7 +1619,7 @@
proof -
have "PROP ?Hyp Env B \<langle>v\<rangle>" by (rule Ass.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain A' where "Env\<turnstile> nrm V' \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"
@@ -1630,11 +1630,11 @@
by (rule da_monotone [THEN conjE])
moreover
have "PROP ?Hyp Env (nrm V) \<langle>e\<rangle>" by (rule Ass.hyps)
- ultimately show ?thesis using that by rules
+ ultimately show ?thesis using that by iprover
qed
ultimately
have "Env\<turnstile> B' \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A'"
- by (rules intro: da.Ass)
+ by (iprover intro: da.Ass)
thus ?case ..
next
case (CondBool A B C E1 E2 Env c e1 e2 B')
@@ -1644,7 +1644,7 @@
proof -
have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
@@ -1655,7 +1655,7 @@
moreover
have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule CondBool.hyps)
ultimately
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
@@ -1666,11 +1666,11 @@
moreover
have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by(rule CondBool.hyps)
ultimately
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
ultimately
obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
- by (rules intro: da.CondBool)
+ by (iprover intro: da.CondBool)
thus ?case ..
next
case (Cond A B C E1 E2 Env c e1 e2 B')
@@ -1680,7 +1680,7 @@
proof -
have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
@@ -1691,7 +1691,7 @@
moreover
have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule Cond.hyps)
ultimately
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
@@ -1702,11 +1702,11 @@
moreover
have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by (rule Cond.hyps)
ultimately
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
ultimately
obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
- by (rules intro: da.Cond)
+ by (iprover intro: da.Cond)
thus ?case ..
next
case (Call A B E Env accC args e mn mode pTs statT B')
@@ -1715,7 +1715,7 @@
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'"
@@ -1726,14 +1726,14 @@
by (rule da_monotone [THEN conjE])
moreover
have "PROP ?Hyp Env (nrm E) \<langle>args\<rangle>" by (rule Call.hyps)
- ultimately show ?thesis using that by rules
+ ultimately show ?thesis using that by iprover
qed
ultimately
have "Env\<turnstile> B' \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs}args)\<rangle>\<guillemotright> A'"
- by (rules intro: da.Call)
+ by (iprover intro: da.Call)
thus ?case ..
next
- case Methd thus ?case by (rules intro: da.Methd)
+ case Methd thus ?case by (iprover intro: da.Methd)
next
case (Body A B C D Env c B')
have B': "B \<subseteq> B'" .
@@ -1747,7 +1747,7 @@
ultimately
have "nrm C \<subseteq> nrm C'"
by (rule da_monotone [THEN conjE])
- with da_c that show ?thesis by rules
+ with da_c that show ?thesis by iprover
qed
moreover
have "Result \<in> nrm C" .
@@ -1756,12 +1756,12 @@
moreover have "jumpNestingOkS {Ret} c" .
ultimately obtain A' where
"Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'"
- by (rules intro: da.Body)
+ by (iprover intro: da.Body)
thus ?case ..
next
- case LVar thus ?case by (rules intro: da.LVar)
+ case LVar thus ?case by (iprover intro: da.LVar)
next
- case FVar thus ?case by (rules intro: da.FVar)
+ case FVar thus ?case by (iprover intro: da.FVar)
next
case (AVar A B E1 Env e1 e2 B')
have B': "B \<subseteq> B'" .
@@ -1769,7 +1769,7 @@
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
@@ -1780,14 +1780,14 @@
by (rule da_monotone [THEN conjE])
moreover
have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule AVar.hyps)
- ultimately show ?thesis using that by rules
+ ultimately show ?thesis using that by iprover
qed
ultimately
have "Env\<turnstile> B' \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A'"
- by (rules intro: da.AVar)
+ by (iprover intro: da.AVar)
thus ?case ..
next
- case Nil thus ?case by (rules intro: da.Nil)
+ case Nil thus ?case by (iprover intro: da.Nil)
next
case (Cons A B E Env e es B')
have B': "B \<subseteq> B'" .
@@ -1795,7 +1795,7 @@
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps)
with B'
- show ?thesis using that by rules
+ show ?thesis using that by iprover
qed
moreover
obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'"
@@ -1806,11 +1806,11 @@
by (rule da_monotone [THEN conjE])
moreover
have "PROP ?Hyp Env (nrm E) \<langle>es\<rangle>" by (rule Cons.hyps)
- ultimately show ?thesis using that by rules
+ ultimately show ?thesis using that by iprover
qed
ultimately
have "Env\<turnstile> B' \<guillemotright>\<langle>e # es\<rangle>\<guillemotright> A'"
- by (rules intro: da.Cons)
+ by (iprover intro: da.Cons)
thus ?case ..
qed
qed
@@ -1841,13 +1841,13 @@
proof -
from da B'
obtain A' where A': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'"
- by (rule da_weaken [elim_format]) rules
+ by (rule da_weaken [elim_format]) iprover
with da B'
have "nrm A \<subseteq> nrm A' \<and> (\<forall> l. brk A l \<subseteq> brk A' l)"
by (rule da_monotone)
with A' ex_mono
show ?thesis
- by rules
+ by iprover
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Sep 22 23:56:15 2005 +0200
@@ -165,7 +165,7 @@
qed (simp_all)
with jumpNestingOk_l' subset
show ?thesis
- by rules
+ by iprover
qed
corollary jumpNestingOk_mono:
@@ -429,7 +429,7 @@
by simp
moreover from jmp_s1 have "?Jmp ({Cont l} \<union> jmps) s1" by simp
ultimately have jmp_s2: "?Jmp ({Cont l} \<union> jmps) s2"
- using wt_c G by rules
+ using wt_c G by iprover
have "?Jmp jmps (abupd (absorb (Cont l)) s2)"
proof -
{
@@ -1701,7 +1701,7 @@
by - (erule halloc_no_abrupt [rule_format])
hence "normal s2" by (cases s2) simp
with NewA.hyps
- show ?thesis by rules
+ show ?thesis by iprover
qed
also
from halloc
@@ -1732,7 +1732,7 @@
hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format])
with BinOp.hyps
have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
- by rules
+ by iprover
also
have "\<dots> \<subseteq> dom (locals (store s2))"
proof -
@@ -1768,7 +1768,7 @@
by - (erule eval_no_abrupt_lemma [rule_format])
with Ass.hyps
have "assigns (In2 va) \<subseteq> dom (locals (store s1))"
- by rules
+ by iprover
also
from Ass.hyps
have "\<dots> \<subseteq> dom (locals (store s2))"
@@ -1776,7 +1776,7 @@
also
from nrm_s2 Ass.hyps
have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
- by rules
+ by iprover
ultimately
have "assigns (In2 va) \<union> assigns (In1l e) \<subseteq> dom (locals (store s2))"
by (rule Un_least)
@@ -1816,7 +1816,7 @@
by - (erule eval_no_abrupt_lemma [rule_format])
with Cond.hyps
have "assigns (In1l e0) \<subseteq> dom (locals (store s1))"
- by rules
+ by iprover
also from Cond.hyps
have "\<dots> \<subseteq> dom (locals (store s2))"
by - (erule dom_locals_eval_mono_elim)
@@ -1868,14 +1868,14 @@
by - (erule eval_no_abrupt_lemma [rule_format])
with Call.hyps
have "assigns (In1l e) \<subseteq> dom (locals (store s1))"
- by rules
+ by iprover
also from Call.hyps
have "\<dots> \<subseteq> dom (locals (store s2))"
by - (erule dom_locals_eval_mono_elim)
also
from nrm_s2 Call.hyps
have "assigns (In3 args) \<subseteq> dom (locals (store s2))"
- by rules
+ by iprover
ultimately have "assigns (In1l e) \<union> assigns (In3 args) \<subseteq> \<dots>"
by (rule Un_least)
also
@@ -1903,7 +1903,7 @@
qed
with FVar.hyps
have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
- by rules
+ by iprover
also
have "\<dots> \<subseteq> dom (locals (store s2'))"
proof -
@@ -1932,14 +1932,14 @@
by - (erule eval_no_abrupt_lemma [rule_format])
with AVar.hyps
have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
- by rules
+ by iprover
also from AVar.hyps
have "\<dots> \<subseteq> dom (locals (store s2))"
by - (erule dom_locals_eval_mono_elim)
also
from AVar.hyps nrm_s2
have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
- by rules
+ by iprover
ultimately
have "assigns (In1l e1) \<union> assigns (In1l e2) \<subseteq> \<dots>"
by (rule Un_least)
@@ -1962,14 +1962,14 @@
proof -
from Cons
have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format])
- with Cons.hyps show ?thesis by rules
+ with Cons.hyps show ?thesis by iprover
qed
also from Cons.hyps
have "\<dots> \<subseteq> dom (locals (store s2))"
by - (erule dom_locals_eval_mono_elim)
also from Cons
have "assigns (In3 es) \<subseteq> dom (locals (store s2))"
- by rules
+ by iprover
ultimately
have "assigns (In1l e) \<union> assigns (In3 es) \<subseteq> dom (locals (store s2))"
by (rule Un_least)
@@ -2043,7 +2043,7 @@
by cases simp
from ce ve
obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s"
- by (rule UnOp.hyps [elim_format]) rules
+ by (rule UnOp.hyps [elim_format]) iprover
from eq_ve_ce const ce v
have "v=c"
by simp
@@ -2066,7 +2066,7 @@
from c1 v1
obtain eq_v1_c1: "v1 = c1" and
nrm_s1: "normal s1"
- by (rule BinOp.hyps [elim_format]) rules
+ by (rule BinOp.hyps [elim_format]) iprover
show ?case
proof (cases "need_second_arg binop v1")
case True
@@ -2074,7 +2074,7 @@
where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v2\<rightarrow> s"
by (cases s1) simp
with c2 obtain "v2 = c2" "normal s"
- by (rule BinOp.hyps [elim_format]) rules
+ by (rule BinOp.hyps [elim_format]) iprover
with c c1 c2 eq_v1_c1 v
show ?thesis by simp
next
@@ -2111,7 +2111,7 @@
by cases simp
from cb vb
obtain eq_vb_cb: "vb = cb" and nrm_s1: "normal s1"
- by (rule Cond.hyps [elim_format]) rules
+ by (rule Cond.hyps [elim_format]) iprover
show ?case
proof (cases "the_Bool vb")
case True
@@ -2123,7 +2123,7 @@
where "G\<turnstile>Norm s1' \<midarrow>e1-\<succ>v\<rightarrow> s"
by (cases s1) simp
with c1 obtain "c1 = v" "normal s"
- by (rule Cond.hyps [elim_format]) rules
+ by (rule Cond.hyps [elim_format]) iprover
ultimately show ?thesis by simp
next
case False
@@ -2135,7 +2135,7 @@
where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v\<rightarrow> s"
by (cases s1) simp
with c2 obtain "c2 = v" "normal s"
- by (rule Cond.hyps [elim_format]) rules
+ by (rule Cond.hyps [elim_format]) iprover
ultimately show ?thesis by simp
qed
next
@@ -2143,7 +2143,7 @@
qed simp_all
with const eval
show ?thesis
- by rules
+ by iprover
qed
lemmas constVal_eval_elim = constVal_eval [THEN conjE]
@@ -2235,7 +2235,7 @@
qed simp_all
with const wt
show ?thesis
- by rules
+ by iprover
qed
lemma assigns_if_good_approx:
@@ -2777,12 +2777,12 @@
show ?case
proof (cases "normal s1")
case True
- with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by rules
+ with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by iprover
with da_c2 obtain C2'
where da_c2': "Env\<turnstile> dom (locals (snd s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
nrm_c2: "nrm C2 \<subseteq> nrm C2'" and
brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
have "PROP ?Hyp (In1r c2) s1 s2" .
with wt_c2 da_c2' G
obtain nrm_c2': "?NormalAssigned s2 C2'" and
@@ -2871,7 +2871,7 @@
where da_c1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
nrm_c1: "nrm C1 \<subseteq> nrm C1'" and
brk_c1: "\<forall> l. brk C1 l \<subseteq> brk C1' l"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
from If.hyps True have "PROP ?Hyp (In1r c1) s1 s2" by simp
with wt_c1 da_c1'
obtain nrm_c1': "?NormalAssigned s2 C1'" and
@@ -2901,7 +2901,7 @@
where da_c2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
nrm_c2: "nrm C2 \<subseteq> nrm C2'" and
brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
from If.hyps False have "PROP ?Hyp (In1r c2) s1 s2" by simp
with wt_c2 da_c2'
obtain nrm_c2': "?NormalAssigned s2 C2'" and
@@ -2993,7 +2993,7 @@
where da_c': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
nrm_C_C': "nrm C \<subseteq> nrm C'" and
brk_C_C': "\<forall> l. brk C l \<subseteq> brk C' l"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
from hyp_c wt_c da_c'
obtain nrm_C': "?NormalAssigned s2 C'" and
brk_C': "?BreakAssigned s1 s2 C'" and
@@ -3855,11 +3855,11 @@
with wt_e1 da_e1 G normal_s1
obtain "?NormalAssigned s1 E1"
by simp
- with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by rules
+ with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by iprover
with da_e2 obtain A'
where da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
from notAndOr have "need_second_arg binop v1" by simp
with BinOp.hyps
have "PROP ?Hyp (In1l e2) s1 s2" by simp
@@ -4004,7 +4004,7 @@
with da_e obtain A'
where da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
from hyp_e wt_e da_e' G normal_s2
obtain "nrm A' \<subseteq> dom (locals (store s2))"
by simp
@@ -4121,7 +4121,7 @@
with da_e1 obtain E1' where
da_e1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
nrm_E1_E1': "nrm E1 \<subseteq> nrm E1'"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
ultimately have "nrm E1' \<subseteq> dom (locals (store s2))"
using wt_e1 G normal_s2 by simp
with nrm_E1_E1' show ?thesis
@@ -4140,7 +4140,7 @@
with da_e2 obtain E2' where
da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
nrm_E2_E2': "nrm E2 \<subseteq> nrm E2'"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
ultimately have "nrm E2' \<subseteq> dom (locals (store s2))"
using wt_e2 G normal_s2 by simp
with nrm_E2_E2' show ?thesis
@@ -4206,7 +4206,7 @@
with da_args obtain A' where
da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
have "PROP ?Hyp (In3 args) s1 s2" .
with da_args' wt_args G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
@@ -4313,7 +4313,7 @@
with da_e obtain A' where
da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
have normal_s2: "normal s2"
proof -
from normal_s3 s3
@@ -4391,7 +4391,7 @@
with da_e2 obtain A' where
da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
have "PROP ?Hyp (In1l e2) s1 s2" .
with da_e2' wt_e2 G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
@@ -4459,7 +4459,7 @@
with da_es obtain A' where
da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
- by (rule da_weakenE) rules
+ by (rule da_weakenE) iprover
have "PROP ?Hyp (In3 es) s1 s2" .
with da_es' wt_es G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
@@ -4523,10 +4523,10 @@
moreover note wt da
moreover from wf have "wf_prog (prg \<lparr>prg=G,cls=C,lcl=L\<rparr>)" by simp
ultimately show ?thesis
- using elim by (rule da_good_approxE) rules+
+ using elim by (rule da_good_approxE) iprover+
qed
ML {*
Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
*}
-end
\ No newline at end of file
+end
--- a/src/HOL/Bali/Eval.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/Eval.thy Thu Sep 22 23:56:15 2005 +0200
@@ -192,7 +192,7 @@
defer
apply (case_tac "a' = Null")
apply simp_all
-apply rules
+apply iprover
done
constdefs
--- a/src/HOL/Bali/Evaln.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/Evaln.thy Thu Sep 22 23:56:15 2005 +0200
@@ -554,7 +554,7 @@
case (Abrupt s t xc)
obtain n where
"G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
- by (rules intro: evaln.Abrupt)
+ by (iprover intro: evaln.Abrupt)
then show ?case ..
next
case Skip
@@ -563,7 +563,7 @@
case (Expr e s0 s1 v)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
- by (rules)
+ by (iprover)
then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
by (rule evaln.Expr)
then show ?case ..
@@ -571,7 +571,7 @@
case (Lab c l s0 s1)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
- by (rules)
+ by (iprover)
then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
by (rule evaln.Lab)
then show ?case ..
@@ -580,7 +580,7 @@
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
- by (rules)
+ by (iprover)
then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
by (blast intro: evaln.Comp dest: evaln_max2 )
then show ?case ..
@@ -589,7 +589,7 @@
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
- by (rules)
+ by (iprover)
then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
by (blast intro: evaln.If dest: evaln_max2)
then show ?case ..
@@ -597,18 +597,18 @@
case (Loop b c e l s0 s1 s2 s3)
from Loop.hyps obtain n1 where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
- by (rules)
+ by (iprover)
moreover from Loop.hyps obtain n2 where
"if the_Bool b
then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and>
G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
else s3 = s1"
- by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
+ by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
ultimately
have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
apply -
apply (rule evaln.Loop)
- apply (rules intro: evaln_nonstrict intro: le_maxI1)
+ apply (iprover intro: evaln_nonstrict intro: le_maxI1)
apply (auto intro: evaln_nonstrict intro: le_maxI2)
done
@@ -622,7 +622,7 @@
case (Throw a e s0 s1)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
- by (rules)
+ by (iprover)
then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
by (rule evaln.Throw)
then show ?case ..
@@ -630,7 +630,7 @@
case (Try catchC c1 c2 s0 s1 s2 s3 vn)
from Try.hyps obtain n1 where
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
- by (rules)
+ by (iprover)
moreover
have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
moreover
@@ -646,7 +646,7 @@
from Fin obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
"G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
- by rules
+ by iprover
moreover
have s3: "s3 = (if \<exists>err. x1 = Some (Error err)
then (x1, s1)
@@ -673,17 +673,17 @@
case (NewC C a s0 s1 s2)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
- by (rules)
+ by (iprover)
with NewC
have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
- by (rules intro: evaln.NewC)
+ by (iprover intro: evaln.NewC)
then show ?case ..
next
case (NewA T a e i s0 s1 s2 s3)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"
- by (rules)
+ by (iprover)
moreover
have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
ultimately
@@ -694,7 +694,7 @@
case (Cast castT e s0 s1 s2 v)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
- by (rules)
+ by (iprover)
moreover
have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
ultimately
@@ -705,7 +705,7 @@
case (Inst T b e s0 s1 v)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
- by (rules)
+ by (iprover)
moreover
have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
ultimately
@@ -721,7 +721,7 @@
case (UnOp e s0 s1 unop v )
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
- by (rules)
+ by (iprover)
hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
by (rule evaln.UnOp)
then show ?case ..
@@ -731,7 +731,7 @@
"G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"
- by (rules)
+ by (iprover)
hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
\<rightarrow> s2"
by (blast intro!: evaln.BinOp dest: evaln_max2)
@@ -749,7 +749,7 @@
case (Acc f s0 s1 v va)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
- by (rules)
+ by (iprover)
then
have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
by (rule evaln.Acc)
@@ -759,7 +759,7 @@
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"
- by (rules)
+ by (iprover)
then
have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
by (blast intro: evaln.Ass dest: evaln_max2)
@@ -769,7 +769,7 @@
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
- by (rules)
+ by (iprover)
then
have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
by (blast intro: evaln.Cond dest: evaln_max2)
@@ -780,7 +780,7 @@
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
- by rules
+ by iprover
moreover
have "invDeclC = invocation_declclass G mode (store s2) a' statT
\<lparr>name=mn,parTs=pTs'\<rparr>" .
@@ -792,7 +792,7 @@
from Call.hyps
obtain m where
"G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
- by rules
+ by iprover
ultimately
have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow>
(set_lvars (locals (store s2))) s4"
@@ -802,7 +802,7 @@
case (Methd D s0 s1 sig v )
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
- by rules
+ by iprover
then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
by (rule evaln.Methd)
then show ?case ..
@@ -811,7 +811,7 @@
from Body.hyps obtain n1 n2 where
evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
- by (rules)
+ by (iprover)
moreover
have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
fst s2 = Some (Jump (Cont l))
@@ -821,33 +821,33 @@
have
"G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
\<rightarrow> abupd (absorb Ret) s3"
- by (rules intro: evaln.Body dest: evaln_max2)
+ by (iprover intro: evaln.Body dest: evaln_max2)
then show ?case ..
next
case (LVar s vn )
obtain n where
"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
- by (rules intro: evaln.LVar)
+ by (iprover intro: evaln.LVar)
then show ?case ..
next
case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
- by rules
+ by iprover
moreover
have "s3 = check_field_access G accC statDeclC fn stat a s2'"
"(v, s2') = fvar statDeclC stat fn a s2" .
ultimately
have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
- by (rules intro: evaln.FVar dest: evaln_max2)
+ by (iprover intro: evaln.FVar dest: evaln_max2)
then show ?case ..
next
case (AVar a e1 e2 i s0 s1 s2 s2' v )
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"
- by rules
+ by iprover
moreover
have "(v, s2') = avar G i a s2" .
ultimately
@@ -856,13 +856,13 @@
then show ?case ..
next
case (Nil s0)
- show ?case by (rules intro: evaln.Nil)
+ show ?case by (iprover intro: evaln.Nil)
next
case (Cons e es s0 s1 s2 v vs)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
- by rules
+ by iprover
then
have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
by (blast intro!: evaln.Cons dest: evaln_max2)
--- a/src/HOL/Bali/TypeSafe.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Thu Sep 22 23:56:15 2005 +0200
@@ -1233,7 +1233,7 @@
next
case (Cons y ys')
have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
- by (rules intro: Hyps map_upd_cong_ext)
+ by (iprover intro: Hyps map_upd_cong_ext)
with Cons show ?thesis
by simp
qed
@@ -1701,7 +1701,7 @@
by cases simp+
from eval_e1 wt_e1 da_e1 wf normal_s1
have "nrm E1' \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approxE') rules
+ by (cases rule: da_good_approxE') iprover
with da_e2 show ?thesis
using that by (rule da_weakenE) (simp add: True)
qed
@@ -1836,7 +1836,7 @@
proof -
from eval_c1 wt_c1 da_c1 wf True
have "nrm C1 \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approxE') rules
+ by (cases rule: da_good_approxE') iprover
with da_c2 show ?thesis
by (rule da_weakenE)
qed
@@ -2806,7 +2806,7 @@
proof -
from eval_var wt_var da_var wf normal_s1
have "nrm V \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approxE') rules
+ by (cases rule: da_good_approxE') iprover
with da_e show ?thesis
by (rule da_weakenE)
qed
@@ -3094,7 +3094,7 @@
proof -
from eval_e wt_e da_e wf normal_s1
have "nrm E \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approxE') rules
+ by (cases rule: da_good_approxE') iprover
with da_args show ?thesis
by (rule da_weakenE)
qed
@@ -3256,7 +3256,7 @@
,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
\<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
res: "Result \<in> nrm M'"
- by (rule wf_mdeclE) rules
+ by (rule wf_mdeclE) iprover
from da_body is_static_eq L' have
"\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr>
\<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
@@ -3308,7 +3308,7 @@
"\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3'))
\<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
using da
- by (rules intro: da.Body assigned.select_convs)
+ by (iprover intro: da.Body assigned.select_convs)
from _ this [simplified]
show ?thesis
by (rule da.Methd [simplified,elim_format])
@@ -3672,7 +3672,7 @@
proof -
from eval_e1 wt_e1 da_e1 wf True
have "nrm E1 \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approxE') rules
+ by (cases rule: da_good_approxE') iprover
with da_e2 show ?thesis
by (rule da_weakenE)
qed
@@ -3768,7 +3768,7 @@
proof -
from eval_e wt_e da_e wf True
have "nrm E \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approxE') rules
+ by (cases rule: da_good_approxE') iprover
with da_es show ?thesis
by (rule da_weakenE)
qed
@@ -3806,7 +3806,7 @@
error_free s0 = error_free s1\<rbrakk> \<Longrightarrow> P"
shows "P"
using eval wt da wf conf
-by (rule eval_type_sound [elim_format]) (rules intro: elim)
+by (rule eval_type_sound [elim_format]) (iprover intro: elim)
corollary eval_ts:
@@ -3995,19 +3995,19 @@
proof -
from eval_c1 wt_c1 da_c1 wf normal_s1
have "nrm C1 \<subseteq> dom (locals (store s1))"
- by (cases rule: da_good_approxE') rules
+ by (cases rule: da_good_approxE') iprover
with da_c2 show ?thesis
by (rule da_weakenE)
qed
with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
by (rule Comp.hyps)
with da show ?thesis
- using elim by rules
+ using elim by iprover
qed
}
with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1
show ?case
- by (rule comp) rules+
+ by (rule comp) iprover+
next
case (If b c1 c2 e s0 s1 s2 L accC T A)
have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
@@ -4058,12 +4058,12 @@
with wt_then_else
have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
by (rule If.hyps)
- with da show ?thesis using elim by rules
+ with da show ?thesis using elim by iprover
qed
}
with eval_e eval_then_else wt_e wt_then_else da_e P_e
show ?case
- by (rule if) rules+
+ by (rule if) iprover+
next
oops
--- a/src/HOL/Datatype_Universe.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Datatype_Universe.thy Thu Sep 22 23:56:15 2005 +0200
@@ -218,17 +218,17 @@
lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
apply (erule equalityE)
-apply (rules intro: equalityI Scons_inject_lemma1)
+apply (iprover intro: equalityI Scons_inject_lemma1)
done
lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'"
apply (erule equalityE)
-apply (rules intro: equalityI Scons_inject_lemma2)
+apply (iprover intro: equalityI Scons_inject_lemma2)
done
lemma Scons_inject:
"[| Scons M N = Scons M' N'; [| M=M'; N=N' |] ==> P |] ==> P"
-by (rules dest: Scons_inject1 Scons_inject2)
+by (iprover dest: Scons_inject1 Scons_inject2)
lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')"
by (blast elim!: Scons_inject)
--- a/src/HOL/Equiv_Relations.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Equiv_Relations.thy Thu Sep 22 23:56:15 2005 +0200
@@ -35,7 +35,7 @@
apply (unfold equiv_def)
apply clarify
apply (rule equalityI)
- apply (rules intro: sym_trans_comp_subset refl_comp_subset)+
+ apply (iprover intro: sym_trans_comp_subset refl_comp_subset)+
done
text {* Second half. *}
@@ -73,7 +73,7 @@
lemma eq_equiv_class:
"r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
- by (rules intro: equalityD2 subset_equiv_class)
+ by (iprover intro: equalityD2 subset_equiv_class)
lemma equiv_class_nondisjoint:
"equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r"
--- a/src/HOL/Finite_Set.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Finite_Set.thy Thu Sep 22 23:56:15 2005 +0200
@@ -604,7 +604,7 @@
have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
with AbB have "finite ?D" by simp
then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
- using finite_imp_foldSet by rules
+ using finite_imp_foldSet by iprover
moreover have cinB: "c \<in> B" using B by auto
ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
by(rule Diff1_foldSet)
--- a/src/HOL/FixedPoint.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/FixedPoint.thy Thu Sep 22 23:56:15 2005 +0200
@@ -31,13 +31,13 @@
by (auto simp add: lfp_def)
lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) \<subseteq> lfp(f)"
-by (rules intro: lfp_greatest subset_trans monoD lfp_lowerbound)
+by (iprover intro: lfp_greatest subset_trans monoD lfp_lowerbound)
lemma lfp_lemma3: "mono(f) ==> lfp(f) \<subseteq> f(lfp(f))"
-by (rules intro: lfp_lemma2 monoD lfp_lowerbound)
+by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
lemma lfp_unfold: "mono(f) ==> lfp(f) = f(lfp(f))"
-by (rules intro: equalityI lfp_lemma2 lfp_lemma3)
+by (iprover intro: equalityI lfp_lemma2 lfp_lemma3)
subsection{*General induction rules for greatest fixed points*}
@@ -105,13 +105,13 @@
by (auto simp add: gfp_def)
lemma gfp_lemma2: "mono(f) ==> gfp(f) \<subseteq> f(gfp(f))"
-by (rules intro: gfp_least subset_trans monoD gfp_upperbound)
+by (iprover intro: gfp_least subset_trans monoD gfp_upperbound)
lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) \<subseteq> gfp(f)"
-by (rules intro: gfp_lemma2 monoD gfp_upperbound)
+by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
lemma gfp_unfold: "mono(f) ==> gfp(f) = f(gfp(f))"
-by (rules intro: equalityI gfp_lemma2 gfp_lemma3)
+by (iprover intro: equalityI gfp_lemma2 gfp_lemma3)
subsection{*Coinduction rules for greatest fixed points*}
@@ -141,7 +141,7 @@
@{term lfp} and @{term gfp}*}
lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
-by (rules intro: subset_refl monoI Un_mono monoD)
+by (iprover intro: subset_refl monoI Un_mono monoD)
lemma coinduct3_lemma:
"[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |]
--- a/src/HOL/Fun.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Fun.thy Thu Sep 22 23:56:15 2005 +0200
@@ -429,11 +429,11 @@
proof
assume "inj_on (swap a b f) A"
with A have "inj_on (swap a b (swap a b f)) A"
- by (rules intro: inj_on_imp_inj_on_swap)
+ by (iprover intro: inj_on_imp_inj_on_swap)
thus "inj_on f A" by simp
next
assume "inj_on f A"
- with A show "inj_on (swap a b f) A" by (rules intro: inj_on_imp_inj_on_swap)
+ with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
qed
lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
--- a/src/HOL/HOL.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/HOL.thy Thu Sep 22 23:56:15 2005 +0200
@@ -287,7 +287,7 @@
subsection {*Equality of booleans -- iff*}
lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
-apply (rules intro: iff [THEN mp, THEN mp] impI prems)
+apply (iprover intro: iff [THEN mp, THEN mp] impI prems)
done
lemma iffD2: "[| P=Q; Q |] ==> P"
@@ -307,7 +307,7 @@
assumes major: "P=Q"
and minor: "[| P --> Q; Q --> P |] ==> R"
shows "R"
-by (rules intro: minor impI major [THEN iffD2] major [THEN iffD1])
+by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
subsection {*True*}
@@ -318,7 +318,7 @@
done
lemma eqTrueI: "P ==> P=True"
-by (rules intro: iffI TrueI)
+by (iprover intro: iffI TrueI)
lemma eqTrueE: "P=True ==> P"
apply (erule iffD2)
@@ -330,7 +330,7 @@
lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)"
apply (unfold All_def)
-apply (rules intro: ext eqTrueI p)
+apply (iprover intro: ext eqTrueI p)
done
lemma spec: "ALL x::'a. P(x) ==> P(x)"
@@ -343,13 +343,13 @@
assumes major: "ALL x. P(x)"
and minor: "P(x) ==> R"
shows "R"
-by (rules intro: minor major [THEN spec])
+by (iprover intro: minor major [THEN spec])
lemma all_dupE:
assumes major: "ALL x. P(x)"
and minor: "[| P(x); ALL x. P(x) |] ==> R"
shows "R"
-by (rules intro: minor major major [THEN spec])
+by (iprover intro: minor major major [THEN spec])
subsection {*False*}
@@ -370,7 +370,7 @@
assumes p: "P ==> False"
shows "~P"
apply (unfold not_def)
-apply (rules intro: impI p)
+apply (iprover intro: impI p)
done
lemma False_not_True: "False ~= True"
@@ -399,24 +399,24 @@
lemma impE:
assumes "P-->Q" "P" "Q ==> R"
shows "R"
-by (rules intro: prems mp)
+by (iprover intro: prems mp)
(* Reduces Q to P-->Q, allowing substitution in P. *)
lemma rev_mp: "[| P; P --> Q |] ==> Q"
-by (rules intro: mp)
+by (iprover intro: mp)
lemma contrapos_nn:
assumes major: "~Q"
and minor: "P==>Q"
shows "~P"
-by (rules intro: notI minor major [THEN notE])
+by (iprover intro: notI minor major [THEN notE])
(*not used at all, but we already have the other 3 combinations *)
lemma contrapos_pn:
assumes major: "Q"
and minor: "P ==> ~Q"
shows "~P"
-by (rules intro: notI minor major notE)
+by (iprover intro: notI minor major notE)
lemma not_sym: "t ~= s ==> s ~= t"
apply (erule contrapos_nn)
@@ -436,7 +436,7 @@
lemma exI: "P x ==> EX x::'a. P x"
apply (unfold Ex_def)
-apply (rules intro: allI allE impI mp)
+apply (iprover intro: allI allE impI mp)
done
lemma exE:
@@ -444,7 +444,7 @@
and minor: "!!x. P(x) ==> Q"
shows "Q"
apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
-apply (rules intro: impI [THEN allI] minor)
+apply (iprover intro: impI [THEN allI] minor)
done
@@ -452,17 +452,17 @@
lemma conjI: "[| P; Q |] ==> P&Q"
apply (unfold and_def)
-apply (rules intro: impI [THEN allI] mp)
+apply (iprover intro: impI [THEN allI] mp)
done
lemma conjunct1: "[| P & Q |] ==> P"
apply (unfold and_def)
-apply (rules intro: impI dest: spec mp)
+apply (iprover intro: impI dest: spec mp)
done
lemma conjunct2: "[| P & Q |] ==> Q"
apply (unfold and_def)
-apply (rules intro: impI dest: spec mp)
+apply (iprover intro: impI dest: spec mp)
done
lemma conjE:
@@ -476,19 +476,19 @@
lemma context_conjI:
assumes prems: "P" "P ==> Q" shows "P & Q"
-by (rules intro: conjI prems)
+by (iprover intro: conjI prems)
subsection {*Disjunction*}
lemma disjI1: "P ==> P|Q"
apply (unfold or_def)
-apply (rules intro: allI impI mp)
+apply (iprover intro: allI impI mp)
done
lemma disjI2: "Q ==> P|Q"
apply (unfold or_def)
-apply (rules intro: allI impI mp)
+apply (iprover intro: allI impI mp)
done
lemma disjE:
@@ -496,7 +496,7 @@
and minorP: "P ==> R"
and minorQ: "Q ==> R"
shows "R"
-by (rules intro: minorP minorQ impI
+by (iprover intro: minorP minorQ impI
major [unfolded or_def, THEN spec, THEN mp, THEN mp])
@@ -536,7 +536,7 @@
assumes p1: "Q"
and p2: "~P ==> ~Q"
shows "P"
-by (rules intro: classical p1 p2 notE)
+by (iprover intro: classical p1 p2 notE)
subsection {*Unique existence*}
@@ -544,14 +544,14 @@
lemma ex1I:
assumes prems: "P a" "!!x. P(x) ==> x=a"
shows "EX! x. P(x)"
-by (unfold Ex1_def, rules intro: prems exI conjI allI impI)
+by (unfold Ex1_def, iprover intro: prems exI conjI allI impI)
text{*Sometimes easier to use: the premises have no shared variables. Safe!*}
lemma ex_ex1I:
assumes ex_prem: "EX x. P(x)"
and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
shows "EX! x. P(x)"
-by (rules intro: ex_prem [THEN exE] ex1I eq)
+by (iprover intro: ex_prem [THEN exE] ex1I eq)
lemma ex1E:
assumes major: "EX! x. P(x)"
@@ -559,7 +559,7 @@
shows "R"
apply (rule major [unfolded Ex1_def, THEN exE])
apply (erule conjE)
-apply (rules intro: minor)
+apply (iprover intro: minor)
done
lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x"
@@ -586,7 +586,7 @@
lemma theI:
assumes "P a" and "!!x. P x ==> x=a"
shows "P (THE x. P x)"
-by (rules intro: prems the_equality [THEN ssubst])
+by (iprover intro: prems the_equality [THEN ssubst])
lemma theI': "EX! x. P x ==> P (THE x. P x)"
apply (erule ex1E)
@@ -600,7 +600,7 @@
lemma theI2:
assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
shows "Q (THE x. P x)"
-by (rules intro: prems theI)
+by (iprover intro: prems theI)
lemma the1_equality: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
apply (rule the_equality)
@@ -627,11 +627,11 @@
lemma disjCI:
assumes "~Q ==> P" shows "P|Q"
apply (rule classical)
-apply (rules intro: prems disjI1 disjI2 notI elim: notE)
+apply (iprover intro: prems disjI1 disjI2 notI elim: notE)
done
lemma excluded_middle: "~P | P"
-by (rules intro: disjCI)
+by (iprover intro: disjCI)
text{*case distinction as a natural deduction rule. Note that @{term "~P"}
is the second case, not the first.*}
@@ -650,7 +650,7 @@
and minor: "~P ==> R" "Q ==> R"
shows "R"
apply (rule excluded_middle [of P, THEN disjE])
-apply (rules intro: minor major [THEN mp])+
+apply (iprover intro: minor major [THEN mp])+
done
(*This version of --> elimination works on Q before P. It works best for
@@ -661,7 +661,7 @@
and minor: "Q ==> R" "~P ==> R"
shows "R"
apply (rule excluded_middle [of P, THEN disjE])
-apply (rules intro: minor major [THEN mp])+
+apply (iprover intro: minor major [THEN mp])+
done
(*Classical <-> elimination. *)
@@ -670,14 +670,14 @@
and minor: "[| P; Q |] ==> R" "[| ~P; ~Q |] ==> R"
shows "R"
apply (rule major [THEN iffE])
-apply (rules intro: minor elim: impCE notE)
+apply (iprover intro: minor elim: impCE notE)
done
lemma exCI:
assumes "ALL x. ~P(x) ==> P(a)"
shows "EX x. P(x)"
apply (rule ccontr)
-apply (rules intro: prems exI allI notI notE [of "\<exists>x. P x"])
+apply (iprover intro: prems exI allI notI notE [of "\<exists>x. P x"])
done
@@ -949,10 +949,10 @@
"!!P. (EX x. t=x & P(x)) = P(t)"
"!!P. (ALL x. x=t --> P(x)) = P(t)"
"!!P. (ALL x. t=x --> P(x)) = P(t)"
- by (blast, blast, blast, blast, blast, rules+)
+ by (blast, blast, blast, blast, blast, iprover+)
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
- by rules
+ by iprover
lemma ex_simps:
"!!P Q. (EX x. P x & Q) = ((EX x. P x) & Q)"
@@ -962,7 +962,7 @@
"!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
"!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
-- {* Miniscoping: pushing in existential quantifiers. *}
- by (rules | blast)+
+ by (iprover | blast)+
lemma all_simps:
"!!P Q. (ALL x. P x & Q) = ((ALL x. P x) & Q)"
@@ -972,7 +972,7 @@
"!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
"!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
-- {* Miniscoping: pushing in universal quantifiers. *}
- by (rules | blast)+
+ by (iprover | blast)+
lemma disj_absorb: "(A | A) = A"
by blast
@@ -989,28 +989,28 @@
lemma eq_ac:
shows eq_commute: "(a=b) = (b=a)"
and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
- and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)
-lemma neq_commute: "(a~=b) = (b~=a)" by rules
+ and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+)
+lemma neq_commute: "(a~=b) = (b~=a)" by iprover
lemma conj_comms:
shows conj_commute: "(P&Q) = (Q&P)"
- and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by rules+
-lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules
+ and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+
+lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover
lemma disj_comms:
shows disj_commute: "(P|Q) = (Q|P)"
- and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by rules+
-lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by rules
+ and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by iprover+
+lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by iprover
-lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by rules
-lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by rules
+lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by iprover
+lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by iprover
-lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by rules
-lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by rules
+lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by iprover
+lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by iprover
-lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by rules
-lemma imp_conjL: "((P&Q) -->R) = (P --> (Q --> R))" by rules
-lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by rules
+lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by iprover
+lemma imp_conjL: "((P&Q) -->R) = (P --> (Q --> R))" by iprover
+lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by iprover
text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
@@ -1019,7 +1019,7 @@
lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
-lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by rules
+lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover
lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
@@ -1028,7 +1028,7 @@
by blast
lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
-lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by rules
+lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover
lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
@@ -1038,11 +1038,11 @@
lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
-lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by rules
-lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by rules
+lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover
+lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
-lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by rules
-lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by rules
+lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
+lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover
text {*
\medskip The @{text "&"} congruence rule: not included by default!
@@ -1050,11 +1050,11 @@
lemma conj_cong:
"(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))"
- by rules
+ by iprover
lemma rev_conj_cong:
"(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))"
- by rules
+ by iprover
text {* The @{text "|"} congruence rule: not included by default! *}
@@ -1063,7 +1063,7 @@
by blast
lemma eq_sym_conv: "(x = y) = (y = x)"
- by rules
+ by iprover
text {* \medskip if-then-else rules *}
@@ -1109,8 +1109,8 @@
apply (simplesubst split_if, blast)
done
-lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
-lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules
+lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
+lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover
text {* \medskip let rules for simproc *}
@@ -1285,11 +1285,11 @@
lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
induct_conj (induct_forall A) (induct_forall B)"
- by (unfold induct_forall_def induct_conj_def) rules
+ by (unfold induct_forall_def induct_conj_def) iprover
lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
induct_conj (induct_implies C A) (induct_implies C B)"
- by (unfold induct_implies_def induct_conj_def) rules
+ by (unfold induct_implies_def induct_conj_def) iprover
lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
proof
--- a/src/HOL/Induct/PropLog.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Induct/PropLog.thy Thu Sep 22 23:56:15 2005 +0200
@@ -236,12 +236,12 @@
apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
apply (simp add: sat_thms_p, safe)
txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *}
- apply (rules intro: thms_excluded_middle_rule
+ apply (iprover intro: thms_excluded_middle_rule
insert_Diff_same [THEN weaken_left]
insert_Diff_subset2 [THEN weaken_left]
hyps_Diff [THEN Diff_weaken_left])
txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *}
- apply (rules intro: thms_excluded_middle_rule
+ apply (iprover intro: thms_excluded_middle_rule
insert_Diff_same [THEN weaken_left]
insert_Diff_subset2 [THEN weaken_left]
hyps_insert [THEN Diff_weaken_left])
@@ -260,7 +260,7 @@
theorem completeness [rule_format]: "finite H ==> \<forall>p. H |= p --> H |- p"
apply (erule finite_induct)
apply (blast intro: completeness_0)
-apply (rules intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
+apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
done
theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
--- a/src/HOL/Integ/Presburger.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Integ/Presburger.thy Thu Sep 22 23:56:15 2005 +0200
@@ -244,10 +244,10 @@
text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
lemma P_eqtrue: "(P=True) = P"
- by rules
+ by iprover
lemma P_eqfalse: "(P=False) = (~P)"
- by rules
+ by iprover
text {*
\medskip Theorems for the generation of the bachwards direction of
@@ -831,10 +831,10 @@
by simp
lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
- by rules
+ by iprover
lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
- by rules
+ by iprover
lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
@@ -952,13 +952,13 @@
apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
nat_0_le cong add: conj_cong)
apply (rule iffI)
- apply rules
+ apply iprover
apply (erule exE)
apply (case_tac "x=0")
apply (rule_tac x=0 in exI)
apply simp
apply (case_tac "0 \<le> k")
- apply rules
+ apply iprover
apply (simp add: linorder_not_le)
apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
apply assumption
--- a/src/HOL/Lambda/Commutation.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Lambda/Commutation.thy Thu Sep 22 23:56:15 2005 +0200
@@ -154,7 +154,7 @@
proof (rule converse_rtranclE)
assume "x = b"
with xc have "(b, c) \<in> R\<^sup>*" by simp
- thus ?thesis by rules
+ thus ?thesis by iprover
next
fix y
assume xy: "(x, y) \<in> R"
@@ -163,23 +163,23 @@
proof (rule converse_rtranclE)
assume "x = c"
with xb have "(c, b) \<in> R\<^sup>*" by simp
- thus ?thesis by rules
+ thus ?thesis by iprover
next
fix y'
assume y'c: "(y', c) \<in> R\<^sup>*"
assume xy': "(x, y') \<in> R"
with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
- then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules
+ then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by iprover
from xy have "(y, x) \<in> R\<inverse>" ..
from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
- then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules
+ then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by iprover
from xy' have "(y', x) \<in> R\<inverse>" ..
moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
moreover note y'c
ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
- then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules
+ then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by iprover
from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
- with cw show ?thesis by rules
+ with cw show ?thesis by iprover
qed
qed
qed
@@ -208,7 +208,7 @@
proof (rule converse_rtranclE)
assume "x = b"
with xc have "(b, c) \<in> R\<^sup>*" by simp
- thus ?thesis by rules
+ thus ?thesis by iprover
next
fix y
assume xy: "(x, y) \<in> R"
@@ -217,7 +217,7 @@
proof (rule converse_rtranclE)
assume "x = c"
with xb have "(c, b) \<in> R\<^sup>*" by simp
- thus ?thesis by rules
+ thus ?thesis by iprover
next
fix y'
assume y'c: "(y', c) \<in> R\<^sup>*"
--- a/src/HOL/Lambda/Eta.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Lambda/Eta.thy Thu Sep 22 23:56:15 2005 +0200
@@ -370,7 +370,7 @@
by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
then have "\<exists>u1 u2 k. s = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1'' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2''" by (rule eta)
then obtain u1 u2 k where s: "s = eta_expand k (u1 \<degree> u2)"
- and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by rules
+ and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by iprover
from u1 u2 eta s' have "\<not> free u1 0" and "\<not> free u2 0"
by (simp_all del: free_par_eta add: free_par_eta [symmetric])
with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (u1[dummy/0] \<degree> u2[dummy/0])"
@@ -399,7 +399,7 @@
then obtain u'' where s': "s' = Abs u''"
by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
then have "\<exists>u k. s = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u''" by (rule eta)
- then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by rules
+ then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by iprover
from eta u s' have "\<not> free u (Suc 0)"
by (simp del: free_par_eta add: free_par_eta [symmetric])
with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))"
@@ -481,7 +481,7 @@
by (blast dest: 2)
from par_eta_subset_eta t' have "t' -e>> s'''" ..
with t'' have "t'' -e>> s'''" by (rule rtrancl_trans)
- with s show ?case by rules
+ with s show ?case by iprover
qed
theorem eta_postponement:
--- a/src/HOL/Lambda/Type.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Lambda/Type.thy Thu Sep 22 23:56:15 2005 +0200
@@ -149,7 +149,7 @@
apply simp
apply (case_tac "ts @ [t]")
apply (simp add: types_snoc_eq)+
- apply rules
+ apply iprover
done
@@ -269,7 +269,7 @@
lemma var_app_typesE: "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow>
(\<And>Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> P) \<Longrightarrow> P"
apply (drule var_app_types [of _ _ "[]", simplified])
- apply (rules intro: typing.Var)+
+ apply (iprover intro: typing.Var)+
done
lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P"
@@ -346,7 +346,7 @@
done
theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T"
- by (induct set: rtrancl) (rules intro: subject_reduction)+
+ by (induct set: rtrancl) (iprover intro: subject_reduction)+
subsection {* Alternative induction rule for types *}
--- a/src/HOL/Lambda/WeakNorm.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Thu Sep 22 23:56:15 2005 +0200
@@ -26,7 +26,7 @@
by (simp add: listall_def)
theorem listall_nil_eq [simp]: "listall P [] = True"
- by (rules intro: listall_nil)
+ by (iprover intro: listall_nil)
theorem listall_cons: "P x \<Longrightarrow> listall P xs \<Longrightarrow> listall P (x # xs)"
apply (simp add: listall_def)
@@ -84,14 +84,14 @@
apply (induct m)
apply (case_tac n)
apply (case_tac [3] n)
- apply (simp only: nat.simps, rules?)+
+ apply (simp only: nat.simps, iprover?)+
done
lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
apply (induct m)
apply (case_tac n)
apply (case_tac [3] n)
- apply (simp del: simp_thms, rules?)+
+ apply (simp del: simp_thms, iprover?)+
done
lemma App_NF_D: assumes NF: "Var n \<degree>\<degree> ts \<in> NF"
@@ -125,11 +125,11 @@
apply (erule NF.App)
apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])
apply simp
- apply (rules intro: NF.App)
+ apply (iprover intro: NF.App)
apply simp
- apply (rules intro: NF.App)
+ apply (iprover intro: NF.App)
apply simp
- apply (rules intro: NF.Abs)
+ apply (iprover intro: NF.Abs)
done
lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
@@ -199,7 +199,7 @@
proof (cases ts)
case Nil
with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp
- with Nil and uNF show ?thesis by simp rules
+ with Nil and uNF show ?thesis by simp iprover
next
case (Cons a as)
with appT have "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> (a # as) : T'" by simp
@@ -235,10 +235,10 @@
then obtain bs' where
bsred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) bs \<rightarrow>\<^sub>\<beta>\<^sup>*
Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs'"
- and bsNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs' \<in> NF" by rules
+ and bsNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs' \<in> NF" by iprover
from snoc have "?R b" by simp
- with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by rules
- then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by rules
+ with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by iprover
+ then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by iprover
from bsNF have "listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t 0) bs')"
by (rule App_NF_D)
moreover have "lift b' 0 \<in> NF" by (rule lift_NF)
@@ -253,20 +253,20 @@
ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
thus ?case ..
qed
- from App and Cons have "listall ?R as" by simp (rules dest: listall_conj2)
+ from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)
with argsT have "\<exists>as'. ?ex Ts as as'" by (rule as)
then obtain as' where
asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"
- and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by rules
+ and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by iprover
from App and Cons have "?R a" by simp
with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> a' \<in> NF"
- by rules
- then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by rules
+ by iprover
+ then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by iprover
from uNF have "lift u 0 \<in> NF" by (rule lift_NF)
hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> u' \<in> NF" by (rule app_Var_NF)
then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "u' \<in> NF"
- by rules
+ by iprover
from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> ua \<in> NF"
proof (rule MI1)
have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
@@ -278,7 +278,7 @@
from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
qed
then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "ua \<in> NF"
- by rules
+ by iprover
from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]"
by (rule subst_preserves_beta2')
also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]"
@@ -305,7 +305,7 @@
with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')
qed
then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"
- and rnf: "r \<in> NF" by rules
+ and rnf: "r \<in> NF" by iprover
from asred have
"(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"
@@ -315,7 +315,7 @@
also note rred
finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" .
with rnf Cons eq show ?thesis
- by (simp add: map_compose [symmetric] o_def) rules
+ by (simp add: map_compose [symmetric] o_def) iprover
qed
next
assume neq: "x \<noteq> i"
@@ -342,10 +342,10 @@
with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
then obtain bs' where
bsred: "\<And>x'. Var x' \<degree>\<degree> map (\<lambda>t. t[u/i]) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var x' \<degree>\<degree> bs'"
- and bsNF: "\<And>x'. Var x' \<degree>\<degree> bs' \<in> NF" by rules
+ and bsNF: "\<And>x'. Var x' \<degree>\<degree> bs' \<in> NF" by iprover
from snoc have "?R b" by simp
- with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by rules
- then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by rules
+ with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by iprover
+ then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by iprover
from bsred bred have "\<And>x'. (Var x' \<degree>\<degree> map (\<lambda>t. t[u/i]) bs) \<degree> b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>*
(Var x' \<degree>\<degree> bs') \<degree> b'" by (rule rtrancl_beta_App)
moreover from bsNF [of 0] have "listall (\<lambda>t. t \<in> NF) bs'"
@@ -355,16 +355,16 @@
ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
thus ?case ..
qed
- from App have "listall ?R ts" by (rules dest: listall_conj2)
+ from App have "listall ?R ts" by (iprover dest: listall_conj2)
with argsT have "\<exists>ts'. ?ex Ts ts ts'" by (rule ts)
then obtain ts' where NF: "?ex Ts ts ts'" ..
from nat_le_dec show ?thesis
proof
assume "i < x"
- with NF show ?thesis by simp rules
+ with NF show ?thesis by simp iprover
next
assume "\<not> (i < x)"
- with NF neq show ?thesis by (simp add: subst_Var) rules
+ with NF neq show ?thesis by (simp add: subst_Var) iprover
qed
qed
qed
@@ -376,7 +376,7 @@
moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" by (rule lift_type)
ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" by (rule Abs)
thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
- by simp (rules intro: rtrancl_beta_Abs NF.Abs)
+ by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
}
qed
qed
@@ -411,15 +411,15 @@
shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using T
proof induct
case Var
- show ?case by (rules intro: Var_NF)
+ show ?case by (iprover intro: Var_NF)
next
case Abs
- thus ?case by (rules intro: rtrancl_beta_Abs NF.Abs)
+ thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
next
case (App T U e s t)
from App obtain s' t' where
sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "s' \<in> NF"
- and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by rules
+ and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by iprover
have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> u \<in> NF"
proof (rule subst_type_NF)
have "lift t' 0 \<in> NF" by (rule lift_NF)
@@ -438,10 +438,10 @@
from sred show "e \<turnstile> s' : T \<Rightarrow> U"
by (rule subject_reduction') (rule rtyping_imp_typing)
qed
- then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp rules
+ then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp iprover
from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans)
- with unf show ?case by rules
+ with unf show ?case by iprover
qed
--- a/src/HOL/List.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/List.thy Thu Sep 22 23:56:15 2005 +0200
@@ -264,7 +264,7 @@
lemma length_induct:
"(!!xs. \<forall>ys. length ys < length xs --> P ys ==> P xs) ==> P xs"
-by (rule measure_induct [of length]) rules
+by (rule measure_induct [of length]) iprover
subsubsection {* @{text length} *}
@@ -550,7 +550,7 @@
by(blast dest:map_injective)
lemma inj_mapI: "inj f ==> inj (map f)"
-by (rules dest: map_injective injD intro: inj_onI)
+by (iprover dest: map_injective injD intro: inj_onI)
lemma inj_mapD: "inj (map f) ==> inj f"
apply (unfold inj_on_def, clarify)
@@ -977,6 +977,9 @@
apply (auto split:nat.split)
done
+lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
+by(induct xs)(auto simp:neq_Nil_conv)
+
subsubsection {* @{text take} and @{text drop} *}
--- a/src/HOL/MicroJava/BV/EffectMono.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Thu Sep 22 23:56:15 2005 +0200
@@ -78,7 +78,7 @@
fix n' assume s: "n = Suc n'"
with l have "n' \<le> length ls" by simp
hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
- then obtain a b where "ls = a @ b" "length a = n'" by rules
+ then obtain a b where "ls = a @ b" "length a = n'" by iprover
with s have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp
thus ?thesis by blast
qed
@@ -91,9 +91,9 @@
assume n: "n < length x"
hence "n \<le> length x" by simp
hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n)
- then obtain r d where x: "x = r@d" "length r = n" by rules
+ then obtain r d where x: "x = r@d" "length r = n" by iprover
with n have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
- then obtain b c where "d = b#c" by rules
+ then obtain b c where "d = b#c" by iprover
with x have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp
thus ?thesis by blast
qed
--- a/src/HOL/Nat.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Nat.thy Thu Sep 22 23:56:15 2005 +0200
@@ -73,7 +73,7 @@
apply (unfold Zero_nat_def Suc_def)
apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
apply (erule Rep_Nat [THEN Nat.induct])
- apply (rules elim: Abs_Nat_inverse [THEN subst])
+ apply (iprover elim: Abs_Nat_inverse [THEN subst])
done
text {* Distinctness of constructors *}
@@ -128,7 +128,7 @@
apply (induct n)
prefer 2
apply (rule allI)
- apply (induct_tac x, rules+)
+ apply (induct_tac x, iprover+)
done
subsection {* Basic properties of "less than" *}
@@ -340,7 +340,7 @@
by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
- by (drule le_Suc_eq [THEN iffD1], rules+)
+ by (drule le_Suc_eq [THEN iffD1], iprover+)
lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
apply (simp add: le_def less_Suc_eq)
@@ -385,7 +385,7 @@
done
lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
- by (rules intro: less_or_eq_imp_le le_imp_less_or_eq)
+ by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
text {* Useful with @{text Blast}. *}
lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
@@ -505,7 +505,7 @@
text {* This theorem is useful with @{text blast} *}
lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
- by (rule iffD1, rule neq0_conv, rules)
+ by (rule iffD1, rule neq0_conv, iprover)
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
by (fast intro: not0_implies_Suc)
@@ -779,7 +779,7 @@
by (rule le_less_trans, rule le_add2, rule lessI)
lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
- by (rules intro!: less_add_Suc1 less_imp_Suc_add)
+ by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
by (rule le_trans, assumption, rule le_add1)
@@ -909,12 +909,12 @@
lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
apply (induct k i rule: diff_induct)
apply (simp_all (no_asm))
- apply rules
+ apply iprover
done
lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
apply (rule diff_self_eq_0 [THEN subst])
- apply (rule zero_induct_lemma, rules+)
+ apply (rule zero_induct_lemma, iprover+)
done
lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
--- a/src/HOL/Presburger.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Presburger.thy Thu Sep 22 23:56:15 2005 +0200
@@ -244,10 +244,10 @@
text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
lemma P_eqtrue: "(P=True) = P"
- by rules
+ by iprover
lemma P_eqfalse: "(P=False) = (~P)"
- by rules
+ by iprover
text {*
\medskip Theorems for the generation of the bachwards direction of
@@ -831,10 +831,10 @@
by simp
lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
- by rules
+ by iprover
lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
- by rules
+ by iprover
lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
@@ -952,13 +952,13 @@
apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
nat_0_le cong add: conj_cong)
apply (rule iffI)
- apply rules
+ apply iprover
apply (erule exE)
apply (case_tac "x=0")
apply (rule_tac x=0 in exI)
apply simp
apply (case_tac "0 \<le> k")
- apply rules
+ apply iprover
apply (simp add: linorder_not_le)
apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
apply assumption
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Sep 22 23:56:15 2005 +0200
@@ -405,7 +405,7 @@
linearformE: "linearform E g"
and a: "\<forall>x \<in> F. g x = f x"
and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
- by (rule abs_HahnBanach [elim_format]) rules
+ by (rule abs_HahnBanach [elim_format]) iprover
txt {* We furthermore have to show that @{text g} is also continuous: *}
--- a/src/HOL/Relation.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Relation.thy Thu Sep 22 23:56:15 2005 +0200
@@ -70,7 +70,7 @@
by (simp add: Id_def)
lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P"
- by (unfold Id_def) (rules elim: CollectE)
+ by (unfold Id_def) (iprover elim: CollectE)
lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
by (unfold Id_def) blast
@@ -100,7 +100,7 @@
lemma diagE [elim!]:
"c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
-- {* The general elimination rule. *}
- by (unfold diag_def) (rules elim!: UN_E singletonE)
+ by (unfold diag_def) (iprover elim!: UN_E singletonE)
lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
by blast
@@ -117,11 +117,11 @@
lemma rel_compE [elim!]: "xz : r O s ==>
(!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r ==> P) ==> P"
- by (unfold rel_comp_def) (rules elim!: CollectE splitE exE conjE)
+ by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
lemma rel_compEpair:
"(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
- by (rules elim: rel_compE Pair_inject ssubst)
+ by (iprover elim: rel_compE Pair_inject ssubst)
lemma R_O_Id [simp]: "R O Id = R"
by fast
@@ -146,7 +146,7 @@
subsection {* Reflexivity *}
lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
- by (unfold refl_def) (rules intro!: ballI)
+ by (unfold refl_def) (iprover intro!: ballI)
lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
by (unfold refl_def) blast
@@ -156,10 +156,10 @@
lemma antisymI:
"(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
- by (unfold antisym_def) rules
+ by (unfold antisym_def) iprover
lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
- by (unfold antisym_def) rules
+ by (unfold antisym_def) iprover
subsection {* Symmetry and Transitivity *}
@@ -169,10 +169,10 @@
lemma transI:
"(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
- by (unfold trans_def) rules
+ by (unfold trans_def) iprover
lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
- by (unfold trans_def) rules
+ by (unfold trans_def) iprover
subsection {* Converse *}
@@ -189,7 +189,7 @@
lemma converseE [elim!]:
"yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P"
-- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
- by (unfold converse_def) (rules elim!: CollectE splitE bexE)
+ by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
lemma converse_converse [simp]: "(r^-1)^-1 = r"
by (unfold converse_def) blast
@@ -219,11 +219,11 @@
by (unfold Domain_def) blast
lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
- by (rules intro!: iffD2 [OF Domain_iff])
+ by (iprover intro!: iffD2 [OF Domain_iff])
lemma DomainE [elim!]:
"a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
- by (rules dest!: iffD1 [OF Domain_iff])
+ by (iprover dest!: iffD1 [OF Domain_iff])
lemma Domain_empty [simp]: "Domain {} = {}"
by blast
@@ -259,10 +259,10 @@
by (simp add: Domain_def Range_def)
lemma RangeI [intro]: "(a, b) : r ==> b : Range r"
- by (unfold Range_def) (rules intro!: converseI DomainI)
+ by (unfold Range_def) (iprover intro!: converseI DomainI)
lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
- by (unfold Range_def) (rules elim!: DomainE dest!: converseD)
+ by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
lemma Range_empty [simp]: "Range {} = {}"
by blast
@@ -305,7 +305,7 @@
lemma ImageE [elim!]:
"b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
- by (unfold Image_def) (rules elim!: CollectE bexE)
+ by (unfold Image_def) (iprover elim!: CollectE bexE)
lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
-- {* This version's more effective when we already have the required @{text a} *}
@@ -334,7 +334,7 @@
by blast
lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
- by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
+ by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
-- {* NOT suitable for rewriting *}
--- a/src/HOL/Set.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Set.thy Thu Sep 22 23:56:15 2005 +0200
@@ -542,7 +542,7 @@
lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
-- {* Anti-symmetry of the subset relation. *}
- by (rules intro: set_ext subsetD)
+ by (iprover intro: set_ext subsetD)
lemmas equalityI [intro!] = subset_antisym
@@ -1046,10 +1046,10 @@
text {* \medskip Big Union -- least upper bound of a set. *}
lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
- by (rules intro: subsetI UnionI)
+ by (iprover intro: subsetI UnionI)
lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
- by (rules intro: subsetI elim: UnionE dest: subsetD)
+ by (iprover intro: subsetI elim: UnionE dest: subsetD)
text {* \medskip General union. *}
@@ -1058,7 +1058,7 @@
by blast
lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
- by (rules intro: subsetI elim: UN_E dest: subsetD)
+ by (iprover intro: subsetI elim: UN_E dest: subsetD)
text {* \medskip Big Intersection -- greatest lower bound of a set. *}
@@ -1071,13 +1071,13 @@
by blast
lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
- by (rules intro: InterI subsetI dest: subsetD)
+ by (iprover intro: InterI subsetI dest: subsetD)
lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
by blast
lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
- by (rules intro: INT_I subsetI dest: subsetD)
+ by (iprover intro: INT_I subsetI dest: subsetD)
text {* \medskip Finite Union -- the least upper bound of two sets. *}
@@ -1809,7 +1809,7 @@
by blast
lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
- by rules
+ by iprover
text {* \medskip Miniscoping: pushing in quantifiers and big Unions
@@ -1955,21 +1955,21 @@
done
lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
- by rules
+ by iprover
lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
- by rules
+ by iprover
lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
- by rules
+ by iprover
lemma imp_refl: "P --> P" ..
lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
- by rules
+ by iprover
lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
- by rules
+ by iprover
lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
by blast
@@ -1983,10 +1983,10 @@
ex_mono Collect_mono in_mono
lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
- by rules
+ by iprover
lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
- by rules
+ by iprover
lemma Least_mono:
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
--- a/src/HOL/Transitive_Closure.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Sep 22 23:56:15 2005 +0200
@@ -74,8 +74,8 @@
shows "P b"
proof -
from a have "a = a --> P b"
- by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
- thus ?thesis by rules
+ by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
+ thus ?thesis by iprover
qed
lemmas rtrancl_induct2 =
@@ -88,7 +88,7 @@
fix x y z
assume "(x, y) \<in> r\<^sup>*"
assume "(y, z) \<in> r\<^sup>*"
- thus "(x, z) \<in> r\<^sup>*" by induct (rules!)+
+ thus "(x, z) \<in> r\<^sup>*" by induct (iprover!)+
qed
lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
@@ -112,7 +112,7 @@
lemma converse_rtrancl_into_rtrancl:
"(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
- by (rule rtrancl_trans) rules+
+ by (rule rtrancl_trans) iprover+
text {*
\medskip More @{term "r^*"} equations and inclusions.
@@ -158,7 +158,7 @@
shows "(y, x) \<in> r^*"
proof -
from r show ?thesis
- by induct (rules intro: rtrancl_trans dest!: converseD)+
+ by induct (iprover intro: rtrancl_trans dest!: converseD)+
qed
theorem rtrancl_converseI:
@@ -166,7 +166,7 @@
shows "(x, y) \<in> (r^-1)^*"
proof -
from r show ?thesis
- by induct (rules intro: rtrancl_trans converseI)+
+ by induct (iprover intro: rtrancl_trans converseI)+
qed
lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
@@ -179,7 +179,7 @@
proof -
from rtrancl_converseI [OF major]
show ?thesis
- by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
+ by induct (iprover intro: cases dest!: converseD rtrancl_converseD)+
qed
lemmas converse_rtrancl_induct2 =
@@ -197,8 +197,8 @@
show ?thesis
apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
apply (rule_tac [2] major [THEN converse_rtrancl_induct])
- prefer 2 apply rules
- prefer 2 apply rules
+ prefer 2 apply iprover
+ prefer 2 apply iprover
apply (erule asm_rl exE disjE conjE prems)+
done
qed
@@ -221,7 +221,7 @@
lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
apply (simp only: split_tupled_all)
apply (erule trancl.induct)
- apply (rules dest: subsetD)+
+ apply (iprover dest: subsetD)+
done
lemma r_into_trancl': "!!p. p : r ==> p : r^+"
@@ -232,15 +232,15 @@
*}
lemma trancl_into_rtrancl: "(a, b) \<in> r^+ ==> (a, b) \<in> r^*"
- by (erule trancl.induct) rules+
+ by (erule trancl.induct) iprover+
lemma rtrancl_into_trancl1: assumes r: "(a, b) \<in> r^*"
shows "!!c. (b, c) \<in> r ==> (a, c) \<in> r^+" using r
- by induct rules+
+ by induct iprover+
lemma rtrancl_into_trancl2: "[| (a,b) : r; (b,c) : r^* |] ==> (a,c) : r^+"
-- {* intro rule from @{text r} and @{text rtrancl} *}
- apply (erule rtranclE, rules)
+ apply (erule rtranclE, iprover)
apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
apply (assumption | rule r_into_rtrancl)+
done
@@ -253,8 +253,8 @@
-- {* Nice induction rule for @{text trancl} *}
proof -
from a have "a = a --> P b"
- by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
- thus ?thesis by rules
+ by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
+ thus ?thesis by iprover
qed
lemma trancl_trans_induct:
@@ -267,7 +267,7 @@
assume major: "(x,y) : r^+"
case rule_context
show ?thesis
- by (rules intro: r_into_trancl major [THEN trancl_induct] prems)
+ by (iprover intro: r_into_trancl major [THEN trancl_induct] prems)
qed
inductive_cases tranclE: "(a, b) : r^+"
@@ -281,14 +281,14 @@
fix x y z
assume "(x, y) \<in> r^+"
assume "(y, z) \<in> r^+"
- thus "(x, z) \<in> r^+" by induct (rules!)+
+ thus "(x, z) \<in> r^+" by induct (iprover!)+
qed
lemmas trancl_trans = trans_trancl [THEN transD, standard]
lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
- by induct (rules intro: trancl_trans)+
+ by induct (iprover intro: trancl_trans)+
lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
by (erule transD [OF trans_trancl r_into_trancl])
@@ -309,13 +309,13 @@
lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x, y) \<in> (r^-1)^+"
apply (drule converseD)
apply (erule trancl.induct)
- apply (rules intro: converseI trancl_trans)+
+ apply (iprover intro: converseI trancl_trans)+
done
lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
apply (rule converseI)
apply (erule trancl.induct)
- apply (rules dest: converseD intro: trancl_trans)+
+ apply (iprover dest: converseD intro: trancl_trans)+
done
lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
--- a/src/HOL/ex/Intuitionistic.thy Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/ex/Intuitionistic.thy Thu Sep 22 23:56:15 2005 +0200
@@ -24,44 +24,44 @@
intuitionstically equivalent to P. [Andy Pitts] *)
lemma "(~~(P&Q)) = ((~~P) & (~~Q))"
- by rules
+ by iprover
lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)"
- by rules
+ by iprover
(* ~~ does NOT distribute over | *)
lemma "(~~(P-->Q)) = (~~P --> ~~Q)"
- by rules
+ by iprover
lemma "(~~~P) = (~P)"
- by rules
+ by iprover
lemma "~~((P --> Q | R) --> (P-->Q) | (P-->R))"
- by rules
+ by iprover
lemma "(P=Q) = (Q=P)"
- by rules
+ by iprover
lemma "((P --> (Q | (Q-->R))) --> R) --> R"
- by rules
+ by iprover
lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J)
--> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C)
--> (((F-->A)-->B) --> I) --> E"
- by rules
+ by iprover
(* Lemmas for the propositional double-negation translation *)
lemma "P --> ~~P"
- by rules
+ by iprover
lemma "~~(~~P --> P)"
- by rules
+ by iprover
lemma "~~P & ~~(P --> Q) --> ~~Q"
- by rules
+ by iprover
(* de Bruijn formulae *)
@@ -70,7 +70,7 @@
lemma "((P=Q) --> P&Q&R) &
((Q=R) --> P&Q&R) &
((R=P) --> P&Q&R) --> P&Q&R"
- by rules
+ by iprover
(*de Bruijn formula with five predicates*)
lemma "((P=Q) --> P&Q&R&S&T) &
@@ -78,7 +78,7 @@
((R=S) --> P&Q&R&S&T) &
((S=T) --> P&Q&R&S&T) &
((T=P) --> P&Q&R&S&T) --> P&Q&R&S&T"
- by rules
+ by iprover
(*** Problems from Sahlin, Franzen and Haridi,
@@ -89,81 +89,81 @@
(*Problem 1.1*)
lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) =
(ALL z. EX y. ALL x. p(x) & q(y) & r(z))"
- by (rules del: allE elim 2: allE')
+ by (iprover del: allE elim 2: allE')
(*Problem 3.1*)
lemma "~ (EX x. ALL y. p y x = (~ p x x))"
- by rules
+ by iprover
(* Intuitionistic FOL: propositional problems based on Pelletier. *)
(* Problem ~~1 *)
lemma "~~((P-->Q) = (~Q --> ~P))"
- by rules
+ by iprover
(* Problem ~~2 *)
lemma "~~(~~P = P)"
- by rules
+ by iprover
(* Problem 3 *)
lemma "~(P-->Q) --> (Q-->P)"
- by rules
+ by iprover
(* Problem ~~4 *)
lemma "~~((~P-->Q) = (~Q --> P))"
- by rules
+ by iprover
(* Problem ~~5 *)
lemma "~~((P|Q-->P|R) --> P|(Q-->R))"
- by rules
+ by iprover
(* Problem ~~6 *)
lemma "~~(P | ~P)"
- by rules
+ by iprover
(* Problem ~~7 *)
lemma "~~(P | ~~~P)"
- by rules
+ by iprover
(* Problem ~~8. Peirce's law *)
lemma "~~(((P-->Q) --> P) --> P)"
- by rules
+ by iprover
(* Problem 9 *)
lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
- by rules
+ by iprover
(* Problem 10 *)
lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P=Q)"
- by rules
+ by iprover
(* 11. Proved in each direction (incorrectly, says Pelletier!!) *)
lemma "P=P"
- by rules
+ by iprover
(* Problem ~~12. Dijkstra's law *)
lemma "~~(((P = Q) = R) = (P = (Q = R)))"
- by rules
+ by iprover
lemma "((P = Q) = R) --> ~~(P = (Q = R))"
- by rules
+ by iprover
(* Problem 13. Distributive law *)
lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
- by rules
+ by iprover
(* Problem ~~14 *)
lemma "~~((P = Q) = ((Q | ~P) & (~Q|P)))"
- by rules
+ by iprover
(* Problem ~~15 *)
lemma "~~((P --> Q) = (~P | Q))"
- by rules
+ by iprover
(* Problem ~~16 *)
lemma "~~((P-->Q) | (Q-->P))"
-by rules
+by iprover
(* Problem ~~17 *)
lemma "~~(((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S)))"
@@ -171,7 +171,7 @@
(*Dijkstra's "Golden Rule"*)
lemma "(P&Q) = (P = (Q = (P|Q)))"
- by rules
+ by iprover
(****Examples with quantifiers****)
@@ -179,19 +179,19 @@
(* The converse is classical in the following implications... *)
lemma "(EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q"
- by rules
+ by iprover
lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
- by rules
+ by iprover
lemma "((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))"
- by rules
+ by iprover
lemma "(ALL x. P(x)) | Q --> (ALL x. P(x) | Q)"
- by rules
+ by iprover
lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
- by rules
+ by iprover
(* Hard examples with quantifiers *)
@@ -201,24 +201,24 @@
(* Problem ~~19 *)
lemma "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))"
- by rules
+ by iprover
(* Problem 20 *)
lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
--> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
- by rules
+ by iprover
(* Problem 21 *)
lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P=Q(x))"
- by rules
+ by iprover
(* Problem 22 *)
lemma "(ALL x. P = Q(x)) --> (P = (ALL x. Q(x)))"
- by rules
+ by iprover
(* Problem ~~23 *)
lemma "~~ ((ALL x. P | Q(x)) = (P | (ALL x. Q(x))))"
- by rules
+ by iprover
(* Problem 25 *)
lemma "(EX x. P(x)) &
@@ -226,7 +226,7 @@
(ALL x. P(x) --> (M(x) & L(x))) &
((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
--> (EX x. Q(x)&P(x))"
- by rules
+ by iprover
(* Problem 27 *)
lemma "(EX x. P(x) & ~Q(x)) &
@@ -234,40 +234,40 @@
(ALL x. M(x) & L(x) --> P(x)) &
((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
--> (ALL x. M(x) --> ~L(x))"
- by rules
+ by iprover
(* Problem ~~28. AMENDED *)
lemma "(ALL x. P(x) --> (ALL x. Q(x))) &
(~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
(~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))
--> (ALL x. P(x) & L(x) --> M(x))"
- by rules
+ by iprover
(* Problem 29. Essentially the same as Principia Mathematica *11.71 *)
lemma "(((EX x. P(x)) & (EX y. Q(y))) -->
(((ALL x. (P(x) --> R(x))) & (ALL y. (Q(y) --> S(y)))) =
(ALL x y. ((P(x) & Q(y)) --> (R(x) & S(y))))))"
- by rules
+ by iprover
(* Problem ~~30 *)
lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) &
(ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
--> (ALL x. ~~S(x))"
- by rules
+ by iprover
(* Problem 31 *)
lemma "~(EX x. P(x) & (Q(x) | R(x))) &
(EX x. L(x) & P(x)) &
(ALL x. ~ R(x) --> M(x))
--> (EX x. L(x) & M(x))"
- by rules
+ by iprover
(* Problem 32 *)
lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
(ALL x. S(x) & R(x) --> L(x)) &
(ALL x. M(x) --> R(x))
--> (ALL x. P(x) & M(x) --> L(x))"
- by rules
+ by iprover
(* Problem ~~33 *)
lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c))) =
@@ -280,50 +280,50 @@
(ALL x. EX y. G x y) &
(ALL x y. J x y | G x y --> (ALL z. J y z | G y z --> H x z))
--> (ALL x. EX y. H x y)"
- by rules
+ by iprover
(* Problem 39 *)
lemma "~ (EX x. ALL y. F y x = (~F y y))"
- by rules
+ by iprover
(* Problem 40. AMENDED *)
lemma "(EX y. ALL x. F x y = F x x) -->
~(ALL x. EX y. ALL z. F z y = (~ F z x))"
- by rules
+ by iprover
(* Problem 44 *)
lemma "(ALL x. f(x) -->
(EX y. g(y) & h x y & (EX y. g(y) & ~ h x y))) &
(EX x. j(x) & (ALL y. g(y) --> h x y))
--> (EX x. j(x) & ~f(x))"
- by rules
+ by iprover
(* Problem 48 *)
lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
- by rules
+ by iprover
(* Problem 51 *)
lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) -->
(EX z. (ALL x. (EX w. ((ALL y. (P x y = (y = w))) = (x = z))))))"
- by rules
+ by iprover
(* Problem 52 *)
(*Almost the same as 51. *)
lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) -->
(EX w. (ALL y. (EX z. ((ALL x. (P x y = (x = z))) = (y = w))))))"
- by rules
+ by iprover
(* Problem 56 *)
lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) = (ALL x. P(x) --> P(f(x)))"
- by rules
+ by iprover
(* Problem 57 *)
lemma "P (f a b) (f b c) & P (f b c) (f a c) &
(ALL x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)"
- by rules
+ by iprover
(* Problem 60 *)
lemma "ALL x. P x (f x) = (EX y. (ALL z. P z y --> P z (f x)) & P x y)"
- by rules
+ by iprover
end