# HG changeset patch # User ballarin # Date 1062163142 -7200 # Node ID f3cafd2929d5b9b4d3690536021c97418865c423 # Parent a3690aeb79d4e821f6b3cb04ed7a4167df06e347 Methods rule_tac etc support static (Isar) contexts. diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/Bali/WellForm.thy --- 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 @@ (\T m. t = ArrayT T \ G\Array T accessible_in (pid S) \ accmethd G S Object sig = Some m \ accmodi m \ Private \ declrefT emh = ClassT Object \ 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) diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/HoareParallel/RG_Examples.thy --- 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'"="\ \X i mod n = i \ (\j. j<\X i \ j mod n = i \ \P(B!j)) \ (\Y i < n * q \ P (B!(\Y i))) \ \X i<\Y i\" in Conseq) + apply(rule_tac pre'="\ \X i mod n = i \ (\j. j<\X i \ j mod n = i \ \P(B!j)) \ (\Y i < n * q \ P (B!(\Y i))) \ \X i<\Y i\" 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'"="\nX \ nY \ \X ! i mod n = i \ (\j. j < \X ! i \ j mod n = i \ \ P (B ! j)) \ (\Y ! i < n * q \ P (B ! (\Y ! i))) \ \X!i<\Y!i\" in Conseq) + apply(rule_tac pre'="\nX \ nY \ \X ! i mod n = i \ (\j. j < \X ! i \ j mod n = i \ \ P (B ! j)) \ (\Y ! i < n * q \ P (B ! (\Y ! i))) \ \X!i<\Y!i\" in Conseq) apply force apply(rule subset_refl)+ apply(rule Cond) diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/MicroJava/Comp/CorrComp.thy --- 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} \ {hp0, os0, lvars0} >- instrs_comb \ {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 @@ \ {G, C, S} \ {hp, os0, lvars} >- instrs_comb \ {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\e::T; gx s' = None; prg E = G \ \ G,gh s'\v::\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) diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/MicroJava/Comp/CorrCompTp.thy --- 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 \ compTpExpr jmb G expr2" - and "f2.0"="popST 2" and "f3.0"="pushST [PrimT Boolean] \ popST 1 \ 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 \ compTpExpr jmb G expr2" + and ?f2.0="popST 2" and ?f3.0="pushST [PrimT Boolean] \ popST 1 \ 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 \ compTpExpr jmb G expr2 \ popST 2" - and "f2.0" = "pushST [PrimT Boolean]" - and "f3.0" = "popST (Suc 0) \ 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 \ compTpExpr jmb G expr2 \ popST 2" + and ?f2.0 = "pushST [PrimT Boolean]" + and ?f3.0 = "popST (Suc 0) \ 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 \ compTpExpr jmb G expr2 \ popST 2 \ 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 \ compTpExpr jmb G expr2 \ popST 2 \ 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 \ compTpExpr jmb G expr2 \ popST 2 \ + ?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 \ compTpExpr jmb G expr2 \ popST 2 \ pushST [PrimT Boolean] \ 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 \ popST 2 \ compTpStmt jmb G stmt1 \ + and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]" + and ?f3.0="compTpExpr jmb G expr \ popST 2 \ compTpStmt jmb G stmt1 \ nochangeST \ 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 \ compTpStmt jmb G stmt1 \ + and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr" + and ?f3.0="popST 2 \ compTpStmt jmb G stmt1 \ nochangeST \ 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] \ compTpExpr jmb G expr" and "f2.0" = "popST 2" - and "f3.0"="compTpStmt jmb G stmt1 \ nochangeST \ compTpStmt jmb G stmt2" + and ?f1.0="pushST [PrimT Boolean] \ compTpExpr jmb G expr" and ?f2.0 = "popST 2" + and ?f3.0="compTpStmt jmb G stmt1 \ nochangeST \ 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] \ compTpExpr jmb G expr \ popST 2" - and "f2.0" = "compTpStmt jmb G stmt1" - and "f3.0"="nochangeST \ 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] \ compTpExpr jmb G expr \ popST 2" + and ?f2.0 = "compTpStmt jmb G stmt1" + and ?f3.0="nochangeST \ 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] \ compTpExpr jmb G expr \ popST 2 \ + and ?bc3.0 = "compStmt jmb stmt2" + and ?f1.0="pushST [PrimT Boolean] \ compTpExpr jmb G expr \ popST 2 \ 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] \ compTpExpr jmb G expr \ popST 2 \ + and ?bc2.0 = "compStmt jmb stmt2" + and ?bc3.0="[]" + and ?f1.0="pushST [PrimT Boolean] \ compTpExpr jmb G expr \ popST 2 \ compTpStmt jmb G stmt1 \ 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 \ popST 2 \ compTpStmt jmb G stmt \ nochangeST" + and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]" + and ?f3.0="compTpExpr jmb G expr \ popST 2 \ compTpStmt jmb G stmt \ 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 \ compTpStmt jmb G stmt \ nochangeST" + and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr" + and ?f3.0="popST 2 \ compTpStmt jmb G stmt \ 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] \ compTpExpr jmb G expr" and "f2.0" = "popST 2" - and "f3.0"="compTpStmt jmb G stmt \ nochangeST" + and ?f1.0="pushST [PrimT Boolean] \ compTpExpr jmb G expr" and ?f2.0 = "popST 2" + and ?f3.0="compTpStmt jmb G stmt \ 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] \ compTpExpr jmb G expr \ 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] \ compTpExpr jmb G expr \ 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] \ compTpExpr jmb G expr \ popST 2 \ + and ?bc3.0 = "[]" + and ?f1.0="pushST [PrimT Boolean] \ compTpExpr jmb G expr \ popST 2 \ 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 \ \ 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)+ diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/MicroJava/J/Conform.thy --- 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\default_val T::\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' \ Null ==> wf_prog wf_mb G ==> G,h\a'::\RefT t --> (\a C fs. a' = Addr a \ h a = Some (C,fs) \ G\Class C\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 diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/MicroJava/J/State.thy --- 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 diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/MicroJava/J/WellForm.thy --- 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) diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/NanoJava/Equivalence.thy --- 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)]: "\s t. s -c-n\ t \ P s \ s \ Null \ P t \ (s -c0-n0\ t \ P s \ c0 = While (x) c \ n0 = n \ P t \ t = 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 diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/NumberTheory/EulerFermat.thy --- 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]) diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/NumberTheory/IntPrimes.thy --- 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) diff -r a3690aeb79d4 -r f3cafd2929d5 src/HOL/Tools/datatype_package.ML --- 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; diff -r a3690aeb79d4 -r f3cafd2929d5 src/Pure/Isar/args.ML --- 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 *) diff -r a3690aeb79d4 -r f3cafd2929d5 src/Pure/Isar/method.ML --- 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")]; diff -r a3690aeb79d4 -r f3cafd2929d5 src/Pure/Isar/proof_context.ML --- 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