nominal2: comparison Nominal/Nominal2.thy

equal deleted inserted replaced

-:d0f83a35950e
+:9bd97ed202f7
 raw_size_thms = raw_size_thms}
 in
 (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_result, lthy1)
 end
 *}
+ML {*
+infix 1 ||>>> |>>>
+fun (x |>>> f) =
+let
+val (x', y') = f x
+in
+([x'], y')
+end
+fun (([], y) ||>>> f) = ([], y)
+| ((xs, y) ||>>> f) =
+let
+val (x', y') = f y
+in
+(xs @ [x'], y')
+end;
+(op ||>>)
+*}
 ML {*
 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
 let
 val _ = trace_msg (K "Defining raw permutations...")
 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = define_raw_perms raw_dt_info lthy0
 (* noting the raw permutations as eqvt theorems *)
-val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
+val lthy3 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a)
 val _ = trace_msg (K "Defining raw fv- and bn-functions...")
 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_inducts, lthy3a) =
 define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy3
 val _ = trace_msg (K "Lifting of theorems...")
 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
 prod.cases}
-val (((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), qbn_inducts),
+val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts,
-lthyA) =
+qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps,
+qalpha_refl_thms ], lthyB) =
 lthy9a
-|> lift_thms qtys [] alpha_distincts
+|>>> lift_thms qtys [] alpha_distincts
-||>> lift_thms qtys eq_iff_simps alpha_eq_iff
+||>>> lift_thms qtys eq_iff_simps alpha_eq_iff
-||>> lift_thms qtys [] raw_fv_defs
+||>>> lift_thms qtys [] raw_fv_defs
-||>> lift_thms qtys [] raw_bn_defs
+||>>> lift_thms qtys [] raw_bn_defs
-||>> lift_thms qtys [] raw_perm_simps
+||>>> lift_thms qtys [] raw_perm_simps
-||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
+||>>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
-||>> lift_thms qtys [] raw_bn_inducts
+||>>> lift_thms qtys [] raw_bn_inducts
+||>>> lift_thms qtys [] raw_size_eqvt
-val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) =
+||>>> lift_thms qtys [] [raw_induct_thm]
-lthyA
+||>>> lift_thms qtys [] raw_exhaust_thms
-|> lift_thms qtys [] raw_size_eqvt
+||>>> lift_thms qtys [] raw_size_thms
-||>> lift_thms qtys [] [raw_induct_thm]
+||>>> lift_thms qtys [] raw_perm_bn_simps
-||>> lift_thms qtys [] raw_exhaust_thms
+||>>> lift_thms qtys [] alpha_refl_thms
-||>> lift_thms qtys [] raw_size_thms
-||>> lift_thms qtys [] raw_perm_bn_simps
-||>> lift_thms qtys [] alpha_refl_thms
 val qinducts = Project_Rule.projections lthyB qinduct
 val _ = trace_msg (K "Proving supp lemmas and fs-instances...")
-val qsupports_thms =
+val qsupports_thms = prove_supports lthyB qperm_simps (flat qtrms)
-prove_supports lthyB qperm_simps (flat qtrms)
 (* finite supp lemmas *)
 val qfsupp_thms = prove_fsupp lthyB qtys qinduct qsupports_thms
 (* fs instances *)
 (constrs @ [(cname, cargs', mx)], sorts')
 end
 fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) =
 let
 val (constrs', sorts') =
 fold prep_constr constrs ([], sorts)
 val constr_trms' =
 map (mk_type tname (rev sorts')) constrs'

changeset 2959	9bd97ed202f7
parent 2957	01ff621599bc
child 2962	7a24d827cba9