# HG changeset patch # User Christian Urban # Date 1271072094 -7200 # Node ID ae176476b5253b3004bb4e79a8de51dc2e0c739a # Parent 894930834ca874ebda3ba8b97872bcb82b721f86 implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _ diff -r 894930834ca8 -r ae176476b525 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Sun Apr 11 22:48:49 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Mon Apr 12 13:34:54 2010 +0200 @@ -11,13 +11,6 @@ ("nominal_permeq.ML") begin -lemma r: "x = x" -apply(auto) -done - -ML {* - prop_of @{thm r} -*} section {* Logical Operators *} @@ -266,10 +259,7 @@ atom_eqvt add_perm_eqvt lemmas [eqvt_raw] = - permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) - -thm eqvts -thm eqvts_raw + permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) text {* helper lemmas for the eqvt_tac *} diff -r 894930834ca8 -r ae176476b525 Nominal-General/nominal_thmdecls.ML --- a/Nominal-General/nominal_thmdecls.ML Sun Apr 11 22:48:49 2010 +0200 +++ b/Nominal-General/nominal_thmdecls.ML Mon Apr 12 13:34:54 2010 +0200 @@ -8,7 +8,11 @@ theorem in the eqvts list and also in the eqvts_raw list. For the latter the theorem is expected to be of the form - p o (c x1 x2 ...) = c (p o x1) (p o x2) ... + p o (c x1 x2 ...) = c (p o x1) (p o x2) ... (1) + + or + + c x1 x2 ... ==> c (p o x1) (p o x2) ... (2) and it is stored in the form @@ -16,11 +20,8 @@ The [eqvt_raw] attribute just adds the theorem to eqvts_raw. - TODO: - - - deal with eqvt-lemmas of the form - - c x1 x2 ... ==> c (p o x1) (p o x2) .. + TODO: In case of the form in (2) one should also + add the equational form to eqvts *) signature NOMINAL_THMDECLS = @@ -38,9 +39,6 @@ structure Nominal_ThmDecls: NOMINAL_THMDECLS = struct -fun mk_equiv r = r RS @{thm eq_reflection}; -fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; - structure EqvtData = Generic_Data ( type T = thm Item_Net.T; val empty = Thm.full_rules; @@ -56,8 +54,8 @@ val eqvts = Item_Net.content o EqvtData.get; val eqvts_raw = Item_Net.content o EqvtRawData.get; -val get_eqvts_thms = eqvts o Context.Proof; -val get_eqvts_raw_thms = eqvts_raw o Context.Proof; +val get_eqvts_thms = eqvts o Context.Proof; +val get_eqvts_raw_thms = eqvts_raw o Context.Proof; val add_thm = EqvtData.map o Item_Net.update; val del_thm = EqvtData.map o Item_Net.remove; @@ -66,13 +64,9 @@ | is_equiv _ = false fun add_raw_thm thm = -let - val trm = prop_of thm -in - if is_equiv trm - then (EqvtRawData.map o Item_Net.update) thm - else raise THM ("Theorem must be a meta-equality", 0, [thm]) -end + case prop_of thm of + Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm) + | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) val del_raw_thm = EqvtRawData.map o Item_Net.remove; @@ -86,7 +80,7 @@ Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm end -fun eqvt_transform_tac thm = REPEAT o FIRST' +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}), rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] @@ -104,25 +98,77 @@ val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) in if c <> c' - then error "eqvt lemma is not of the right form (constants do not agree)" + then error "Eqvt lemma is not of the right form (constants do not agree)" else if eargs' <> map (mk_perm p) eargs - then error "eqvt lemma is not of the right form (arguments do not agree)" + then error "Eqvt lemma is not of the right form (arguments do not agree)" else if args = [] then thm else Goal.prove ctxt [p_str] [] goal - (fn _ => eqvt_transform_tac thm 1) + (fn _ => eq_transform_tac thm 1) +end + + +(* tests whether the lists of pis all agree, and that there is at least one p *) +fun is_bad_list [] = true + | 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 + val cp = Thm.cterm_of thy p + val cp' = Thm.cterm_of thy (mk_minus p') + val thm' = Drule.cterm_instantiate [(cp, cp')] thm + val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} +in + EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, + rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] end +fun transform_imp ctxt thm = +let + val thy = ProofContext.theory_of ctxt + val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) + val (c, prem_args) = strip_comb prem + val (c', concl_args) = strip_comb concl + val ps = map (fst o dest_perm) concl_args handle TERM _ => [] + val p = try hd ps +in + if c <> c' + then error "Eqvt lemma is not of the right form (constants do not agree)" + else if is_bad_list ps + then error "Eqvt lemma is not of the right form (permutations do not agree)" + else if concl_args <> map (mk_perm (the p)) prem_args + then error "Eqvt lemma is not of the right form (arguments do not agree)" + else + let + val prem' = Const (@{const_name "permute"}, @{typ "perm => bool => bool"}) $ (the p) $ prem + val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) + val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt + in + Goal.prove ctxt' [] [] goal' + (fn _ => imp_transform_tac thy (the p) p' thm 1) + |> singleton (ProofContext.export ctxt' ctxt) + |> transform_eq ctxt + 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 in case (prop_of thm) of - @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => - addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context - | @{const "==>"} $ _ $ _ => - error ("not yet implemented") - | _ => raise (error "only (op=) case implemented yet") + @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ + (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => + addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context + | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => + addel_fun (safe_mk_equiv (transform_imp ctxt thm)) context + | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." end val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm)); @@ -133,10 +179,10 @@ val setup = Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) - (cat_lines ["declaration of equivariance lemmas - they will automtically be", - "brought into the form p o c = c"]) #> + (cat_lines ["Declaration of equivariance lemmas - they will automtically be", + "brought into the form p o c == c"]) #> Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) - (cat_lines ["declaration of equivariance lemmas - no", + (cat_lines ["Declaration of equivariance lemmas - no", "transformation is performed"]) #> PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); diff -r 894930834ca8 -r ae176476b525 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Sun Apr 11 22:48:49 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Mon Apr 12 13:34:54 2010 +0200 @@ -132,8 +132,14 @@ atac ]) *} +ML {* try hd [1] *} -lemma +ML {* +Skip_Proof.cheat_tac +*} + + +lemma [eqvt]: assumes a: "valid Gamma" shows "valid (p \ Gamma)" using a @@ -142,13 +148,8 @@ apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) done -lemma - "(p \ valid) = valid" -oops - -lemma temp[eqvt_raw]: - "(p \ valid) \ valid" -sorry +thm eqvts +thm eqvts_raw inductive typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) @@ -157,7 +158,7 @@ | 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 +lemma uu[eqvt]: assumes a: "Gamma \ t : T" shows "(p \ Gamma) \ (p \ t) : (p \ T)" using a @@ -167,6 +168,9 @@ apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *}) done +thm eqvts +thm eqvts_raw + declare permute_lam_raw.simps[eqvt] thm alpha_gen_real_eqvt[no_vars]