--- a/Nominal/nominal_dt_rawperm.ML Fri Sep 10 09:17:40 2010 +0800
+++ b/Nominal/nominal_dt_rawperm.ML Sat Sep 11 05:56:49 2010 +0800
@@ -21,109 +21,109 @@
(** proves the two pt-type class properties **)
fun prove_permute_zero induct perm_defs perm_fns lthy =
-let
- val perm_types = map (body_type o fastype_of) perm_fns
- val perm_indnames = Datatype_Prop.make_tnames perm_types
+ let
+ val perm_types = map (body_type o fastype_of) perm_fns
+ val perm_indnames = 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))
+ 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 goals =
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
- val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
+ val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
- val tac = (Datatype_Aux.indtac induct perm_indnames
- THEN_ALL_NEW asm_simp_tac simps) 1
-in
- Goal.prove lthy perm_indnames [] goals (K tac)
- |> Datatype_Aux.split_conj_thm
-end
+ val tac = (Datatype_Aux.indtac induct perm_indnames
+ THEN_ALL_NEW asm_simp_tac simps) 1
+ in
+ Goal.prove lthy perm_indnames [] goals (K tac)
+ |> Datatype_Aux.split_conj_thm
+ end
fun prove_permute_plus induct perm_defs perm_fns lthy =
-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
+ 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
- fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq
+ 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 =
- HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
- (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
+ val goals =
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
- val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
+ val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
- val tac = (Datatype_Aux.indtac induct perm_indnames
- THEN_ALL_NEW asm_simp_tac simps) 1
-in
- Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
- |> Datatype_Aux.split_conj_thm
-end
+ val tac = (Datatype_Aux.indtac induct perm_indnames
+ THEN_ALL_NEW asm_simp_tac simps) 1
+ in
+ Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
+ |> Datatype_Aux.split_conj_thm
+ end
fun mk_perm_eq ty_perm_assoc cnstr =
-let
- fun lookup_perm p (ty, arg) =
- case (AList.lookup (op=) ty_perm_assoc ty) of
- SOME perm => perm $ p $ arg
- | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg
+ let
+ fun lookup_perm p (ty, arg) =
+ case (AList.lookup (op=) ty_perm_assoc ty) of
+ SOME perm => perm $ p $ arg
+ | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg
- val p = Free ("p", @{typ perm})
- val (arg_tys, ty) =
- fastype_of cnstr
- |> strip_type
+ 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 args = map Free (arg_names ~~ arg_tys)
+ val arg_names = Name.variant_list ["p"] (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 lhs = lookup_perm p (ty, list_comb (cnstr, args))
+ val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-in
- (Attrib.empty_binding, eq)
-end
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ in
+ (Attrib.empty_binding, eq)
+ end
fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy =
-let
- val perm_fn_names = full_ty_names
- |> map Long_Name.base_name
- |> map (prefix "permute_")
+ let
+ val perm_fn_names = full_ty_names
+ |> map Long_Name.base_name
+ |> map (prefix "permute_")
- val perm_fn_types = map perm_ty tys
- 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_fn_types = map perm_ty tys
+ 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 (tys ~~ perm_fn_frees)) constrs
+ val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
- fun tac _ (_, _, simps) =
- Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
+ fun tac _ (_, _, simps) =
+ Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
- fun morphism phi (fvs, dfs, simps) =
- (map (Morphism.term phi) fvs,
- map (Morphism.thm phi) dfs,
- map (Morphism.thm phi) 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 (full_ty_names, tvs, @{sort pt})
- |> Primrec.add_primrec perm_fn_binds perm_eqs
+ val ((perm_funs, perm_eq_thms), lthy') =
+ lthy
+ |> Local_Theory.exit_global
+ |> Class.instantiation (full_ty_names, tvs, @{sort pt})
+ |> Primrec.add_primrec perm_fn_binds perm_eqs
- val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
- val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy'
-in
- lthy'
- |> Class.prove_instantiation_exit_result morphism tac
- (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
- ||> Named_Target.theory_init
-end
+ val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
+ val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy'
+ in
+ lthy'
+ |> Class.prove_instantiation_exit_result morphism tac
+ (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
+ ||> Named_Target.theory_init
+ end
end (* structure *)