# HG changeset patch # User narboux # Date 1175549092 -7200 # Node ID 80b814fe284ba6d10c42d89f8e92c0d33a290875 # Parent 705d4fb9e628250adb080b008095b015987e3310 rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name diff -r 705d4fb9e628 -r 80b814fe284b src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Mon Apr 02 11:31:08 2007 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Mon Apr 02 23:24:52 2007 +0200 @@ -72,6 +72,7 @@ fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name); fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) (Name name); +fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st); (* needed in the process of fully simplifying permutations *) val strong_congs = [thm "if_cong"] @@ -131,7 +132,7 @@ end (* function for simplyfying permutations *) -fun perm_simp_gen dyn_thms ss i = +fun perm_simp_gen dyn_thms f ss i = ("general simplification of permutations", fn st => let @@ -141,7 +142,7 @@ val perm_sp_app = Simplifier.simproc (theory_of_thm st) "perm_simproc_app" ["Nominal.perm pi x"] (perm_simproc_app st); - val ss' = ss addsimps (List.concat (map (dynamic_thms st) dyn_thms)) + val ss' = ss addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@(f st)) delcongs weak_congs addcongs strong_congs addsimprocs [perm_sp_fun, perm_sp_app] @@ -150,8 +151,10 @@ end); (* general simplification of permutations and permutation that arose from eqvt-problems *) -val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp"]; -val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp","eqvts"]; +val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp"] (fn st => []); +val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp"] eqvts_thms; + +(* FIXME removes the name lookup for these theorems use an ml value instead *) (* main simplification tactics for permutations *) (* FIXME: perm_simp_tac should simplify more permutations *) diff -r 705d4fb9e628 -r 80b814fe284b src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Mon Apr 02 11:31:08 2007 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon Apr 02 23:24:52 2007 +0200 @@ -2,7 +2,7 @@ Authors: Julien Narboux and Christian Urban This file introduces the infrastructure for the lemma - declaration "eqvt" "bij" and "fresh". + declaration "eqvts" "bijs" and "freshs". By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored in a data-slot in the theory context. Possible modifiers @@ -30,12 +30,12 @@ structure Data = GenericDataFun ( val name = "HOL/Nominal/eqvt"; - type T = {eqvts:thm list, fresh:thm list, bij:thm list}; - val empty = ({eqvts=[], fresh=[], bij=[]}:T); + type T = {eqvts:thm list, freshs:thm list, bijs:thm list}; + val empty = ({eqvts=[], freshs=[], bijs=[]}:T); val extend = I; fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2), - fresh = Drule.merge_rules (#fresh r1, #fresh r2), - bij = Drule.merge_rules (#bij r1, #bij r2)} + freshs = Drule.merge_rules (#freshs r1, #freshs r2), + bijs = Drule.merge_rules (#bijs r1, #bijs r2)} fun print context (data:T) = let fun print_aux msg thms = @@ -43,8 +43,8 @@ (map (ProofContext.pretty_thm (Context.proof_of context)) thms)) in (print_aux "Equivariance lemmas: " (#eqvts data); - print_aux "Freshness lemmas: " (#fresh data); - print_aux "Bijection lemmas: " (#bij data)) + print_aux "Freshness lemmas: " (#freshs data); + print_aux "Bijection lemmas: " (#bijs data)) end; ); @@ -62,8 +62,8 @@ val print_data = Data.print o Context.Proof; val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts; -val get_fresh_thms = Context.Theory #> Data.get #> #fresh; -val get_bij_thms = Context.Theory #> Data.get #> #bij; +val get_fresh_thms = Context.Theory #> Data.get #> #freshs; +val get_bij_thms = Context.Theory #> Data.get #> #bijs; (* FIXME: should be a function in a library *) fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); @@ -195,13 +195,13 @@ Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' end -fun bij_add_del_aux f = simple_add_del_aux #bij "bij" f -fun fresh_add_del_aux f = simple_add_del_aux #fresh "fresh" f +fun bij_add_del_aux f = simple_add_del_aux #bijs "bijs" f +fun fresh_add_del_aux f = simple_add_del_aux #freshs "freshs" f fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvts "eqvts" f -fun eqvt_map f th (r:Data.T) = {eqvts = (f th (#eqvts r)), fresh = #fresh r, bij = #bij r}; -fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, fresh = (f th (#fresh r)), bij = #bij r}; -fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, fresh = #fresh r, bij = (f th (#bij r))}; +fun eqvt_map f th (r:Data.T) = {eqvts = (f th (#eqvts r)), freshs = #freshs r, bijs = #bijs r}; +fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r}; +fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))}; val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));