changed the name of the type "nOption" to "noption".
authorurbanc
Thu Jan 05 12:09:26 2006 +0100 (2006-01-05)
changeset 18579002d371401f5
parent 18578 68420ce82a0b
child 18580 4fdd39ea2f40
changed the name of the type "nOption" to "noption".
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Jan 04 20:20:25 2006 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Jan 05 12:09:26 2006 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4    perm_none_def:  "pi\<bullet>None    = None"
     1.5  
     1.6  (* a "private" copy of the option type used in the abstraction function *)
     1.7 -datatype 'a nOption = nSome 'a | nNone
     1.8 +datatype 'a noption = nSome 'a | nNone
     1.9  
    1.10  primrec (perm_noption)
    1.11    perm_Nsome_def:  "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
    1.12 @@ -793,7 +793,7 @@
    1.13  
    1.14  lemma pt_noption_inst:
    1.15    assumes pta: "pt TYPE('a) TYPE('x)"
    1.16 -  shows  "pt TYPE('a nOption) TYPE('x)"
    1.17 +  shows  "pt TYPE('a noption) TYPE('x)"
    1.18  apply(auto simp only: pt_def)
    1.19  apply(case_tac "x")
    1.20  apply(simp_all add: pt1[OF pta])
    1.21 @@ -2110,7 +2110,7 @@
    1.22  
    1.23  lemma cp_noption_inst:
    1.24    assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
    1.25 -  shows "cp TYPE ('a nOption) TYPE('x) TYPE('y)"
    1.26 +  shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
    1.27  using c1
    1.28  apply(simp add: cp_def)
    1.29  apply(auto)
    1.30 @@ -2158,11 +2158,11 @@
    1.31  lemma pt_abs_fun_inst:
    1.32    assumes pt: "pt TYPE('a) TYPE('x)"
    1.33    and     at: "at TYPE('x)"
    1.34 -  shows "pt TYPE('x\<Rightarrow>('a nOption)) TYPE('x)"
    1.35 +  shows "pt TYPE('x\<Rightarrow>('a noption)) TYPE('x)"
    1.36    by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at])
    1.37  
    1.38  constdefs
    1.39 -  abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a nOption))" ("[_]._" [100,100] 100)
    1.40 +  abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a noption))" ("[_]._" [100,100] 100)
    1.41    "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))"
    1.42  
    1.43  lemma abs_fun_if: 
    1.44 @@ -2511,12 +2511,12 @@
    1.45  section {* abstraction type for the parsing in nominal datatype *}
    1.46  (*==============================================================*)
    1.47  consts
    1.48 -  "ABS_set" :: "('x\<Rightarrow>('a nOption)) set"
    1.49 +  "ABS_set" :: "('x\<Rightarrow>('a noption)) set"
    1.50  inductive ABS_set
    1.51    intros
    1.52    ABS_in: "(abs_fun a x)\<in>ABS_set"
    1.53  
    1.54 -typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a nOption)) set"
    1.55 +typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a noption)) set"
    1.56  proof 
    1.57    fix x::"'a" and a::"'x"
    1.58    show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Jan 04 20:20:25 2006 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Jan 05 12:09:26 2006 +0100
     2.3 @@ -406,7 +406,7 @@
     2.4  
     2.5       (* show that                       *)
     2.6       (*      fun(pt_<ak>,pt_<ak>)       *)
     2.7 -     (*      nOption(pt_<ak>)           *)
     2.8 +     (*      noption(pt_<ak>)           *)
     2.9       (*      option(pt_<ak>)            *)
    2.10       (*      list(pt_<ak>)              *)
    2.11       (*      *(pt_<ak>,pt_<ak>)         *)
    2.12 @@ -433,7 +433,7 @@
    2.13         in 
    2.14  	thy
    2.15  	|> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    2.16 -        |> AxClass.add_inst_arity_i ("nominal.nOption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    2.17 +        |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    2.18          |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    2.19          |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    2.20          |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    2.21 @@ -575,7 +575,7 @@
    2.22           |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
    2.23           |> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
    2.24           |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    2.25 -         |> AxClass.add_inst_arity_i ("nominal.nOption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    2.26 +         |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    2.27          end) ak_names thy) ak_names thy25;
    2.28         
    2.29       (* show that discrete nominal types are permutation types, finitely     *) 
     3.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Jan 04 20:20:25 2006 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Jan 05 12:09:26 2006 +0100
     3.3 @@ -115,7 +115,7 @@
     3.4      val rps = map Library.swap ps;
     3.5  
     3.6      fun replace_types (Type ("nominal.ABS", [T, U])) = 
     3.7 -          Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])
     3.8 +          Type ("fun", [T, Type ("nominal.noption", [replace_types U])])
     3.9        | replace_types (Type (s, Ts)) =
    3.10            Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
    3.11        | replace_types T = T;
    3.12 @@ -386,16 +386,16 @@
    3.13        (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
    3.14      val big_rep_name =
    3.15        space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
    3.16 -        (fn (i, ("nominal.nOption", _, _)) => NONE
    3.17 +        (fn (i, ("nominal.noption", _, _)) => NONE
    3.18            | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
    3.19      val _ = warning ("big_rep_name: " ^ big_rep_name);
    3.20  
    3.21      fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
    3.22            (case AList.lookup op = descr i of
    3.23 -             SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
    3.24 +             SOME ("nominal.noption", _, [(_, [dt']), _]) =>
    3.25                 apfst (cons dt) (strip_option dt')
    3.26             | _ => ([], dtf))
    3.27 -      | strip_option (DtType ("fun", [dt, DtType ("nominal.nOption", [dt'])])) =
    3.28 +      | strip_option (DtType ("fun", [dt, DtType ("nominal.noption", [dt'])])) =
    3.29            apfst (cons dt) (strip_option dt')
    3.30        | strip_option dt = ([], dt);
    3.31  
    3.32 @@ -417,7 +417,7 @@
    3.33              fun mk_abs_fun (T, (i, t)) =
    3.34                let val U = fastype_of t
    3.35                in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
    3.36 -                Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)
    3.37 +                Type ("nominal.noption", [U])) $ mk_Free "y" T i $ t)
    3.38                end
    3.39            in (j + 1, j' + length Ts,
    3.40              case dt'' of
    3.41 @@ -438,7 +438,7 @@
    3.42  
    3.43      val (intr_ts, ind_consts) =
    3.44        apfst List.concat (ListPair.unzip (List.mapPartial
    3.45 -        (fn ((_, ("nominal.nOption", _, _)), _) => NONE
    3.46 +        (fn ((_, ("nominal.noption", _, _)), _) => NONE
    3.47            | ((i, (_, _, constrs)), rep_set_name) =>
    3.48                let val T = nth_dtyp i
    3.49                in SOME (map (make_intr rep_set_name T) constrs,
    3.50 @@ -456,7 +456,7 @@
    3.51      val _ = warning "proving closure under permutation...";
    3.52  
    3.53      val perm_indnames' = List.mapPartial
    3.54 -      (fn (x, (_, ("nominal.nOption", _, _))) => NONE | (x, _) => SOME x)
    3.55 +      (fn (x, (_, ("nominal.noption", _, _))) => NONE | (x, _) => SOME x)
    3.56        (perm_indnames ~~ descr);
    3.57  
    3.58      fun mk_perm_closed name = map (fn th => standard (th RS mp))
    3.59 @@ -580,11 +580,11 @@
    3.60          val U = fastype_of t
    3.61        in
    3.62          Const ("nominal.abs_fun", T --> U --> T -->
    3.63 -          Type ("nominal.nOption", [U])) $ x $ t
    3.64 +          Type ("nominal.noption", [U])) $ x $ t
    3.65        end;
    3.66  
    3.67      val (ty_idxs, _) = foldl
    3.68 -      (fn ((i, ("nominal.nOption", _, _)), p) => p
    3.69 +      (fn ((i, ("nominal.noption", _, _)), p) => p
    3.70          | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
    3.71  
    3.72      fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
    3.73 @@ -599,7 +599,7 @@
    3.74        in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
    3.75  
    3.76      val (descr'', ndescr) = ListPair.unzip (List.mapPartial
    3.77 -      (fn (i, ("nominal.nOption", _, _)) => NONE
    3.78 +      (fn (i, ("nominal.noption", _, _)) => NONE
    3.79          | (i, (s, dts, constrs)) =>
    3.80               let
    3.81                 val SOME index = AList.lookup op = ty_idxs i;
    3.82 @@ -624,7 +624,7 @@
    3.83        Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
    3.84  
    3.85      val recTs' = List.mapPartial
    3.86 -      (fn ((_, ("nominal.nOption", _, _)), T) => NONE
    3.87 +      (fn ((_, ("nominal.noption", _, _)), T) => NONE
    3.88          | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
    3.89      val recTs = get_rec_types descr'' sorts';
    3.90      val newTs' = Library.take (length new_type_names, recTs');