# HG changeset patch
# User urbanc
# Date 1136459366 -3600
# Node ID 002d371401f58bc018d8cdd76f0fd9524301297b
# Parent  68420ce82a0b6e5ff7cca67acb772ffe47a58925
changed the name of the type "nOption" to "noption".

diff -r 68420ce82a0b -r 002d371401f5 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Jan 04 20:20:25 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Jan 05 12:09:26 2006 +0100
@@ -82,7 +82,7 @@
   perm_none_def:  "pi\<bullet>None    = None"
 
 (* a "private" copy of the option type used in the abstraction function *)
-datatype 'a nOption = nSome 'a | nNone
+datatype 'a noption = nSome 'a | nNone
 
 primrec (perm_noption)
   perm_Nsome_def:  "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
@@ -793,7 +793,7 @@
 
 lemma pt_noption_inst:
   assumes pta: "pt TYPE('a) TYPE('x)"
-  shows  "pt TYPE('a nOption) TYPE('x)"
+  shows  "pt TYPE('a noption) TYPE('x)"
 apply(auto simp only: pt_def)
 apply(case_tac "x")
 apply(simp_all add: pt1[OF pta])
@@ -2110,7 +2110,7 @@
 
 lemma cp_noption_inst:
   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
-  shows "cp TYPE ('a nOption) TYPE('x) TYPE('y)"
+  shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
 using c1
 apply(simp add: cp_def)
 apply(auto)
@@ -2158,11 +2158,11 @@
 lemma pt_abs_fun_inst:
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
-  shows "pt TYPE('x\<Rightarrow>('a nOption)) TYPE('x)"
+  shows "pt TYPE('x\<Rightarrow>('a noption)) TYPE('x)"
   by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at])
 
 constdefs
-  abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a nOption))" ("[_]._" [100,100] 100)
+  abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a noption))" ("[_]._" [100,100] 100)
   "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))"
 
 lemma abs_fun_if: 
@@ -2511,12 +2511,12 @@
 section {* abstraction type for the parsing in nominal datatype *}
 (*==============================================================*)
 consts
-  "ABS_set" :: "('x\<Rightarrow>('a nOption)) set"
+  "ABS_set" :: "('x\<Rightarrow>('a noption)) set"
 inductive ABS_set
   intros
   ABS_in: "(abs_fun a x)\<in>ABS_set"
 
-typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a nOption)) set"
+typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a noption)) set"
 proof 
   fix x::"'a" and a::"'x"
   show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
diff -r 68420ce82a0b -r 002d371401f5 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Jan 04 20:20:25 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Jan 05 12:09:26 2006 +0100
@@ -406,7 +406,7 @@
 
      (* show that                       *)
      (*      fun(pt_<ak>,pt_<ak>)       *)
-     (*      nOption(pt_<ak>)           *)
+     (*      noption(pt_<ak>)           *)
      (*      option(pt_<ak>)            *)
      (*      list(pt_<ak>)              *)
      (*      *(pt_<ak>,pt_<ak>)         *)
@@ -433,7 +433,7 @@
        in 
 	thy
 	|> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
-        |> AxClass.add_inst_arity_i ("nominal.nOption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
+        |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
         |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
         |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
@@ -575,7 +575,7 @@
          |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
          |> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
          |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
-         |> AxClass.add_inst_arity_i ("nominal.nOption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+         |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
         end) ak_names thy) ak_names thy25;
        
      (* show that discrete nominal types are permutation types, finitely     *) 
diff -r 68420ce82a0b -r 002d371401f5 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Jan 04 20:20:25 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Jan 05 12:09:26 2006 +0100
@@ -115,7 +115,7 @@
     val rps = map Library.swap ps;
 
     fun replace_types (Type ("nominal.ABS", [T, U])) = 
-          Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])
+          Type ("fun", [T, Type ("nominal.noption", [replace_types U])])
       | replace_types (Type (s, Ts)) =
           Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
       | replace_types T = T;
@@ -386,16 +386,16 @@
       (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
     val big_rep_name =
       space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
-        (fn (i, ("nominal.nOption", _, _)) => NONE
+        (fn (i, ("nominal.noption", _, _)) => NONE
           | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
     val _ = warning ("big_rep_name: " ^ big_rep_name);
 
     fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
           (case AList.lookup op = descr i of
-             SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
+             SOME ("nominal.noption", _, [(_, [dt']), _]) =>
                apfst (cons dt) (strip_option dt')
            | _ => ([], dtf))
-      | strip_option (DtType ("fun", [dt, DtType ("nominal.nOption", [dt'])])) =
+      | strip_option (DtType ("fun", [dt, DtType ("nominal.noption", [dt'])])) =
           apfst (cons dt) (strip_option dt')
       | strip_option dt = ([], dt);
 
@@ -417,7 +417,7 @@
             fun mk_abs_fun (T, (i, t)) =
               let val U = fastype_of t
               in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
-                Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)
+                Type ("nominal.noption", [U])) $ mk_Free "y" T i $ t)
               end
           in (j + 1, j' + length Ts,
             case dt'' of
@@ -438,7 +438,7 @@
 
     val (intr_ts, ind_consts) =
       apfst List.concat (ListPair.unzip (List.mapPartial
-        (fn ((_, ("nominal.nOption", _, _)), _) => NONE
+        (fn ((_, ("nominal.noption", _, _)), _) => NONE
           | ((i, (_, _, constrs)), rep_set_name) =>
               let val T = nth_dtyp i
               in SOME (map (make_intr rep_set_name T) constrs,
@@ -456,7 +456,7 @@
     val _ = warning "proving closure under permutation...";
 
     val perm_indnames' = List.mapPartial
-      (fn (x, (_, ("nominal.nOption", _, _))) => NONE | (x, _) => SOME x)
+      (fn (x, (_, ("nominal.noption", _, _))) => NONE | (x, _) => SOME x)
       (perm_indnames ~~ descr);
 
     fun mk_perm_closed name = map (fn th => standard (th RS mp))
@@ -580,11 +580,11 @@
         val U = fastype_of t
       in
         Const ("nominal.abs_fun", T --> U --> T -->
-          Type ("nominal.nOption", [U])) $ x $ t
+          Type ("nominal.noption", [U])) $ x $ t
       end;
 
     val (ty_idxs, _) = foldl
-      (fn ((i, ("nominal.nOption", _, _)), p) => p
+      (fn ((i, ("nominal.noption", _, _)), p) => p
         | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
 
     fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
@@ -599,7 +599,7 @@
       in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
 
     val (descr'', ndescr) = ListPair.unzip (List.mapPartial
-      (fn (i, ("nominal.nOption", _, _)) => NONE
+      (fn (i, ("nominal.noption", _, _)) => NONE
         | (i, (s, dts, constrs)) =>
              let
                val SOME index = AList.lookup op = ty_idxs i;
@@ -624,7 +624,7 @@
       Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
 
     val recTs' = List.mapPartial
-      (fn ((_, ("nominal.nOption", _, _)), T) => NONE
+      (fn ((_, ("nominal.noption", _, _)), T) => NONE
         | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
     val recTs = get_rec_types descr'' sorts';
     val newTs' = Library.take (length new_type_names, recTs');