nominal2: comparison Nominal/NewParser.thy

equal deleted inserted replaced

-:74bd7bfb484b
+:837b889fcf59
 in
 map (map (map rawify_bclause)) bclauses
 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
 Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
 | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
 ||>> pair raw_bclauses
 ||>> pair raw_bns
 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:
 Parser.thy/raw_nominal_decls
 raw_nominal_decls dts bn_funs bn_eqs bclauses 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 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_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
 ((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_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
+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 *)
 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 alpha_eq_iff_simp lthy6;
 val alpha_equivp =
-build_equivps alpha_ts reflps alpha_induct
+if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
-inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
+else build_equivps alpha_ts reflps alpha_induct
+inject alpha_eq_iff_simp distincts 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
 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
 val raw_consts =
 flat (map (fn (i, (_, _, l)) =>
 map (fn (cname, dts) =>
-Const (cname, map (typ_of_dtyp descr sorts) dts --->
+Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
-typ_of_dtyp descr sorts (DtRec i))) l) descr);
+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;
 val (bns_rsp_pre, lthy9) = fold_map (
 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]
 (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) (fv @ fvbn) lthy9;
 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 exhausts 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
+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 (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+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)
 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
 val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
 val lthy16 = note_simp_suffix "fv" q_fv lthy15;
 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
 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;
 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
 val lthy22 = Class.prove_instantiation_instance tac lthy21
 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
 *}
 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
 (main_parser >> nominal_datatype2_cmd)
 *}
-atom_decl name
+(*atom_decl name
 nominal_datatype lam =
 Var name
 | App lam lam
 | Lam x::name t::lam  bind_set x in t
 Al xs::"name fset" t::"ty" bind_res xs in t
 thm ty_tys.fv[simplified ty_tys.supp]
 thm ty_tys.eq_iff
+*)
 (* some further tests *)
 (*
 nominal_datatype ty2 =

changeset 2034	837b889fcf59
parent 2027	68b2d2d7b4ed
child 2035	3622cae9b10e