--- a/Nominal/NewParser.thy Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/NewParser.thy Tue May 04 16:18:07 2010 +0200
@@ -159,8 +159,9 @@
end
*}
-text {* What does the prep_bn code do? Cezary's Function? *}
-
+(* strip_bn_fun takes a bn function defined by the user as a union or
+ append of elements and returns those elements together with bn functions
+ applied *)
ML {*
fun strip_bn_fun t =
case t of
@@ -258,6 +259,31 @@
end
*}
+lemma equivp_hack: "equivp x"
+sorry
+ML {*
+fun equivp_hack ctxt rel =
+let
+ val thy = ProofContext.theory_of ctxt
+ val ty = domain_type (fastype_of rel)
+ val cty = ctyp_of thy ty
+ val ct = cterm_of thy rel
+in
+ Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
+end
+*}
+
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
+ML {* val cheat_equivp = Unsynchronized.ref false *}
+ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
+ML {* val cheat_supp_eq = Unsynchronized.ref false *}
+
+ML {*
+fun remove_loop t =
+ let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end
+ handle TERM _ => @{thm eqTrueI} OF [t]
+*}
text {*
nominal_datatype2 does the following things in order:
@@ -324,31 +350,45 @@
29) prove supp = fv
*}
+ML {*
+(* for testing porposes - to exit the procedure early *)
+exception TEST of Proof.context
+
+val STEPS = 10
+*}
ML {*
fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
let
(* definition of the raw datatype and raw bn-functions *)
val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
- raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+ if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+ else raise TEST lthy
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
val {descr, sorts, ...} = dtinfo;
val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
- val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
+ val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr)
+ val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
- val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
- val inject = flat (map #inject dtinfos);
- val distincts = flat (map #distinct dtinfos);
- val rel_dtinfos = List.take (dtinfos, (length dts));
- val rel_distinct = map #distinct rel_dtinfos;
- val induct = #induct dtinfo;
- val exhausts = map #exhaust dtinfos;
+
+ (* what is the difference between raw_dt_names and all_full_tnames ? *)
+ (* what is the purpose of dtinfo and dtinfos ? *)
+ val _ = tracing ("raw_dt_names " ^ commas raw_dt_names)
+ val _ = tracing ("all_full_tnames " ^ commas all_full_tnames)
+
+ val inject_thms = flat (map #inject dtinfos);
+ val distinct_thms = flat (map #distinct dtinfos);
+ val rel_dtinfos = List.take (dtinfos, (length dts));
+ val rel_distinct = map #distinct rel_dtinfos; (* thm list list *)
+ val induct_thm = #induct dtinfo;
+ val exhaust_thms = map #exhaust dtinfos;
(* definitions of raw permutations *)
val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
- Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
+ if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
+ else raise TEST lthy1
val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
@@ -362,11 +402,18 @@
val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
(* definition of raw fv_functions *)
- val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+ val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
+ val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls)
+ val ((fv, fvbn), fv_def, lthy3a) =
+ if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
+ else raise TEST lthy3
+
(* definition of raw alphas *)
val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
- define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
+ if STEPS > 4 then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a
+ else raise TEST lthy3a
+
val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
@@ -379,22 +426,27 @@
((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
(* definition of raw_alpha_eq_iff lemmas *)
- val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
-
+ val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
+ val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
+ val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);
+
(* proving equivariance lemmas *)
val _ = warning "Proving equivariance";
- val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
- val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
- fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
+ val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
+ val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
+ fun alpha_eqvt_tac' _ =
+ if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
+ else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
- (* provind alpha equivalence *)
+ (* proving alpha equivalence *)
val _ = warning "Proving equivalence";
val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
- val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
+ val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6;
val alpha_equivp =
- build_equivps alpha_ts reflps alpha_induct
- inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
+ if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
+ else build_equivps alpha_ts reflps alpha_induct
+ inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6;
val qty_binds = map (fn (_, b, _, _) => b) dts;
val qty_names = map Name.of_binding qty_binds;
val qty_full_names = map (Long_Name.qualify thy_name) qty_names
@@ -403,8 +455,8 @@
val raw_consts =
flat (map (fn (i, (_, _, l)) =>
map (fn (cname, dts) =>
- Const (cname, map (typ_of_dtyp descr sorts) dts --->
- typ_of_dtyp descr sorts (DtRec i))) l) descr);
+ Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
+ Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
val _ = warning "Proving respects";
val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
@@ -412,8 +464,9 @@
fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
resolve_tac bns_rsp_pre' 1)) bns lthy8;
val bns_rsp = flat (map snd bns_rsp_pre);
- (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*)
- fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy
+
+ fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
+ else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
val (fv_rsp_pre, lthy10) = fold_map
(fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
@@ -421,11 +474,14 @@
val fv_rsp = flat (map snd fv_rsp_pre);
val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
(fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
+ fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
+ else
+ let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
- (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11
+ alpha_bn_rsp_tac) alpha_ts_bn lthy11
fun const_rsp_tac _ =
- let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
- in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+ let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a
+ in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
const_rsp_tac) raw_consts lthy11a
val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn)
@@ -445,7 +501,7 @@
fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
val _ = warning "Lifting induction";
val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
- val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct);
+ val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm);
fun note_suffix s th ctxt =
snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
fun note_simp_suffix s th ctxt =
@@ -463,7 +519,7 @@
val lthy17 = note_simp_suffix "bn" q_bn lthy16;
val _ = warning "Lifting eq-iff";
(*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
- val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
+ val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp
val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
@@ -487,11 +543,14 @@
val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
val (names, supp_eq_t) = supp_eq fv_alpha_all;
val _ = warning "Support Equations";
- val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
+ fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else
+ supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
+ val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>
+ let val _ = warning ("Support eqs failed") in [] end;
val lthy23 = note_suffix "supp" q_supp lthy22;
in
(0, lthy23)
-end
+end handle TEST ctxt => (0, ctxt)
*}
section {* Preparing and parsing of the specification *}
@@ -660,6 +719,7 @@
(main_parser >> nominal_datatype2_cmd)
*}
+(*
atom_decl name
nominal_datatype lam =
@@ -676,6 +736,10 @@
"bn (P1 x) = {atom x}"
| "bn (P2 p1 p2) = bn p1 \<union> bn p2"
+find_theorems Var_raw
+
+
+
thm lam_pt.bn
thm lam_pt.fv[simplified lam_pt.supp(1-2)]
thm lam_pt.eq_iff
@@ -740,7 +804,7 @@
thm ty_tys.fv[simplified ty_tys.supp]
thm ty_tys.eq_iff
-
+*)
(* some further tests *)