--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Dec 25 17:39:06 2013 +0100
@@ -442,7 +442,7 @@
(********************************************************************************)
lemma max_of_list_elem: "x \<in> set xs \<Longrightarrow> x \<le> (max_of_list xs)"
-by (induct xs, auto intro: le_maxI1 simp: le_max_iff_disj max_of_list_def)
+by (induct xs, auto intro: max.cobounded1 simp: le_max_iff_disj max_of_list_def)
lemma max_of_list_sublist: "set xs \<subseteq> set ys
\<Longrightarrow> (max_of_list xs) \<le> (max_of_list ys)"
@@ -1053,7 +1053,7 @@
lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
\<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1064,7 +1064,7 @@
bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def ssize_sto_def max_of_list_def)
- apply (simp add: check_type_simps min_max.sup_absorb1)
+ apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="(length ST)" in exI)
apply simp+
@@ -1087,7 +1087,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1106,7 +1106,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1124,7 +1124,7 @@
\<Longrightarrow> bc_mt_corresp [Load i]
(\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1148,7 +1148,7 @@
apply (simp add: max_ssize_def max_of_list_def)
apply (simp add: ssize_sto_def)
apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule conjI)
apply (rule_tac x="(length ST)" in exI)
@@ -1162,7 +1162,7 @@
apply (simp add: sup_state_conv)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="(length ST)" in exI)
apply simp+
@@ -1172,7 +1172,7 @@
lemma bc_mt_corresp_Dup: "
bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1185,7 +1185,7 @@
lemma bc_mt_corresp_Dup_x1: "
bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1202,7 +1202,7 @@
(PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
- apply (simp add: check_type_simps min_max.sup_absorb1)
+ apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
@@ -1245,7 +1245,7 @@
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+