# HG changeset patch
# User urbanc
# Date 1208305506 -7200
# Node ID ab629324081cdb7113bcc6468dc991c4d84424e3
# Parent  fb8039e26c6a98289d132a18504178361a0b75ce
removed test artefacts

diff -r fb8039e26c6a -r ab629324081c src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Tue Apr 15 22:09:24 2008 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Apr 16 02:25:06 2008 +0200
@@ -358,128 +358,6 @@
   shows "valid \<Gamma>"
 using a by (induct) (auto elim: typing_implies_valid)
 
-lemma test30:
-  fixes x::"name"
-  assumes a: "(x,T) \<in> set \<Gamma>"
-  shows "x\<in>supp \<Gamma>"
-using a
-apply(induct \<Gamma>)
-apply(auto simp add: supp_list_cons supp_prod supp_atm)
-done
-
-lemma supp_ty[simp]: 
-  fixes T::"ty"
-  shows "(supp T) = ({}::name set)"
-apply(simp add: supp_def)
-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
-apply(induct)
-apply(auto simp add: trm.supp supp_atm supp_list_cons abs_supp supp_prod)
-apply(simp add: test30)
-apply(simp add: supp_def perm_nat_def)
-done
-
-lemma test3b:
-  shows "supp (t\<^isub>1[x::=t\<^isub>2]) \<subseteq> ((supp ([x].t\<^isub>1,t\<^isub>2))::name set)"
-apply(nominal_induct t\<^isub>1 avoiding: x t\<^isub>2 rule: trm.induct)
-apply(auto simp add: trm.supp supp_prod abs_supp supp_atm)
-apply(blast)
-apply(blast)
-apply(simp add: supp_def perm_nat_def)
-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
-apply(induct)
-apply(auto simp add: supp_prod  supp_list_cons trm.supp abs_supp supp_atm)
-apply(drule test3a)
-apply(blast)
-apply(subgoal_tac "supp (t\<^isub>1[x::=t\<^isub>2]) \<subseteq> ((supp ([x].t\<^isub>1,t\<^isub>2))::name set)")
-apply(auto simp add: supp_prod abs_supp)[1]
-apply(rule test3b)
-apply(case_tac "x=xa")
-apply(simp add: fresh_def supp_prod)
-apply(blast)
-apply(case_tac "x=xa")
-apply(simp add: fresh_def supp_prod)
-apply(blast)
-apply(drule test3a)
-apply(blast)
-apply(drule test3a)+
-apply(blast)
-done
-
-lemma test0:
-  assumes a: "(x,T\<^isub>1)#\<Gamma> \<turnstile> s\<^isub>1 \<equiv> t\<^isub>1 : T\<^isub>2" 
-  and     b: "\<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>1"
-  shows "\<Gamma> \<turnstile> App (Lam [x]. s\<^isub>1) s\<^isub>2 \<equiv> t\<^isub>1[x::=t\<^isub>2] : T\<^isub>2"
-using a b
-apply(rule_tac Q_Beta)
-apply(auto)
-apply(drule def_equiv_implies_valid)
-apply(drule valid.cases)
-apply(auto)
-apply(drule test3)
-apply(auto simp add: fresh_def supp_prod)
-done
-
-lemma test1:
-  assumes a: "\<forall>x. x\<sharp>\<Gamma> \<longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
-  shows "\<Gamma> \<turnstile> s \<equiv> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
-using a
-apply -
-apply(generate_fresh "name")
-apply(rule_tac x="c" in Q_Ext)
-apply(simp)
-apply(simp add: fresh_prod)
-done
-
-lemma test2:
-  assumes a: "x\<sharp>(\<Gamma>,s,t) \<and> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
-  shows "\<forall>x. x\<sharp>(\<Gamma>,s,t) \<longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
-using a
-apply -
-apply(rule allI)
-apply(case_tac "xa=x")
-apply(simp)
-apply(rule impI)
-apply(erule conjE)
-apply(drule_tac pi="[(x,xa)]" in def_equiv.eqvt)
-apply(simp add: eqvts)
-apply(simp add: calc_atm)
-apply(perm_simp)
-done
-
-lemma test2b:
-  assumes a: "x\<sharp>(\<Gamma>,s,t) \<and> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
-  shows "\<forall>x. x\<sharp>\<Gamma> \<longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
-using a
-apply -
-apply(rule allI)
-apply(case_tac "xa=x")
-apply(simp)
-apply(rule impI)
-apply(erule conjE)
-apply(frule test3)
-apply(simp add: supp_prod supp_list_cons supp_atm trm.supp)
-apply(subgoal_tac "xa\<sharp>(s,t)")
-apply(drule_tac pi="[(x,xa)]" in def_equiv.eqvt)
-apply(simp add: eqvts)
-apply(simp add: calc_atm)
-apply(perm_simp)
-apply(simp add: fresh_def supp_prod)
-apply(auto)
-done
-
-
 section {* Weak Head Reduction *}
 
 inductive
@@ -570,19 +448,6 @@
   then show "a=b" using ih hl by auto
 qed (auto)
 
-lemma test4a:
-  shows "s \<leadsto> t \<Longrightarrow> (supp t) \<subseteq> ((supp s)::name set)"
-apply(induct s t rule: whr_def.induct)
-apply(insert test3b)
-apply(simp add: trm.supp supp_prod abs_supp)
-apply(auto simp add: trm.supp)
-done
-
-lemma test4b:
-  shows "s \<Down> t \<Longrightarrow> (supp t) \<subseteq> ((supp s)::name set)"
-apply(induct s t rule: whn_def.induct)
-apply(auto dest: test4a)
-done
 
 section {* Algorithmic Term Equivalence and Algorithmic Path Equivalence *}