some cleaning up to do with contexts
authorurbanc
Thu Sep 13 23:58:38 2007 +0200 (2007-09-13)
changeset 24571a6d0428dea8e
parent 24570 621b60b1df00
child 24572 7be5353ec4bd
some cleaning up to do with contexts
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_thmdecls.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Sep 13 18:11:59 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 13 23:58:38 2007 +0200
     1.3 @@ -1224,6 +1224,18 @@
     1.4  apply(rule pt1[OF pt])
     1.5  done
     1.6  
     1.7 +lemma pt_swap_bij'':
     1.8 +  fixes a  :: "'x"
     1.9 +  and   x  :: "'a"
    1.10 +  assumes pt: "pt TYPE('a) TYPE('x)"
    1.11 +  and     at: "at TYPE('x)"
    1.12 +  shows "[(a,a)]\<bullet>x = x"
    1.13 +apply(rule trans)
    1.14 +apply(rule pt3[OF pt])
    1.15 +apply(rule at_ds1[OF at])
    1.16 +apply(rule pt1[OF pt])
    1.17 +done
    1.18 +
    1.19  lemma pt_set_bij1:
    1.20    fixes pi :: "'x prm"
    1.21    and   x  :: "'a"
    1.22 @@ -1754,6 +1766,7 @@
    1.23  
    1.24  section {* equivaraince for some connectives *}
    1.25  
    1.26 +(*
    1.27  lemma pt_all_eqvt:
    1.28    fixes  pi :: "'x prm"
    1.29    and     x :: "'a"
    1.30 @@ -1764,6 +1777,18 @@
    1.31  apply(drule_tac x="pi\<bullet>x" in spec)
    1.32  apply(simp add: pt_rev_pi[OF pt, OF at])
    1.33  done
    1.34 +*)
    1.35 +
    1.36 +lemma pt_all_eqvt:
    1.37 +  fixes  pi :: "'x prm"
    1.38 +  and     x :: "'a"
    1.39 +  assumes pt: "pt TYPE('a) TYPE('x)"
    1.40 +  and     at: "at TYPE('x)"
    1.41 +  shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). P ((rev pi)\<bullet>x))"
    1.42 +apply(auto simp add: perm_bool)
    1.43 +apply(drule_tac x="pi\<bullet>x" in spec)
    1.44 +apply(simp add: pt_rev_pi[OF pt, OF at])
    1.45 +done
    1.46  
    1.47  lemma pt_ex_eqvt:
    1.48    fixes  pi :: "'x prm"
     2.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Sep 13 18:11:59 2007 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Sep 13 23:58:38 2007 +0200
     2.3 @@ -147,7 +147,7 @@
     2.4        InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
     2.5      val raw_induct = atomize_induct raw_induct;
     2.6      val monos = InductivePackage.get_monos ctxt;
     2.7 -    val eqvt_thms = NominalThmDecls.get_eqvt_thms thy;
     2.8 +    val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     2.9      val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of
    2.10          [] => ()
    2.11        | xs => error ("Missing equivariance theorem for predicate(s): " ^
    2.12 @@ -461,7 +461,7 @@
    2.13        end;
    2.14      val perm_pi_simp = PureThy.get_thms thy (Name "perm_pi_simp");
    2.15      val eqvt_ss = HOL_basic_ss addsimps
    2.16 -      (NominalThmDecls.get_eqvt_thms thy @ perm_pi_simp) addsimprocs
    2.17 +      (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
    2.18        [mk_perm_bool_simproc names];
    2.19      val t = Logic.unvarify (concl_of raw_induct);
    2.20      val pi = Name.variant (add_term_names (t, [])) "pi";
     3.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Thu Sep 13 18:11:59 2007 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Sep 13 23:58:38 2007 +0200
     3.3 @@ -133,7 +133,7 @@
     3.4     end
     3.5  
     3.6  (* function for simplyfying permutations *)
     3.7 -fun perm_simp_gen dyn_thms f ss i = 
     3.8 +fun perm_simp_gen dyn_thms eqvt_thms ss i = 
     3.9      ("general simplification of permutations", fn st =>
    3.10      let
    3.11  
    3.12 @@ -143,7 +143,7 @@
    3.13         val perm_sp_app = Simplifier.simproc (theory_of_thm st) "perm_simproc_app" 
    3.14  	                 ["Nominal.perm pi x"] (perm_simproc_app st);
    3.15  
    3.16 -       val ss' = ss addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@(f st))
    3.17 +       val ss' = ss addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@eqvt_thms)
    3.18                      delcongs weak_congs
    3.19                      addcongs strong_congs
    3.20                      addsimprocs [perm_sp_fun, perm_sp_app]
    3.21 @@ -152,23 +152,21 @@
    3.22      end);
    3.23  
    3.24  (* general simplification of permutations and permutation that arose from eqvt-problems *)
    3.25 -val perm_simp = 
    3.26 +fun perm_simp ss = 
    3.27      let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
    3.28      in 
    3.29 -	perm_simp_gen simps (fn st => [])
    3.30 +	perm_simp_gen simps [] ss
    3.31      end;
    3.32  
    3.33 -val eqvt_simp = 
    3.34 +fun eqvt_simp ss = 
    3.35      let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
    3.36 -	fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
    3.37 +	val eqvts_thms = NominalThmDecls.get_eqvt_thms (Simplifier.the_context ss);
    3.38      in 
    3.39 -	perm_simp_gen simps eqvts_thms
    3.40 +	perm_simp_gen simps eqvts_thms ss
    3.41      end;
    3.42  
    3.43 -(* FIXME removes the name lookup for these theorems use an ml value instead *)
    3.44  
    3.45  (* main simplification tactics for permutations *)
    3.46 -(* FIXME: perm_simp_tac should simplify more permutations *)
    3.47  fun perm_simp_tac tactical ss i = DETERM (tactical (perm_simp ss i));
    3.48  fun eqvt_simp_tac tactical ss i = DETERM (tactical (eqvt_simp ss i)); 
    3.49  
    3.50 @@ -384,6 +382,7 @@
    3.51  val perm_full_simp_meth_debug = local_simp_meth_setup (perm_full_simp_tac DEBUG_tac);
    3.52  val supports_meth             = local_simp_meth_setup (supports_tac NO_DEBUG_tac);
    3.53  val supports_meth_debug       = local_simp_meth_setup (supports_tac DEBUG_tac);
    3.54 +
    3.55  val finite_guess_meth         = basic_simp_meth_setup false (finite_guess_tac NO_DEBUG_tac);
    3.56  val finite_guess_meth_debug   = basic_simp_meth_setup true (finite_guess_tac DEBUG_tac);
    3.57  val fresh_guess_meth          = basic_simp_meth_setup false (fresh_guess_tac NO_DEBUG_tac);
     4.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Thu Sep 13 18:11:59 2007 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Sep 13 23:58:38 2007 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4     declaration "eqvts" "bijs" and "freshs".
     4.5  
     4.6     By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
     4.7 -   in a data-slot in the theory context. Possible modifiers
     4.8 +   in a data-slot in the context. Possible modifiers
     4.9     are [attribute add] and [attribute del] for adding and deleting,
    4.10     respectively the lemma from the data-slot.
    4.11  *)
    4.12 @@ -18,9 +18,9 @@
    4.13    val eqvt_force_add: attribute
    4.14    val eqvt_force_del: attribute
    4.15    val setup: theory -> theory
    4.16 -  val get_eqvt_thms: theory -> thm list
    4.17 -  val get_fresh_thms: theory -> thm list
    4.18 -  val get_bij_thms: theory -> thm list
    4.19 +  val get_eqvt_thms: Proof.context -> thm list
    4.20 +  val get_fresh_thms: Proof.context -> thm list
    4.21 +  val get_bij_thms: Proof.context -> thm list
    4.22  
    4.23  
    4.24    val NOMINAL_EQVT_DEBUG : bool ref
    4.25 @@ -62,18 +62,13 @@
    4.26        pretty_thms "Bijection lemmas:" (#bijs data)])
    4.27    end;
    4.28  
    4.29 -
    4.30 -val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
    4.31 -val get_fresh_thms = Context.Theory #> Data.get #> #freshs;
    4.32 -val get_bij_thms = Context.Theory #> Data.get #> #bijs;
    4.33 +val get_eqvt_thms = Context.Proof #> Data.get #> #eqvts;
    4.34 +val get_fresh_thms = Context.Proof #> Data.get #> #freshs;
    4.35 +val get_bij_thms = Context.Proof #> Data.get #> #bijs;
    4.36  
    4.37  (* FIXME: should be a function in a library *)
    4.38  fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
    4.39  
    4.40 -val perm_boolE = thm "perm_boolE";
    4.41 -val perm_boolI = thm "perm_boolI";
    4.42 -val perm_fun_def = thm "perm_fun_def";
    4.43 -
    4.44  val NOMINAL_EQVT_DEBUG = ref false;
    4.45  
    4.46  fun tactic (msg,tac) =
    4.47 @@ -90,14 +85,12 @@
    4.48          val perm_pi_simp = dynamic_thms ctx "perm_pi_simp"
    4.49      in
    4.50          EVERY [tactic ("iffI applied",rtac iffI 1),
    4.51 -	       tactic ("remove pi with perm_boolE",
    4.52 -                          (dtac perm_boolE 1)),
    4.53 -               tactic ("solve with orig_thm",
    4.54 -                          (etac orig_thm 1)),
    4.55 +	       tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)),
    4.56 +               tactic ("solve with orig_thm", (etac orig_thm 1)),
    4.57                 tactic ("applies orig_thm instantiated with rev pi",
    4.58                            dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
    4.59  	       tactic ("getting rid of the pi on the right",
    4.60 -                          (rtac perm_boolI 1)),
    4.61 +                          (rtac @{thm perm_boolI} 1)),
    4.62                 tactic ("getting rid of all remaining perms",
    4.63                            full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)]
    4.64      end;