# HG changeset patch # User Christian Urban # Date 1285190245 -7200 # Node ID 37941f58ab8f8d52fa14c8fc22dd61dd18268f49 # Parent 0c2eb0ed30a04cf870ee887b81fe5e5be88819c3 removed dead code diff -r 0c2eb0ed30a0 -r 37941f58ab8f Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Wed Sep 22 18:13:26 2010 +0200 +++ b/Nominal/Nominal2.thy Wed Sep 22 23:17:25 2010 +0200 @@ -563,7 +563,7 @@ val _ = warning "Proving Equality between fv and supp" val qfv_supp_thms = if get_STEPS lthy > 31 - then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs + then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC else [] diff -r 0c2eb0ed30a0 -r 37941f58ab8f Nominal/nominal_dt_supp.ML --- a/Nominal/nominal_dt_supp.ML Wed Sep 22 18:13:26 2010 +0200 +++ b/Nominal/nominal_dt_supp.ML Wed Sep 22 23:17:25 2010 +0200 @@ -13,7 +13,7 @@ val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> local_theory -> local_theory - val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> thm list -> + val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list end @@ -155,14 +155,12 @@ fun q_tac msg i = if true then print_tac ("qtest: " ^ msg) else all_tac -fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps +fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps fv_bn_eqvts qinduct bclausess ctxt = let val goals1 = map mk_fvs_goals fvs val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns - - fun tac ctxt = SUBGOAL (fn (goal, i) => let @@ -190,55 +188,6 @@ induct_prove qtys (goals1 @ goals2) qinduct tac ctxt end -(* - fun fv_tac bclauses ctxt = - SOLVED' (EVERY' [ - (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ " with " ^ (@{make_string} bclauses))), - TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), - p_tac "A", - TRY o EVERY' (mk_supp_abs_tac ctxt bclauses), - p_tac "B", - TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), - p_tac "C", - TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], - p_tac "D", - TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), - p_tac "E", - TRY o asm_full_simp_tac (add_ss thms3), - p_tac "F", - TRY o simp_tac (add_ss thms2), - p_tac "G", - TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), - p_tac "H", - (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i)) - ]) - - fun fv_tacs ctxt = map (fv_tac ctxt) bclausess - (*fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps*) -*) - -(* - fun bn_tac ctxt bn_simp = - SOLVED' (EVERY' [ - (fn i => print_tac ("BN Goal: " ^ string_of_int i)), - TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), - q_tac "A", - TRY o mk_bn_supp_abs_tac bn_simp, - q_tac "B", - TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), - q_tac "C", - TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], - q_tac "D", - TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), - q_tac "E", - TRY o asm_full_simp_tac (add_ss thms3), - q_tac "F", - TRY o simp_tac (add_ss thms2), - q_tac "G", - TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), - (fn i => print_tac ("finished with BN Goal: " ^ string_of_int i)) - ]) -*) end (* structure *)