src/HOL/Nominal/Nominal.thy
changeset 18579 002d371401f5
parent 18578 68420ce82a0b
child 18600 20ad06db427b
     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)