nominal2: comparison Nominal/Nominal2.thy

equal deleted inserted replaced

-:add799cf0817
+:82e37a4595c7
 val (cnstr_head, cnstr_args) = strip_comb cnstr
 val rhs_elements = strip_bn_fun lthy cnstr_args rhs
 in
 (dt_index, (bn_fun, (cnstr_head, rhs_elements)))
 end
 fun order dts i ts =
 let
 val dt = nth dts i
 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt)
 val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts
 (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*)
 in
 ordered'
 end
 fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
 if null raw_bn_funs
 then ([], [], [], [], lthy)
 else
 let
 val raw_bn_info =
 prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
 in
 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
 end
 *}
 ML {*
 fun define_raw_dts dts bn_funs bn_eqs binds lthy =
 let
 |> uncurry drop
 (* definitions of raw permutations by primitive recursion *)
 val _ = warning "Definition of raw permutations";
 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
-if get_STEPS lthy0 > 1
+if get_STEPS lthy0 > 0
 then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0
 else raise TEST lthy0
 (* noting the raw permutations as eqvt theorems *)
 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
-(* definition of raw fv_functions *)
+(* definition of raw fv and bn functions *)
-val _ = warning "Definition of raw fv-functions";
+val _ = warning "Definition of raw fv- and bn-functions";
 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
-if get_STEPS lthy3 > 2
+if get_STEPS lthy3 > 1
 then define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs
 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
 else raise TEST lthy3
-val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) =
+(* defining the permute_bn functions *)
-if get_STEPS lthy3a > 3
+val (_, _, lthy3b) =
-then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses
+if get_STEPS lthy3a > 2
+then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info
 (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a
 else raise TEST lthy3a
+val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) =
+if get_STEPS lthy3b > 3
+then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses
+(raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
+else raise TEST lthy3b
 (* definition of raw alphas *)
 val _ = warning "Definition of alphas";
 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
-if get_STEPS lthy3b > 4
+if get_STEPS lthy3c > 4
-then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3b
+then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
-else raise TEST lthy3b
+else raise TEST lthy3c
 val alpha_tys = map (domain_type o fastype_of) alpha_trms
 (* definition of alpha-distinct lemmas *)
 val _ = warning "Distinct theorems";
 val alpha_distincts =

changeset 2560	82e37a4595c7
parent 2559	add799cf0817
child 2561	7926f1cb45eb