# HG changeset patch # User Cezary Kaliszyk # Date 1269428643 -3600 # Node ID 9db725590fe932b33578493b522d0d26db19c9fb # Parent 0d7d0b8adca56ae09dfe1e60d37e2b120a208ec8# Parent 17a2c6fddc0c15f3916b3a340234eee1b36826b7 merge diff -r 17a2c6fddc0c -r 9db725590fe9 Nominal/ExCoreHaskell.thy --- a/Nominal/ExCoreHaskell.thy Wed Mar 24 07:23:53 2010 +0100 +++ b/Nominal/ExCoreHaskell.thy Wed Mar 24 12:04:03 2010 +0100 @@ -4,8 +4,11 @@ (* core haskell *) -ML {* val _ = recursive := false *} - +ML {* val _ = recursive := false *} +ML {* val _ = cheat_bn_eqvt := true *} +ML {* val _ = cheat_bn_rsp := true *} +ML {* val _ = cheat_const_rsp := true *} +ML {* val _ = cheat_alpha_bn_rsp := true *} atom_decl var atom_decl tvar @@ -59,30 +62,31 @@ | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t and pat = K "char" "tvtk_lst" "tvck_lst" "vt_lst" +and vt_lst = + VTNil +| VTCons "var" "ty" "vt_lst" and tvtk_lst = TVTKNil | TVTKCons "tvar" "tkind" "tvtk_lst" and tvck_lst = TVCKNil | TVCKCons "tvar" "ckind" "tvck_lst" -and vt_lst = - VTNil -| VTCons "var" "ty" "vt_lst" binder bv :: "pat \ atom set" -(*and bv_vt :: "vt_lst \ atom set" +and bv_vt :: "vt_lst \ atom set" and bv_tvtk :: "tvtk_lst \ atom set" -and bv_tvck :: "tvck_lst \ atom set"*) +and bv_tvck :: "tvck_lst \ atom set" where - "bv (K s tvts tvcs vs) = {}" (*(bv_tvtk tvts) \ (bv_tvck tvcs) \ (bv_vt vs) *) -(*| "bv_vt VTNil = {}" + "bv (K s tvts tvcs vs) = (bv_tvtk tvts) \ (bv_tvck tvcs) \ (bv_vt vs)" +| "bv_vt VTNil = {}" | "bv_vt (VTCons v k t) = {atom v} \ bv_vt t" | "bv_tvtk TVTKNil = {}" | "bv_tvtk (TVTKCons v k t) = {atom v} \ bv_tvtk t" | "bv_tvck TVCKNil = {}" -| "bv_tvck (TVCKCons v k t) = {atom v} \ bv_tvck t"*) +| "bv_tvck (TVCKCons v k t) = {atom v} \ bv_tvck t" -thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_tvtk_lst_tvck_lst_vt_lst.fv +lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15) +lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] end diff -r 17a2c6fddc0c -r 9db725590fe9 Nominal/Fv.thy --- a/Nominal/Fv.thy Wed Mar 24 07:23:53 2010 +0100 +++ b/Nominal/Fv.thy Wed Mar 24 12:04:03 2010 +0100 @@ -278,8 +278,6 @@ end *} -ML AList.lookup - (* We assume no bindings in the type on which bn is defined *) (* TODO: currently works only with current fv_bn function *) ML {* @@ -296,8 +294,8 @@ fun fv_arg ((dt, x), arg_no) = let val ty = fastype_of x - val _ = tracing (PolyML.makestring args_in_bn); - val _ = tracing (PolyML.makestring bn_fvbn); +(* val _ = tracing ("B 1" ^ PolyML.makestring args_in_bn);*) +(* val _ = tracing ("B 2" ^ PolyML.makestring bn_fvbn);*) in case AList.lookup (op=) args_in_bn arg_no of SOME NONE => @{term "{} :: atom set"} @@ -420,7 +418,11 @@ "fv_" ^ name_of_typ (nth_dtyp i)) descr); val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; val fv_frees = map Free (fv_names ~~ fv_types); - val nr_bns = non_rec_binds bindsall; +(* TODO: We need a transitive closure, but instead we do this hack considering + all binding functions as recursive or not *) + val nr_bns = + if (non_rec_binds bindsall) = [] then [] + else map (fn (bn, _, _) => bn) bns; val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns; val fvbns = map snd bn_fv_bns; @@ -1089,8 +1091,11 @@ asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) *} diff -r 17a2c6fddc0c -r 9db725590fe9 Nominal/Parser.thy --- a/Nominal/Parser.thy Wed Mar 24 07:23:53 2010 +0100 +++ b/Nominal/Parser.thy Wed Mar 24 12:04:03 2010 +0100 @@ -286,13 +286,13 @@ end *} -(* This one is not needed for the proper examples *) ML {* val cheat_equivp = Unsynchronized.ref false *} - -(* These 4 are not needed any more *) -ML {* val cheat_fv_rsp = Unsynchronized.ref false *} +ML {* val cheat_bn_eqvt = Unsynchronized.ref false *} ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} +ML {* val cheat_bn_rsp = Unsynchronized.ref false *} +ML {* val cheat_fv_rsp = Unsynchronized.ref false *} +ML {* val cheat_const_rsp = Unsynchronized.ref false *} ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} ML {* fun map_option _ NONE = NONE @@ -345,6 +345,11 @@ ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn)) val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4 val _ = tracing "Proving equivariance"; + fun build_bv_eqvt simps inducts (t, n) ctxt = + build_eqvts Binding.empty [t] + (if !cheat_bn_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) + else build_eqvts_tac (nth inducts n) simps ctxt + ) ctxt val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; val fv_eqvt_tac = if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) @@ -384,8 +389,9 @@ val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); val _ = tracing "Proving respects"; val (bns_rsp_pre, lthy9) = fold_map ( - fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] - (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8; + fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => + if !cheat_bn_rsp then (Skip_Proof.cheat_tac thy) else + fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8; val bns_rsp = flat (map snd bns_rsp_pre); fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy else fvbv_rsp_tac alpha_induct fv_def lthy8 1; @@ -396,13 +402,19 @@ val fv_rsp = flat (map snd fv_rsp_pre); val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; - val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11; - fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 + fun const_rsp_tac _ = + if !cheat_const_rsp then Skip_Proof.cheat_tac thy + else let val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11 + in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] const_rsp_tac) raw_consts lthy11 - val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] - (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a + (fn _ => + if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy + else + let val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts + (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) in + asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end)) alpha_ts_bn lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; diff -r 17a2c6fddc0c -r 9db725590fe9 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Wed Mar 24 07:23:53 2010 +0100 +++ b/Nominal/Rsp.thy Wed Mar 24 12:04:03 2010 +0100 @@ -212,11 +212,6 @@ *} ML {* -fun build_bv_eqvt simps inducts (t, n) ctxt = - build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt -*} - -ML {* fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt = let val (fvs_alphas, ls) = split_list fv_alphas_lst;