nominal2: comparison Nominal/NewParser.thy

equal deleted inserted replaced

-:c39d4fe31100
+:871d8a5e0c67
 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
 *}
 ML {*
+(* exports back the results *)
 fun add_primrec_wrapper funs eqs lthy =
-if null funs then (([], []), lthy)
+if null funs then ([], [], lthy)
 else
 let
 val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs
 val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs
 val ((funs'', eqs''), lthy') = Primrec.add_primrec funs' eqs' lthy
 val phi = ProofContext.export_morphism lthy' lthy
 in
-((map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs''), lthy')
+(map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs'', lthy')
 end
 *}
 ML {*
 fun add_datatype_wrapper dt_names dts =
 in
 map (map (map rawify_bclause)) bclauses
 end
 *}
-(* strip_bn_fun takes a bn function defined by the user as a union or
+(* strip_bn_fun takes a rhs of a bn function: this can only contain unions or
-append of elements and returns those elements together with bn functions
+appends of elements; in case of recursive calls it retruns also the applied
-applied *)
+bn function *)
 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
 in
 ordered'
 end
 *}
-ML {* add_primrec_wrapper *}
 ML {*
 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
 let
 val thy = ProofContext.theory_of lthy
 val thy_name = Context.theory_name thy
 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
 (bn_fun_strs ~~ bn_fun_strs')
 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs
 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds
 val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
 val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
-val ((raw_bn_funs, raw_bn_eqs), lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
+val (raw_bn_funs, raw_bn_eqs, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
 val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
 in
 fun get_STEPS ctxt = Config.get ctxt STEPS
 *}
 setup STEPS_setup
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
-(* definition of the raw datatype and raw bn-functions *)
+(* definition of the raw datatypes and raw bn-functions *)
 val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) =
 if get_STEPS lthy > 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 dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names)
-val {descr, sorts, ...} = dtinfo;
+val {descr, sorts, ...} = dtinfo
-val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
+val all_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 all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
+val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames
-val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) 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) =
+val ((perms, raw_perm_defs, raw_perm_simps), lthy2) =
-if get_STEPS lthy > 2
+if get_STEPS lthy1 > 2
 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
 else raise TEST lthy1
 val (_, lthy2a) = Local_Theory.note ((Binding.empty,
-[Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2;
+[Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_defs) lthy2;
 val thy = Local_Theory.exit_global lthy2a;
 val thy_name = Context.theory_name thy
 (* definition of raw fv_functions *)
 val lthy3 = Theory_Target.init NONE thy;
 val raw_bn_funs = map (fn (f, _, _) => f) raw_bns;
 val ((fv, fvbn), fv_def, lthy3a) =
-if get_STEPS lthy > 3
+if get_STEPS lthy2 > 3
 then define_raw_fv descr sorts raw_bns raw_bclauses lthy3
 else raise TEST lthy3
 (* definition of raw alphas *)
 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_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
+val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4
-val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
+val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5
 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
 (* 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;
 else build_equivps alpha_ts reflps alpha_induct
 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a;
 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 lthy6a;
+val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts_nobn alpha_equivp lthy6a;
 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 (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
 [Attrib.internal (K (Rule_Cases.case_names constr_names))]),
 [Rule_Cases.name constr_names q_induct]) lthy13;
 val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
-val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
+val q_perm = map (lift_thm qtys lthy14) raw_perm_defs;
 val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
 val q_fv = map (lift_thm qtys lthy15) fv_def;
 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;

changeset 2143	871d8a5e0c67
parent 2142	c39d4fe31100
child 2144	e900526e95c4