# HG changeset patch # User Cezary Kaliszyk # Date 1271254264 -7200 # Node ID b435ee87d9c8728504af2c6ad863aeb161c95656 # Parent 9a8decba77c50cc9cca5017be1db98e909518833# Parent 636de31888a642b5d7f5a023b9c1458740f4a22a merge diff -r 9a8decba77c5 -r b435ee87d9c8 Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Wed Apr 14 16:10:44 2010 +0200 +++ b/Nominal-General/Nominal2_Base.thy Wed Apr 14 16:11:04 2010 +0200 @@ -6,6 +6,7 @@ *) theory Nominal2_Base imports Main Infinite_Set +uses ("nominal_library.ML") begin section {* Atoms and Sorts *} @@ -1059,4 +1060,7 @@ by auto qed +(* nominal infrastructure *) +use "nominal_library.ML" + end diff -r 9a8decba77c5 -r b435ee87d9c8 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Wed Apr 14 16:10:44 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Wed Apr 14 16:11:04 2010 +0200 @@ -9,6 +9,7 @@ imports Nominal2_Base Nominal2_Atoms uses ("nominal_thmdecls.ML") ("nominal_permeq.ML") + ("nominal_eqvt.ML") begin @@ -284,6 +285,7 @@ shows "p \ unpermute p x \ x" unfolding unpermute_def by simp +(* provides perm_simp methods *) use "nominal_permeq.ML" setup Nominal_Permeq.setup @@ -371,4 +373,8 @@ (* apply(perm_strict_simp) *) oops +(* automatic equivariance procedure for + inductive definitions *) +use "nominal_eqvt.ML" + end diff -r 9a8decba77c5 -r b435ee87d9c8 Nominal-General/nominal_eqvt.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal-General/nominal_eqvt.ML Wed Apr 14 16:11:04 2010 +0200 @@ -0,0 +1,172 @@ +(* Title: nominal_eqvt.ML + Author: Stefan Berghofer (original code) + Author: Christian Urban + + Automatic proofs for equivariance of inductive predicates. +*) + +signature NOMINAL_EQVT = +sig + val equivariance: string -> Proof.context -> local_theory + val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic + val eqvt_rel_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic +end + +structure Nominal_Eqvt : NOMINAL_EQVT = +struct + +open Nominal_Permeq; +open Nominal_ThmDecls; + +val atomize_conv = + MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) + (HOL_basic_ss addsimps @{thms induct_atomize}); +val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); +fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 + (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); + + +(** + proves F[f t] from F[t] which is the given theorem + - F needs to be monotone + - f returns either SOME for a term it fires + and NONE elsewhere +**) +fun map_term f t = + (case f t of + NONE => map_term' f t + | x => x) +and map_term' f (t $ u) = + (case (map_term f t, map_term f u) of + (NONE, NONE) => NONE + | (SOME t'', NONE) => SOME (t'' $ u) + | (NONE, SOME u'') => SOME (t $ u'') + | (SOME t'', SOME u'') => SOME (t'' $ u'')) + | map_term' f (Abs (s, T, t)) = + (case map_term f t of + NONE => NONE + | SOME t'' => SOME (Abs (s, T, t''))) + | map_term' _ _ = NONE; + +fun map_thm_tac ctxt tac thm = +let + val monos = Inductive.get_monos ctxt +in + EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, + REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), + REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] +end + +fun map_thm ctxt f tac thm = +let + val opt_goal_trm = map_term f (prop_of thm) +in + case opt_goal_trm of + NONE => thm + | SOME goal => + Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) +end + +(* + inductive premises can be of the form + R ... /\ P ...; split_conj picks out + the part P ... +*) +fun transform_prem ctxt names thm = +let + fun split_conj names (Const ("op &", _) $ p $ q) = + (case head_of p of + Const (name, _) => if name mem names then SOME q else NONE + | _ => NONE) + | split_conj _ _ = NONE; +in + map_thm ctxt (split_conj names) (etac conjunct2 1) thm +end + + +(** equivariance tactics **) + +fun eqvt_rel_case_tac ctxt pred_names pi intro = +let + val thy = ProofContext.theory_of ctxt + val cpi = Thm.cterm_of thy (mk_minus pi) + val rule = Drule.instantiate' [] [SOME cpi] @{thm permute_boolE} + val permute_cancel = @{thms permute_minus_cancel(2)} +in + eqvt_strict_tac ctxt [] [] THEN' + SUBPROOF (fn {prems, context, ...} => + let + val prems' = map (transform_prem ctxt pred_names) prems + val side_cond_tac = EVERY' + [ rtac rule, eqvt_strict_tac context permute_cancel [], + resolve_tac prems' ] + in + (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) 1 + end) ctxt +end + +fun eqvt_rel_tac ctxt pred_names pi induct intros = +let + val cases = map (eqvt_rel_case_tac ctxt pred_names pi) intros +in + EVERY' (rtac induct :: cases) +end + + +(** equivariance procedure *) + +(* sets up goal and makes sure parameters + are untouched PROBLEM: this violates the + form of eqvt lemmas *) +fun prepare_goal params_no pi pred = +let + val (c, xs) = strip_comb pred; + val (xs1, xs2) = chop params_no xs +in + HOLogic.mk_imp (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2)) +end + +(* 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) +in + Local_Theory.note ((thm_name, [attr]), [thm]) ctxt +end + +fun equivariance pred_name ctxt = +let + val thy = ProofContext.theory_of ctxt + val ({names, ...}, {raw_induct, intrs, ...}) = + Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) + val raw_induct = atomize_induct ctxt raw_induct + val intros = map atomize_intr intrs + val params_no = length (Inductive.params_of raw_induct) + val (([raw_concl], [raw_pi]), ctxt') = ctxt + |> Variable.import_terms false [concl_of raw_induct] + ||>> Variable.variant_fixes ["pi"] + val pi = Free (raw_pi, @{typ perm}) + val preds = map (fst o HOLogic.dest_imp) + (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); + val goal = HOLogic.mk_Trueprop + (foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds)) + val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal + (fn {context,...} => eqvt_rel_tac context names pi raw_induct intros 1) + |> singleton (ProofContext.export ctxt' ctxt)) + val thms' = map (fn th => zero_var_indexes (th RS mp)) thms +in + ctxt |> fold_map note_named_thm (names ~~ thms') |> snd +end + + +local structure P = OuterParse and K = OuterKeyword in + +val _ = + OuterSyntax.local_theory "equivariance" + "prove equivariance for inductive predicate involving nominal datatypes" + K.thy_decl (P.xname >> equivariance); +end; + +end (* structure *) \ No newline at end of file diff -r 9a8decba77c5 -r b435ee87d9c8 Nominal-General/nominal_library.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal-General/nominal_library.ML Wed Apr 14 16:11:04 2010 +0200 @@ -0,0 +1,39 @@ +(* Title: nominal_library.ML + Author: Christian Urban + + Basic function for nominal. +*) + +signature NOMINAL_LIBRARY = +sig + val mk_minus: term -> term + val mk_perm: term -> term -> term + val dest_perm: term -> term * term + + val mk_equiv: thm -> thm + val safe_mk_equiv: thm -> thm +end + + +structure Nominal_Library: NOMINAL_LIBRARY = +struct + +fun mk_minus p = + Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p + +fun mk_perm p trm = +let + val ty = fastype_of trm +in + Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm +end + +fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) + | dest_perm t = raise TERM ("dest_perm", [t]) + +fun mk_equiv r = r RS @{thm eq_reflection}; +fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; + +end (* structure *) + +open Nominal_Library; \ No newline at end of file diff -r 9a8decba77c5 -r b435ee87d9c8 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Wed Apr 14 16:10:44 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Wed Apr 14 16:11:04 2010 +0200 @@ -120,9 +120,6 @@ Conv.all_conv ctrm end -fun mk_equiv r = r RS @{thm eq_reflection}; -fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; - (* main conversion *) fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm = let diff -r 9a8decba77c5 -r b435ee87d9c8 Nominal-General/nominal_thmdecls.ML --- a/Nominal-General/nominal_thmdecls.ML Wed Apr 14 16:10:44 2010 +0200 +++ b/Nominal-General/nominal_thmdecls.ML Wed Apr 14 16:11:04 2010 +0200 @@ -60,9 +60,6 @@ val add_thm = EqvtData.map o Item_Net.update; val del_thm = EqvtData.map o Item_Net.remove; -fun is_equiv (Const ("==", _) $ _ $ _) = true - | is_equiv _ = false - fun add_raw_thm thm = case prop_of thm of Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm) @@ -70,16 +67,6 @@ val del_raw_thm = EqvtRawData.map o Item_Net.remove; -fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) - | dest_perm t = raise TERM ("dest_perm", [t]) - -fun mk_perm p trm = -let - val ty = fastype_of trm -in - Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm -end - fun eq_transform_tac thm = REPEAT o FIRST' [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}), rtac (thm RS @{thm trans}), @@ -113,8 +100,6 @@ | is_bad_list [_] = false | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true -fun mk_minus p = - Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p fun imp_transform_tac thy p p' thm = let @@ -155,9 +140,6 @@ end end -fun mk_equiv r = r RS @{thm eq_reflection}; -fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; - fun transform addel_fun thm context = let val ctxt = Context.proof_of context diff -r 9a8decba77c5 -r b435ee87d9c8 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed Apr 14 16:10:44 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Wed Apr 14 16:11:04 2010 +0200 @@ -127,211 +127,60 @@ | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" - -ML {* -fun map_term f t = - (case f t of - NONE => map_term' f t - | x => x) -and map_term' f (t $ u) = - (case (map_term f t, map_term f u) of - (NONE, NONE) => NONE - | (SOME t'', NONE) => SOME (t'' $ u) - | (NONE, SOME u'') => SOME (t $ u'') - | (SOME t'', SOME u'') => SOME (t'' $ u'')) - | map_term' f (Abs (s, T, t)) = - (case map_term f t of - NONE => NONE - | SOME t'' => SOME (Abs (s, T, t''))) - | map_term' _ _ = NONE; - -fun map_thm_tac ctxt tac thm = -let - val monos = Inductive.get_monos ctxt -in - EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, - REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), - REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] -end - -(* - proves F[f t] from F[t] where F[t] is the given theorem - - - F needs to be monotone - - f returns either SOME for a term it fires - and NONE elsewhere -*) -fun map_thm ctxt f tac thm = -let - val opt_goal_trm = map_term f (prop_of thm) - fun prove goal = - Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) -in - case opt_goal_trm of - NONE => thm - | SOME goal => prove goal -end +inductive + typing' :: "(name\ty) list\lam\ty\bool" ("_ \ _ : _" [60,60,60] 60) +where + t'_Var[intro]: "\valid \; (x,T)\set \\ \ \ \ Var x : T" + | t'_App[intro]: "\\ \ t1 : T1\T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" + | t'_Lam[intro]: "\atom x\\;(x,T1)#\ \ t : T2\ \ \ \ Lam x t : T1\T2" -fun transform_prem ctxt names thm = -let - fun split_conj names (Const ("op &", _) $ p $ q) = - (case head_of p of - Const (name, _) => if name mem names then SOME q else NONE - | _ => NONE) - | split_conj _ _ = NONE; -in - map_thm ctxt (split_conj names) (etac conjunct2 1) thm -end -*} - -ML {* -open Nominal_Permeq -*} - -ML {* -fun single_case_tac ctxt pred_names pi intro = -let - val rule = Drule.instantiate' [] [SOME pi] @{thm permute_boolE} -in - eqvt_strict_tac ctxt [] [] THEN' - SUBPROOF (fn {prems, context as ctxt, ...} => - let - val prems' = map (transform_prem ctxt pred_names) prems - val side_cond_tac = EVERY' - [ rtac rule, - eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], - resolve_tac prems' ] - in - HEADGOAL (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) - end) ctxt -end -*} - -ML {* -fun eqvt_rel_tac pred_name = -let - val thy = ProofContext.theory_of ctxt - val ({names, ...}, {raw_induct, intrs, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) - val param_no = length (Inductive.params_of raw_induct) - val (([raw_concl], [pi]), ctxt') = - ctxt |> Variable.import_terms false [concl_of raw_induct] - ||>> Variable.variant_fixes ["pi"]; - val preds = map (fst o HOLogic.dest_imp) - (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); -in +inductive + typing2' :: "(name\ty) list\lam\ty\bool" ("_ 2\ _ : _" [60,60,60] 60) +where + t2'_Var[intro]: "\valid \; (x,T)\set \\ \ \ 2\ Var x : T" + | t2'_App[intro]: "\\ 2\ t1 : T1\T2 \ \ 2\ t2 : T1\ \ \ 2\ App t1 t2 : T2" + | t2'_Lam[intro]: "\atom x\\;(x,T1)#\ 2\ t : T2\ \ \ 2\ Lam x t : T1\T2" -end -*} - - - -lemma [eqvt]: - assumes a: "valid Gamma" - shows "valid (p \ Gamma)" -using a -apply(induct) -apply(tactic {* my_tac @{context} ["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(1)} 1 *}) -apply(tactic {* my_tac @{context }["Lambda.valid"] @{cterm "- p"} @{thm valid.intros(2)} 1 *}) -done - -lemma - shows "Gamma \ t : T \ (p \ Gamma) \ (p \ t) : (p \ T)" -ML_prf {* -val ({names, ...}, {raw_induct, ...}) = - Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") -*} -apply(tactic {* rtac raw_induct 1 *}) -apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(1)} 1 *}) -apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(2)} 1 *}) -apply(tactic {* my_tac @{context} ["Lambda.typing"] @{cterm "- p"} @{thm typing.intros(3)} 1 *}) -done - -lemma uu[eqvt]: - assumes a: "Gamma \ t : T" - shows "(p \ Gamma) \ (p \ t) : (p \ T)" -using a -apply(induct) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -apply(perm_strict_simp) -apply(rule typing.intros) -apply(rule conj_mono[THEN mp]) -prefer 3 -apply(assumption) -apply(rule impI) -prefer 2 -apply(rule impI) -apply(simp) -apply(auto)[1] -apply(simp) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -done +inductive + typing'' :: "(name\ty) list\lam\ty\bool" ("_ |\ _ : _" [60,60,60] 60) +and valid' :: "(name\ty) list \ bool" +where + v1[intro]: "valid' []" + | v2[intro]: "\valid' \;atom x\\\\ valid' ((x,T)#\)" + | t'_Var[intro]: "\valid' \; (x,T)\set \\ \ \ |\ Var x : T" + | t'_App[intro]: "\\ |\ t1 : T1\T2; \ |\ t2 : T1\ \ \ |\ App t1 t2 : T2" + | t'_Lam[intro]: "\atom x\\;(x,T1)#\ |\ t : T2\ \ \ |\ Lam x t : T1\T2" -(* -inductive - typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) -where - t_Var[intro]: "\valid \; (x, T) \ set \\ \ \ \ Var x : T" - | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" - | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" - -lemma uu[eqvt]: - assumes a: "Gamma \ t : T" - shows "(p \ Gamma) \ (p \ t) : (p \ T)" -using a -apply(induct) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) -done -*) - -ML {* -val inductive_atomize = @{thms induct_atomize}; +use "../../Nominal-General/nominal_eqvt.ML" -val atomize_conv = - MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) - (HOL_basic_ss addsimps inductive_atomize); -val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); -fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 - (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); -*} - -ML {* -val ({names, ...}, {raw_induct, intrs, elims, ...}) = - Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") -*} +equivariance valid +equivariance typing -ML {* val ind_params = Inductive.params_of raw_induct *} -ML {* val raw_induct = atomize_induct @{context} raw_induct; *} -ML {* val elims = map (atomize_induct @{context}) elims; *} -ML {* val monos = Inductive.get_monos @{context}; *} - -lemma - shows "Gamma \ t : T \ (p \ Gamma) \ (p \ t) : (p \ T)" -apply(tactic {* rtac raw_induct 1 *}) -apply(tactic {* my_tac @{context} intrs 1 *}) -apply(perm_strict_simp) -apply(rule typing.intros) -oops - - +thm valid.eqvt +thm typing.eqvt thm eqvts thm eqvts_raw -declare permute_lam_raw.simps[eqvt] -thm alpha_gen_real_eqvt -(*declare alpha_gen_real_eqvt[eqvt]*) +equivariance typing' +equivariance typing2' +equivariance typing'' + +ML {* +fun mk_minus p = + Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p +*} -lemma - assumes a: "alpha_lam_raw t1 t2" - shows "alpha_lam_raw (p \ t1) (p \ t2)" -using a -apply(induct) -apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *}) -oops +inductive + tt :: "('a \ 'a \ bool) \ ('a \ 'a \ bool)" + for r :: "('a \ 'a \ bool)" +where + aa: "tt r a a" + | bb: "tt r a b ==> tt r a c" -thm alpha_lam_raw.intros[no_vars] +(* PROBLEM: derived eqvt-theorem does not conform with [eqvt] +equivariance tt +*) + inductive alpha_lam_raw' @@ -342,18 +191,15 @@ | "\pi. ({atom name}, lam_raw) \gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \ alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" +declare permute_lam_raw.simps[eqvt] +(*declare alpha_gen_real_eqvt[eqvt]*) +(*equivariance alpha_lam_raw'*) + lemma assumes a: "alpha_lam_raw' t1 t2" shows "alpha_lam_raw' (p \ t1) (p \ t2)" using a apply(induct) -apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *}) -apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *}) -apply(perm_strict_simp) -apply(rule alpha_lam_raw'.intros) -apply(simp add: alphas) -apply(rule_tac p="- p" in permute_boolE) -apply(perm_simp permute_minus_cancel(2)) oops