--- 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 \<Rightarrow> atom set"
-(*and bv_vt :: "vt_lst \<Rightarrow> atom set"
+and bv_vt :: "vt_lst \<Rightarrow> atom set"
and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set"
-and bv_tvck :: "tvck_lst \<Rightarrow> atom set"*)
+and bv_tvck :: "tvck_lst \<Rightarrow> atom set"
where
- "bv (K s tvts tvcs vs) = {}" (*(bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs) *)
-(*| "bv_vt VTNil = {}"
+ "bv (K s tvts tvcs vs) = (bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs)"
+| "bv_vt VTNil = {}"
| "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t"
| "bv_tvtk TVTKNil = {}"
| "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t"
| "bv_tvck TVCKNil = {}"
-| "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"*)
+| "bv_tvck (TVCKCons v k t) = {atom v} \<union> 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
--- 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})
*}
--- 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;
--- 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;