# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263492188 -3600
# Node ID 99e811fc1366ba956857eec9125ce8009ef7ae61
# Parent  6a8858ba01f67d5267bbb054f4c1374e547fe38c
a few more lemmas...except supp of lambda-abstractions

diff -r 6a8858ba01f6 -r 99e811fc1366 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Thu Jan 14 18:41:50 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 19:03:08 2010 +0100
@@ -241,6 +241,33 @@
   "(Var a = Var b) = (a = b)"
   by (lifting rvar_inject)
 
+
+lemma app_inject: 
+  "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
+sorry
+
+lemma var_supp1:
+  shows "(supp (Var a)) = ((supp a)::name set)"
+apply(simp add: supp_def pi_var1 var_inject)
+done
+
+lemma var_supp:
+  shows "(supp (Var a)) = {a::name}"
+using var_supp1
+apply(simp add: supp_atm)
+done
+
+lemma app_supp:
+  shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)"
+apply(simp only: supp_def pi_app app_inject)
+apply(simp add: Collect_imp_eq Collect_neg_eq)
+done
+
+lemma lam_supp:
+  shows "supp (Lam x t) = ((supp ([x].t))::name set)"
+apply(simp add: supp_def pi_lam)
+sorry
+
 lemma lam_induct:
   "\<lbrakk>\<And>name. P (Var name);
     \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
@@ -250,15 +277,33 @@
 
 instance lam::pt_name
 apply(default)
-sorry
+apply(induct_tac x rule: lam_induct)
+apply(simp add: pi_var1)
+apply(simp add: pi_app)
+apply(simp add: pi_lam)
+apply(induct_tac x rule: lam_induct)
+apply(simp add: pi_var1 pt_name2)
+apply(simp add: pi_app)
+apply(simp add: pi_lam pt_name2)
+apply(induct_tac x rule: lam_induct)
+apply(simp add: pi_var1 pt_name3)
+apply(simp add: pi_app)
+apply(simp add: pi_lam pt_name3)
+done
 
 instance lam::fs_name
 apply(default)
+apply(induct_tac x rule: lam_induct)
+apply(simp add: var_supp)
+apply(simp add: app_supp)
 sorry
 
 lemma fresh_lam:
   "(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)"
-sorry
+apply(simp add: fresh_def)
+apply(simp add: lam_supp abs_supp)
+apply(auto)
+done
 
 lemma lam_induct_strong:
   fixes a::"'a::fs_name"