# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268394155 -3600
# Node ID d2d8020cd20aeb65e5a49a6be93315cae633d2cb
# Parent  7a9217a7f68166d4468aa62c78f7881b462aa467
Still don't know how to prove supp=fv for simplest Let...

diff -r 7a9217a7f681 -r d2d8020cd20a Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 20:49:31 2010 +0100
+++ b/Nominal/Parser.thy	Fri Mar 12 12:42:35 2010 +0100
@@ -510,7 +510,7 @@
   fun prep_bn env bn_str =
     case (Syntax.read_term lthy bn_str) of
        Free (x, _) => (NONE, env_lookup env x)
-     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), false), env_lookup env x)
+     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
   fun prep_typ env (i, opt_name) = 
diff -r 7a9217a7f681 -r d2d8020cd20a Nominal/Term1.thy
--- a/Nominal/Term1.thy	Thu Mar 11 20:49:31 2010 +0100
+++ b/Nominal/Term1.thy	Fri Mar 12 12:42:35 2010 +0100
@@ -146,7 +146,7 @@
 
 instance trm1 and bp :: fs
 apply default
-apply (rule rtrm1_bp_fs)+
+apply (simp_all add: rtrm1_bp_fs)
 done
 
 lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp"
@@ -220,25 +220,22 @@
   shows "\<lbrakk>fv_trm1 trm11 = supp trm11; fv_trm1 trm12 = supp trm12\<rbrakk>
        \<Longrightarrow> supp (Lt1 bp trm11 trm12) = fv_trm1 (Lt1 bp trm11 trm12)"
 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv])
+apply simp
 apply(fold supp_Abs)
 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric])
-apply(simp (no_asm) only: supp_def permute_set_eq permute_trm1 alpha1_INJ)
-apply(simp only: ex_out Collect_neg_conj permute_ABS Abs_eq_iff)
-(*apply(simp only: alpha_bp_eq fv_eq_bv)*)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: permute_set_eq permute_trm1)
+apply(simp only: alpha1_INJ)
+apply(simp only: ex_out)
+apply(simp only: Collect_neg_conj)
+apply(simp only: permute_ABS)
+apply(simp only: Abs_eq_iff)
 apply(simp only: alpha_gen fv_eq_bv supp_Pair)
+apply(simp only: inf_or[symmetric])
+apply(simp only: Collect_disj_eq)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric])
-apply(simp only: Un_left_commute)
-apply simp
-apply(simp add: fresh_star_def) apply(fold fresh_star_def)
 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric])
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
-apply(simp only: Un_assoc[symmetric])
-apply(simp only: Un_commute)
-apply(simp only: Un_left_commute)
-apply(simp only: Un_assoc[symmetric])
-apply(simp only: Un_commute)
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
-apply(simp only: Collect_disj_eq[symmetric] inf_or)
 apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric])
 sorry