# HG changeset patch
# User wenzelm
# Date 1419883369 -3600
# Node ID cb8e5f7a5e4a58f24bd250d9a1984b48b9e3ca8e
# Parent  c73933e07c03ef364aceafd7ae59850ea7bc3538
tuned;

diff -r c73933e07c03 -r cb8e5f7a5e4a src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/List.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -3836,7 +3836,7 @@
 text{* Courtesy of Matthias Daum: *}
 lemma append_replicate_commute:
   "replicate n x @ replicate k x = replicate k x @ replicate n x"
-apply (simp add: replicate_add [THEN sym])
+apply (simp add: replicate_add [symmetric])
 apply (simp add: add.commute)
 done
 
diff -r c73933e07c03 -r cb8e5f7a5e4a src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -175,7 +175,7 @@
 lemma approx_stk_rev_lem:
   "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
   apply (unfold approx_stk_def approx_loc_def)
-  apply (simp add: rev_map [THEN sym])
+  apply (simp add: rev_map [symmetric])
   done
 
 lemma approx_stk_rev:
diff -r c73933e07c03 -r cb8e5f7a5e4a src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -551,7 +551,7 @@
 apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")
 apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd del: map_map)
 apply (intro strip)
-apply (simp (no_asm_simp) only: append_Cons [THEN sym])
+apply (simp (no_asm_simp) only: append_Cons [symmetric])
 apply (rule progression_lvar_init_aux)
 apply (auto simp: unique_def map_of_in_set disjoint_varnames_def)
 done
@@ -648,8 +648,8 @@
 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])
-apply (simp only: surjective_pairing [THEN sym])
+apply (simp (no_asm_use) add: surjective_pairing [symmetric])
+apply (simp only: surjective_pairing [symmetric])
 apply (auto simp add: gs_def gx_def)
 done
 
@@ -662,9 +662,9 @@
 apply (frule eval_evals_exec_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]]]) 
 apply (subgoal_tac "G \<turnstile> (gx s, (gh s, gl s)) -es[\<succ>]vs-> (gx s', (gh s', gl s'))")
 apply assumption
-apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym])
+apply (simp add: gx_def gh_def gl_def surjective_pairing [symmetric])
 apply (case_tac E)
-apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [THEN sym])
+apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [symmetric])
 done
 
 lemma eval_of_class: "\<lbrakk> G \<turnstile> s -e\<succ>a'-> s'; E \<turnstile> e :: Class C; 
@@ -1062,7 +1062,7 @@
 apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst)
 
 (* establish \<exists> lc. a' = Addr lc *)
-apply (frule (5) eval_of_class, rule env_of_jmb_fst [THEN sym])
+apply (frule (5) eval_of_class, rule env_of_jmb_fst [symmetric])
 apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class C")
 apply (subgoal_tac "is_class G dynT")
 
@@ -1097,7 +1097,7 @@
 (* establish length pns = length pTs *)
 apply (frule method_preserves_length, assumption, assumption) 
 (* establish length pvs = length ps *)
-apply (frule evals_preserves_length [THEN sym])
+apply (frule evals_preserves_length [symmetric])
 
 (** start evaluating subexpressions **)
 apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)
@@ -1179,10 +1179,10 @@
 apply (simp only: env_of_jmb_fst) 
 apply (simp add: conforms_def xconf_def gs_def)
 apply simp
-apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
+apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [symmetric])
 apply (simp (no_asm_use) only: ty_exprs_list_all2) apply simp
 apply simp
-apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
+apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [symmetric])
     (* list_all2 (\<lambda>T T'. G \<turnstile> T \<preceq> T') pTsa pTs *)
     apply (rule max_spec_widen, simp only: env_of_jmb_fst)
 
diff -r c73933e07c03 -r cb8e5f7a5e4a src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -89,7 +89,7 @@
 lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs"
 apply (induct xs)
 apply simp
-apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym]
+apply (simp add: unique_def map_of_append map_of_as_map_upds [symmetric]
                  Map.map_of_append[symmetric] del:Map.map_of_append)
 done
 
@@ -101,7 +101,7 @@
 apply (subgoal_tac "\<exists> x xr. xs = x # xr")
 apply clarify
 apply (drule_tac x=xr in spec)
-apply (simp add: map_upds_append [THEN sym])
+apply (simp add: map_upds_append [symmetric])
   (* subgoal *)
 apply (case_tac xs)
 apply auto
@@ -119,7 +119,7 @@
  apply (simp only: rev.simps)
  apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
   apply (simp split:split_if_asm)
- apply (simp add: map_upds_append [THEN sym])
+ apply (simp add: map_upds_append [symmetric])
 apply (case_tac ks)
  apply auto
 done
@@ -144,7 +144,7 @@
 apply (frule map_upds_SomeD)
 apply (rule map_upds_takeWhile)
 apply (simp (no_asm_simp))
-apply (simp add: map_upds_append [THEN sym])
+apply (simp add: map_upds_append [symmetric])
 apply (simp add: map_upds_rev)
 
   (* show length (pns @ map fst lvars) = length (pTs @ map snd lvars) *)
@@ -432,7 +432,7 @@
 \<Longrightarrow>(sttp_of (compTpInitLvars jmb lvars (ST, start_LT C pTs (length lvars))))
   = (ST, inited_LT C pTs lvars)"
 apply (simp add: start_LT_def inited_LT_def)
-apply (simp only: append_Cons [THEN sym])
+apply (simp only: append_Cons [symmetric])
 apply (rule compTpInitLvars_LT_ST_aux)
 apply (auto dest: wf_java_mdecl_length_pTs_pns wf_java_mdecl_disjoint_varnames)
 done
@@ -1288,7 +1288,7 @@
   -- {* @{text "<=s"} *}
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   apply (simp add: wf_prog_ws_prog [THEN comp_method])
-  apply (simp add: max_spec_preserves_length [THEN sym])
+  apply (simp add: max_spec_preserves_length [symmetric])
 
   -- "@{text check_type}"
 apply (simp add: max_ssize_def ssize_sto_def)
@@ -2493,10 +2493,10 @@
 apply (rule_tac T=T and LT="inited_LT C pTs lvars" and ST=start_ST in wt_method_comp_aux)
 
   (* bc *)
-apply (simp only: append_assoc [THEN sym])
+apply (simp only: append_assoc [symmetric])
 
   (* comb *)
-apply (simp only: comb_assoc [THEN sym])
+apply (simp only: comb_assoc [symmetric])
 
   (* bc_corresp *)
 apply (rule wt_method_comp_wo_return)
diff -r c73933e07c03 -r cb8e5f7a5e4a src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -95,7 +95,7 @@
 "(class G C = None) = (class (comp G) C = None)"
 apply (simp add: class_def comp_def compClass_def)
 apply (simp add: map_of_in_set)
-apply (simp add: image_comp [THEN sym] o_def split_beta)
+apply (simp add: image_comp [symmetric] o_def split_beta)
 done
 
 lemma comp_is_class: "is_class (comp G) C = is_class G C"
@@ -186,7 +186,7 @@
 apply (rule sym)
 apply (simp add: ws_prog_def comp_ws_cdecl comp_unique)
 apply (simp add: comp_wf_syscls)
-apply (auto simp add: comp_ws_cdecl [THEN sym] TranslComp.comp_def)
+apply (auto simp add: comp_ws_cdecl [symmetric] TranslComp.comp_def)
 done
 
 
diff -r c73933e07c03 -r cb8e5f7a5e4a src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -172,10 +172,10 @@
 apply(induct_tac "vs")
  apply(clarsimp)
 apply(clarsimp)
-apply(frule list_all2_lengthD [THEN sym])
+apply(frule list_all2_lengthD [symmetric])
 apply(simp (no_asm_use) add: length_Suc_conv)
 apply(safe)
-apply(frule list_all2_lengthD [THEN sym])
+apply(frule list_all2_lengthD [symmetric])
 apply(simp (no_asm_use) add: length_Suc_conv)
 apply(clarify)
 apply(fast elim: conf_widen)
diff -r c73933e07c03 -r cb8e5f7a5e4a src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -434,7 +434,7 @@
 apply     (simp (no_asm))
 apply     (tactic e) -- "XcptE"
 apply    (simp (no_asm))
-apply   (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
+apply   (rule surjective_pairing [symmetric, THEN[2]trans], subst Pair_eq, force)
 apply  (simp (no_asm))
 apply (simp (no_asm))
 apply (tactic e) -- "XcptE"
diff -r c73933e07c03 -r cb8e5f7a5e4a src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Mon Dec 29 20:51:42 2014 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Dec 29 21:02:49 2014 +0100
@@ -140,7 +140,7 @@
 apply(clarify)
 apply( drule (1) class_wf_struct)
 apply( unfold ws_cdecl_def)
-apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
+apply(force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
 done
 
 lemma wf_cdecl_supD: 
@@ -600,7 +600,7 @@
 apply (erule disjE)
 apply (simp (no_asm_use) add: map_of_map) apply blast
 apply blast
-apply (rule trans [THEN sym], rule sym, assumption)
+apply (rule trans [symmetric], rule sym, assumption)
 apply (rule_tac x=vn in fun_cong)
 apply (rule trans, rule field_rec, assumption+)
 apply (simp (no_asm_simp) add: wf_prog_ws_prog)