# HG changeset patch # User blanchet # Date 1410288696 -7200 # Node ID 6c907aad90bae2fae7a0a9960d8d41c062f6d371 # Parent 85b13d75b2e4c477fe0d71a596052851ca8b8cd8 ported MicroJava to new datatypes diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/BV/BVNoTypeError.thy --- 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 diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/BV/JType.thy --- 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) diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/Comp/CorrComp.thy --- 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) diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/Comp/CorrCompTp.thy --- 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 \ 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 \ field (G, cname) vname = Some (cname, T)") + apply (rename_tac cname x2 vname ST LT T Ca, subgoal_tac "is_class G cname \ field (G, cname) vname = Some (cname, T)") apply simp (* show is_class G cname \ 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]: " (\ sttp. (length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex))) \ (\ 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) \ 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 @ diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/Comp/TypeInf.thy --- 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\e :: T1 \ E\e :: T2 \ T1 = T2) \ (\ (E\'a prog \ (vname \ ty option)) Ts1 Ts2. E\es [::] Ts1 \ E\es [::] Ts2 \ 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+ diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/J/Conform.thy --- 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 diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/J/JTypeSafe.thy --- 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\v::\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 \ Class cname \? Class D" for cname, simp) diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/J/Term.thy --- 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" diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/J/WellType.thy --- 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: "\T. (typeof dt (default_val ty) = Some T) \ G\ T \ ty" apply (case_tac ty) -apply (case_tac prim_ty) +apply (rename_tac prim_ty, case_tac prim_ty) apply auto done