# HG changeset patch # User Cezary Kaliszyk # Date 1308456877 -32400 # Node ID b9a16d627bfde9a71aabb8d375f2244841762669 # Parent 9c0df9901acfe4286a4411cf6a7abb53afbe4a85# Parent 2b8e387d2dfc3eecc79b57bc9eab99fb78b4297b merge diff -r 9c0df9901acf -r b9a16d627bfd Nominal/Ex/Datatypes.thy --- a/Nominal/Ex/Datatypes.thy Sun Jun 19 13:10:15 2011 +0900 +++ b/Nominal/Ex/Datatypes.thy Sun Jun 19 13:14:37 2011 +0900 @@ -56,6 +56,7 @@ Baz x::name t::foo bind x in t + thm baz.distinct thm baz.induct thm baz.exhaust @@ -78,7 +79,7 @@ | Fun "nat \ nat" | Var "name" | Lam x::"name" t::"set_ty" bind x in t - +thm meta_eq_to_obj_eq thm set_ty.distinct thm set_ty.induct thm set_ty.exhaust diff -r 9c0df9901acf -r b9a16d627bfd Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Sun Jun 19 13:10:15 2011 +0900 +++ b/Nominal/Ex/Lambda.thy Sun Jun 19 13:14:37 2011 +0900 @@ -10,7 +10,8 @@ | App "lam" "lam" | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) -text {* free name function *} + +section {* free name function *} text {* first returns an atom list *} @@ -20,7 +21,8 @@ "frees_lst (Var x) = [atom x]" | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" - unfolding eqvt_def frees_lst_graph_def + unfolding eqvt_def + unfolding frees_lst_graph_def apply (rule, perm_simp, rule) apply(rule TrueI) apply(rule_tac y="x" in lam.exhaust) @@ -74,7 +76,9 @@ by (metis fresh_fun_app) -text {* A test with a locale and an interpretation. *} +section {* A test with a locale and an interpretation. *} + +text {* conclusion: it is no necessary *} locale test = fixes f1::"name \ ('a::pt)" @@ -126,7 +130,7 @@ apply (simp_all add: eqvt_def permute_fun_def permute_pure) done -text {* height function *} +section {* height function *} nominal_primrec height :: "lam \ int" @@ -149,7 +153,7 @@ thm height.simps -text {* capture - avoiding substitution *} +section {* capture-avoiding substitution *} nominal_primrec subst :: "lam \ name \ lam \ lam" ("_ [_ ::= _]" [90, 90, 90] 90) diff -r 9c0df9901acf -r b9a16d627bfd Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Sun Jun 19 13:10:15 2011 +0900 +++ b/Nominal/Nominal2.thy Sun Jun 19 13:14:37 2011 +0900 @@ -261,43 +261,45 @@ val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) - val (alpha_eqvt, lthy6) = - Nominal_Eqvt.raw_equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 + val alpha_eqvt = + Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 + + val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt val _ = trace_msg (K "Proving equivalence of alpha...") val alpha_refl_thms = - raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6 + raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy5 val alpha_sym_thms = - raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6 + raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct alpha_eqvt_norm lthy5 val alpha_trans_thms = raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) - alpha_intros alpha_induct alpha_cases lthy6 + alpha_intros alpha_induct alpha_cases alpha_eqvt_norm lthy5 val (alpha_equivp_thms, alpha_bn_equivp_thms) = raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms - alpha_trans_thms lthy6 + alpha_trans_thms lthy5 val _ = trace_msg (K "Proving alpha implies bn...") val alpha_bn_imp_thms = - raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 + raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 val _ = trace_msg (K "Proving respectfulness...") val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs - raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6 + raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct - (raw_size_thms @ raw_size_eqvt) lthy6 + (raw_size_thms @ raw_size_eqvt) lthy5 |> map mk_funs_rsp val raw_constrs_rsp = raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros - (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 + (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy5 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt @@ -306,19 +308,19 @@ val raw_perm_bn_rsp = raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct - alpha_intros raw_perm_bn_simps lthy6 + alpha_intros raw_perm_bn_simps lthy5 (* noting the quot_respects lemmas *) - val (_, lthy6a) = + val (_, lthy6) = Local_Theory.note ((Binding.empty, [rsp_attr]), raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ - alpha_bn_rsp @ raw_perm_bn_rsp) lthy6 + alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 val _ = trace_msg (K "Defining the quotient types...") val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts val (qty_infos, lthy7) = - define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a + define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 val qtys = map #qtyp qty_infos val qty_full_names = map (fst o dest_Type) qtys diff -r 9c0df9901acf -r b9a16d627bfd Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Sun Jun 19 13:10:15 2011 +0900 +++ b/Nominal/Nominal2_Base.thy Sun Jun 19 13:14:37 2011 +0900 @@ -1626,6 +1626,12 @@ definition "eqvt f \ \p. p \ f = f" +lemma eqvt_boolI: + fixes f::"bool" + shows "eqvt f" +unfolding eqvt_def by (simp add: permute_bool_def) + + text {* equivariance of a function at a given argument *} definition diff -r 9c0df9901acf -r b9a16d627bfd Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Sun Jun 19 13:10:15 2011 +0900 +++ b/Nominal/nominal_dt_alpha.ML Sun Jun 19 13:14:37 2011 +0900 @@ -26,8 +26,9 @@ (Proof.context -> int -> tactic) -> Proof.context -> thm list val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list - val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list - val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list + val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list + val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list -> + Proof.context -> thm list val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> Proof.context -> thm list * thm list @@ -492,7 +493,7 @@ by (erule exE, rule_tac x="-p" in exI, auto)} (* for premises that contain binders *) -fun prem_bound_tac pred_names ctxt = +fun prem_bound_tac pred_names alpha_eqvt ctxt = let fun trans_prem_tac pred_names ctxt = SUBPROOF (fn {prems, context, ...} => @@ -507,20 +508,20 @@ [ etac exi_neg, resolve_tac @{thms alpha_sym_eqvt}, asm_full_simp_tac (HOL_ss addsimps prod_simps), - eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl}, - trans_prem_tac pred_names ctxt ] + eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, + trans_prem_tac pred_names ctxt] end -fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt = +fun raw_prove_sym alpha_trms alpha_intros alpha_induct alpha_eqvt ctxt = let val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms - + fun tac ctxt = let val alpha_names = map (fst o dest_Const) alpha_trms in resolve_tac alpha_intros THEN_ALL_NEW - FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt] + FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt] end in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt @@ -549,7 +550,7 @@ HEADGOAL (rtac exi_inst) end) -fun non_trivial_cases_tac pred_names intros ctxt = +fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = let val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def} in @@ -562,15 +563,15 @@ resolve_tac @{thms alpha_trans_eqvt}, atac, aatac pred_names ctxt, - eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl}, + eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) end -fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt = +fun prove_trans_tac pred_names raw_dt_thms intros cases alpha_eqvt ctxt = let fun all_cases ctxt = asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) - THEN' TRY o non_trivial_cases_tac pred_names intros ctxt + THEN' TRY o non_trivial_cases_tac pred_names intros alpha_eqvt ctxt in EVERY' [ rtac @{thm allI}, rtac @{thm impI}, ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ] @@ -585,13 +586,13 @@ HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) end -fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = +fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases alpha_eqvt ctxt = let val alpha_names = map (fst o dest_Const) alpha_trms val props = map prep_trans_goal alpha_trms in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct - (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt + (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases alpha_eqvt) ctxt end diff -r 9c0df9901acf -r b9a16d627bfd Nominal/nominal_eqvt.ML --- a/Nominal/nominal_eqvt.ML Sun Jun 19 13:10:15 2011 +0900 +++ b/Nominal/nominal_eqvt.ML Sun Jun 19 13:14:37 2011 +0900 @@ -8,8 +8,7 @@ signature NOMINAL_EQVT = sig - val raw_equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory - val equivariance: string -> Proof.context -> (thm list * local_theory) + val raw_equivariance: term list -> thm -> thm list -> Proof.context -> thm list val equivariance_cmd: string -> Proof.context -> local_theory end @@ -75,20 +74,10 @@ (* stores thm under name.eqvt and adds [eqvt]-attribute *) -fun note_named_thm (name, thm) ctxt = - let - val thm_name = Binding.qualified_name - (Long_Name.qualify (Long_Name.base_name name) "eqvt") - val attr = Attrib.internal (K eqvt_add) - val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt - in - (thm', ctxt') - end - fun get_name (Const (a, _)) = a | get_name (Free (a, _)) = a -fun raw_equivariance note_flag pred_trms raw_induct intrs ctxt = +fun raw_equivariance pred_trms raw_induct intrs ctxt = let val is_already_eqvt = filter (is_eqvt ctxt) pred_trms @@ -110,36 +99,34 @@ (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); val goal = HOLogic.mk_Trueprop - (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) - - val thms = Goal.prove ctxt' [] [] goal + (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) + in + Goal.prove ctxt' [] [] goal (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |> Datatype_Aux.split_conj_thm |> ProofContext.export ctxt' ctxt |> map (fn th => th RS mp) |> map zero_var_indexes - in - if note_flag - then fold_map note_named_thm (pred_names ~~ thms) ctxt - else (thms, ctxt) end -fun equivariance pred_name ctxt = +fun note_named_thm (name, thm) ctxt = let - val thy = ProofContext.theory_of ctxt - val (_, {preds, raw_induct, intrs, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) + val thm_name = Binding.qualified_name + (Long_Name.qualify (Long_Name.base_name name) "eqvt") + val attr = Attrib.internal (K eqvt_add) + val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt in - raw_equivariance false preds raw_induct intrs ctxt + (thm', ctxt') end fun equivariance_cmd pred_name ctxt = let val thy = ProofContext.theory_of ctxt - val (_, {preds, raw_induct, intrs, ...}) = + val ({names, ...}, {preds, raw_induct, intrs, ...}) = Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) + val thms = raw_equivariance preds raw_induct intrs ctxt in - raw_equivariance true preds raw_induct intrs ctxt |> snd + fold_map note_named_thm (names ~~ thms) ctxt |> snd end local structure P = Parse and K = Keyword in diff -r 9c0df9901acf -r b9a16d627bfd Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Sun Jun 19 13:10:15 2011 +0900 +++ b/Nominal/nominal_library.ML Sun Jun 19 13:14:37 2011 +0900 @@ -479,8 +479,10 @@ (* inductive premises can be of the form - R ... /\ P ...; split_conj_i picks out - the part R or P part + + R ... /\ P ...; + + split_conj_i picks out the part R or P part *) fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = (case head_of f1 of