Exported perm_of_pair, mk_not_sym, and perm_simproc.
authorberghofe
Tue Mar 27 17:54:37 2007 +0200 (2007-03-27)
changeset 22529902ed60d53a7
parent 22528 8501c4a62a3c
child 22530 c192c5d1a6f2
Exported perm_of_pair, mk_not_sym, and perm_simproc.
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Mar 27 12:28:42 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Mar 27 17:54:37 2007 +0200
     1.3 @@ -14,6 +14,9 @@
     1.4    val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
     1.5    val get_nominal_datatype : theory -> string -> nominal_datatype_info option
     1.6    val mk_perm: typ list -> term -> term -> term
     1.7 +  val perm_of_pair: term * term -> term
     1.8 +  val mk_not_sym: thm list -> thm list
     1.9 +  val perm_simproc: simproc
    1.10    val setup: theory -> theory
    1.11  end
    1.12  
    1.13 @@ -220,6 +223,18 @@
    1.14      val U = fastype_of1 (Ts, u)
    1.15    in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
    1.16  
    1.17 +fun perm_of_pair (x, y) =
    1.18 +  let
    1.19 +    val T = fastype_of x;
    1.20 +    val pT = mk_permT T
    1.21 +  in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
    1.22 +    HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
    1.23 +  end;
    1.24 +
    1.25 +fun mk_not_sym ths = maps (fn th => case prop_of th of
    1.26 +    _ $ (Const ("Not", _) $ _) => [th, th RS not_sym]
    1.27 +  | _ => [th]) ths;
    1.28 +
    1.29  fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
    1.30    let
    1.31      (* this theory is used just for parsing *)
    1.32 @@ -1592,14 +1607,6 @@
    1.33      val perm_fresh_fresh = PureThy.get_thms thy11 (Name "perm_fresh_fresh");
    1.34      val perm_swap = PureThy.get_thms thy11 (Name "perm_swap");
    1.35  
    1.36 -    fun perm_of_pair (x, y) =
    1.37 -      let
    1.38 -        val T = fastype_of x;
    1.39 -        val pT = mk_permT T
    1.40 -      in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
    1.41 -        HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
    1.42 -      end;
    1.43 -
    1.44      val finite_premss = map (fn aT =>
    1.45        map (fn (f, T) => HOLogic.mk_Trueprop
    1.46          (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
    1.47 @@ -1798,10 +1805,6 @@
    1.48                      val pi2 = map perm_of_pair (boundsr ~~ freshs1);
    1.49                      val rpi2 = rev pi2;
    1.50  
    1.51 -                    fun mk_not_sym ths = List.concat (map (fn th =>
    1.52 -                      case prop_of th of
    1.53 -                          _ $ (Const ("Not", _) $ _) => [th, th RS not_sym]
    1.54 -                        | _ => [th]) ths);
    1.55                      val fresh_prems' = mk_not_sym fresh_prems;
    1.56                      val freshs2' = mk_not_sym freshs2;
    1.57