summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 22 Sep 2005 23:56:15 +0200 | |

changeset 17589 | 58eeffd73be1 |

parent 17588 | f2bd501398ee |

child 17590 | 56dc95e8b5c5 |

renamed rules to iprover

--- 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