# HG changeset patch
# User wenzelm
# Date 1186937583 -7200
# Node ID 85fb973a8207e5873e421add195de50c686f1990
# Parent  f63bca3e574e2b9a01a06b6ace9c142e0ed0e8b0
added type constraints to resolve syntax ambiguities;

diff -r f63bca3e574e -r 85fb973a8207 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Sun Aug 12 14:14:24 2007 +0200
+++ b/src/HOL/Lambda/Eta.thy	Sun Aug 12 18:53:03 2007 +0200
@@ -142,11 +142,13 @@
   done
 
 lemma rtrancl_eta_subst':
+  fixes s t :: dB
   assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
   shows "s[u/i] \<rightarrow>\<^sub>\<eta>\<^sup>* t[u/i]" using eta
   by induct (iprover intro: eta_subst)+
 
 lemma rtrancl_eta_subst'':
+  fixes s t :: dB
   assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
   shows "u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" using eta
   by induct (iprover intro: rtrancl_eta_subst rtranclp_trans)+
@@ -238,6 +240,7 @@
 *}
 
 theorem eta_case:
+  fixes s :: dB
   assumes free: "\<not> free s 0"
   and s: "s[dummy/0] => u"
   shows "\<exists>t'. Abs (s \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u"
diff -r f63bca3e574e -r 85fb973a8207 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Sun Aug 12 14:14:24 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Sun Aug 12 18:53:03 2007 +0200
@@ -274,6 +274,7 @@
   "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>a T. (a,T)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (a,T)\<in>set \<Gamma>\<^isub>2"
 
 lemma valid_monotonicity[elim]:
+ fixes \<Gamma> \<Gamma>' :: Ctxt
  assumes a: "\<Gamma> \<subseteq> \<Gamma>'" 
  and     b: "x\<sharp>\<Gamma>'"
  shows "(x,T\<^isub>1)#\<Gamma> \<subseteq> (x,T\<^isub>1)#\<Gamma>'"
@@ -373,6 +374,7 @@
 done
 
 lemma test3a:
+  fixes \<Gamma> :: Ctxt and t :: trm
   assumes a: "\<Gamma> \<turnstile> t : T"
   shows "(supp t) \<subseteq> ((supp \<Gamma>)::name set)"
 using a
@@ -392,6 +394,7 @@
 done
 
 lemma test3:
+  fixes \<Gamma> :: Ctxt and s t :: trm
   assumes a: "\<Gamma> \<turnstile> s \<equiv> t : T"
   shows "(supp (s,t)) \<subseteq> ((supp \<Gamma>)::name set)"
 using a
@@ -765,7 +768,8 @@
 apply(auto)
 done
 
-lemma logical_monotonicity :
+lemma logical_monotonicity:
+ fixes \<Gamma> \<Gamma>' :: Ctxt
  assumes a1: "\<Gamma> \<turnstile> s is t : T" 
  and     a2: "\<Gamma> \<subseteq> \<Gamma>'" 
  and     a3: "valid \<Gamma>'"
@@ -915,6 +919,7 @@
 qed
 
 lemma logical_subst_monotonicity :
+  fixes \<Gamma> \<Gamma>' \<Gamma>'' :: Ctxt
   assumes a: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   and     b: "\<Gamma>' \<subseteq> \<Gamma>''"
   and     c: "valid \<Gamma>''"
diff -r f63bca3e574e -r 85fb973a8207 src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Sun Aug 12 14:14:24 2007 +0200
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Sun Aug 12 18:53:03 2007 +0200
@@ -143,6 +143,7 @@
   "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2"
 
 lemma weakening_almost_automatic:
+  fixes \<Gamma>1 \<Gamma>2 :: cxt
   assumes a: "\<Gamma>1 \<turnstile> t : T"
   and     b: "\<Gamma>1 \<subseteq> \<Gamma>2"
   and     c: "valid \<Gamma>2"
@@ -155,6 +156,7 @@
 done
 
 lemma weakening_in_more_detail:
+  fixes \<Gamma>1 \<Gamma>2 :: cxt
   assumes a: "\<Gamma>1 \<turnstile> t : T"
   and     b: "\<Gamma>1 \<subseteq> \<Gamma>2"
   and     c: "valid \<Gamma>2"
diff -r f63bca3e574e -r 85fb973a8207 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Sun Aug 12 14:14:24 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Sun Aug 12 18:53:03 2007 +0200
@@ -366,6 +366,7 @@
 qed
 
 lemma weakening: 
+  fixes \<Gamma>\<^isub>1 \<Gamma>\<^isub>2 :: "(name\<times>ty) list"
   assumes "\<Gamma>\<^isub>1 \<turnstile> e: T" and "valid \<Gamma>\<^isub>2" and "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2"
   shows "\<Gamma>\<^isub>2 \<turnstile> e: T"
   using assms
diff -r f63bca3e574e -r 85fb973a8207 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Sun Aug 12 14:14:24 2007 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Sun Aug 12 18:53:03 2007 +0200
@@ -59,6 +59,7 @@
 text {* Now it comes: The Weakening Lemma *}
 
 lemma weakening_version1: 
+  fixes \<Gamma>1 \<Gamma>2 :: "(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T" 
   and     b: "valid \<Gamma>2" 
   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
@@ -97,7 +98,8 @@
   with vc show "\<Gamma>2 \<turnstile> Lam [x].t : T1\<rightarrow>T2" by auto
 qed (auto) (* app case *)
 
-lemma weakening_version3: 
+lemma weakening_version3:
+  fixes \<Gamma>1 \<Gamma>2 :: "(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T"
   and     b: "valid \<Gamma>2" 
   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
@@ -120,6 +122,7 @@
        is not strong enough - even this simple lemma fails to be simple ;o) *}
 
 lemma weakening_too_weak: 
+  fixes \<Gamma>1 \<Gamma>2 :: "(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T"
   and     b: "valid \<Gamma>2" 
   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"