# HG changeset patch # User Christian Urban # Date 1289524853 0 # Node ID 82e37a4595c78ced2c2134cee995627ba9822afa # Parent add799cf08177178f38a6ca45a1f3286d2fd713c automated permute_bn functions (raw ones first) diff -r add799cf0817 -r 82e37a4595c7 Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Wed Nov 10 13:46:21 2010 +0000 +++ b/Nominal-General/Nominal2_Base.thy Fri Nov 12 01:20:53 2010 +0000 @@ -142,6 +142,7 @@ "Rep_perm p1 = Rep_perm p2 \ p1 = p2" by (simp add: fun_eq_iff Rep_perm_inject [symmetric]) +instance perm :: size .. subsection {* Permutations form a group *} diff -r add799cf0817 -r 82e37a4595c7 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Wed Nov 10 13:46:21 2010 +0000 +++ b/Nominal-General/nominal_library.ML Fri Nov 12 01:20:53 2010 +0000 @@ -258,22 +258,37 @@ fun prove_termination_tac size_simps ctxt = let - fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) = - SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT) - | mk_size_measure T = size_const T + val natT = @{typ nat} + fun prod_size_const fT sT = + let + val fT_fun = fT --> natT + val sT_fun = sT --> natT + val prodT = Type (@{type_name prod}, [fT, sT]) + in + Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT) + end + + fun mk_size_measure T = + case T of + (Type (@{type_name Sum_Type.sum}, [fT, sT])) => + SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT) + | (Type (@{type_name Product_Type.prod}, [fT, sT])) => + prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT) + | _ => size_const T fun mk_measure_trm T = HOLogic.dest_setT T |> fst o HOLogic.dest_prodT |> mk_size_measure - |> curry (op $) (Const (@{const_name measure}, dummyT)) + |> curry (op $) (Const (@{const_name "measure"}, dummyT)) |> Syntax.check_term ctxt - + val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral - zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals + zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps + val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals in Function_Relation.relation_tac ctxt mk_measure_trm - THEN_ALL_NEW simp_tac ss + THEN_ALL_NEW simp_tac ss' end fun prove_termination size_simps ctxt = diff -r add799cf0817 -r 82e37a4595c7 Nominal/Ex/Foo1.thy --- a/Nominal/Ex/Foo1.thy Wed Nov 10 13:46:21 2010 +0000 +++ b/Nominal/Ex/Foo1.thy Fri Nov 12 01:20:53 2010 +0000 @@ -42,21 +42,6 @@ thm foo.supp thm foo.fresh -primrec - permute_bn1_raw -where - "permute_bn1_raw p (As_raw x y t) = As_raw (p \ x) y t" - -primrec - permute_bn2_raw -where - "permute_bn2_raw p (As_raw x y t) = As_raw x (p \ y) t" - -primrec - permute_bn3_raw -where - "permute_bn3_raw p (As_raw x y t) = As_raw (p \ x) (p \ y) t" - quotient_definition "permute_bn1 :: perm \ assg \ assg" is diff -r add799cf0817 -r 82e37a4595c7 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Wed Nov 10 13:46:21 2010 +0000 +++ b/Nominal/Ex/Let.thy Fri Nov 12 01:20:53 2010 +0000 @@ -18,6 +18,8 @@ "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)" +thm permute_bn_raw.simps + thm at_set_avoiding2 thm trm_assn.fv_defs thm trm_assn.eq_iff @@ -30,12 +32,6 @@ thm trm_assn.fresh thm trm_assn.exhaust[where y="t", no_vars] -primrec - permute_bn_raw -where - "permute_bn_raw p (ANil_raw) = ANil_raw" -| "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \ a) t (permute_bn_raw p l)" - quotient_definition "permute_bn :: perm \ assn \ assn" is diff -r add799cf0817 -r 82e37a4595c7 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Wed Nov 10 13:46:21 2010 +0000 +++ b/Nominal/Ex/SingleLet.thy Fri Nov 12 01:20:53 2010 +0000 @@ -36,11 +36,6 @@ thm single_let.supp thm single_let.fresh -primrec - permute_bn_raw -where - "permute_bn_raw p (As_raw x y t) = As_raw (p \ x) y t" - quotient_definition "permute_bn :: perm \ assg \ assg" is diff -r add799cf0817 -r 82e37a4595c7 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Wed Nov 10 13:46:21 2010 +0000 +++ b/Nominal/Nominal2.thy Fri Nov 12 01:20:53 2010 +0000 @@ -169,6 +169,7 @@ in (dt_index, (bn_fun, (cnstr_head, rhs_elements))) end + fun order dts i ts = let val dt = nth dts i @@ -190,7 +191,6 @@ 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) @@ -210,6 +210,7 @@ in (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) end + *} ML {* @@ -298,33 +299,40 @@ (* 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 *) - val _ = warning "Definition of raw fv-functions"; + (* definition of raw fv and bn 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) = - if get_STEPS lthy3a > 3 - then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses + (* defining the permute_bn functions *) + val (_, _, lthy3b) = + 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 - then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3b - else raise TEST lthy3b + 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 lthy3c + else raise TEST lthy3c val alpha_tys = map (domain_type o fastype_of) alpha_trms (* definition of alpha-distinct lemmas *) diff -r add799cf0817 -r 82e37a4595c7 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Wed Nov 10 13:46:21 2010 +0000 +++ b/Nominal/nominal_dt_alpha.ML Fri Nov 12 01:20:53 2010 +0000 @@ -7,8 +7,9 @@ signature NOMINAL_DT_ALPHA = sig - val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> - term list -> Proof.context -> term list * term list * thm list * thm list * thm * local_theory + val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> + bclause list list list -> term list -> Proof.context -> + term list * term list * thm list * thm list * thm * local_theory val mk_alpha_distincts: Proof.context -> thm list -> thm list -> term list -> typ list -> thm list diff -r add799cf0817 -r 82e37a4595c7 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Wed Nov 10 13:46:21 2010 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Fri Nov 12 01:20:53 2010 +0000 @@ -11,7 +11,7 @@ type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list (* info of raw binding functions *) - type bn_info = (term * int * (int * term option) list list) list + type bn_info = term * int * (int * term option) list list (* binding modes and binding clauses *) @@ -28,13 +28,17 @@ val setify: Proof.context -> term -> term val listify: Proof.context -> term -> term - (* TODO: should be here + (* FIXME: should be here - currently in Nominal2.thy val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> - (term list * thm list * bn_info * thm list * local_theory) *) + (term list * thm list * bn_info list * thm list * local_theory) + *) - val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> + val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory + + val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> + local_theory -> (term list * thm list * local_theory) val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list end @@ -56,7 +60,7 @@ int * term option - is number of the corresponding argument with possibly recursive call with bn-function term *) -type bn_info = (term * int * (int * term option) list list) list +type bn_info = term * int * (int * term option) list list datatype bmode = Lst | Res | Set @@ -148,7 +152,6 @@ else t - (** functions that construct the equations for fv and fv_bn **) fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = @@ -284,6 +287,68 @@ end +(** definition of raw permute_bn functions **) + +fun mk_perm_bn_eq_rhs p perm_bn_map bn_args (i, arg) = + case AList.lookup (op=) bn_args i of + NONE => arg + | SOME (NONE) => mk_perm p arg + | SOME (SOME bn) => (lookup perm_bn_map bn) $ p $ arg + + +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 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 + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + end + +fun mk_perm_bn_eqs lthy perm_bn_map cns_info (bn_trm, bn_n, bn_argss) = + let + val nth_cns_info = nth cns_info bn_n + in + map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info + end + +fun define_raw_bn_perms raw_tys bn_info cns_info cns_thms size_thms lthy = + if null bn_info + then ([], [], lthy) + else + let + val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) + val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns + val perm_bn_names = map (prefix "permute_") bn_names + val perm_bn_arg_tys = map (nth raw_tys) bn_tys + val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys + val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys) + val perm_bn_map = bns ~~ perm_bn_frees + + val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map cns_info) bn_info + + val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names + val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs) + + val prod_simps = @{thms prod.inject HOL.simp_thms} + + val (_, lthy') = Function.add_function all_fun_names all_fun_eqs + Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy + + val (info, lthy'') = prove_termination size_thms (Local_Theory.restore lthy') + + val {fs, simps, ...} = info; + + val morphism = ProofContext.export_morphism lthy'' lthy + val simps_exp = map (Morphism.thm morphism) (the simps) + in + (fs, simps_exp, lthy'') + end + + (** equivarance proofs **) val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}