nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:b2e1a7b83e05
+:67370521c09c
 val raw_bn_induct = (the inducts)
 val raw_bn_eqs = the simps
 val raw_bn_info =
-prep_bn_info lthy raw_dt_names raw_dts fs (map prop_of raw_bn_eqs)
+prep_bn_info lthy raw_dt_names raw_dts fs (map Thm.prop_of raw_bn_eqs)
 in
 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
 end
 | Res => (fold_union, bind_set)
 in
 binders
 |> map (bind_fn lthy args)
 |> split_list
-|> pairself combine_fn
+|> apply2 combine_fn
 end
 val t1 = map (mk_fv_body fv_map args) bodies
 val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders
 in
 | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
 end
 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses =
 let
-val arg_names = Datatype_Prop.make_tnames arg_tys
+val arg_names = Old_Datatype_Prop.make_tnames arg_tys
 val args = map Free (arg_names ~~ arg_tys)
 val fv = lookup fv_map ty
 val lhs = fv $ list_comb (constr, args)
 val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses
 val rhs = fold_union rhs_trms
 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
 let
-val arg_names = Datatype_Prop.make_tnames arg_tys
+val arg_names = Old_Datatype_Prop.make_tnames arg_tys
 val args = map Free (arg_names ~~ arg_tys)
 val fv_bn = lookup fv_bn_map bn_trm
 val lhs = fv_bn $ list_comb (constr, args)
 val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses
 val rhs = fold_union rhs_trms
 fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) =
 let
 val p = Free ("p", @{typ perm})
-val arg_names = Datatype_Prop.make_tnames arg_tys
+val arg_names = Old_Datatype_Prop.make_tnames arg_tys
 val args = map Free (arg_names ~~ arg_tys)
 val perm_bn = lookup perm_bn_map bn_trm
 val lhs = perm_bn $ p $ list_comb (constr, args)
 val rhs = list_comb (constr, map_index (mk_perm_bn_eq_rhs p perm_bn_map bn_args) args)
 in
 (** proves the two pt-type class properties **)
 fun prove_permute_zero induct perm_defs perm_fns ctxt =
 let
 val perm_types = map (body_type o fastype_of) perm_fns
-val perm_indnames = Datatype_Prop.make_tnames perm_types
+val perm_indnames = Old_Datatype_Prop.make_tnames perm_types
 fun single_goal ((perm_fn, T), x) =
 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
 val goals =
 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
 val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs)
-val tac = (Datatype_Aux.ind_tac induct perm_indnames
+val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames
 THEN_ALL_NEW asm_simp_tac simpset) 1
 in
 Goal.prove ctxt perm_indnames [] goals (K tac)
-|> Datatype_Aux.split_conj_thm
+|> Old_Datatype_Aux.split_conj_thm
 end
 fun prove_permute_plus induct perm_defs perm_fns ctxt =
 let
 val p = Free ("p", @{typ perm})
 val q = Free ("q", @{typ perm})
 val perm_types = map (body_type o fastype_of) perm_fns
-val perm_indnames = Datatype_Prop.make_tnames perm_types
+val perm_indnames = Old_Datatype_Prop.make_tnames perm_types
 fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq
 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
 val goals =
 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
 (* FIXME proper goal context *)
 val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs)
-val tac = (Datatype_Aux.ind_tac induct perm_indnames
+val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames
 THEN_ALL_NEW asm_simp_tac simpset) 1
 in
 Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (K tac)
-|> Datatype_Aux.split_conj_thm
+|> Old_Datatype_Aux.split_conj_thm
 end
 fun mk_perm_eq ty_perm_assoc cnstr =
 let
 val p = Free ("p", @{typ perm})
 val (arg_tys, ty) =
 fastype_of cnstr
 |> strip_type
-val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
+val arg_names = Name.variant_list ["p"] (Old_Datatype_Prop.make_tnames arg_tys)
 val args = map Free (arg_names ~~ arg_tys)
 val lhs = lookup_perm p (ty, list_comb (cnstr, args))
 val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
 val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names
 val perm_eqs = map (mk_perm_eq (raw_tys ~~ perm_fn_frees)) (flat raw_all_cns)
-fun tac _ (_, _, simps) =
+fun tac ctxt (_, _, simps) =
-Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
+Class.intro_classes_tac ctxt [] THEN ALLGOALS (resolve_tac ctxt simps)
 fun morphism phi (fvs, dfs, simps) =
 (map (Morphism.term phi) fvs,
 map (Morphism.thm phi) dfs,
 map (Morphism.thm phi) simps);
 val ((perm_funs, perm_eq_thms), lthy') =
 lthy
 |> Local_Theory.exit_global
 |> Class.instantiation (raw_dt_names, raw_ty_args, @{sort pt})
-|> Primrec.add_primrec perm_fn_binds perm_eqs
+|> BNF_LFP_Compat.primrec perm_fn_binds perm_eqs
 val perm_zero_thms = prove_permute_zero raw_induct_thm perm_eq_thms perm_funs lthy'
 val perm_plus_thms = prove_permute_plus raw_induct_thm perm_eq_thms perm_funs lthy'
 in
 lthy'
 THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps (prems @ [eqvt_apply_sym]))))
 fun prove_eqvt_tac insts ind_thms const_names simps ctxt =
 HEADGOAL
 (Object_Logic.full_atomize_tac ctxt
-THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms))
+THEN' (DETERM o (Induct_Tacs.induct_tac ctxt insts (SOME ind_thms)))
 THEN_ALL_NEW  subproof_tac const_names simps ctxt)
 fun mk_eqvt_goal pi const arg =
 let
 val lhs = mk_perm pi (const $ arg)
 val arg_tys =
 consts
 |> map fastype_of
 |> map domain_type
 val (arg_names, ctxt'') =
-Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt'
+Variable.variant_fixes (Old_Datatype_Prop.make_tnames arg_tys) ctxt'
 val args = map Free (arg_names ~~ arg_tys)
 val goals = map2 (mk_eqvt_goal p) consts args
 val insts = map (single o SOME) arg_names
 val const_names = map (fst o dest_Const) consts
 in
-Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} =>
+Goal.prove_common ctxt'' NONE [] [] goals (fn {context, ...} =>
 prove_eqvt_tac insts ind_thms const_names simps context)
 |> Proof_Context.export ctxt'' ctxt
 end

changeset 3239	67370521c09c
parent 3226	780b7a2c50b6
child 3243	c4f31f1564b7