auxiliary dynamic_thm(s) for fact lookup;
authorwenzelm
Wed Mar 19 22:28:17 2008 +0100 (2008-03-19 ago)
changeset 26338f8ed02f22433
parent 26337 44473c957672
child 26339 7825c83c9eff
auxiliary dynamic_thm(s) for fact lookup;
renamed local dynamic_thm(s) to goal_thm(s);
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Mar 19 22:28:08 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Mar 19 22:28:17 2008 +0100
     1.3 @@ -71,8 +71,8 @@
     1.4  val supports_fresh_rule = @{thm "supports_fresh"};
     1.5  
     1.6  (* pulls out dynamically a thm via the proof state *)
     1.7 -fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
     1.8 -fun dynamic_thm  st name = PureThy.get_thm  (theory_of_thm st) (Name name);
     1.9 +fun global_thms st name = PureThy.get_thms (theory_of_thm st) (Facts.Named (name, NONE));
    1.10 +fun global_thm  st name = PureThy.get_thm  (theory_of_thm st) (Facts.Named (name, NONE));
    1.11  
    1.12  
    1.13  (* needed in the process of fully simplifying permutations *)
    1.14 @@ -111,8 +111,8 @@
    1.15              (if (applicable_app f) then
    1.16                let
    1.17                  val name = Sign.base_name n
    1.18 -                val at_inst = PureThy.get_thm sg (Name ("at_" ^ name ^ "_inst"))
    1.19 -                val pt_inst = PureThy.get_thm sg (Name ("pt_" ^ name ^ "_inst"))
    1.20 +                val at_inst = dynamic_thm sg ("at_" ^ name ^ "_inst")
    1.21 +                val pt_inst = dynamic_thm sg ("pt_" ^ name ^ "_inst")
    1.22                in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
    1.23              else NONE)
    1.24        | _ => NONE
    1.25 @@ -146,7 +146,7 @@
    1.26      ("general simplification of permutations", fn st =>
    1.27      let
    1.28         val ss' = Simplifier.theory_context (theory_of_thm st) ss
    1.29 -         addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@eqvt_thms)
    1.30 +         addsimps ((List.concat (map (global_thms st) dyn_thms))@eqvt_thms)
    1.31           delcongs weak_congs
    1.32           addcongs strong_congs
    1.33           addsimprocs [perm_simproc_fun, perm_simproc_app]
    1.34 @@ -198,13 +198,13 @@
    1.35            SOME (Drule.instantiate'
    1.36              [SOME (ctyp_of sg (fastype_of t))]
    1.37              [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
    1.38 -            (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
    1.39 -             PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
    1.40 +            (mk_meta_eq ([dynamic_thm sg ("pt_"^tname'^"_inst"),
    1.41 +             dynamic_thm sg ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
    1.42          else
    1.43            SOME (Drule.instantiate'
    1.44              [SOME (ctyp_of sg (fastype_of t))]
    1.45              [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
    1.46 -            (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS 
    1.47 +            (mk_meta_eq (dynamic_thm sg ("cp_"^tname'^"_"^uname'^"_inst") RS 
    1.48               cp1_aux)))
    1.49        else NONE
    1.50      end
    1.51 @@ -307,7 +307,7 @@
    1.52                Logic.strip_assums_concl (hd (prems_of supports_rule'));
    1.53              val supports_rule'' = Drule.cterm_instantiate
    1.54                [(cert (head_of S), cert s')] supports_rule'
    1.55 -            val fin_supp = dynamic_thms st ("fin_supp")
    1.56 +            val fin_supp = global_thms st ("fin_supp")
    1.57              val ss' = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
    1.58            in
    1.59              (tactical ("guessing of the right supports-set",
    1.60 @@ -326,8 +326,8 @@
    1.61  fun fresh_guess_tac tactical ss i st =
    1.62      let 
    1.63  	val goal = List.nth(cprems_of st, i-1)
    1.64 -        val fin_supp = dynamic_thms st ("fin_supp")
    1.65 -        val fresh_atm = dynamic_thms st ("fresh_atm")
    1.66 +        val fin_supp = global_thms st ("fin_supp")
    1.67 +        val fresh_atm = global_thms st ("fresh_atm")
    1.68  	val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
    1.69          val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
    1.70      in