# HG changeset patch # User Christian Urban # Date 1269009839 -3600 # Node ID 50838e25f73c1f0043148b55cf34dc4a0cdc4902 # Parent 66d388a84e3cc008cef567c3317bef7afec5bd74# Parent 74888979e9cd70d2953e0014a014fcf5c427841a merged diff -r 66d388a84e3c -r 50838e25f73c Nominal/Fv.thy --- a/Nominal/Fv.thy Fri Mar 19 15:43:43 2010 +0100 +++ b/Nominal/Fv.thy Fri Mar 19 15:43:59 2010 +0100 @@ -908,7 +908,7 @@ fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW ( rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set - supp_fmap_atom finite_insert finite.emptyI finite_Un}) + supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp}) *} ML {* diff -r 66d388a84e3c -r 50838e25f73c Nominal/LFex.thy --- a/Nominal/LFex.thy Fri Mar 19 15:43:43 2010 +0100 +++ b/Nominal/LFex.thy Fri Mar 19 15:43:59 2010 +0100 @@ -8,8 +8,6 @@ ML {* val _ = cheat_fv_rsp := false *} ML {* val _ = cheat_const_rsp := false *} ML {* val _ = cheat_equivp := false *} -ML {* val _ = cheat_fv_eqvt := false *} -ML {* val _ = cheat_alpha_eqvt := false *} nominal_datatype kind = Type diff -r 66d388a84e3c -r 50838e25f73c Nominal/Parser.thy --- a/Nominal/Parser.thy Fri Mar 19 15:43:43 2010 +0100 +++ b/Nominal/Parser.thy Fri Mar 19 15:43:59 2010 +0100 @@ -271,9 +271,9 @@ ML {* val cheat_equivp = Unsynchronized.ref true *} -(* Fixes for these 2 are known *) -ML {* val cheat_fv_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *) -ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *) +(* These 2 are not needed any more *) +ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} +ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} ML {* @@ -408,8 +408,8 @@ val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; val _ = tracing "Finite Support"; - val supports = map (prove_supports lthy20 q_perm) consts handle _ => [] - val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys) handle _ => [] + val supports = map (prove_supports lthy20 q_perm) consts; + val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys); val thy3 = Local_Theory.exit_global lthy20; val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) diff -r 66d388a84e3c -r 50838e25f73c Nominal/Test.thy --- a/Nominal/Test.thy Fri Mar 19 15:43:43 2010 +0100 +++ b/Nominal/Test.thy Fri Mar 19 15:43:59 2010 +0100 @@ -6,13 +6,6 @@ atom_decl name -(* maybe should be added to Infinite.thy *) -lemma infinite_Un: - shows "infinite (S \ T) \ infinite S \ infinite T" - by simp - -ML {* val _ = cheat_alpha_eqvt := false *} -ML {* val _ = cheat_fv_eqvt := false *} ML {* val _ = recursive := false *} nominal_datatype lm = @@ -247,6 +240,11 @@ thm lam'_bp'.distinct ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} +lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \ supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" +apply (simp add: supp_Abs supp_Pair) +apply blast +done + lemma supp_fv': shows "supp t = fv_lam' t" and "supp bp = fv_bp' bp" @@ -439,7 +437,7 @@ VarTS "name" | FunTS "t" "t" and tyS = - All xs::"name set" ty::"t" bind xs in ty + All xs::"name fset" ty::"t" bind xs in ty thm t_tyS.fv thm t_tyS.eq_iff @@ -480,16 +478,16 @@ apply(simp only: infinite_Un) apply(simp only: Collect_disj_eq) (* All case *) -apply(rule_tac t="supp (All fun t)" and s="supp (Abs (atom ` fun) t)" in subst) +apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst) apply(simp (no_asm) only: supp_def) apply(simp only: t_tyS.perm) apply(simp only: permute_ABS) apply(simp only: t_tyS.eq_iff) apply(simp only: Abs_eq_iff) -apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw) +apply(simp only: eqvts) apply(simp only: alpha_gen) apply(simp only: supp_eqvt[symmetric]) -apply(simp only: eqvts) +apply(simp only: eqvts eqvts_raw) apply(rule trans) apply(rule finite_supp_Abs) apply(simp add: finite_fv_t_tyS) @@ -570,6 +568,27 @@ thm trm5_lts.induct thm trm5_lts.distinct +lemma + shows "fv_trm5 t = supp t" + and "fv_lts l = supp l \ fv_bv5 l = {a. infinite {b. \alpha_bv5 ((a \ b) \ l) l}}" +apply(induct t and l rule: trm5_lts.inducts) +apply(simp_all only: trm5_lts.fv) +apply(simp_all only: supp_Abs[symmetric]) +(*apply(simp_all only: supp_abs_sum)*) +apply(simp_all (no_asm) only: supp_def) +apply(simp_all only: trm5_lts.perm) +apply(simp_all only: permute_ABS) +apply(simp_all only: trm5_lts.eq_iff Abs_eq_iff) +(*apply(simp_all only: alpha_gen2)*) +apply(simp_all only: alpha_gen) +apply(simp_all only: eqvts[symmetric] supp_Pair) +apply(simp_all only: eqvts Pair_eq) +apply(simp_all only: supp_at_base[symmetric,simplified supp_def]) +apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric]) +apply(simp_all only: de_Morgan_conj[symmetric]) +apply simp_all +done + (* example from my PHD *) atom_decl coname diff -r 66d388a84e3c -r 50838e25f73c Nominal/TySch.thy --- a/Nominal/TySch.thy Fri Mar 19 15:43:43 2010 +0100 +++ b/Nominal/TySch.thy Fri Mar 19 15:43:59 2010 +0100 @@ -7,8 +7,6 @@ ML {* val _ = cheat_fv_rsp := false *} ML {* val _ = cheat_const_rsp := false *} ML {* val _ = cheat_equivp := false *} -ML {* val _ = cheat_fv_eqvt := false *} -ML {* val _ = cheat_alpha_eqvt := false *} nominal_datatype t = Var "name"