src/HOL/Nominal/nominal_atoms.ML
changeset 41562 90fb3d7474df
parent 41163 3f21a269780e
child 44684 8dde3352d5c4
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jan 15 12:35:29 2011 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jan 15 12:38:56 2011 +0100
     1.3 @@ -172,26 +172,31 @@
     1.4      (* overloades then the general swap-function                       *) 
     1.5      val (swap_eqs, thy3) = fold_map (fn (ak_name, T) => fn thy =>
     1.6        let
     1.7 +        val thy' = Sign.add_path "rec" thy;
     1.8          val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
     1.9 -        val swap_name = Sign.full_bname thy ("swap_" ^ ak_name);
    1.10 +        val swap_name = "swap_" ^ ak_name;
    1.11 +        val full_swap_name = Sign.full_bname thy' swap_name;
    1.12          val a = Free ("a", T);
    1.13          val b = Free ("b", T);
    1.14          val c = Free ("c", T);
    1.15          val ab = Free ("ab", HOLogic.mk_prodT (T, T))
    1.16          val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
    1.17 -        val cswap_akname = Const (swap_name, swapT);
    1.18 +        val cswap_akname = Const (full_swap_name, swapT);
    1.19          val cswap = Const ("Nominal.swap", swapT)
    1.20  
    1.21 -        val name = "swap_"^ak_name^"_def";
    1.22 +        val name = swap_name ^ "_def";
    1.23          val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.24 -                (cswap_akname $ HOLogic.mk_prod (a,b) $ c,
    1.25 +                (Free (swap_name, swapT) $ HOLogic.mk_prod (a,b) $ c,
    1.26                      cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
    1.27          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
    1.28        in
    1.29 -        thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)] 
    1.30 -            |> Global_Theory.add_defs_unchecked true [((Binding.name name, def2),[])]
    1.31 -            |> snd
    1.32 -            |> OldPrimrec.add_primrec_unchecked_i "" [(("", def1),[])]
    1.33 +        thy' |>
    1.34 +        Primrec.add_primrec_global
    1.35 +          [(Binding.name swap_name, SOME swapT, NoSyn)]
    1.36 +          [(Attrib.empty_binding, def1)] ||>
    1.37 +        Sign.parent_path ||>>
    1.38 +        Global_Theory.add_defs_unchecked true
    1.39 +          [((Binding.name name, def2), [])] |>> (snd o fst)
    1.40        end) ak_names_types thy1;
    1.41      
    1.42      (* declares a permutation function for every atom-kind acting  *)
    1.43 @@ -201,25 +206,29 @@
    1.44      (* <ak>_prm_<ak> (x#xs) a = swap_<ak> x (perm xs a)            *)
    1.45      val (prm_eqs, thy4) = fold_map (fn (ak_name, T) => fn thy =>
    1.46        let
    1.47 +        val thy' = Sign.add_path "rec" thy;
    1.48          val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
    1.49 -        val swap_name = Sign.full_bname thy ("swap_" ^ ak_name)
    1.50 +        val swap_name = Sign.full_bname thy' ("swap_" ^ ak_name)
    1.51          val prmT = mk_permT T --> T --> T;
    1.52          val prm_name = ak_name ^ "_prm_" ^ ak_name;
    1.53 -        val qu_prm_name = Sign.full_bname thy prm_name;
    1.54 +        val prm = Free (prm_name, prmT);
    1.55          val x  = Free ("x", HOLogic.mk_prodT (T, T));
    1.56          val xs = Free ("xs", mk_permT T);
    1.57          val a  = Free ("a", T) ;
    1.58  
    1.59          val cnil  = Const ("List.list.Nil", mk_permT T);
    1.60          
    1.61 -        val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (qu_prm_name, prmT) $ cnil $ a, a));
    1.62 +        val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (prm $ cnil $ a, a));
    1.63  
    1.64          val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.65 -                   (Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
    1.66 -                    Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
    1.67 +                   (prm $ mk_Cons x xs $ a,
    1.68 +                    Const (swap_name, swapT) $ x $ (prm $ xs $ a)));
    1.69        in
    1.70 -        thy |> Sign.add_consts_i [(Binding.name prm_name, mk_permT T --> T --> T, NoSyn)] 
    1.71 -            |> OldPrimrec.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
    1.72 +        thy' |>
    1.73 +        Primrec.add_primrec_global
    1.74 +          [(Binding.name prm_name, SOME prmT, NoSyn)]
    1.75 +          [(Attrib.empty_binding, def1), (Attrib.empty_binding, def2)] ||>
    1.76 +        Sign.parent_path
    1.77        end) ak_names_types thy3;
    1.78      
    1.79      (* defines permutation functions for all combinations of atom-kinds; *)
    1.80 @@ -238,13 +247,15 @@
    1.81            val pi = Free ("pi", mk_permT T);
    1.82            val a  = Free ("a", T');
    1.83            val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
    1.84 -          val cperm_def = Const (Sign.full_bname thy' perm_def_name, mk_permT T --> T' --> T');
    1.85 +          val thy'' = Sign.add_path "rec" thy'
    1.86 +          val cperm_def = Const (Sign.full_bname thy'' perm_def_name, mk_permT T --> T' --> T');
    1.87 +          val thy''' = Sign.parent_path thy'';
    1.88  
    1.89            val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
    1.90            val def = Logic.mk_equals
    1.91                      (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
    1.92          in
    1.93 -          Global_Theory.add_defs_unchecked true [((Binding.name name, def),[])] thy'
    1.94 +          Global_Theory.add_defs_unchecked true [((Binding.name name, def), [])] thy'''
    1.95          end) ak_names_types thy) ak_names_types thy4;
    1.96      
    1.97      (* proves that every atom-kind is an instance of at *)