# HG changeset patch
# User urbanc
# Date 1136995811 -3600
# Node ID 73cebafb9a8981649fb19cd43bc3815dcfd0e9b5
# Parent  94782c7c42479475d0b357c579e1be953b1fc1ac
merged the silly lemmas into the eqvt proof of subtype

diff -r 94782c7c4247 -r 73cebafb9a89 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Jan 11 17:07:57 2006 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Jan 11 17:10:11 2006 +0100
@@ -90,7 +90,7 @@
 lemma domain_eqvt:
   fixes pi::"tyvrs prm"
   shows "pi\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)" 
-  by (induct \<Gamma>, auto simp add: perm_set_def)
+  by (induct \<Gamma>, simp_all add: perm_empty perm_insert perm_fst)
 
 lemma finite_domain:
   shows "finite (domain \<Gamma>)"
@@ -328,34 +328,18 @@
   ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
 qed
 
-text {* Two silly lemmas that are helpful for showing that @{text "subtype_of"} is
-  equivariant. They are needed until we have a tactic that shows the property
-  of equivariance automatically. *}
-
-lemma silly_eqvt1:
-  fixes X::"'a::pt_tyvrs"
-  and   S::"'b::pt_tyvrs"
-  and   pi::"tyvrs prm"
- shows "(X,S) \<in> set \<Gamma> \<Longrightarrow> (pi\<bullet>X,pi\<bullet>S) \<in> set (pi\<bullet>\<Gamma>)"
-apply(drule_tac pi="pi" in pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-apply(simp add: pt_list_set_pi[OF pt_tyvrs_inst])
-done
-
-lemma silly_eqvt2:
-  fixes X::"tyvrs"
-  and   pi::"tyvrs prm"
- shows "X \<in> (domain \<Gamma>) \<Longrightarrow> (pi\<bullet>X) \<in> (domain (pi\<bullet>\<Gamma>))"
-apply(drule_tac pi="pi" in pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
-apply(simp add: domain_eqvt pt_list_set_pi[OF pt_tyvrs_inst] )
-done
-
 lemma subtype_eqvt:
   fixes pi::"tyvrs prm"
   shows "\<Gamma> \<turnstile> S <: T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>S) <: (pi\<bullet>T)"
 apply(erule subtype_of.induct)
 apply(force intro: valid_eqvt closed_in_eqvt)
-apply(force intro: closed_in_eqvt valid_eqvt silly_eqvt1)
-apply(force intro: valid_eqvt silly_eqvt2)
+apply(force intro!: S_Var
+            intro: closed_in_eqvt valid_eqvt 
+            dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]
+            simp add: pt_list_set_pi[OF pt_tyvrs_inst, symmetric])
+apply(force intro: valid_eqvt
+            dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]
+            simp add: domain_eqvt)
 apply(force)
 apply(force intro!: S_Forall simp add: fresh_prod fresh_eqvt)
 done