nominal2: comparison Nominal/NewParser.thy

equal deleted inserted replaced

-:6800fcaafa2a
+:73c50e913db6
 28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
 Equivp.thy/supp_eq
 29) prove supp = fv
 *}
+ML {*
+(* for testing porposes - to exit the procedure early *)
+exception TEST of Proof.context
+val STEPS = 3
+*}
 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 => 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);
+(* what is the difference between raw_dt_names and all_full_tnames ? *)
-val rel_dtinfos = List.take (dtinfos, (length dts));
+(* what is the purpose of dtinfo and dtinfos ? *)
-val rel_distinct = map #distinct rel_dtinfos;
+val _ = tracing ("raw_dt_names " ^ commas raw_dt_names)
-val induct = #induct dtinfo;
+val _ = tracing ("all_full_tnames " ^ commas all_full_tnames)
-val exhausts = map #exhaust dtinfos;
+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_thms = #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 (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);
 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
 val lthy3 = Theory_Target.init NONE thy;
 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 dtinfo 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);
 val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
 (rel_distinct ~~ alpha_ts_nobn));
 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 = 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 (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thms (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
+val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thms (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_simp lthy6;
+val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thms alpha_eq_iff_simp lthy6;
 val alpha_equivp =
 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
 else build_equivps alpha_ts reflps alpha_induct
-inject alpha_eq_iff_simp distincts alpha_cases alpha_eqvt lthy6;
+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
 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 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;
+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]
 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_simp alpha_ts_bn lthy11a
 in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
 val lthy13 = Theory_Target.init NONE thy';
 val q_name = space_implode "_" qty_names;
 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_thms);
 fun note_suffix s th ctxt =
 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
 fun note_simp_suffix s th ctxt =
 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
 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 *}
 ML {*
 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
 (main_parser >> nominal_datatype2_cmd)
 *}
+(*
 atom_decl name
 nominal_datatype lam =
 Var name
 | App lam lam
 bn::"pt \<Rightarrow> atom set"
 where
 "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
 thm lam_pt.induct
 thm lam_pt.perm

changeset 2046	73c50e913db6
parent 2037	205ac2d13339
child 2047	31ba33a199c7