Methods rule_tac etc support static (Isar) contexts.
authorballarin
Fri Aug 29 15:19:02 2003 +0200 (2003-08-29)
changeset 14174f3cafd2929d5
parent 14173 a3690aeb79d4
child 14175 dbd16ebaf907
Methods rule_tac etc support static (Isar) contexts.
src/HOL/Bali/WellForm.thy
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/Tools/datatype_package.ML
src/Pure/Isar/args.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/HOL/Bali/WellForm.thy	Fri Aug 29 13:18:45 2003 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Fri Aug 29 15:19:02 2003 +0200
     1.3 @@ -1943,7 +1943,7 @@
     1.4   (\<exists>T m. t = ArrayT T \<and> G\<turnstile>Array T accessible_in (pid S) \<and>
     1.5          accmethd G S Object sig = Some m \<and> accmodi m \<noteq> Private \<and> 
     1.6          declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh)"
     1.7 -apply (rule_tac "ref_ty1"="t" in ref_ty_ty.induct [THEN conjunct1])
     1.8 +apply (rule_tac ref_ty1="t" in ref_ty_ty.induct [THEN conjunct1])
     1.9  apply auto
    1.10  apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def)
    1.11  apply (auto  dest!: accmethd_SomeD)
     2.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Fri Aug 29 13:18:45 2003 +0200
     2.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Fri Aug 29 15:19:02 2003 +0200
     2.3 @@ -320,7 +320,7 @@
     2.4      apply force
     2.5     apply force
     2.6    apply force
     2.7 - 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)
     2.8 + 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)
     2.9       apply force
    2.10      apply(rule subset_refl)+
    2.11   apply(rule Cond)
    2.12 @@ -375,7 +375,7 @@
    2.13      apply force
    2.14     apply force
    2.15    apply force
    2.16 - 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)
    2.17 + 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)
    2.18       apply force
    2.19      apply(rule subset_refl)+
    2.20   apply(rule Cond)
     3.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Fri Aug 29 13:18:45 2003 +0200
     3.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Fri Aug 29 15:19:02 2003 +0200
     3.3 @@ -132,7 +132,7 @@
     3.4    {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
     3.5  apply (simp only: progression_def)
     3.6  apply (intro strip)
     3.7 -apply (rule_tac "s1.0" = "Norm (hp1, (os1, lvars1, C, S, 
     3.8 +apply (rule_tac ?s1.0 = "Norm (hp1, (os1, lvars1, C, S, 
     3.9                            length pre + length instrs0) # frs)"  
    3.10         in exec_all_trans)
    3.11  apply (simp only: append_assoc)
    3.12 @@ -191,7 +191,7 @@
    3.13    \<Longrightarrow> {G, C, S} \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
    3.14  apply (simp only: progression_def jump_fwd_def)
    3.15  apply (intro strip)
    3.16 -apply (rule_tac "s1.0" = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans)
    3.17 +apply (rule_tac ?s1.0 = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans)
    3.18  apply (simp only: append_assoc)
    3.19  apply (subgoal_tac "pre @ (instr # instrs0 @ instrs1) @ post = pre @ instr # instrs0 @ (instrs1 @ post)")
    3.20  apply blast
    3.21 @@ -305,8 +305,8 @@
    3.22  apply force
    3.23  apply (intro strip)
    3.24  apply (frule_tac
    3.25 -  "P1.0" = "wf_mdecl wf_mb G Ca" and
    3.26 -  "P2.0" = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop)
    3.27 +  ?P1.0 = "wf_mdecl wf_mb G Ca" and
    3.28 +  ?P2.0 = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop)
    3.29  apply (force simp: wf_cdecl_def)
    3.30  
    3.31  apply clarify
    3.32 @@ -455,7 +455,7 @@
    3.33  apply (case_tac "v1 = v2")
    3.34  
    3.35  (* case v1 = v2 *)
    3.36 -apply (rule_tac "instrs1.0" = "[LitPush (Bool True)]" in jump_fwd_progression)
    3.37 +apply (rule_tac ?instrs1.0 = "[LitPush (Bool True)]" in jump_fwd_progression)
    3.38  apply (auto simp: nat_add_distrib)
    3.39  apply (rule progression_one_step) apply simp
    3.40  
    3.41 @@ -464,7 +464,7 @@
    3.42  apply auto
    3.43  apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) 
    3.44  apply auto
    3.45 -apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
    3.46 +apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
    3.47  apply (auto simp: nat_add_distrib intro: progression_refl)
    3.48  done
    3.49  
    3.50 @@ -522,9 +522,9 @@
    3.51  apply (case_tac lvals) apply simp
    3.52  apply (simp (no_asm_simp) )
    3.53  
    3.54 -apply (rule_tac "lvars1.0" = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
    3.55 +apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
    3.56  apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def)
    3.57 -apply (rule_tac "instrs0.0" = "[load_default_val b]" in progression_transitive, simp)
    3.58 +apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
    3.59  apply (rule progression_one_step)
    3.60  apply (simp (no_asm_simp) add: load_default_val_def)
    3.61  apply (rule conjI, simp)+ apply (rule HOL.refl)
    3.62 @@ -650,7 +650,7 @@
    3.63    E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk> 
    3.64    \<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T"
    3.65  apply (simp add: gh_def)
    3.66 -apply (rule_tac x3="fst s" and "s3"="snd s"and "x'3"="fst s'"  
    3.67 +apply (rule_tac x3="fst s" and s3="snd s"and x'3="fst s'"  
    3.68    in eval_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]], simplified])
    3.69  apply assumption+
    3.70  apply (simp (no_asm_use) add: surjective_pairing [THEN sym])
    3.71 @@ -769,7 +769,7 @@
    3.72  apply (frule raise_if_NoneD)
    3.73  apply (frule wtpd_expr_cast)
    3.74  apply simp
    3.75 -apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, simp)
    3.76 +apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, simp)
    3.77  apply blast
    3.78  apply (rule progression_one_step)
    3.79  apply (simp add: raise_system_xcpt_def  gh_def comp_cast_ok)
    3.80 @@ -791,8 +791,8 @@
    3.81  
    3.82  
    3.83  apply (simp (no_asm_use) only: compExpr_compExprs.simps)
    3.84 -apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast
    3.85 -apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast
    3.86 +apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast
    3.87 +apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast
    3.88  apply (case_tac bop)
    3.89    (*subcase bop = Eq *)  apply simp apply (rule progression_Eq)
    3.90    (*subcase bop = Add *) apply simp apply (rule progression_one_step) apply simp
    3.91 @@ -814,10 +814,10 @@
    3.92  apply (frule wtpd_expr_lass, erule conjE, erule conjE)
    3.93  apply (simp add: compExpr_compExprs.simps)
    3.94  
    3.95 -apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
    3.96 +apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
    3.97  apply blast
    3.98  
    3.99 -apply (rule_tac "instrs0.0" = "[Dup]" in progression_transitive, simp)
   3.100 +apply (rule_tac ?instrs0.0 = "[Dup]" in progression_transitive, simp)
   3.101  apply (rule progression_one_step)
   3.102  apply (simp add: gh_def)
   3.103  apply (rule conjI, simp)+ apply simp
   3.104 @@ -837,7 +837,7 @@
   3.105  apply (frule wtpd_expr_facc)
   3.106  
   3.107  apply (simp (no_asm_use) only: compExpr_compExprs.simps)
   3.108 -apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   3.109 +apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   3.110  apply blast
   3.111  apply (rule progression_one_step)
   3.112  apply (simp add: gh_def)
   3.113 @@ -860,11 +860,11 @@
   3.114  
   3.115  apply (simp only: compExpr_compExprs.simps)
   3.116  
   3.117 -apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl)
   3.118 +apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl)
   3.119  apply fast (* blast does not seem to work - why? *)
   3.120 -apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl)
   3.121 +apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl)
   3.122  apply fast
   3.123 -apply (rule_tac "instrs0.0" = "[Dup_x1]" and "instrs1.0" = "[Putfield fn T]" in progression_transitive, simp)
   3.124 +apply (rule_tac ?instrs0.0 = "[Dup_x1]" and ?instrs1.0 = "[Putfield fn T]" in progression_transitive, simp)
   3.125  
   3.126     (* Dup_x1 *)
   3.127     apply (rule progression_one_step)
   3.128 @@ -899,7 +899,7 @@
   3.129  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)
   3.130  
   3.131  apply simp
   3.132 -apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   3.133 +apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   3.134  apply fast
   3.135  apply fast
   3.136  
   3.137 @@ -916,7 +916,7 @@
   3.138  apply (intro allI impI)
   3.139  apply (frule wtpd_stmt_expr)
   3.140  apply simp
   3.141 -apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   3.142 +apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   3.143  apply fast
   3.144  apply (rule progression_one_step)
   3.145  apply simp
   3.146 @@ -930,7 +930,7 @@
   3.147  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)
   3.148  
   3.149  apply simp
   3.150 -apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl)
   3.151 +apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl)
   3.152  apply fast
   3.153  apply fast
   3.154  
   3.155 @@ -950,29 +950,29 @@
   3.156  apply (erule exE)
   3.157  
   3.158  apply simp
   3.159 -apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   3.160 +apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   3.161  apply (rule progression_one_step,  simp)
   3.162  apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   3.163  
   3.164 -apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   3.165 +apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   3.166  apply fast
   3.167  
   3.168  apply (case_tac b)
   3.169   (* case b= True *)
   3.170  apply simp
   3.171 -apply (rule_tac "instrs0.0" = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
   3.172 +apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
   3.173  apply (rule progression_one_step) apply simp
   3.174  apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   3.175 -apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
   3.176 +apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
   3.177  apply fast
   3.178 -apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
   3.179 +apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
   3.180  apply (simp, rule conjI, (rule HOL.refl)+)
   3.181  apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
   3.182  apply (rule progression_refl)
   3.183  
   3.184   (* case b= False *)
   3.185  apply simp
   3.186 -apply (rule_tac "instrs1.0" = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
   3.187 +apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
   3.188  apply (simp, rule conjI, (rule HOL.refl)+)
   3.189  apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
   3.190  apply fast
   3.191 @@ -993,14 +993,14 @@
   3.192   (* case b= False *)
   3.193  apply simp
   3.194  
   3.195 -apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   3.196 +apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   3.197  apply (rule progression_one_step)
   3.198     apply simp 
   3.199     apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   3.200  
   3.201 -apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   3.202 +apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   3.203  apply fast
   3.204 -apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
   3.205 +apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
   3.206  apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
   3.207  apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
   3.208  apply (rule progression_refl)
   3.209 @@ -1028,19 +1028,19 @@
   3.210  apply simp
   3.211  apply (rule conjI, (rule HOL.refl)+)
   3.212  
   3.213 -apply (rule_tac "instrs0.0" = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   3.214 +apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   3.215  apply (rule progression_one_step)
   3.216     apply simp 
   3.217     apply (rule conjI, simp)+ apply simp
   3.218  
   3.219 -apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   3.220 +apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   3.221  apply fast
   3.222  
   3.223  apply (case_tac b)
   3.224   (* case b= True *)
   3.225  apply simp
   3.226  
   3.227 -apply (rule_tac "instrs0.0" = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
   3.228 +apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
   3.229  apply (rule progression_one_step) apply simp
   3.230  apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   3.231  apply fast
   3.232 @@ -1116,11 +1116,11 @@
   3.233  apply (simp (no_asm_use) only: compExpr_compExprs.simps)
   3.234  
   3.235    (* evaluate e *)
   3.236 -apply (rule_tac "instrs0.0" = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   3.237 +apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   3.238  apply fast
   3.239  
   3.240    (* evaluate parameters *)
   3.241 -apply (rule_tac "instrs0.0" = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl)
   3.242 +apply (rule_tac ?instrs0.0 = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl)
   3.243  apply fast
   3.244  
   3.245    (* invokation *)
   3.246 @@ -1136,14 +1136,14 @@
   3.247  apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def)
   3.248  
   3.249         (* var. initialization *)
   3.250 -apply (rule_tac "instrs0.0" = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
   3.251 +apply (rule_tac ?instrs0.0 = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
   3.252  apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption)
   3.253  apply (simp (no_asm_simp)) (* length pns = length pvs *)
   3.254  apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) arbitrary) *)
   3.255  
   3.256  
   3.257         (* body statement *)
   3.258 -apply (rule_tac "instrs0.0" = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl)
   3.259 +apply (rule_tac ?instrs0.0 = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl)
   3.260  apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
   3.261  apply (simp (no_asm_simp))
   3.262  apply (simp only: gh_conv)
     4.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Aug 29 13:18:45 2003 +0200
     4.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Aug 29 15:19:02 2003 +0200
     4.3 @@ -1739,14 +1739,14 @@
     4.4    apply (rule bc_mt_corresp_zero) apply (simp add: length_compTpExpr) 
     4.5    apply (simp (no_asm_simp))
     4.6  
     4.7 -apply (drule_tac "bc1.0"="[]" and "bc2.0" = "compExpr jmb expr1" 
     4.8 -  and "f1.0"=comb_nil and "f2.0" = "compTpExpr jmb G expr1" 
     4.9 +apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "compExpr jmb expr1" 
    4.10 +  and ?f1.0=comb_nil and ?f2.0 = "compTpExpr jmb G expr1" 
    4.11    in bc_mt_corresp_comb_inside)
    4.12    apply (simp (no_asm_simp))+
    4.13    apply blast
    4.14    apply (simp (no_asm_simp) add: length_compTpExpr)+
    4.15  
    4.16 -apply (drule_tac "bc2.0" = "compExpr jmb expr2" and "f2.0" = "compTpExpr jmb G expr2" 
    4.17 +apply (drule_tac ?bc2.0 = "compExpr jmb expr2" and ?f2.0 = "compTpExpr jmb G expr2" 
    4.18    in bc_mt_corresp_comb_inside)
    4.19    apply (simp (no_asm_simp))+
    4.20    apply (simp only: compTpExpr_LT_ST)
    4.21 @@ -1754,10 +1754,10 @@
    4.22    apply (simp (no_asm_simp))
    4.23    apply (simp (no_asm_simp))
    4.24  
    4.25 -apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2" 
    4.26 -    and inst = "Ifcmpeq 3" and "bc3.0" = "[LitPush (Bool False),Goto 2, LitPush (Bool True)]"
    4.27 -  and "f1.0"="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2"
    4.28 -  and "f2.0"="popST 2" and "f3.0"="pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]"
    4.29 +apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2" 
    4.30 +    and inst = "Ifcmpeq 3" and ?bc3.0 = "[LitPush (Bool False),Goto 2, LitPush (Bool True)]"
    4.31 +  and ?f1.0="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2"
    4.32 +  and ?f2.0="popST 2" and ?f3.0="pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]"
    4.33    in bc_mt_corresp_comb_wt_instr)
    4.34    apply (simp (no_asm_simp) add: length_compTpExpr)+
    4.35  
    4.36 @@ -1772,12 +1772,12 @@
    4.37    apply (case_tac Ta) apply (simp (no_asm_simp)) apply (simp (no_asm_simp))
    4.38    apply (rule contracting_popST)		(* contracting (popST 2)  *)
    4.39  
    4.40 -apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3]"
    4.41 -  and "bc2.0" = "[LitPush (Bool False)]" 
    4.42 -  and "bc3.0" = "[Goto 2, LitPush (Bool True)]" 
    4.43 -  and "f1.0" = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2"
    4.44 -  and "f2.0" = "pushST [PrimT Boolean]" 
    4.45 -  and "f3.0" = "popST (Suc 0) \<box> pushST [PrimT Boolean]"
    4.46 +apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3]"
    4.47 +  and ?bc2.0 = "[LitPush (Bool False)]" 
    4.48 +  and ?bc3.0 = "[Goto 2, LitPush (Bool True)]" 
    4.49 +  and ?f1.0 = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2"
    4.50 +  and ?f2.0 = "pushST [PrimT Boolean]" 
    4.51 +  and ?f3.0 = "popST (Suc 0) \<box> pushST [PrimT Boolean]"
    4.52    in bc_mt_corresp_comb_inside)
    4.53    apply (simp (no_asm_simp))+
    4.54    apply (simp add: compTpExpr_LT_ST_rewr popST_def)
    4.55 @@ -1787,10 +1787,10 @@
    4.56    apply (simp (no_asm_simp) add: start_sttp_resp_def)
    4.57  
    4.58  
    4.59 -apply (drule_tac "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False)]" 
    4.60 -    and inst = "Goto 2" and "bc3.0" = "[LitPush (Bool True)]"
    4.61 -  and "f1.0"="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> pushST [PrimT Boolean]"
    4.62 -  and "f2.0"="popST 1" and "f3.0"="pushST [PrimT Boolean]"
    4.63 +apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False)]" 
    4.64 +    and inst = "Goto 2" and ?bc3.0 = "[LitPush (Bool True)]"
    4.65 +  and ?f1.0="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> pushST [PrimT Boolean]"
    4.66 +  and ?f2.0="popST 1" and ?f3.0="pushST [PrimT Boolean]"
    4.67    in bc_mt_corresp_comb_wt_instr)
    4.68    apply (simp (no_asm_simp) add: length_compTpExpr)+
    4.69  
    4.70 @@ -1804,13 +1804,13 @@
    4.71    apply (rule contracting_popST)		(* contracting (popST 1) *)
    4.72  
    4.73  apply (drule_tac 
    4.74 -  "bc1.0" = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False), Goto 2]" 
    4.75 -  and "bc2.0" = "[LitPush (Bool True)]"
    4.76 -  and "bc3.0" = "[]"
    4.77 -  and "f1.0" = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> 
    4.78 +  ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False), Goto 2]" 
    4.79 +  and ?bc2.0 = "[LitPush (Bool True)]"
    4.80 +  and ?bc3.0 = "[]"
    4.81 +  and ?f1.0 = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> 
    4.82                  pushST [PrimT Boolean] \<box> popST (Suc 0)"
    4.83 -  and "f2.0" = "pushST [PrimT Boolean]"
    4.84 -  and "f3.0" = "comb_nil" 
    4.85 +  and ?f2.0 = "pushST [PrimT Boolean]"
    4.86 +  and ?f3.0 = "comb_nil" 
    4.87    in bc_mt_corresp_comb_inside)
    4.88    apply (simp (no_asm_simp))+
    4.89    apply (simp add: compTpExpr_LT_ST_rewr popST_def) 
    4.90 @@ -1859,8 +1859,8 @@
    4.91  apply clarify
    4.92  apply (simp (no_asm_use))
    4.93  apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast)
    4.94 -apply (rule_tac "bc1.0"="[Dup]" and "bc2.0"="[Store (index (pns, lvars, blk, res) vname)]" 
    4.95 -       and "f1.0"="dupST" and "f2.0"="popST (Suc 0)"
    4.96 +apply (rule_tac ?bc1.0="[Dup]" and ?bc2.0="[Store (index (pns, lvars, blk, res) vname)]" 
    4.97 +       and ?f1.0="dupST" and ?f2.0="popST (Suc 0)"
    4.98         in bc_mt_corresp_comb) 
    4.99    apply (simp (no_asm_simp))+
   4.100    apply (rule bc_mt_corresp_Dup)
   4.101 @@ -1898,7 +1898,7 @@
   4.102    apply (simp only: compTpExpr_LT_ST)
   4.103  apply (rule bc_mt_corresp_comb, (rule HOL.refl)+) apply blast
   4.104    apply (simp only: compTpExpr_LT_ST)
   4.105 -apply (rule_tac "bc1.0"="[Dup_x1]" and "bc2.0"="[Putfield vname cname]" in bc_mt_corresp_comb) 
   4.106 +apply (rule_tac ?bc1.0="[Dup_x1]" and ?bc2.0="[Putfield vname cname]" in bc_mt_corresp_comb) 
   4.107    apply (simp (no_asm_simp))+
   4.108  apply (rule bc_mt_corresp_Dup_x1)
   4.109    apply (simp (no_asm_simp) add: dup_x1ST_def)
   4.110 @@ -2010,24 +2010,24 @@
   4.111    apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
   4.112    apply (simp (no_asm_simp))
   4.113  
   4.114 -apply (drule_tac "bc1.0"="[]" and "bc2.0" = "[LitPush (Bool False)]" 
   4.115 -  and "bc3.0"="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
   4.116 +apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "[LitPush (Bool False)]" 
   4.117 +  and ?bc3.0="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
   4.118              compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
   4.119              compStmt jmb stmt2" 
   4.120 -  and "f1.0"=comb_nil and "f2.0" = "pushST [PrimT Boolean]" 
   4.121 -  and "f3.0"="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt1 \<box>
   4.122 +  and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]" 
   4.123 +  and ?f3.0="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt1 \<box>
   4.124              nochangeST \<box> compTpStmt jmb G stmt2"
   4.125    in bc_mt_corresp_comb_inside)
   4.126    apply (simp (no_asm_simp))+
   4.127    apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
   4.128    apply (simp (no_asm_simp) add: start_sttp_resp_def)+
   4.129  
   4.130 -apply (drule_tac "bc1.0"="[LitPush (Bool False)]" and "bc2.0" = "compExpr jmb expr"
   4.131 -  and "bc3.0"="Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
   4.132 +apply (drule_tac ?bc1.0="[LitPush (Bool False)]" and ?bc2.0 = "compExpr jmb expr"
   4.133 +  and ?bc3.0="Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
   4.134              compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
   4.135              compStmt jmb stmt2" 
   4.136 -  and "f1.0"="pushST [PrimT Boolean]" and "f2.0" = "compTpExpr jmb G expr"
   4.137 -  and "f3.0"="popST 2 \<box> compTpStmt jmb G stmt1 \<box>
   4.138 +  and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr"
   4.139 +  and ?f3.0="popST 2 \<box> compTpStmt jmb G stmt1 \<box>
   4.140              nochangeST \<box> compTpStmt jmb G stmt2"
   4.141    in bc_mt_corresp_comb_inside)
   4.142    apply (simp (no_asm_simp))+
   4.143 @@ -2036,12 +2036,12 @@
   4.144        apply (simp (no_asm_simp))+
   4.145  
   4.146  
   4.147 -apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr" 
   4.148 +apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr" 
   4.149      and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt1)))" 
   4.150 -  and "bc3.0" = "compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
   4.151 +  and ?bc3.0 = "compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
   4.152              compStmt jmb stmt2"
   4.153 -  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and "f2.0" = "popST 2"
   4.154 -  and "f3.0"="compTpStmt jmb G stmt1 \<box> nochangeST \<box> compTpStmt jmb G stmt2"
   4.155 +  and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and ?f2.0 = "popST 2"
   4.156 +  and ?f3.0="compTpStmt jmb G stmt1 \<box> nochangeST \<box> compTpStmt jmb G stmt2"
   4.157    in bc_mt_corresp_comb_wt_instr)
   4.158    apply (simp (no_asm_simp) add: length_compTpExpr)+
   4.159    apply (simp (no_asm_simp) add: start_sttp_resp_comb)
   4.160 @@ -2079,13 +2079,13 @@
   4.161    apply (rule contracting_popST)
   4.162  
   4.163  apply (drule_tac 
   4.164 -  "bc1.0"="[LitPush (Bool False)] @ compExpr jmb expr @ 
   4.165 +  ?bc1.0="[LitPush (Bool False)] @ compExpr jmb expr @ 
   4.166             [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] " 
   4.167 -  and "bc2.0" = "compStmt jmb stmt1"
   4.168 -  and "bc3.0"="Goto (1 + int (length (compStmt jmb stmt2))) # compStmt jmb stmt2"
   4.169 -  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" 
   4.170 -  and "f2.0" = "compTpStmt jmb G stmt1"
   4.171 -  and "f3.0"="nochangeST \<box> compTpStmt jmb G stmt2"
   4.172 +  and ?bc2.0 = "compStmt jmb stmt1"
   4.173 +  and ?bc3.0="Goto (1 + int (length (compStmt jmb stmt2))) # compStmt jmb stmt2"
   4.174 +  and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" 
   4.175 +  and ?f2.0 = "compTpStmt jmb G stmt1"
   4.176 +  and ?f3.0="nochangeST \<box> compTpStmt jmb G stmt2"
   4.177    in bc_mt_corresp_comb_inside)
   4.178    apply (simp (no_asm_simp))+
   4.179    apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
   4.180 @@ -2094,13 +2094,13 @@
   4.181    apply (simp (no_asm_simp) add: length_compTpExpr)+
   4.182  
   4.183  
   4.184 -apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ compStmt jmb stmt1" 
   4.185 +apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ compStmt jmb stmt1" 
   4.186      and inst = "Goto (1 + int (length (compStmt jmb stmt2)))"
   4.187 -  and "bc3.0" = "compStmt jmb stmt2"
   4.188 -  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
   4.189 +  and ?bc3.0 = "compStmt jmb stmt2"
   4.190 +  and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
   4.191                compTpStmt jmb G stmt1" 
   4.192 -  and "f2.0" = "nochangeST"
   4.193 -  and "f3.0"="compTpStmt jmb G stmt2"
   4.194 +  and ?f2.0 = "nochangeST"
   4.195 +  and ?f3.0="compTpStmt jmb G stmt2"
   4.196    in bc_mt_corresp_comb_wt_instr)
   4.197    apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
   4.198    apply (intro strip)
   4.199 @@ -2120,15 +2120,15 @@
   4.200  
   4.201  
   4.202  apply (drule_tac 
   4.203 -  "bc1.0"= "[LitPush (Bool False)] @ compExpr jmb expr @ 
   4.204 +  ?bc1.0= "[LitPush (Bool False)] @ compExpr jmb expr @ 
   4.205              [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ 
   4.206              compStmt jmb stmt1 @ [Goto (1 + int (length (compStmt jmb stmt2)))]"
   4.207 -  and "bc2.0" = "compStmt jmb stmt2"
   4.208 -  and "bc3.0"="[]"
   4.209 -  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
   4.210 +  and ?bc2.0 = "compStmt jmb stmt2"
   4.211 +  and ?bc3.0="[]"
   4.212 +  and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
   4.213                compTpStmt jmb G stmt1 \<box> nochangeST"
   4.214 -  and "f2.0" = "compTpStmt jmb G stmt2"
   4.215 -  and "f3.0"="comb_nil"
   4.216 +  and ?f2.0 = "compTpStmt jmb G stmt2"
   4.217 +  and ?f3.0="comb_nil"
   4.218    in bc_mt_corresp_comb_inside)
   4.219    apply (simp (no_asm_simp))+
   4.220    apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def compTpExpr_LT_ST)
   4.221 @@ -2152,23 +2152,23 @@
   4.222    apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
   4.223    apply (simp (no_asm_simp))
   4.224  
   4.225 -apply (drule_tac "bc1.0"="[]" and "bc2.0" = "[LitPush (Bool False)]" 
   4.226 -  and "bc3.0"="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
   4.227 +apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "[LitPush (Bool False)]" 
   4.228 +  and ?bc3.0="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
   4.229              compStmt jmb stmt @ 
   4.230              [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" 
   4.231 -  and "f1.0"=comb_nil and "f2.0" = "pushST [PrimT Boolean]" 
   4.232 -  and "f3.0"="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
   4.233 +  and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]" 
   4.234 +  and ?f3.0="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
   4.235    in bc_mt_corresp_comb_inside)
   4.236    apply (simp (no_asm_simp))+
   4.237    apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
   4.238    apply (simp (no_asm_simp) add: start_sttp_resp_def)+
   4.239  
   4.240 -apply (drule_tac "bc1.0"="[LitPush (Bool False)]" and "bc2.0" = "compExpr jmb expr"
   4.241 -  and "bc3.0"="Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
   4.242 +apply (drule_tac ?bc1.0="[LitPush (Bool False)]" and ?bc2.0 = "compExpr jmb expr"
   4.243 +  and ?bc3.0="Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
   4.244              compStmt jmb stmt @ 
   4.245              [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" 
   4.246 -  and "f1.0"="pushST [PrimT Boolean]" and "f2.0" = "compTpExpr jmb G expr"
   4.247 -  and "f3.0"="popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
   4.248 +  and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr"
   4.249 +  and ?f3.0="popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
   4.250    in bc_mt_corresp_comb_inside)
   4.251    apply (simp (no_asm_simp))+
   4.252    apply (simp (no_asm_simp)  add: pushST_def)
   4.253 @@ -2176,12 +2176,12 @@
   4.254        apply (simp (no_asm_simp))+
   4.255  
   4.256  
   4.257 -apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr" 
   4.258 +apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr" 
   4.259      and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt)))" 
   4.260 -  and "bc3.0" = "compStmt jmb stmt @ 
   4.261 +  and ?bc3.0 = "compStmt jmb stmt @ 
   4.262         [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
   4.263 -  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and "f2.0" = "popST 2"
   4.264 -  and "f3.0"="compTpStmt jmb G stmt \<box> nochangeST"
   4.265 +  and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and ?f2.0 = "popST 2"
   4.266 +  and ?f3.0="compTpStmt jmb G stmt \<box> nochangeST"
   4.267    in bc_mt_corresp_comb_wt_instr)
   4.268    apply (simp (no_asm_simp) add: length_compTpExpr)+
   4.269    apply (simp (no_asm_simp) add: start_sttp_resp_comb)
   4.270 @@ -2219,13 +2219,13 @@
   4.271    apply (rule contracting_popST)
   4.272  
   4.273  apply (drule_tac 
   4.274 -  "bc1.0"="[LitPush (Bool False)] @ compExpr jmb expr @ 
   4.275 +  ?bc1.0="[LitPush (Bool False)] @ compExpr jmb expr @ 
   4.276             [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] " 
   4.277 -  and "bc2.0" = "compStmt jmb stmt"
   4.278 -  and "bc3.0"="[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
   4.279 -  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" 
   4.280 -  and "f2.0" = "compTpStmt jmb G stmt"
   4.281 -  and "f3.0"="nochangeST"
   4.282 +  and ?bc2.0 = "compStmt jmb stmt"
   4.283 +  and ?bc3.0="[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
   4.284 +  and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" 
   4.285 +  and ?f2.0 = "compTpStmt jmb G stmt"
   4.286 +  and ?f3.0="nochangeST"
   4.287    in bc_mt_corresp_comb_inside)
   4.288    apply (simp (no_asm_simp))+
   4.289    apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
   4.290 @@ -2234,13 +2234,13 @@
   4.291    apply (simp (no_asm_simp) add: length_compTpExpr)+
   4.292  
   4.293  
   4.294 -apply (drule_tac "bc1.0" = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] @ compStmt jmb stmt" 
   4.295 +apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] @ compStmt jmb stmt" 
   4.296      and inst = "Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))"
   4.297 -  and "bc3.0" = "[]"
   4.298 -  and "f1.0"="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
   4.299 +  and ?bc3.0 = "[]"
   4.300 +  and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
   4.301                compTpStmt jmb G stmt" 
   4.302 -  and "f2.0" = "nochangeST"
   4.303 -  and "f3.0"="comb_nil"
   4.304 +  and ?f2.0 = "nochangeST"
   4.305 +  and ?f3.0="comb_nil"
   4.306    in bc_mt_corresp_comb_wt_instr)
   4.307    apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+ 
   4.308    apply (intro strip)
   4.309 @@ -2277,7 +2277,7 @@
   4.310    is_type G ty \<rbrakk>
   4.311    \<Longrightarrow> bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)"
   4.312  apply (simp add: compInit_def compTpInit_def split_beta)
   4.313 -apply (rule_tac "bc1.0"="[load_default_val ty]" and "bc2.0"="[Store (index jmb vn)]" 
   4.314 +apply (rule_tac ?bc1.0="[load_default_val ty]" and ?bc2.0="[Store (index jmb vn)]" 
   4.315    in bc_mt_corresp_comb) 
   4.316    apply simp+
   4.317    apply (simp add: load_default_val_def)
   4.318 @@ -2311,7 +2311,7 @@
   4.319  apply (drule_tac x="lvars_pre @ [a]" in spec)
   4.320  apply (drule_tac x="lvars0" in spec)
   4.321  apply (simp (no_asm_simp) add: compInitLvars_def)
   4.322 -apply (rule_tac "bc1.0"="compInit jmb a" and "bc2.0"="compInitLvars jmb list"
   4.323 +apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb list"
   4.324    in bc_mt_corresp_comb)
   4.325  apply (simp (no_asm_simp) add: compInitLvars_def)+
   4.326  
     5.1 --- a/src/HOL/MicroJava/J/Conform.thy	Fri Aug 29 13:18:45 2003 +0200
     5.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Fri Aug 29 15:19:02 2003 +0200
     5.3 @@ -120,9 +120,9 @@
     5.4  lemma defval_conf [rule_format (no_asm)]: 
     5.5    "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
     5.6  apply (unfold conf_def)
     5.7 -apply (rule_tac "y" = "T" in ty.exhaust)
     5.8 +apply (rule_tac y = "T" in ty.exhaust)
     5.9  apply  (erule ssubst)
    5.10 -apply  (rule_tac "y" = "prim_ty" in prim_ty.exhaust)
    5.11 +apply  (rule_tac y = "prim_ty" in prim_ty.exhaust)
    5.12  apply    (auto simp add: widen.null)
    5.13  done
    5.14  
    5.15 @@ -178,7 +178,7 @@
    5.16  lemma non_np_objD' [rule_format (no_asm)]: 
    5.17    "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t --> 
    5.18    (\<exists>a C fs. a' = Addr a \<and>  h a = Some (C,fs) \<and>  G\<turnstile>Class C\<preceq>RefT t)"
    5.19 -apply(rule_tac "y" = "t" in ref_ty.exhaust)
    5.20 +apply(rule_tac y = "t" in ref_ty.exhaust)
    5.21   apply (fast dest: conf_NullTD)
    5.22  apply (fast dest: non_np_objD)
    5.23  done
     6.1 --- a/src/HOL/MicroJava/J/State.thy	Fri Aug 29 13:18:45 2003 +0200
     6.2 +++ b/src/HOL/MicroJava/J/State.thy	Fri Aug 29 15:19:02 2003 +0200
     6.3 @@ -73,7 +73,7 @@
     6.4  apply(simp add: Pair_fst_snd_eq Eps_split)
     6.5  apply(rule someI)
     6.6  apply(rule disjI2)
     6.7 -apply(rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
     6.8 +apply(rule_tac r = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
     6.9  apply auto
    6.10  done
    6.11  
     7.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Fri Aug 29 13:18:45 2003 +0200
     7.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Fri Aug 29 15:19:02 2003 +0200
     7.3 @@ -547,7 +547,7 @@
     7.4    apply (assumption)
     7.5   apply (assumption)
     7.6  apply (clarify)
     7.7 -apply (erule_tac "x" = "Da" in allE)
     7.8 +apply (erule_tac x = "Da" in allE)
     7.9  apply (clarsimp)
    7.10   apply (simp add: map_of_map)
    7.11   apply (clarify)
    7.12 @@ -571,7 +571,7 @@
    7.13    apply (assumption)
    7.14   apply (assumption)
    7.15  apply (clarify)
    7.16 -apply (erule_tac "x" = "Da" in allE)
    7.17 +apply (erule_tac x = "Da" in allE)
    7.18  apply (clarsimp)
    7.19   apply (simp add: map_of_map)
    7.20   apply (clarify)
     8.1 --- a/src/HOL/NanoJava/Equivalence.thy	Fri Aug 29 13:18:45 2003 +0200
     8.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Fri Aug 29 15:19:02 2003 +0200
     8.3 @@ -83,7 +83,7 @@
     8.4  lemma Loop_sound_lemma [rule_format (no_asm)]: 
     8.5  "\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<x> \<noteq> Null \<longrightarrow> P t \<Longrightarrow> 
     8.6    (s -c0-n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<x> = Null)"
     8.7 -apply (rule_tac "P2.1"="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
     8.8 +apply (rule_tac ?P2.1="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
     8.9  apply clarsimp+
    8.10  done
    8.11  
     9.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Fri Aug 29 13:18:45 2003 +0200
     9.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Fri Aug 29 15:19:02 2003 +0200
     9.3 @@ -145,7 +145,7 @@
     9.4     apply (rule_tac [2] m = m in zcong_zless_imp_eq)
     9.5         apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
     9.6  	 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
     9.7 -  apply (rule_tac "x" = b in exI, safe)
     9.8 +  apply (rule_tac x = b in exI, safe)
     9.9    apply (rule Bnor_mem_if)
    9.10      apply (case_tac [2] "b = 0")
    9.11       apply (auto intro: order_less_le [THEN iffD2])
    10.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Fri Aug 29 13:18:45 2003 +0200
    10.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Fri Aug 29 15:19:02 2003 +0200
    10.3 @@ -400,7 +400,7 @@
    10.4  lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
    10.5    apply (unfold zcong_def)
    10.6    apply (rule_tac t = "a - b" in ssubst)
    10.7 -  apply (rule_tac "m" = m in zcong_zmod_aux)
    10.8 +  apply (rule_tac m = m in zcong_zmod_aux)
    10.9    apply (rule trans)
   10.10     apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
   10.11    apply (simp add: zadd_commute)
    11.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Aug 29 13:18:45 2003 +0200
    11.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Aug 29 15:19:02 2003 +0200
    11.3 @@ -189,7 +189,7 @@
    11.4  
    11.5  in
    11.6  
    11.7 -fun gen_induct_tac (varss, opt_rule) i state =
    11.8 +fun gen_induct_tac inst_tac (varss, opt_rule) i state =
    11.9    let
   11.10      val (_, _, Bi, _) = Thm.dest_state (state, i);
   11.11      val {sign, ...} = Thm.rep_thm state;
   11.12 @@ -203,33 +203,39 @@
   11.13      val concls = HOLogic.dest_concls (Thm.concl_of rule);
   11.14      val insts = flat (map prep_inst (concls ~~ varss)) handle LIST _ =>
   11.15        error (rule_name ^ " has different numbers of variables");
   11.16 -  in occs_in_prems (Tactic.res_inst_tac insts rule) (map #2 insts) i state end;
   11.17 +  in occs_in_prems (inst_tac insts rule) (map #2 insts) i state end;
   11.18  
   11.19 -fun induct_tac s = gen_induct_tac (map (Library.single o Some) (Syntax.read_idents s), None);
   11.20 +fun induct_tac s =
   11.21 +  gen_induct_tac Tactic.res_inst_tac
   11.22 +    (map (Library.single o Some) (Syntax.read_idents s), None);
   11.23  
   11.24  fun induct_thm_tac th s =
   11.25 -  gen_induct_tac ([map Some (Syntax.read_idents s)], Some th);
   11.26 +  gen_induct_tac Tactic.res_inst_tac
   11.27 +    ([map Some (Syntax.read_idents s)], Some th);
   11.28  
   11.29  end;
   11.30  
   11.31  
   11.32  (* generic case tactic for datatypes *)
   11.33  
   11.34 -fun case_inst_tac t rule i state =
   11.35 +fun case_inst_tac inst_tac t rule i state =
   11.36    let
   11.37      val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
   11.38        (hd (Logic.strip_assums_hyp (hd (Thm.prems_of rule))));
   11.39      val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)));
   11.40 -  in Tactic.res_inst_tac [(exh_vname, t)] rule i state end;
   11.41 +  in inst_tac [(exh_vname, t)] rule i state end;
   11.42  
   11.43 -fun gen_case_tac (t, Some rule) i state = case_inst_tac t rule i state
   11.44 -  | gen_case_tac (t, None) i state =
   11.45 +fun gen_case_tac inst_tac (t, Some rule) i state =
   11.46 +      case_inst_tac inst_tac t rule i state
   11.47 +  | gen_case_tac inst_tac (t, None) i state =
   11.48        let val tn = infer_tname state i t in
   11.49 -        if tn = HOLogic.boolN then Tactic.res_inst_tac [("P", t)] case_split_thm i state
   11.50 -        else case_inst_tac t (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn)) i state
   11.51 +        if tn = HOLogic.boolN then inst_tac [("P", t)] case_split_thm i state
   11.52 +        else case_inst_tac inst_tac t
   11.53 +               (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn))
   11.54 +               i state
   11.55        end;
   11.56  
   11.57 -fun case_tac t = gen_case_tac (t, None);
   11.58 +fun case_tac t = gen_case_tac Tactic.res_inst_tac (t, None);
   11.59  
   11.60  
   11.61  
   11.62 @@ -242,13 +248,23 @@
   11.63  
   11.64  val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
   11.65  
   11.66 +fun mk_ixn (vars, s) = (fst (Term.dest_Var (Syntax.read_var ("?" ^ vars))), s)
   11.67 +  handle _ => error (vars ^ " not a variable name");
   11.68 +fun inst_tac ctxt sinsts =
   11.69 +  Method.bires_inst_tac false ctxt (map mk_ixn sinsts);
   11.70 +
   11.71 +fun induct_meth ctxt (varss, opt_rule) =
   11.72 +  gen_induct_tac (inst_tac ctxt) (varss, opt_rule);
   11.73 +fun case_meth ctxt (varss, opt_rule) =
   11.74 +  gen_case_tac (inst_tac ctxt) (varss, opt_rule);
   11.75 +
   11.76  in
   11.77  
   11.78  val tactic_emulations =
   11.79 - [("induct_tac", Method.goal_args' (varss -- opt_rule) gen_induct_tac,
   11.80 -    "induct_tac emulation (dynamic instantiation!)"),
   11.81 -  ("case_tac", Method.goal_args' (Scan.lift Args.name -- opt_rule) gen_case_tac,
   11.82 -    "case_tac emulation (dynamic instantiation!)")];
   11.83 + [("induct_tac", Method.goal_args_ctxt' (varss -- opt_rule) induct_meth,
   11.84 +    "induct_tac emulation (dynamic instantiation)"),
   11.85 +  ("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) case_meth,
   11.86 +    "case_tac emulation (dynamic instantiation)")];
   11.87  
   11.88  end;
   11.89  
    12.1 --- a/src/Pure/Isar/args.ML	Fri Aug 29 13:18:45 2003 +0200
    12.2 +++ b/src/Pure/Isar/args.ML	Fri Aug 29 15:19:02 2003 +0200
    12.3 @@ -142,14 +142,23 @@
    12.4    Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
    12.5  
    12.6  fun kind f = Scan.one (K true) :--
    12.7 -  (fn Arg (Ident, (x, _)) =>
    12.8 +  ((fn Arg (Ident, (x, _)) =>
    12.9      (case f x of Some y => Scan.succeed y | _ => Scan.fail)
   12.10 -  | _ => Scan.fail) >> #2;
   12.11 +  | _ => Scan.fail)
   12.12 +(* o (fn (t as Arg (i, (s, _))) =>
   12.13 +  (warning (
   12.14 +    (case i of Ident => "Ident: " | String => "String: "
   12.15 +            | Keyword => "Keyword: " | EOF => "EOF: ")
   12.16 +    ^ s); t)) *) ) >> #2;
   12.17  
   12.18  val nat = kind Syntax.read_nat;
   12.19  val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
   12.20 -val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
   12.21  
   12.22 +(* Read variable name.  Leading `?' may be omitted if name contains no dot. *)
   12.23 +val var = kind (apsome #1 o
   12.24 +      (fn s => (Some (Term.dest_Var (Syntax.read_var s)))
   12.25 +         handle _ => (Some (Term.dest_Var (Syntax.read_var ("?" ^ s))))
   12.26 +         handle _ => None));
   12.27  
   12.28  (* enumerations *)
   12.29  
    13.1 --- a/src/Pure/Isar/method.ML	Fri Aug 29 13:18:45 2003 +0200
    13.2 +++ b/src/Pure/Isar/method.ML	Fri Aug 29 15:19:02 2003 +0200
    13.3 @@ -45,7 +45,7 @@
    13.4    val frule: int -> thm list -> Proof.method
    13.5    val this: Proof.method
    13.6    val assumption: Proof.context -> Proof.method
    13.7 -  val impose_hyps_tac: Proof.context -> tactic
    13.8 +  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list -> thm -> int -> tactic
    13.9    val set_tactic: (Proof.context -> thm list -> tactic) -> unit
   13.10    val tactic: string -> Proof.context -> Proof.method
   13.11    exception METHOD_FAIL of (string * Position.T) * exn
   13.12 @@ -111,6 +111,10 @@
   13.13      -> Args.src -> Proof.context -> Proof.method
   13.14    val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
   13.15      -> ('a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   13.16 +  val goal_args_ctxt: (Args.T list -> 'a * Args.T list) -> (Proof.context -> 'a -> int -> tactic)
   13.17 +    -> Args.src -> Proof.context -> Proof.method
   13.18 +  val goal_args_ctxt': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
   13.19 +    -> (Proof.context -> 'a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   13.20    val setup: (theory -> theory) list
   13.21  end;
   13.22  
   13.23 @@ -322,23 +326,149 @@
   13.24  
   13.25  (* res_inst_tac etc. *)
   13.26  
   13.27 -(*robustify instantiation by imposing (part of) the present static context*)
   13.28 -val impose_hyps_tac =
   13.29 -  PRIMITIVE o Drule.impose_hyps o flat o map #1 o ProofContext.assumptions_of;
   13.30 +(* Reimplemented to support both static (Isar) and dynamic (proof state)
   13.31 +   context.  By Clemens Ballarin. *)
   13.32  
   13.33 -(*Note: insts refer to the implicit (!!) goal context; use at your own risk*)
   13.34 -fun gen_res_inst _ tac _ (quant, ([], thms)) =
   13.35 -      METHOD (fn facts => (quant (insert_tac facts THEN' tac thms)))
   13.36 -  | gen_res_inst tac _ ctxt (quant, (insts, [thm])) =
   13.37 -      METHOD (fn facts => (impose_hyps_tac ctxt THEN quant (insert_tac facts THEN' tac insts thm)))
   13.38 -  | gen_res_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
   13.39 +fun bires_inst_tac bires_flag ctxt insts thm =
   13.40 +  let
   13.41 +    val sign = ProofContext.sign_of ctxt;
   13.42 +    (* Separate type and term insts *)
   13.43 +    fun has_type_var ((x, _), _) = (case Symbol.explode x of
   13.44 +          "'"::cs => true | cs => false);
   13.45 +    val Tinsts = filter has_type_var insts;
   13.46 +    val tinsts = filter_out has_type_var insts;
   13.47 +    (* Tactic *)
   13.48 +    fun tac i st =
   13.49 +      let
   13.50 +        (* Preprocess state: extract environment information:
   13.51 +           - variables and their types
   13.52 +           - type variables and their sorts
   13.53 +           - parameters and their types *)
   13.54 +        val (types, sorts) = types_sorts st;
   13.55 +    (* Process type insts: Tinsts_env *)
   13.56 +    fun absent xi = error
   13.57 +	  ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
   13.58 +    val (rtypes, rsorts) = types_sorts thm;
   13.59 +    fun readT (xi, s) =
   13.60 +        let val S = case rsorts xi of Some S => S | None => absent xi;
   13.61 +            val T = Sign.read_typ (sign, sorts) s;
   13.62 +        in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T)
   13.63 +           else error
   13.64 +             ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
   13.65 +        end;
   13.66 +    val Tinsts_env = map readT Tinsts;
   13.67 +    (* Preprocess rule: extract vars and their types, apply Tinsts *)
   13.68 +    fun get_typ xi =
   13.69 +      (case rtypes xi of
   13.70 +           Some T => typ_subst_TVars Tinsts_env T
   13.71 +         | None => absent xi);
   13.72 +    val (xis, ss) = Library.split_list tinsts;
   13.73 +    val Ts = map get_typ xis;
   13.74 +	val (_, _, Bi, _) = dest_state(st,i)
   13.75 +	val params = Logic.strip_params Bi
   13.76 +			     (* params of subgoal i as string typ pairs *)
   13.77 +	val params = rev(Term.rename_wrt_term Bi params)
   13.78 +						 (* as they are printed *)
   13.79 +        fun types' (a, ~1) = (case assoc (params, a) of
   13.80 +                None => types (a, ~1)
   13.81 +              | some => some)
   13.82 +          | types' xi = types xi;
   13.83 +        val used = add_term_tvarnames
   13.84 +                  (prop_of st $ prop_of thm,[])
   13.85 +	val (ts, envT) =
   13.86 +	  ProofContext.read_termTs_env (types', sorts, used) ctxt (ss ~~ Ts);
   13.87 +	val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env);
   13.88 +	val cenv =
   13.89 +	  map
   13.90 +	    (fn (xi, t) =>
   13.91 +	      pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
   13.92 +	    (gen_distinct
   13.93 +	      (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
   13.94 +	      (xis ~~ ts));
   13.95 +	(* Lift and instantiate rule *)
   13.96 +	val {maxidx, ...} = rep_thm st;
   13.97 +	val paramTs = map #2 params
   13.98 +	and inc = maxidx+1
   13.99 +	fun liftvar (Var ((a,j), T)) =
  13.100 +	      Var((a, j+inc), paramTs ---> incr_tvar inc T)
  13.101 +	  | liftvar t = raise TERM("Variable expected", [t]);
  13.102 +	fun liftterm t = list_abs_free
  13.103 +	      (params, Logic.incr_indexes(paramTs,inc) t)
  13.104 +	fun liftpair (cv,ct) =
  13.105 +	      (cterm_fun liftvar cv, cterm_fun liftterm ct)
  13.106 +	fun lifttvar((a,i),ctyp) =
  13.107 +	    let val {T,sign} = rep_ctyp ctyp
  13.108 +	    in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
  13.109 +	val rule = Drule.instantiate
  13.110 +	      (map lifttvar cenvT, map liftpair cenv)
  13.111 +	      (lift_rule (st, i) thm)
  13.112 +      in
  13.113 +	if i > nprems_of st then no_tac st
  13.114 +	else st |>
  13.115 +	  compose_tac (bires_flag, rule, nprems_of thm) i
  13.116 +      end
  13.117 +	   handle TERM (msg,_)   => (warning msg; no_tac st)
  13.118 +		| THM  (msg,_,_) => (warning msg; no_tac st);
  13.119 +  in
  13.120 +    tac
  13.121 +  end;
  13.122  
  13.123 -val res_inst = gen_res_inst Tactic.res_inst_tac Tactic.resolve_tac;
  13.124 -val eres_inst = gen_res_inst Tactic.eres_inst_tac Tactic.eresolve_tac;
  13.125 -val dres_inst = gen_res_inst Tactic.dres_inst_tac Tactic.dresolve_tac;
  13.126 -val forw_inst = gen_res_inst Tactic.forw_inst_tac Tactic.forward_tac;
  13.127 -val cut_inst = gen_res_inst Tactic.cut_inst_tac Tactic.cut_rules_tac;
  13.128 +fun gen_inst _ tac _ (quant, ([], thms)) =
  13.129 +      METHOD (fn facts => quant (insert_tac facts THEN' tac thms))
  13.130 +  | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
  13.131 +      METHOD (fn facts =>
  13.132 +        quant (insert_tac facts THEN' inst_tac ctxt insts thm))
  13.133 +  | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
  13.134 +      
  13.135 +val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
  13.136 +
  13.137 +val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac;
  13.138 +
  13.139 +(* Preserve Var indexes of rl; increment revcut_rl instead.
  13.140 +   Copied from tactic.ML *)
  13.141 +fun make_elim_preserve rl =
  13.142 +  let val {maxidx,...} = rep_thm rl
  13.143 +      fun cvar xi = cterm_of (Theory.sign_of ProtoPure.thy) (Var(xi,propT));
  13.144 +      val revcut_rl' =
  13.145 +          instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
  13.146 +                             (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
  13.147 +      val arg = (false, rl, nprems_of rl)
  13.148 +      val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
  13.149 +  in  th  end
  13.150 +  handle Bind => raise THM("make_elim_preserve", 1, [rl]);
  13.151  
  13.152 +val cut_inst_meth =
  13.153 +  gen_inst
  13.154 +    (fn ctxt => fn insts => fn thm =>
  13.155 +       bires_inst_tac false ctxt insts (make_elim_preserve thm))
  13.156 +    Tactic.cut_rules_tac;
  13.157 +
  13.158 +val dres_inst_meth =
  13.159 +  gen_inst
  13.160 +    (fn ctxt => fn insts => fn rule =>
  13.161 +       bires_inst_tac true ctxt insts (make_elim_preserve rule))
  13.162 +    Tactic.dresolve_tac;
  13.163 +
  13.164 +val forw_inst_meth =
  13.165 +  gen_inst
  13.166 +    (fn ctxt => fn insts => fn rule =>
  13.167 +       bires_inst_tac false ctxt insts (make_elim_preserve rule) THEN'
  13.168 +       assume_tac)
  13.169 +    Tactic.forward_tac;
  13.170 +
  13.171 +fun subgoal_tac ctxt sprop =
  13.172 +  DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl THEN'
  13.173 +  SUBGOAL (fn (prop, _) =>
  13.174 +    let val concl' = Logic.strip_assums_concl prop in
  13.175 +      if null (term_tvars concl') then ()
  13.176 +      else warning "Type variables in new subgoal: add a type constraint?";
  13.177 +      all_tac
  13.178 +  end);
  13.179 +
  13.180 +fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
  13.181 +
  13.182 +fun thin_tac ctxt s =
  13.183 +  bires_inst_tac true ctxt [(("V", 0), s)] thin_rl;
  13.184  
  13.185  (* simple Prolog interpreter *)
  13.186  
  13.187 @@ -536,13 +666,23 @@
  13.188  
  13.189  fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
  13.190  
  13.191 +val insts_var =
  13.192 +  Scan.optional
  13.193 +    (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
  13.194 +      Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss;
  13.195 +
  13.196 +fun inst_args_var f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
  13.197  
  13.198  fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
  13.199 -  (fn (quant, s) => SIMPLE_METHOD' quant (K (impose_hyps_tac ctxt) THEN' tac s))) src ctxt);
  13.200 +  (fn (quant, s) => SIMPLE_METHOD' quant ( (*K (impose_hyps_tac ctxt) THEN' *) tac s))) src ctxt);
  13.201  
  13.202  fun goal_args args tac = goal_args' (Scan.lift args) tac;
  13.203  
  13.204 +fun goal_args_ctxt' args tac src ctxt =
  13.205 +  #2 (syntax (Args.goal_spec HEADGOAL -- args >>
  13.206 +  (fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt);
  13.207  
  13.208 +fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
  13.209  
  13.210  (** method text **)
  13.211  
  13.212 @@ -629,8 +769,8 @@
  13.213  
  13.214  (* misc tactic emulations *)
  13.215  
  13.216 -val subgoal_meth = goal_args (Scan.repeat1 Args.name) Tactic.subgoals_tac;
  13.217 -val thin_meth = goal_args Args.name Tactic.thin_tac;
  13.218 +val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac;
  13.219 +val thin_meth = goal_args_ctxt Args.name thin_tac;
  13.220  val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac;
  13.221  val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac;
  13.222  
  13.223 @@ -655,14 +795,14 @@
  13.224    ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
  13.225    ("this", no_args this, "apply current facts as rules"),
  13.226    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
  13.227 -  ("rule_tac", inst_args res_inst, "apply rule (dynamic instantiation!)"),
  13.228 -  ("erule_tac", inst_args eres_inst, "apply rule in elimination manner (dynamic instantiation!)"),
  13.229 -  ("drule_tac", inst_args dres_inst, "apply rule in destruct manner (dynamic instantiation!)"),
  13.230 -  ("frule_tac", inst_args forw_inst, "apply rule in forward manner (dynamic instantiation!)"),
  13.231 -  ("cut_tac", inst_args cut_inst, "cut rule (dynamic instantiation!)"),
  13.232 -  ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation!)"),
  13.233 -  ("thin_tac", thin_meth, "remove premise (dynamic instantiation!)"),
  13.234 -  ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation!)"),
  13.235 +  ("rule_tac", inst_args_var res_inst_meth, "apply rule (dynamic instantiation)"),
  13.236 +  ("erule_tac", inst_args_var eres_inst_meth, "apply rule in elimination manner (dynamic instantiation)"),
  13.237 +  ("drule_tac", inst_args_var dres_inst_meth, "apply rule in destruct manner (dynamic instantiation)"),
  13.238 +  ("frule_tac", inst_args_var forw_inst_meth, "apply rule in forward manner (dynamic instantiation)"),
  13.239 +  ("cut_tac", inst_args_var cut_inst_meth, "cut rule (dynamic instantiation)"),
  13.240 +  ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation)"),
  13.241 +  ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"),
  13.242 +  ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"),
  13.243    ("rotate_tac", rotate_meth, "rotate assumptions of goal"),
  13.244    ("prolog", thms_args prolog, "simple prolog interpreter"),
  13.245    ("tactic", simple_args Args.name tactic, "ML tactic as proof method")];
    14.1 --- a/src/Pure/Isar/proof_context.ML	Fri Aug 29 13:18:45 2003 +0200
    14.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Aug 29 15:19:02 2003 +0200
    14.3 @@ -30,6 +30,7 @@
    14.4    val get_skolem: context -> string -> string
    14.5    val extern_skolem: context -> term -> term
    14.6    val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
    14.7 +  val read_termTs_env: (indexname -> typ option) * (indexname -> sort option) * string list -> context -> (string * typ) list -> term list * (indexname * typ) list
    14.8    val read_term: context -> string -> term
    14.9    val read_prop: context -> string -> term
   14.10    val read_prop_schematic: context -> string -> term
   14.11 @@ -440,12 +441,15 @@
   14.12      raise CONTEXT ("Illegal reference to internal variable: " ^ quote x, ctxt)
   14.13    else x;
   14.14  
   14.15 -fun intern_skolem ctxt =
   14.16 +fun intern_skolem ctxt env =
   14.17 +(* env contains names that are not to be internalised *)
   14.18    let
   14.19      fun intern (t as Free (x, T)) =
   14.20 -          (case lookup_skolem ctxt (no_skolem false ctxt x) of
   14.21 -            Some x' => Free (x', T)
   14.22 -          | None => t)
   14.23 +          (case env (x, ~1) of
   14.24 +              Some _ => t
   14.25 +            | None => (case lookup_skolem ctxt (no_skolem false ctxt x) of
   14.26 +		  Some x' => Free (x', T)
   14.27 +		| None => t))
   14.28        | intern (t $ u) = intern t $ intern u
   14.29        | intern (Abs (x, T, t)) = Abs (x, T, intern t)
   14.30        | intern a = a;
   14.31 @@ -513,7 +517,7 @@
   14.32    let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
   14.33    in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
   14.34  
   14.35 -fun norm_term (ctxt as Context {binds, ...}) schematic =
   14.36 +fun norm_term (ctxt as Context {binds, ...}) schematic allow_vars =
   14.37    let
   14.38      (*raised when norm has no effect on a term, to do sharing instead of copying*)
   14.39      exception SAME;
   14.40 @@ -523,11 +527,12 @@
   14.41              Some (Some (u, U)) =>
   14.42                let
   14.43                  val env = unifyT ctxt (T, U) handle Type.TUNIFY =>
   14.44 -                  raise TYPE ("norm_term: ill-typed variable assigment", [T, U], [t, u]);
   14.45 +                  raise TYPE ("norm_term: ill-typed variable assignment", [T, U], [t, u]);
   14.46                  val u' = Term.subst_TVars_Vartab env u;
   14.47                in norm u' handle SAME => u' end
   14.48            | _ =>
   14.49              if schematic then raise SAME
   14.50 +            else if allow_vars then t
   14.51              else raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt))
   14.52        | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
   14.53        | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
   14.54 @@ -552,29 +557,59 @@
   14.55  
   14.56  local
   14.57  
   14.58 -fun gen_read read app is_pat dummies schematic (ctxt as Context {defs = (_, _, used, _), ...}) s =
   14.59 -  (transform_error (read (syn_of ctxt)
   14.60 -      (sign_of ctxt) (def_type ctxt is_pat, def_sort ctxt, used)) s
   14.61 -    handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   14.62 -    | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   14.63 -  |> app (intern_skolem ctxt)
   14.64 -  |> app (if is_pat then I else norm_term ctxt schematic)
   14.65 -  |> app (if is_pat then prepare_dummies else if dummies then I else reject_dummies ctxt);
   14.66 -
   14.67 +fun gen_read read app env_opt allow_vars is_pat dummies schematic
   14.68 +    (ctxt as Context {defs = (_, _, used, _), ...}) s =
   14.69 +  let
   14.70 +    (* Use environment of ctxt with the following modification:
   14.71 +       bindings in env_opt take precedence (needed for rule_tac) *)
   14.72 +    val types = def_type ctxt is_pat;
   14.73 +    val types' = case env_opt of
   14.74 +                     None => types
   14.75 +                   | Some (env, _, _) =>
   14.76 +                       (fn ixn => case env ixn of
   14.77 +                                      None => types ixn
   14.78 +                                    | some => some);
   14.79 +    val sorts = def_sort ctxt;
   14.80 +    val sorts' = case env_opt of
   14.81 +                     None => sorts
   14.82 +                   | Some (_, envT, _) =>
   14.83 +                       (fn ixn => case envT ixn of
   14.84 +                                      None => sorts ixn
   14.85 +                                    | some => some);
   14.86 +    val used' = case env_opt of
   14.87 +                    None => used
   14.88 +                  | Some (_, _, used'') => used @ used'';
   14.89 +  in
   14.90 +    (transform_error (read (syn_of ctxt)
   14.91 +	(sign_of ctxt) (types', sorts', used')) s
   14.92 +      handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   14.93 +      | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   14.94 +    |> app (intern_skolem ctxt (case env_opt of None => K None | Some (env, _, _) => env))
   14.95 +    |> app (if is_pat then I else norm_term ctxt schematic allow_vars)
   14.96 +    |> app (if is_pat then prepare_dummies
   14.97 +	 else if dummies then I else reject_dummies ctxt)
   14.98 +  end
   14.99  in
  14.100  
  14.101 -val read_termTs = gen_read (read_def_termTs false) (apfst o map) false false false;
  14.102 -val read_termT_pats = #1 oo gen_read (read_def_termTs false) (apfst o map) true false false;
  14.103 +val read_termTs =
  14.104 +  gen_read (read_def_termTs false) (apfst o map) None false false false false;
  14.105 +(* For rule_tac:
  14.106 +   takes extra environment (types, sorts and used type vars) *)
  14.107 +fun read_termTs_env env =
  14.108 +  gen_read (read_def_termTs false) (apfst o map) (Some env) true false false false;
  14.109 +val read_termT_pats =
  14.110 +  #1 oo gen_read (read_def_termTs false) (apfst o map) None false true false false;
  14.111  
  14.112  fun read_term_pats T ctxt pats = read_termT_pats ctxt (map (rpair T) pats);
  14.113  val read_prop_pats = read_term_pats propT;
  14.114  
  14.115 -val read_term = gen_read (read_term_sg true) I false false false;
  14.116 -val read_term_dummies = gen_read (read_term_sg true) I false true false;
  14.117 -val read_prop = gen_read (read_prop_sg true) I false false false;
  14.118 -val read_prop_schematic = gen_read (read_prop_sg true) I false false true;
  14.119 -val read_terms = gen_read (read_terms_sg true) map false false false;
  14.120 -val read_props = gen_read (read_props_sg true) map false false;
  14.121 +val read_term = gen_read (read_term_sg true) I None false false false false;
  14.122 +val read_term_dummies = gen_read (read_term_sg true) I None false false true false;
  14.123 +val read_prop = gen_read (read_prop_sg true) I None false false false false;
  14.124 +val read_prop_schematic =
  14.125 +  gen_read (read_prop_sg true) I None false false false true;
  14.126 +val read_terms = gen_read (read_terms_sg true) map None false false false false;
  14.127 +val read_props = gen_read (read_props_sg true) map None false false false;
  14.128  
  14.129  end;
  14.130  
  14.131 @@ -584,7 +619,7 @@
  14.132  local
  14.133  
  14.134  fun gen_cert cert is_pat schematic ctxt t = t
  14.135 -  |> (if is_pat then I else norm_term ctxt schematic)
  14.136 +  |> (if is_pat then I else norm_term ctxt schematic false)
  14.137    |> (fn t' => cert (sign_of ctxt) t' handle TERM (msg, _) => raise CONTEXT (msg, ctxt));
  14.138  
  14.139  in