--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Sep 09 20:51:36 2014 +0200
@@ -95,15 +95,15 @@
apply simp
apply (case_tac a)
apply auto
- apply (case_tac prim_ty)
+ apply (rename_tac prim_ty, case_tac prim_ty)
apply auto
- apply (case_tac prim_ty)
+ apply (rename_tac prim_ty, case_tac prim_ty)
apply auto
apply (case_tac list)
apply auto
apply (case_tac a)
apply auto
- apply (case_tac prim_ty)
+ apply (rename_tac prim_ty, case_tac prim_ty)
apply auto
done
--- a/src/HOL/MicroJava/BV/JType.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/BV/JType.thy Tue Sep 09 20:51:36 2014 +0200
@@ -91,7 +91,7 @@
apply (case_tac y)
apply simp
apply simp
- apply (case_tac ref_ty)
+ apply (rename_tac ref_ty ref_tya, case_tac ref_ty)
apply (case_tac ref_tya)
apply simp
apply simp
@@ -116,6 +116,7 @@
apply (case_tac T)
apply (fastforce simp add: PrimT_PrimT2)
apply simp
+ apply (rename_tac ref_ty)
apply (subgoal_tac "ref_ty = NullT")
apply simp
apply (rule_tac x = NT in bexI)
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Tue Sep 09 20:51:36 2014 +0200
@@ -785,7 +785,7 @@
apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp)) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
-apply (simp (no_asm_use) only: compExpr_compExprs.simps)
+apply (simp (no_asm_use) only: compExpr.simps 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 (case_tac bop)
@@ -831,7 +831,7 @@
apply (simp (no_asm_use) only: gx_conv, frule np_NoneD)
apply (frule wtpd_expr_facc)
-apply (simp (no_asm_use) only: compExpr_compExprs.simps)
+apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
apply blast
apply (rule progression_one_step)
@@ -853,7 +853,7 @@
apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst)
apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
-apply (simp only: compExpr_compExprs.simps)
+apply (simp only: compExpr.simps compExprs.simps)
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? *)
@@ -1100,7 +1100,7 @@
apply (frule evals_preserves_length [THEN sym])
(** start evaluating subexpressions **)
-apply (simp (no_asm_use) only: compExpr_compExprs.simps)
+apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)
(* evaluate e *)
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Sep 09 20:51:36 2014 +0200
@@ -236,7 +236,7 @@
is_inited_LT C pTs lvars LT \<longrightarrow>
sttp_of (compTpExprs jmb G exs (ST, LT)) = ((rev Ts) @ ST, LT))"
-apply (rule expr.induct)
+apply (rule compat_expr_expr_list.induct)
(* expresssions *)
@@ -262,7 +262,7 @@
apply (drule_tac x=ST in spec)
apply (drule_tac x="Ta # ST" in spec)
apply ((drule spec)+, (drule mp, assumption)+)
- apply (case_tac binop)
+ apply (rename_tac binop x2 x3 ST LT T Ta, case_tac binop)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: popST_def pushST_def)
apply (simp)
@@ -295,7 +295,7 @@
(* show snd (the (field (G, cname) vname)) = T *)
apply (subgoal_tac "is_class G Ca")
- apply (subgoal_tac "is_class G cname \<and> field (G, cname) vname = Some (cname, T)")
+ apply (rename_tac cname x2 vname ST LT T Ca, subgoal_tac "is_class G cname \<and> field (G, cname) vname = Some (cname, T)")
apply simp
(* show is_class G cname \<and> field (G, cname) vname = Some (cname, T) *)
@@ -317,7 +317,7 @@
apply (intro strip)
apply (drule Call_invers, clarify)
apply (drule_tac x=ST in spec)
-apply (drule_tac x="Class cname # ST" in spec)
+apply (rename_tac cname x2 x3 x4 x5 ST LT T pTsa md, drule_tac x="Class cname # ST" in spec)
apply ((drule spec)+, (drule mp, assumption)+)
apply (simp add: replST_def)
@@ -823,9 +823,9 @@
lemma length_compTpExpr_Exprs [rule_format]: "
(\<forall> sttp. (length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)))
\<and> (\<forall> sttp. (length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)))"
-apply (rule expr.induct)
+apply (rule compat_expr_expr_list.induct)
apply simp+
-apply (case_tac binop)
+apply (rename_tac binop a b, case_tac binop)
apply simp+
apply (simp add: pushST_def split_beta)
apply simp+
@@ -1648,7 +1648,7 @@
(is_inited_LT C pTs lvars LT)
\<longrightarrow> bc_mt_corresp (compExprs jmb exs) (compTpExprs jmb G exs) (ST, LT) (comp G) rT (length LT) (length (compExprs jmb exs)))"
-apply (rule expr.induct)
+apply (rule compat_expr_expr_list.induct)
(* expresssions *)
@@ -1690,7 +1690,7 @@
apply (intro allI impI)
apply (simp (no_asm_simp) only:)
apply (drule BinOp_invers, erule exE, (erule conjE)+)
-apply (case_tac binop)
+apply (rename_tac binop expr1 expr2 ST LT T bc' f' Ta, case_tac binop)
apply (simp (no_asm_simp))
(* case Eq *)
@@ -1819,9 +1819,10 @@
apply clarify
apply (simp (no_asm_use))
apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast)
+apply (rename_tac vname x2 ST LT T Ta)
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)
+ in bc_mt_corresp_comb)
apply (simp (no_asm_simp))+
apply (rule bc_mt_corresp_Dup)
apply (simp only: compTpExpr_LT_ST)
@@ -1858,6 +1859,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 (rename_tac cname x2 vname x4 ST LT T Ta Ca)
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)
@@ -1970,6 +1972,7 @@
apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
apply (simp (no_asm_simp))
+apply (rename_tac expr stmt1 stmt2 ST LT bc' f')
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))) #
@@ -2111,6 +2114,7 @@
apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
apply (simp (no_asm_simp))
+apply (rename_tac expr stmt ST LT bc' f')
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 @
--- a/src/HOL/MicroJava/Comp/TypeInf.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/Comp/TypeInf.thy Tue Sep 09 20:51:36 2014 +0200
@@ -109,10 +109,10 @@
E\<turnstile>e :: T1 \<longrightarrow> E\<turnstile>e :: T2 \<longrightarrow> T1 = T2) \<and>
(\<forall> (E\<Colon>'a prog \<times> (vname \<Rightarrow> ty option)) Ts1 Ts2.
E\<turnstile>es [::] Ts1 \<longrightarrow> E\<turnstile>es [::] Ts2 \<longrightarrow> Ts1 = Ts2)"
-apply (rule expr.induct)
+apply (rule compat_expr_expr_list.induct)
(* NewC *)
-apply (intro strip)
+apply (intro strip)
apply (erule ty_expr.cases) apply simp+
apply (erule ty_expr.cases) apply simp+
@@ -128,7 +128,7 @@
(* BinOp *)
apply (intro strip)
-apply (case_tac binop)
+apply (rename_tac binop x2 x3 E T1 T2, case_tac binop)
(* Eq *)
apply (erule ty_expr.cases) apply simp+
apply (erule ty_expr.cases) apply simp+
--- a/src/HOL/MicroJava/J/Conform.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Tue Sep 09 20:51:36 2014 +0200
@@ -108,7 +108,7 @@
apply (unfold conf_def)
apply (rule_tac y = "T" in ty.exhaust)
apply (erule ssubst)
-apply (rule_tac y = "prim_ty" in prim_ty.exhaust)
+apply (rename_tac prim_ty, rule_tac y = "prim_ty" in prim_ty.exhaust)
apply (auto simp add: widen.null)
done
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Tue Sep 09 20:51:36 2014 +0200
@@ -22,7 +22,7 @@
==> G,h\<turnstile>v::\<preceq>Class D"
apply (case_tac "CC")
apply simp
-apply (case_tac "ref_ty")
+apply (rename_tac ref_ty, case_tac "ref_ty")
apply (clarsimp simp add: conf_def)
apply simp
apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp)
--- a/src/HOL/MicroJava/J/Term.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Tue Sep 09 20:51:36 2014 +0200
@@ -19,7 +19,9 @@
| FAss cname expr vname
expr ("{_}_.._:=_" [10,90,99,90]90) -- "field ass."
| Call cname expr mname
- "ty list" "expr list" ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call"
+ "ty list" "expr list" ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call"
+
+datatype_compat expr
datatype_new stmt
= Skip -- "empty statement"
--- a/src/HOL/MicroJava/J/WellType.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Tue Sep 09 20:51:36 2014 +0200
@@ -94,7 +94,7 @@
lemma typeof_default_val: "\<exists>T. (typeof dt (default_val ty) = Some T) \<and> G\<turnstile> T \<preceq> ty"
apply (case_tac ty)
-apply (case_tac prim_ty)
+apply (rename_tac prim_ty, case_tac prim_ty)
apply auto
done