# HG changeset patch
# User wenzelm
# Date 1346869177 -7200
# Node ID 3d7a695385f1e4bf908829e6a650aa794a7e691b
# Parent  03bee3a6a1b7bcf9eb0c747b6708c48170b46e5d
tuned proofs;

diff -r 03bee3a6a1b7 -r 3d7a695385f1 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Sep 05 19:51:00 2012 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Sep 05 20:19:37 2012 +0200
@@ -225,7 +225,7 @@
   assumes a: "x\<sharp>\<theta>"
   shows "\<theta><Var x> = Var x"
 using a
-by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm)
+by (induct \<theta> arbitrary: x) (auto simp add:fresh_list_cons fresh_prod fresh_atm)
 
 lemma psubst_subst_propagate: 
   assumes "x\<sharp>\<theta>" 
@@ -529,7 +529,7 @@
 lemma alg_path_equiv_implies_valid:
   shows  "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" 
   and    "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
-by (induct rule : alg_equiv_alg_path_equiv.inducts, auto)
+by (induct rule : alg_equiv_alg_path_equiv.inducts) auto
 
 lemma algorithmic_symmetry:
   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T" 
diff -r 03bee3a6a1b7 -r 3d7a695385f1 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Sep 05 19:51:00 2012 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Sep 05 20:19:37 2012 +0200
@@ -140,12 +140,12 @@
 lemma finite_vrs:
   shows "finite (tyvrs_of x)"
   and   "finite (vrs_of x)"
-by (nominal_induct rule:binding.strong_induct, auto)
+by (nominal_induct rule:binding.strong_induct) auto
  
 lemma finite_doms:
   shows "finite (ty_dom \<Gamma>)"
   and   "finite (trm_dom \<Gamma>)"
-by (induct \<Gamma>, auto simp add: finite_vrs)
+by (induct \<Gamma>) (auto simp add: finite_vrs)
 
 lemma ty_dom_supp:
   shows "(supp (ty_dom  \<Gamma>)) = (ty_dom  \<Gamma>)"
@@ -155,13 +155,13 @@
 lemma ty_dom_inclusion:
   assumes a: "(TVarB X T)\<in>set \<Gamma>" 
   shows "X\<in>(ty_dom \<Gamma>)"
-using a by (induct \<Gamma>, auto)
+using a by (induct \<Gamma>) (auto)
 
 lemma ty_binding_existence:
   assumes "X \<in> (tyvrs_of a)"
   shows "\<exists>T.(TVarB X T=a)"
   using assms
-by (nominal_induct a rule: binding.strong_induct, auto)
+by (nominal_induct a rule: binding.strong_induct) (auto)
 
 lemma ty_dom_existence:
   assumes a: "X\<in>(ty_dom \<Gamma>)" 
@@ -176,7 +176,7 @@
 lemma doms_append:
   shows "ty_dom (\<Gamma>@\<Delta>) = ((ty_dom \<Gamma>) \<union> (ty_dom \<Delta>))"
   and   "trm_dom (\<Gamma>@\<Delta>) = ((trm_dom \<Gamma>) \<union> (trm_dom \<Delta>))"
-  by (induct \<Gamma>, auto)
+  by (induct \<Gamma>) (auto)
 
 lemma ty_vrs_prm_simp:
   fixes pi::"vrs prm"
@@ -1069,7 +1069,7 @@
 lemma typing_ok:
   assumes "\<Gamma> \<turnstile> t : T"
   shows   "\<turnstile> \<Gamma> ok"
-using assms by (induct, auto)
+using assms by (induct) (auto)
 
 nominal_inductive typing
 by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh
@@ -1208,7 +1208,7 @@
 
 lemma ty_dom_cons:
   shows "ty_dom (\<Gamma>@[VarB X Q]@\<Delta>) = ty_dom (\<Gamma>@\<Delta>)"
-by (induct \<Gamma>, auto)
+by (induct \<Gamma>) (auto)
 
 lemma closed_in_cons: 
   assumes "S closed_in (\<Gamma> @ VarB X Q # \<Delta>)"
@@ -1251,7 +1251,7 @@
 
 lemma ty_dom_vrs:
   shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)"
-by (induct G, auto)
+by (induct G) (auto)
 
 lemma valid_cons':
   assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
diff -r 03bee3a6a1b7 -r 3d7a695385f1 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Wed Sep 05 19:51:00 2012 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Wed Sep 05 20:19:37 2012 +0200
@@ -321,7 +321,7 @@
 proof (nominal_induct e e\<^isub>1 avoiding: e\<^isub>2 rule: big.strong_induct)
   case (b_Lam x e t\<^isub>2)
   have "Lam [x].e \<Down> t\<^isub>2" by fact
-  thus "Lam [x].e = t\<^isub>2" by (cases, simp_all add: trm.inject)
+  thus "Lam [x].e = t\<^isub>2" by cases (simp_all add: trm.inject)
 next
   case (b_App x e\<^isub>1 e\<^isub>2 e' e\<^isub>1' e\<^isub>2' t\<^isub>2)
   have ih1: "\<And>t. e\<^isub>1 \<Down> t \<Longrightarrow> Lam [x].e\<^isub>1' = t" by fact