Methods rule_tac etc support static (Isar) contexts.
--- a/src/HOL/Bali/WellForm.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/Bali/WellForm.thy Fri Aug 29 15:19:02 2003 +0200
@@ -1943,7 +1943,7 @@
(\<exists>T m. t = ArrayT T \<and> G\<turnstile>Array T accessible_in (pid S) \<and>
accmethd G S Object sig = Some m \<and> accmodi m \<noteq> Private \<and>
declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh)"
-apply (rule_tac "ref_ty1"="t" in ref_ty_ty.induct [THEN conjunct1])
+apply (rule_tac ref_ty1="t" in ref_ty_ty.induct [THEN conjunct1])
apply auto
apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def)
apply (auto dest!: accmethd_SomeD)
--- a/src/HOL/HoareParallel/RG_Examples.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy Fri Aug 29 15:19:02 2003 +0200
@@ -320,7 +320,7 @@
apply force
apply force
apply force
- apply(rule_tac "pre'"="\<lbrace> \<acute>X i mod n = i \<and> (\<forall>j. j<\<acute>X i \<longrightarrow> j mod n = i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i < n * q \<longrightarrow> P (B!(\<acute>Y i))) \<and> \<acute>X i<\<acute>Y i\<rbrace>" in Conseq)
+ apply(rule_tac pre'="\<lbrace> \<acute>X i mod n = i \<and> (\<forall>j. j<\<acute>X i \<longrightarrow> j mod n = i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i < n * q \<longrightarrow> P (B!(\<acute>Y i))) \<and> \<acute>X i<\<acute>Y i\<rbrace>" in Conseq)
apply force
apply(rule subset_refl)+
apply(rule Cond)
@@ -375,7 +375,7 @@
apply force
apply force
apply force
- apply(rule_tac "pre'"="\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> \<acute>X ! i mod n = i \<and> (\<forall>j. j < \<acute>X ! i \<longrightarrow> j mod n = i \<longrightarrow> \<not> P (B ! j)) \<and> (\<acute>Y ! i < n * q \<longrightarrow> P (B ! (\<acute>Y ! i))) \<and> \<acute>X!i<\<acute>Y!i\<rbrace>" in Conseq)
+ apply(rule_tac pre'="\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> \<acute>X ! i mod n = i \<and> (\<forall>j. j < \<acute>X ! i \<longrightarrow> j mod n = i \<longrightarrow> \<not> P (B ! j)) \<and> (\<acute>Y ! i < n * q \<longrightarrow> P (B ! (\<acute>Y ! i))) \<and> \<acute>X!i<\<acute>Y!i\<rbrace>" in Conseq)
apply force
apply(rule subset_refl)+
apply(rule Cond)
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Fri Aug 29 15:19:02 2003 +0200
@@ -132,7 +132,7 @@
{G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
apply (simp only: progression_def)
apply (intro strip)
-apply (rule_tac "s1.0" = "Norm (hp1, (os1, lvars1, C, S,
+apply (rule_tac ?s1.0 = "Norm (hp1, (os1, lvars1, C, S,
length pre + length instrs0) # frs)"
in exec_all_trans)
apply (simp only: append_assoc)
@@ -191,7 +191,7 @@
\<Longrightarrow> {G, C, S} \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
apply (simp only: progression_def jump_fwd_def)
apply (intro strip)
-apply (rule_tac "s1.0" = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans)
+apply (rule_tac ?s1.0 = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans)
apply (simp only: append_assoc)
apply (subgoal_tac "pre @ (instr # instrs0 @ instrs1) @ post = pre @ instr # instrs0 @ (instrs1 @ post)")
apply blast
@@ -305,8 +305,8 @@
apply force
apply (intro strip)
apply (frule_tac
- "P1.0" = "wf_mdecl wf_mb G Ca" and
- "P2.0" = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop)
+ ?P1.0 = "wf_mdecl wf_mb G Ca" and
+ ?P2.0 = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop)
apply (force simp: wf_cdecl_def)
apply clarify
@@ -455,7 +455,7 @@
apply (case_tac "v1 = v2")
(* case v1 = v2 *)
-apply (rule_tac "instrs1.0" = "[LitPush (Bool True)]" in jump_fwd_progression)
+apply (rule_tac ?instrs1.0 = "[LitPush (Bool True)]" in jump_fwd_progression)
apply (auto simp: nat_add_distrib)
apply (rule progression_one_step) apply simp
@@ -464,7 +464,7 @@
apply auto
apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified])
apply auto
-apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
+apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
apply (auto simp: nat_add_distrib intro: progression_refl)
done
@@ -522,9 +522,9 @@
apply (case_tac lvals) apply simp
apply (simp (no_asm_simp) )
-apply (rule_tac "lvars1.0" = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def)
-apply (rule_tac "instrs0.0" = "[load_default_val b]" in progression_transitive, simp)
+apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
apply (rule progression_one_step)
apply (simp (no_asm_simp) add: load_default_val_def)
apply (rule conjI, simp)+ apply (rule HOL.refl)
@@ -650,7 +650,7 @@
E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk>
\<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T"
apply (simp add: gh_def)
-apply (rule_tac x3="fst s" and "s3"="snd s"and "x'3"="fst s'"
+apply (rule_tac x3="fst s" and s3="snd s"and x'3="fst s'"
in eval_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]], simplified])
apply assumption+
apply (simp (no_asm_use) add: surjective_pairing [THEN sym])
@@ -769,7 +769,7 @@
apply (frule raise_if_NoneD)
apply (frule wtpd_expr_cast)
apply simp
-apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, simp)
+apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, simp)
apply blast
apply (rule progression_one_step)
apply (simp add: raise_system_xcpt_def gh_def comp_cast_ok)
@@ -791,8 +791,8 @@
apply (simp (no_asm_use) only: compExpr_compExprs.simps)
-apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast
-apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast
+apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast
+apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast
apply (case_tac bop)
(*subcase bop = Eq *) apply simp apply (rule progression_Eq)
(*subcase bop = Add *) apply simp apply (rule progression_one_step) apply simp
@@ -814,10 +814,10 @@
apply (frule wtpd_expr_lass, erule conjE, erule conjE)
apply (simp add: compExpr_compExprs.simps)
-apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
apply blast
-apply (rule_tac "instrs0.0" = "[Dup]" in progression_transitive, simp)
+apply (rule_tac ?instrs0.0 = "[Dup]" in progression_transitive, simp)
apply (rule progression_one_step)
apply (simp add: gh_def)
apply (rule conjI, simp)+ apply simp
@@ -837,7 +837,7 @@
apply (frule wtpd_expr_facc)
apply (simp (no_asm_use) only: compExpr_compExprs.simps)
-apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
apply blast
apply (rule progression_one_step)
apply (simp add: gh_def)
@@ -860,11 +860,11 @@
apply (simp only: compExpr_compExprs.simps)
-apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl)
apply fast (* blast does not seem to work - why? *)
-apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl)
apply fast
-apply (rule_tac "instrs0.0" = "[Dup_x1]" and "instrs1.0" = "[Putfield fn T]" in progression_transitive, simp)
+apply (rule_tac ?instrs0.0 = "[Dup_x1]" and ?instrs1.0 = "[Putfield fn T]" in progression_transitive, simp)
(* Dup_x1 *)
apply (rule progression_one_step)
@@ -899,7 +899,7 @@
apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
apply simp
-apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
apply fast
apply fast
@@ -916,7 +916,7 @@
apply (intro allI impI)
apply (frule wtpd_stmt_expr)
apply simp
-apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
apply fast
apply (rule progression_one_step)
apply simp
@@ -930,7 +930,7 @@
apply (frule_tac st=c1 in state_ok_exec) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
apply simp
-apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl)
apply fast
apply fast
@@ -950,29 +950,29 @@
apply (erule exE)
apply simp
-apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
+apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
apply (rule progression_one_step, simp)
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
-apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
apply fast
apply (case_tac b)
(* case b= True *)
apply simp
-apply (rule_tac "instrs0.0" = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
+apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
apply (rule progression_one_step) apply simp
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
-apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
+apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
apply fast
-apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
+apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
apply (simp, rule conjI, (rule HOL.refl)+)
apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
apply (rule progression_refl)
(* case b= False *)
apply simp
-apply (rule_tac "instrs1.0" = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
+apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
apply (simp, rule conjI, (rule HOL.refl)+)
apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
apply fast
@@ -993,14 +993,14 @@
(* case b= False *)
apply simp
-apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
+apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
apply (rule progression_one_step)
apply simp
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
-apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
apply fast
-apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
+apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
apply (rule progression_refl)
@@ -1028,19 +1028,19 @@
apply simp
apply (rule conjI, (rule HOL.refl)+)
-apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
+apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
apply (rule progression_one_step)
apply simp
apply (rule conjI, simp)+ apply simp
-apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
apply fast
apply (case_tac b)
(* case b= True *)
apply simp
-apply (rule_tac "instrs0.0" = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
+apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
apply (rule progression_one_step) apply simp
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
apply fast
@@ -1116,11 +1116,11 @@
apply (simp (no_asm_use) only: compExpr_compExprs.simps)
(* evaluate e *)
-apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
apply fast
(* evaluate parameters *)
-apply (rule_tac "instrs0.0" = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl)
apply fast
(* invokation *)
@@ -1136,14 +1136,14 @@
apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def)
(* var. initialization *)
-apply (rule_tac "instrs0.0" = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption)
apply (simp (no_asm_simp)) (* length pns = length pvs *)
apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) arbitrary) *)
(* body statement *)
-apply (rule_tac "instrs0.0" = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?instrs0.0 = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl)
apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
apply (simp (no_asm_simp))
apply (simp only: gh_conv)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Aug 29 15:19:02 2003 +0200
@@ -1739,14 +1739,14 @@
apply (rule bc_mt_corresp_zero) apply (simp add: length_compTpExpr)
apply (simp (no_asm_simp))
-apply (drule_tac "bc1.0"="[]" and "bc2.0" = "compExpr jmb expr1"
- and "f1.0"=comb_nil and "f2.0" = "compTpExpr jmb G expr1"
+apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "compExpr jmb expr1"
+ and ?f1.0=comb_nil and ?f2.0 = "compTpExpr jmb G expr1"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply blast
apply (simp (no_asm_simp) add: length_compTpExpr)+
-apply (drule_tac "bc2.0" = "compExpr jmb expr2" and "f2.0" = "compTpExpr jmb G expr2"
+apply (drule_tac ?bc2.0 = "compExpr jmb expr2" and ?f2.0 = "compTpExpr jmb G expr2"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (simp only: compTpExpr_LT_ST)
@@ -1754,10 +1754,10 @@
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
-apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2"
- and inst = "Ifcmpeq 3" and "bc3.0" = "[LitPush (Bool False),Goto 2, LitPush (Bool True)]"
- and "f1.0"="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2"
- and "f2.0"="popST 2" and "f3.0"="pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]"
+apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2"
+ and inst = "Ifcmpeq 3" and ?bc3.0 = "[LitPush (Bool False),Goto 2, LitPush (Bool True)]"
+ and ?f1.0="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2"
+ and ?f2.0="popST 2" and ?f3.0="pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]"
in bc_mt_corresp_comb_wt_instr)
apply (simp (no_asm_simp) add: length_compTpExpr)+
@@ -1772,12 +1772,12 @@
apply (case_tac Ta) apply (simp (no_asm_simp)) apply (simp (no_asm_simp))
apply (rule contracting_popST) (* contracting (popST 2) *)
-apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3]"
- and "bc2.0" = "[LitPush (Bool False)]"
- and "bc3.0" = "[Goto 2, LitPush (Bool True)]"
- and "f1.0" = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2"
- and "f2.0" = "pushST [PrimT Boolean]"
- and "f3.0" = "popST (Suc 0) \<box> pushST [PrimT Boolean]"
+apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3]"
+ and ?bc2.0 = "[LitPush (Bool False)]"
+ and ?bc3.0 = "[Goto 2, LitPush (Bool True)]"
+ and ?f1.0 = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2"
+ and ?f2.0 = "pushST [PrimT Boolean]"
+ and ?f3.0 = "popST (Suc 0) \<box> pushST [PrimT Boolean]"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (simp add: compTpExpr_LT_ST_rewr popST_def)
@@ -1787,10 +1787,10 @@
apply (simp (no_asm_simp) add: start_sttp_resp_def)
-apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False)]"
- and inst = "Goto 2" and "bc3.0" = "[LitPush (Bool True)]"
- and "f1.0"="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> pushST [PrimT Boolean]"
- and "f2.0"="popST 1" and "f3.0"="pushST [PrimT Boolean]"
+apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False)]"
+ and inst = "Goto 2" and ?bc3.0 = "[LitPush (Bool True)]"
+ and ?f1.0="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> pushST [PrimT Boolean]"
+ and ?f2.0="popST 1" and ?f3.0="pushST [PrimT Boolean]"
in bc_mt_corresp_comb_wt_instr)
apply (simp (no_asm_simp) add: length_compTpExpr)+
@@ -1804,13 +1804,13 @@
apply (rule contracting_popST) (* contracting (popST 1) *)
apply (drule_tac
- "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False), Goto 2]"
- and "bc2.0" = "[LitPush (Bool True)]"
- and "bc3.0" = "[]"
- and "f1.0" = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box>
+ ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False), Goto 2]"
+ and ?bc2.0 = "[LitPush (Bool True)]"
+ and ?bc3.0 = "[]"
+ and ?f1.0 = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box>
pushST [PrimT Boolean] \<box> popST (Suc 0)"
- and "f2.0" = "pushST [PrimT Boolean]"
- and "f3.0" = "comb_nil"
+ and ?f2.0 = "pushST [PrimT Boolean]"
+ and ?f3.0 = "comb_nil"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (simp add: compTpExpr_LT_ST_rewr popST_def)
@@ -1859,8 +1859,8 @@
apply clarify
apply (simp (no_asm_use))
apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast)
-apply (rule_tac "bc1.0"="[Dup]" and "bc2.0"="[Store (index (pns, lvars, blk, res) vname)]"
- and "f1.0"="dupST" and "f2.0"="popST (Suc 0)"
+apply (rule_tac ?bc1.0="[Dup]" and ?bc2.0="[Store (index (pns, lvars, blk, res) vname)]"
+ and ?f1.0="dupST" and ?f2.0="popST (Suc 0)"
in bc_mt_corresp_comb)
apply (simp (no_asm_simp))+
apply (rule bc_mt_corresp_Dup)
@@ -1898,7 +1898,7 @@
apply (simp only: compTpExpr_LT_ST)
apply (rule bc_mt_corresp_comb, (rule HOL.refl)+) apply blast
apply (simp only: compTpExpr_LT_ST)
-apply (rule_tac "bc1.0"="[Dup_x1]" and "bc2.0"="[Putfield vname cname]" in bc_mt_corresp_comb)
+apply (rule_tac ?bc1.0="[Dup_x1]" and ?bc2.0="[Putfield vname cname]" in bc_mt_corresp_comb)
apply (simp (no_asm_simp))+
apply (rule bc_mt_corresp_Dup_x1)
apply (simp (no_asm_simp) add: dup_x1ST_def)
@@ -2010,24 +2010,24 @@
apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
apply (simp (no_asm_simp))
-apply (drule_tac "bc1.0"="[]" and "bc2.0" = "[LitPush (Bool False)]"
- and "bc3.0"="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
+apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "[LitPush (Bool False)]"
+ and ?bc3.0="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
compStmt jmb stmt2"
- and "f1.0"=comb_nil and "f2.0" = "pushST [PrimT Boolean]"
- and "f3.0"="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt1 \<box>
+ and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]"
+ and ?f3.0="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt1 \<box>
nochangeST \<box> compTpStmt jmb G stmt2"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
apply (simp (no_asm_simp) add: start_sttp_resp_def)+
-apply (drule_tac "bc1.0"="[LitPush (Bool False)]" and "bc2.0" = "compExpr jmb expr"
- and "bc3.0"="Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
+apply (drule_tac ?bc1.0="[LitPush (Bool False)]" and ?bc2.0 = "compExpr jmb expr"
+ and ?bc3.0="Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
compStmt jmb stmt2"
- and "f1.0"="pushST [PrimT Boolean]" and "f2.0" = "compTpExpr jmb G expr"
- and "f3.0"="popST 2 \<box> compTpStmt jmb G stmt1 \<box>
+ and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr"
+ and ?f3.0="popST 2 \<box> compTpStmt jmb G stmt1 \<box>
nochangeST \<box> compTpStmt jmb G stmt2"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
@@ -2036,12 +2036,12 @@
apply (simp (no_asm_simp))+
-apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr"
+apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr"
and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt1)))"
- and "bc3.0" = "compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
+ and ?bc3.0 = "compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
compStmt jmb stmt2"
- and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and "f2.0" = "popST 2"
- and "f3.0"="compTpStmt jmb G stmt1 \<box> nochangeST \<box> compTpStmt jmb G stmt2"
+ and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and ?f2.0 = "popST 2"
+ and ?f3.0="compTpStmt jmb G stmt1 \<box> nochangeST \<box> compTpStmt jmb G stmt2"
in bc_mt_corresp_comb_wt_instr)
apply (simp (no_asm_simp) add: length_compTpExpr)+
apply (simp (no_asm_simp) add: start_sttp_resp_comb)
@@ -2079,13 +2079,13 @@
apply (rule contracting_popST)
apply (drule_tac
- "bc1.0"="[LitPush (Bool False)] @ compExpr jmb expr @
+ ?bc1.0="[LitPush (Bool False)] @ compExpr jmb expr @
[Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] "
- and "bc2.0" = "compStmt jmb stmt1"
- and "bc3.0"="Goto (1 + int (length (compStmt jmb stmt2))) # compStmt jmb stmt2"
- and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2"
- and "f2.0" = "compTpStmt jmb G stmt1"
- and "f3.0"="nochangeST \<box> compTpStmt jmb G stmt2"
+ and ?bc2.0 = "compStmt jmb stmt1"
+ and ?bc3.0="Goto (1 + int (length (compStmt jmb stmt2))) # compStmt jmb stmt2"
+ and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2"
+ and ?f2.0 = "compTpStmt jmb G stmt1"
+ and ?f3.0="nochangeST \<box> compTpStmt jmb G stmt2"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
@@ -2094,13 +2094,13 @@
apply (simp (no_asm_simp) add: length_compTpExpr)+
-apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ compStmt jmb stmt1"
+apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ compStmt jmb stmt1"
and inst = "Goto (1 + int (length (compStmt jmb stmt2)))"
- and "bc3.0" = "compStmt jmb stmt2"
- and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box>
+ and ?bc3.0 = "compStmt jmb stmt2"
+ and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box>
compTpStmt jmb G stmt1"
- and "f2.0" = "nochangeST"
- and "f3.0"="compTpStmt jmb G stmt2"
+ and ?f2.0 = "nochangeST"
+ and ?f3.0="compTpStmt jmb G stmt2"
in bc_mt_corresp_comb_wt_instr)
apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
apply (intro strip)
@@ -2120,15 +2120,15 @@
apply (drule_tac
- "bc1.0"= "[LitPush (Bool False)] @ compExpr jmb expr @
+ ?bc1.0= "[LitPush (Bool False)] @ compExpr jmb expr @
[Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @
compStmt jmb stmt1 @ [Goto (1 + int (length (compStmt jmb stmt2)))]"
- and "bc2.0" = "compStmt jmb stmt2"
- and "bc3.0"="[]"
- and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box>
+ and ?bc2.0 = "compStmt jmb stmt2"
+ and ?bc3.0="[]"
+ and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box>
compTpStmt jmb G stmt1 \<box> nochangeST"
- and "f2.0" = "compTpStmt jmb G stmt2"
- and "f3.0"="comb_nil"
+ and ?f2.0 = "compTpStmt jmb G stmt2"
+ and ?f3.0="comb_nil"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def compTpExpr_LT_ST)
@@ -2152,23 +2152,23 @@
apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
apply (simp (no_asm_simp))
-apply (drule_tac "bc1.0"="[]" and "bc2.0" = "[LitPush (Bool False)]"
- and "bc3.0"="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
+apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "[LitPush (Bool False)]"
+ and ?bc3.0="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
compStmt jmb stmt @
[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
- and "f1.0"=comb_nil and "f2.0" = "pushST [PrimT Boolean]"
- and "f3.0"="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
+ and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]"
+ and ?f3.0="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
apply (simp (no_asm_simp) add: start_sttp_resp_def)+
-apply (drule_tac "bc1.0"="[LitPush (Bool False)]" and "bc2.0" = "compExpr jmb expr"
- and "bc3.0"="Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
+apply (drule_tac ?bc1.0="[LitPush (Bool False)]" and ?bc2.0 = "compExpr jmb expr"
+ and ?bc3.0="Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
compStmt jmb stmt @
[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
- and "f1.0"="pushST [PrimT Boolean]" and "f2.0" = "compTpExpr jmb G expr"
- and "f3.0"="popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
+ and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr"
+ and ?f3.0="popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (simp (no_asm_simp) add: pushST_def)
@@ -2176,12 +2176,12 @@
apply (simp (no_asm_simp))+
-apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr"
+apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr"
and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt)))"
- and "bc3.0" = "compStmt jmb stmt @
+ and ?bc3.0 = "compStmt jmb stmt @
[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
- and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and "f2.0" = "popST 2"
- and "f3.0"="compTpStmt jmb G stmt \<box> nochangeST"
+ and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and ?f2.0 = "popST 2"
+ and ?f3.0="compTpStmt jmb G stmt \<box> nochangeST"
in bc_mt_corresp_comb_wt_instr)
apply (simp (no_asm_simp) add: length_compTpExpr)+
apply (simp (no_asm_simp) add: start_sttp_resp_comb)
@@ -2219,13 +2219,13 @@
apply (rule contracting_popST)
apply (drule_tac
- "bc1.0"="[LitPush (Bool False)] @ compExpr jmb expr @
+ ?bc1.0="[LitPush (Bool False)] @ compExpr jmb expr @
[Ifcmpeq (2 + int (length (compStmt jmb stmt)))] "
- and "bc2.0" = "compStmt jmb stmt"
- and "bc3.0"="[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
- and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2"
- and "f2.0" = "compTpStmt jmb G stmt"
- and "f3.0"="nochangeST"
+ and ?bc2.0 = "compStmt jmb stmt"
+ and ?bc3.0="[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
+ and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2"
+ and ?f2.0 = "compTpStmt jmb G stmt"
+ and ?f3.0="nochangeST"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
@@ -2234,13 +2234,13 @@
apply (simp (no_asm_simp) add: length_compTpExpr)+
-apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] @ compStmt jmb stmt"
+apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] @ compStmt jmb stmt"
and inst = "Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))"
- and "bc3.0" = "[]"
- and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box>
+ and ?bc3.0 = "[]"
+ and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box>
compTpStmt jmb G stmt"
- and "f2.0" = "nochangeST"
- and "f3.0"="comb_nil"
+ and ?f2.0 = "nochangeST"
+ and ?f3.0="comb_nil"
in bc_mt_corresp_comb_wt_instr)
apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
apply (intro strip)
@@ -2277,7 +2277,7 @@
is_type G ty \<rbrakk>
\<Longrightarrow> bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)"
apply (simp add: compInit_def compTpInit_def split_beta)
-apply (rule_tac "bc1.0"="[load_default_val ty]" and "bc2.0"="[Store (index jmb vn)]"
+apply (rule_tac ?bc1.0="[load_default_val ty]" and ?bc2.0="[Store (index jmb vn)]"
in bc_mt_corresp_comb)
apply simp+
apply (simp add: load_default_val_def)
@@ -2311,7 +2311,7 @@
apply (drule_tac x="lvars_pre @ [a]" in spec)
apply (drule_tac x="lvars0" in spec)
apply (simp (no_asm_simp) add: compInitLvars_def)
-apply (rule_tac "bc1.0"="compInit jmb a" and "bc2.0"="compInitLvars jmb list"
+apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb list"
in bc_mt_corresp_comb)
apply (simp (no_asm_simp) add: compInitLvars_def)+
--- a/src/HOL/MicroJava/J/Conform.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Aug 29 15:19:02 2003 +0200
@@ -120,9 +120,9 @@
lemma defval_conf [rule_format (no_asm)]:
"is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
apply (unfold conf_def)
-apply (rule_tac "y" = "T" in ty.exhaust)
+apply (rule_tac y = "T" in ty.exhaust)
apply (erule ssubst)
-apply (rule_tac "y" = "prim_ty" in prim_ty.exhaust)
+apply (rule_tac y = "prim_ty" in prim_ty.exhaust)
apply (auto simp add: widen.null)
done
@@ -178,7 +178,7 @@
lemma non_np_objD' [rule_format (no_asm)]:
"a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t -->
(\<exists>a C fs. a' = Addr a \<and> h a = Some (C,fs) \<and> G\<turnstile>Class C\<preceq>RefT t)"
-apply(rule_tac "y" = "t" in ref_ty.exhaust)
+apply(rule_tac y = "t" in ref_ty.exhaust)
apply (fast dest: conf_NullTD)
apply (fast dest: non_np_objD)
done
--- a/src/HOL/MicroJava/J/State.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/MicroJava/J/State.thy Fri Aug 29 15:19:02 2003 +0200
@@ -73,7 +73,7 @@
apply(simp add: Pair_fst_snd_eq Eps_split)
apply(rule someI)
apply(rule disjI2)
-apply(rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
+apply(rule_tac r = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
apply auto
done
--- a/src/HOL/MicroJava/J/WellForm.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Fri Aug 29 15:19:02 2003 +0200
@@ -547,7 +547,7 @@
apply (assumption)
apply (assumption)
apply (clarify)
-apply (erule_tac "x" = "Da" in allE)
+apply (erule_tac x = "Da" in allE)
apply (clarsimp)
apply (simp add: map_of_map)
apply (clarify)
@@ -571,7 +571,7 @@
apply (assumption)
apply (assumption)
apply (clarify)
-apply (erule_tac "x" = "Da" in allE)
+apply (erule_tac x = "Da" in allE)
apply (clarsimp)
apply (simp add: map_of_map)
apply (clarify)
--- a/src/HOL/NanoJava/Equivalence.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Fri Aug 29 15:19:02 2003 +0200
@@ -83,7 +83,7 @@
lemma Loop_sound_lemma [rule_format (no_asm)]:
"\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<x> \<noteq> Null \<longrightarrow> P t \<Longrightarrow>
(s -c0-n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<x> = Null)"
-apply (rule_tac "P2.1"="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
+apply (rule_tac ?P2.1="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
apply clarsimp+
done
--- a/src/HOL/NumberTheory/EulerFermat.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Fri Aug 29 15:19:02 2003 +0200
@@ -145,7 +145,7 @@
apply (rule_tac [2] m = m in zcong_zless_imp_eq)
apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
- apply (rule_tac "x" = b in exI, safe)
+ apply (rule_tac x = b in exI, safe)
apply (rule Bnor_mem_if)
apply (case_tac [2] "b = 0")
apply (auto intro: order_less_le [THEN iffD2])
--- a/src/HOL/NumberTheory/IntPrimes.thy Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Fri Aug 29 15:19:02 2003 +0200
@@ -400,7 +400,7 @@
lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
apply (unfold zcong_def)
apply (rule_tac t = "a - b" in ssubst)
- apply (rule_tac "m" = m in zcong_zmod_aux)
+ apply (rule_tac m = m in zcong_zmod_aux)
apply (rule trans)
apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
apply (simp add: zadd_commute)
--- a/src/HOL/Tools/datatype_package.ML Fri Aug 29 13:18:45 2003 +0200
+++ b/src/HOL/Tools/datatype_package.ML Fri Aug 29 15:19:02 2003 +0200
@@ -189,7 +189,7 @@
in
-fun gen_induct_tac (varss, opt_rule) i state =
+fun gen_induct_tac inst_tac (varss, opt_rule) i state =
let
val (_, _, Bi, _) = Thm.dest_state (state, i);
val {sign, ...} = Thm.rep_thm state;
@@ -203,33 +203,39 @@
val concls = HOLogic.dest_concls (Thm.concl_of rule);
val insts = flat (map prep_inst (concls ~~ varss)) handle LIST _ =>
error (rule_name ^ " has different numbers of variables");
- in occs_in_prems (Tactic.res_inst_tac insts rule) (map #2 insts) i state end;
+ in occs_in_prems (inst_tac insts rule) (map #2 insts) i state end;
-fun induct_tac s = gen_induct_tac (map (Library.single o Some) (Syntax.read_idents s), None);
+fun induct_tac s =
+ gen_induct_tac Tactic.res_inst_tac
+ (map (Library.single o Some) (Syntax.read_idents s), None);
fun induct_thm_tac th s =
- gen_induct_tac ([map Some (Syntax.read_idents s)], Some th);
+ gen_induct_tac Tactic.res_inst_tac
+ ([map Some (Syntax.read_idents s)], Some th);
end;
(* generic case tactic for datatypes *)
-fun case_inst_tac t rule i state =
+fun case_inst_tac inst_tac t rule i state =
let
val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
(hd (Logic.strip_assums_hyp (hd (Thm.prems_of rule))));
val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)));
- in Tactic.res_inst_tac [(exh_vname, t)] rule i state end;
+ in inst_tac [(exh_vname, t)] rule i state end;
-fun gen_case_tac (t, Some rule) i state = case_inst_tac t rule i state
- | gen_case_tac (t, None) i state =
+fun gen_case_tac inst_tac (t, Some rule) i state =
+ case_inst_tac inst_tac t rule i state
+ | gen_case_tac inst_tac (t, None) i state =
let val tn = infer_tname state i t in
- if tn = HOLogic.boolN then Tactic.res_inst_tac [("P", t)] case_split_thm i state
- else case_inst_tac t (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn)) i state
+ if tn = HOLogic.boolN then inst_tac [("P", t)] case_split_thm i state
+ else case_inst_tac inst_tac t
+ (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn))
+ i state
end;
-fun case_tac t = gen_case_tac (t, None);
+fun case_tac t = gen_case_tac Tactic.res_inst_tac (t, None);
@@ -242,13 +248,23 @@
val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
+fun mk_ixn (vars, s) = (fst (Term.dest_Var (Syntax.read_var ("?" ^ vars))), s)
+ handle _ => error (vars ^ " not a variable name");
+fun inst_tac ctxt sinsts =
+ Method.bires_inst_tac false ctxt (map mk_ixn sinsts);
+
+fun induct_meth ctxt (varss, opt_rule) =
+ gen_induct_tac (inst_tac ctxt) (varss, opt_rule);
+fun case_meth ctxt (varss, opt_rule) =
+ gen_case_tac (inst_tac ctxt) (varss, opt_rule);
+
in
val tactic_emulations =
- [("induct_tac", Method.goal_args' (varss -- opt_rule) gen_induct_tac,
- "induct_tac emulation (dynamic instantiation!)"),
- ("case_tac", Method.goal_args' (Scan.lift Args.name -- opt_rule) gen_case_tac,
- "case_tac emulation (dynamic instantiation!)")];
+ [("induct_tac", Method.goal_args_ctxt' (varss -- opt_rule) induct_meth,
+ "induct_tac emulation (dynamic instantiation)"),
+ ("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) case_meth,
+ "case_tac emulation (dynamic instantiation)")];
end;
--- a/src/Pure/Isar/args.ML Fri Aug 29 13:18:45 2003 +0200
+++ b/src/Pure/Isar/args.ML Fri Aug 29 15:19:02 2003 +0200
@@ -142,14 +142,23 @@
Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
fun kind f = Scan.one (K true) :--
- (fn Arg (Ident, (x, _)) =>
+ ((fn Arg (Ident, (x, _)) =>
(case f x of Some y => Scan.succeed y | _ => Scan.fail)
- | _ => Scan.fail) >> #2;
+ | _ => Scan.fail)
+(* o (fn (t as Arg (i, (s, _))) =>
+ (warning (
+ (case i of Ident => "Ident: " | String => "String: "
+ | Keyword => "Keyword: " | EOF => "EOF: ")
+ ^ s); t)) *) ) >> #2;
val nat = kind Syntax.read_nat;
val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
-val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
+(* Read variable name. Leading `?' may be omitted if name contains no dot. *)
+val var = kind (apsome #1 o
+ (fn s => (Some (Term.dest_Var (Syntax.read_var s)))
+ handle _ => (Some (Term.dest_Var (Syntax.read_var ("?" ^ s))))
+ handle _ => None));
(* enumerations *)
--- a/src/Pure/Isar/method.ML Fri Aug 29 13:18:45 2003 +0200
+++ b/src/Pure/Isar/method.ML Fri Aug 29 15:19:02 2003 +0200
@@ -45,7 +45,7 @@
val frule: int -> thm list -> Proof.method
val this: Proof.method
val assumption: Proof.context -> Proof.method
- val impose_hyps_tac: Proof.context -> tactic
+ val bires_inst_tac: bool -> Proof.context -> (indexname * string) list -> thm -> int -> tactic
val set_tactic: (Proof.context -> thm list -> tactic) -> unit
val tactic: string -> Proof.context -> Proof.method
exception METHOD_FAIL of (string * Position.T) * exn
@@ -111,6 +111,10 @@
-> Args.src -> Proof.context -> Proof.method
val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
-> ('a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
+ val goal_args_ctxt: (Args.T list -> 'a * Args.T list) -> (Proof.context -> 'a -> int -> tactic)
+ -> Args.src -> Proof.context -> Proof.method
+ val goal_args_ctxt': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
+ -> (Proof.context -> 'a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
val setup: (theory -> theory) list
end;
@@ -322,23 +326,149 @@
(* res_inst_tac etc. *)
-(*robustify instantiation by imposing (part of) the present static context*)
-val impose_hyps_tac =
- PRIMITIVE o Drule.impose_hyps o flat o map #1 o ProofContext.assumptions_of;
+(* Reimplemented to support both static (Isar) and dynamic (proof state)
+ context. By Clemens Ballarin. *)
-(*Note: insts refer to the implicit (!!) goal context; use at your own risk*)
-fun gen_res_inst _ tac _ (quant, ([], thms)) =
- METHOD (fn facts => (quant (insert_tac facts THEN' tac thms)))
- | gen_res_inst tac _ ctxt (quant, (insts, [thm])) =
- METHOD (fn facts => (impose_hyps_tac ctxt THEN quant (insert_tac facts THEN' tac insts thm)))
- | gen_res_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
+fun bires_inst_tac bires_flag ctxt insts thm =
+ let
+ val sign = ProofContext.sign_of ctxt;
+ (* Separate type and term insts *)
+ fun has_type_var ((x, _), _) = (case Symbol.explode x of
+ "'"::cs => true | cs => false);
+ val Tinsts = filter has_type_var insts;
+ val tinsts = filter_out has_type_var insts;
+ (* Tactic *)
+ fun tac i st =
+ let
+ (* Preprocess state: extract environment information:
+ - variables and their types
+ - type variables and their sorts
+ - parameters and their types *)
+ val (types, sorts) = types_sorts st;
+ (* Process type insts: Tinsts_env *)
+ fun absent xi = error
+ ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
+ val (rtypes, rsorts) = types_sorts thm;
+ fun readT (xi, s) =
+ let val S = case rsorts xi of Some S => S | None => absent xi;
+ val T = Sign.read_typ (sign, sorts) s;
+ in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T)
+ else error
+ ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
+ end;
+ val Tinsts_env = map readT Tinsts;
+ (* Preprocess rule: extract vars and their types, apply Tinsts *)
+ fun get_typ xi =
+ (case rtypes xi of
+ Some T => typ_subst_TVars Tinsts_env T
+ | None => absent xi);
+ val (xis, ss) = Library.split_list tinsts;
+ val Ts = map get_typ xis;
+ val (_, _, Bi, _) = dest_state(st,i)
+ val params = Logic.strip_params Bi
+ (* params of subgoal i as string typ pairs *)
+ val params = rev(Term.rename_wrt_term Bi params)
+ (* as they are printed *)
+ fun types' (a, ~1) = (case assoc (params, a) of
+ None => types (a, ~1)
+ | some => some)
+ | types' xi = types xi;
+ val used = add_term_tvarnames
+ (prop_of st $ prop_of thm,[])
+ val (ts, envT) =
+ ProofContext.read_termTs_env (types', sorts, used) ctxt (ss ~~ Ts);
+ val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env);
+ val cenv =
+ map
+ (fn (xi, t) =>
+ pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
+ (gen_distinct
+ (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
+ (xis ~~ ts));
+ (* Lift and instantiate rule *)
+ val {maxidx, ...} = rep_thm st;
+ val paramTs = map #2 params
+ and inc = maxidx+1
+ fun liftvar (Var ((a,j), T)) =
+ Var((a, j+inc), paramTs ---> incr_tvar inc T)
+ | liftvar t = raise TERM("Variable expected", [t]);
+ fun liftterm t = list_abs_free
+ (params, Logic.incr_indexes(paramTs,inc) t)
+ fun liftpair (cv,ct) =
+ (cterm_fun liftvar cv, cterm_fun liftterm ct)
+ fun lifttvar((a,i),ctyp) =
+ let val {T,sign} = rep_ctyp ctyp
+ in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
+ val rule = Drule.instantiate
+ (map lifttvar cenvT, map liftpair cenv)
+ (lift_rule (st, i) thm)
+ in
+ if i > nprems_of st then no_tac st
+ else st |>
+ compose_tac (bires_flag, rule, nprems_of thm) i
+ end
+ handle TERM (msg,_) => (warning msg; no_tac st)
+ | THM (msg,_,_) => (warning msg; no_tac st);
+ in
+ tac
+ end;
-val res_inst = gen_res_inst Tactic.res_inst_tac Tactic.resolve_tac;
-val eres_inst = gen_res_inst Tactic.eres_inst_tac Tactic.eresolve_tac;
-val dres_inst = gen_res_inst Tactic.dres_inst_tac Tactic.dresolve_tac;
-val forw_inst = gen_res_inst Tactic.forw_inst_tac Tactic.forward_tac;
-val cut_inst = gen_res_inst Tactic.cut_inst_tac Tactic.cut_rules_tac;
+fun gen_inst _ tac _ (quant, ([], thms)) =
+ METHOD (fn facts => quant (insert_tac facts THEN' tac thms))
+ | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
+ METHOD (fn facts =>
+ quant (insert_tac facts THEN' inst_tac ctxt insts thm))
+ | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
+
+val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
+
+val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac;
+
+(* Preserve Var indexes of rl; increment revcut_rl instead.
+ Copied from tactic.ML *)
+fun make_elim_preserve rl =
+ let val {maxidx,...} = rep_thm rl
+ fun cvar xi = cterm_of (Theory.sign_of ProtoPure.thy) (Var(xi,propT));
+ val revcut_rl' =
+ instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)),
+ (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
+ val arg = (false, rl, nprems_of rl)
+ val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
+ in th end
+ handle Bind => raise THM("make_elim_preserve", 1, [rl]);
+val cut_inst_meth =
+ gen_inst
+ (fn ctxt => fn insts => fn thm =>
+ bires_inst_tac false ctxt insts (make_elim_preserve thm))
+ Tactic.cut_rules_tac;
+
+val dres_inst_meth =
+ gen_inst
+ (fn ctxt => fn insts => fn rule =>
+ bires_inst_tac true ctxt insts (make_elim_preserve rule))
+ Tactic.dresolve_tac;
+
+val forw_inst_meth =
+ gen_inst
+ (fn ctxt => fn insts => fn rule =>
+ bires_inst_tac false ctxt insts (make_elim_preserve rule) THEN'
+ assume_tac)
+ Tactic.forward_tac;
+
+fun subgoal_tac ctxt sprop =
+ DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl THEN'
+ SUBGOAL (fn (prop, _) =>
+ let val concl' = Logic.strip_assums_concl prop in
+ if null (term_tvars concl') then ()
+ else warning "Type variables in new subgoal: add a type constraint?";
+ all_tac
+ end);
+
+fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
+
+fun thin_tac ctxt s =
+ bires_inst_tac true ctxt [(("V", 0), s)] thin_rl;
(* simple Prolog interpreter *)
@@ -536,13 +666,23 @@
fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
+val insts_var =
+ Scan.optional
+ (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
+ Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss;
+
+fun inst_args_var f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
- (fn (quant, s) => SIMPLE_METHOD' quant (K (impose_hyps_tac ctxt) THEN' tac s))) src ctxt);
+ (fn (quant, s) => SIMPLE_METHOD' quant ( (*K (impose_hyps_tac ctxt) THEN' *) tac s))) src ctxt);
fun goal_args args tac = goal_args' (Scan.lift args) tac;
+fun goal_args_ctxt' args tac src ctxt =
+ #2 (syntax (Args.goal_spec HEADGOAL -- args >>
+ (fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt);
+fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
(** method text **)
@@ -629,8 +769,8 @@
(* misc tactic emulations *)
-val subgoal_meth = goal_args (Scan.repeat1 Args.name) Tactic.subgoals_tac;
-val thin_meth = goal_args Args.name Tactic.thin_tac;
+val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac;
+val thin_meth = goal_args_ctxt Args.name thin_tac;
val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac;
val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac;
@@ -655,14 +795,14 @@
("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
("this", no_args this, "apply current facts as rules"),
("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
- ("rule_tac", inst_args res_inst, "apply rule (dynamic instantiation!)"),
- ("erule_tac", inst_args eres_inst, "apply rule in elimination manner (dynamic instantiation!)"),
- ("drule_tac", inst_args dres_inst, "apply rule in destruct manner (dynamic instantiation!)"),
- ("frule_tac", inst_args forw_inst, "apply rule in forward manner (dynamic instantiation!)"),
- ("cut_tac", inst_args cut_inst, "cut rule (dynamic instantiation!)"),
- ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation!)"),
- ("thin_tac", thin_meth, "remove premise (dynamic instantiation!)"),
- ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation!)"),
+ ("rule_tac", inst_args_var res_inst_meth, "apply rule (dynamic instantiation)"),
+ ("erule_tac", inst_args_var eres_inst_meth, "apply rule in elimination manner (dynamic instantiation)"),
+ ("drule_tac", inst_args_var dres_inst_meth, "apply rule in destruct manner (dynamic instantiation)"),
+ ("frule_tac", inst_args_var forw_inst_meth, "apply rule in forward manner (dynamic instantiation)"),
+ ("cut_tac", inst_args_var cut_inst_meth, "cut rule (dynamic instantiation)"),
+ ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation)"),
+ ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"),
+ ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"),
("rotate_tac", rotate_meth, "rotate assumptions of goal"),
("prolog", thms_args prolog, "simple prolog interpreter"),
("tactic", simple_args Args.name tactic, "ML tactic as proof method")];
--- a/src/Pure/Isar/proof_context.ML Fri Aug 29 13:18:45 2003 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Aug 29 15:19:02 2003 +0200
@@ -30,6 +30,7 @@
val get_skolem: context -> string -> string
val extern_skolem: context -> term -> term
val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
+ val read_termTs_env: (indexname -> typ option) * (indexname -> sort option) * string list -> context -> (string * typ) list -> term list * (indexname * typ) list
val read_term: context -> string -> term
val read_prop: context -> string -> term
val read_prop_schematic: context -> string -> term
@@ -440,12 +441,15 @@
raise CONTEXT ("Illegal reference to internal variable: " ^ quote x, ctxt)
else x;
-fun intern_skolem ctxt =
+fun intern_skolem ctxt env =
+(* env contains names that are not to be internalised *)
let
fun intern (t as Free (x, T)) =
- (case lookup_skolem ctxt (no_skolem false ctxt x) of
- Some x' => Free (x', T)
- | None => t)
+ (case env (x, ~1) of
+ Some _ => t
+ | None => (case lookup_skolem ctxt (no_skolem false ctxt x) of
+ Some x' => Free (x', T)
+ | None => t))
| intern (t $ u) = intern t $ intern u
| intern (Abs (x, T, t)) = Abs (x, T, intern t)
| intern a = a;
@@ -513,7 +517,7 @@
let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
-fun norm_term (ctxt as Context {binds, ...}) schematic =
+fun norm_term (ctxt as Context {binds, ...}) schematic allow_vars =
let
(*raised when norm has no effect on a term, to do sharing instead of copying*)
exception SAME;
@@ -523,11 +527,12 @@
Some (Some (u, U)) =>
let
val env = unifyT ctxt (T, U) handle Type.TUNIFY =>
- raise TYPE ("norm_term: ill-typed variable assigment", [T, U], [t, u]);
+ raise TYPE ("norm_term: ill-typed variable assignment", [T, U], [t, u]);
val u' = Term.subst_TVars_Vartab env u;
in norm u' handle SAME => u' end
| _ =>
if schematic then raise SAME
+ else if allow_vars then t
else raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt))
| norm (Abs (a, T, body)) = Abs (a, T, norm body)
| norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
@@ -552,29 +557,59 @@
local
-fun gen_read read app is_pat dummies schematic (ctxt as Context {defs = (_, _, used, _), ...}) s =
- (transform_error (read (syn_of ctxt)
- (sign_of ctxt) (def_type ctxt is_pat, def_sort ctxt, used)) s
- handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
- | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
- |> app (intern_skolem ctxt)
- |> app (if is_pat then I else norm_term ctxt schematic)
- |> app (if is_pat then prepare_dummies else if dummies then I else reject_dummies ctxt);
-
+fun gen_read read app env_opt allow_vars is_pat dummies schematic
+ (ctxt as Context {defs = (_, _, used, _), ...}) s =
+ let
+ (* Use environment of ctxt with the following modification:
+ bindings in env_opt take precedence (needed for rule_tac) *)
+ val types = def_type ctxt is_pat;
+ val types' = case env_opt of
+ None => types
+ | Some (env, _, _) =>
+ (fn ixn => case env ixn of
+ None => types ixn
+ | some => some);
+ val sorts = def_sort ctxt;
+ val sorts' = case env_opt of
+ None => sorts
+ | Some (_, envT, _) =>
+ (fn ixn => case envT ixn of
+ None => sorts ixn
+ | some => some);
+ val used' = case env_opt of
+ None => used
+ | Some (_, _, used'') => used @ used'';
+ in
+ (transform_error (read (syn_of ctxt)
+ (sign_of ctxt) (types', sorts', used')) s
+ handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
+ | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
+ |> app (intern_skolem ctxt (case env_opt of None => K None | Some (env, _, _) => env))
+ |> app (if is_pat then I else norm_term ctxt schematic allow_vars)
+ |> app (if is_pat then prepare_dummies
+ else if dummies then I else reject_dummies ctxt)
+ end
in
-val read_termTs = gen_read (read_def_termTs false) (apfst o map) false false false;
-val read_termT_pats = #1 oo gen_read (read_def_termTs false) (apfst o map) true false false;
+val read_termTs =
+ gen_read (read_def_termTs false) (apfst o map) None false false false false;
+(* For rule_tac:
+ takes extra environment (types, sorts and used type vars) *)
+fun read_termTs_env env =
+ gen_read (read_def_termTs false) (apfst o map) (Some env) true false false false;
+val read_termT_pats =
+ #1 oo gen_read (read_def_termTs false) (apfst o map) None false true false false;
fun read_term_pats T ctxt pats = read_termT_pats ctxt (map (rpair T) pats);
val read_prop_pats = read_term_pats propT;
-val read_term = gen_read (read_term_sg true) I false false false;
-val read_term_dummies = gen_read (read_term_sg true) I false true false;
-val read_prop = gen_read (read_prop_sg true) I false false false;
-val read_prop_schematic = gen_read (read_prop_sg true) I false false true;
-val read_terms = gen_read (read_terms_sg true) map false false false;
-val read_props = gen_read (read_props_sg true) map false false;
+val read_term = gen_read (read_term_sg true) I None false false false false;
+val read_term_dummies = gen_read (read_term_sg true) I None false false true false;
+val read_prop = gen_read (read_prop_sg true) I None false false false false;
+val read_prop_schematic =
+ gen_read (read_prop_sg true) I None false false false true;
+val read_terms = gen_read (read_terms_sg true) map None false false false false;
+val read_props = gen_read (read_props_sg true) map None false false false;
end;
@@ -584,7 +619,7 @@
local
fun gen_cert cert is_pat schematic ctxt t = t
- |> (if is_pat then I else norm_term ctxt schematic)
+ |> (if is_pat then I else norm_term ctxt schematic false)
|> (fn t' => cert (sign_of ctxt) t' handle TERM (msg, _) => raise CONTEXT (msg, ctxt));
in