Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Nominal/Nominal2_Eqvt.thy
changeset 1037 2845e736dc1a
parent 947 fa810f01f7b5
child 1039 0d832c36b1bb
equal deleted inserted replaced
1032:135bf399c036 1037:2845e736dc1a 
     4     Equivariance, Supp and Fresh Lemmas for Operators. 
     4     Equivariance, Supp and Fresh Lemmas for Operators. 
     5 *)
 
     5 *)
 
     6 theory Nominal2_Eqvt
 
     6 theory Nominal2_Eqvt
 
     7 imports Nominal2_Base
 
     7 imports Nominal2_Base
 
     8 uses ("nominal_thmdecls.ML")
 
     8 uses ("nominal_thmdecls.ML")
 
       
     9      ("nominal_permeq.ML")
 
     9 begin
 
    10 begin
 
    10 
    11 
    11 section {* Logical Operators *}
 
    12 section {* Logical Operators *}
 
    12 
    13 
    13 lemma eq_eqvt:
 
    14 lemma eq_eqvt:
 
    41 lemma Not_eqvt:
 
    42 lemma Not_eqvt:
 
    42   shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
 
    43   shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
 
    43   by (simp add: permute_bool_def)
 
    44   by (simp add: permute_bool_def)
 
    44 
    45 
    45 lemma all_eqvt:
 
    46 lemma all_eqvt:
 
       
    47   shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
 
       
    48   unfolding permute_fun_def permute_bool_def
 
       
    49   by (auto, drule_tac x="p \<bullet> x" in spec, simp)
 
       
    50 
       
    51 lemma all_eqvt2:
 
    46   shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
 
    52   shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
 
    47   unfolding permute_fun_def permute_bool_def
 
    53   unfolding permute_fun_def permute_bool_def
 
    48   by (auto, drule_tac x="p \<bullet> x" in spec, simp)
 
    54   by (auto, drule_tac x="p \<bullet> x" in spec, simp)
 
    49 
    55 
    50 lemma ex_eqvt:
 
    56 lemma ex_eqvt:
 
       
    57   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
 
       
    58   unfolding permute_fun_def permute_bool_def
 
       
    59   by (auto, rule_tac x="p \<bullet> x" in exI, simp)
 
       
    60 
       
    61 lemma ex_eqvt2:
 
    51   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
 
    62   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
 
    52   unfolding permute_fun_def permute_bool_def
 
    63   unfolding permute_fun_def permute_bool_def
 
    53   by (auto, rule_tac x="p \<bullet> x" in exI, simp)
 
    64   by (auto, rule_tac x="p \<bullet> x" in exI, simp)
 
    54 
    65 
    55 lemma ex1_eqvt:
 
    66 lemma ex1_eqvt:
 
       
    67   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
 
       
    68   unfolding Ex1_def 
       
    69   by (simp add: ex_eqvt permute_fun_def conj_eqvt all_eqvt imp_eqvt eq_eqvt)
 
       
    70 
       
    71 lemma ex1_eqvt2:
 
    56   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
 
    72   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
 
    57   unfolding Ex1_def ex_eqvt conj_eqvt all_eqvt imp_eqvt eq_eqvt
 
    73   unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt
 
    58   by simp
 
    74   by simp
 
    59 
    75 
    60 lemma the_eqvt:
 
    76 lemma the_eqvt:
 
    61   assumes unique: "\<exists>!x. P x"
 
    77   assumes unique: "\<exists>!x. P x"
 
    62   shows "p \<bullet> (THE x. P x) = (THE x. p \<bullet> P (- p \<bullet> x))"
 
    78   shows "p \<bullet> (THE x. P x) = (THE x. p \<bullet> P (- p \<bullet> x))"
 
    63   apply(rule the1_equality [symmetric])
 
    79   apply(rule the1_equality [symmetric])
 
    64   apply(simp add: ex1_eqvt[symmetric])
 
    80   apply(simp add: ex1_eqvt2[symmetric])
 
    65   apply(simp add: permute_bool_def unique)
 
    81   apply(simp add: permute_bool_def unique)
 
    66   apply(simp add: permute_bool_def)
 
    82   apply(simp add: permute_bool_def)
 
    67   apply(rule theI'[OF unique])
 
    83   apply(rule theI'[OF unique])
 
    68   done
 
    84   done
 
    69 
    85 
    76 lemma not_mem_eqvt:
 
    92 lemma not_mem_eqvt:
 
    77   shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
 
    93   shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
 
    78   unfolding mem_def permute_fun_def by (simp add: Not_eqvt)
 
    94   unfolding mem_def permute_fun_def by (simp add: Not_eqvt)
 
    79 
    95 
    80 lemma Collect_eqvt:
 
    96 lemma Collect_eqvt:
 
       
    97   shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
 
       
    98   unfolding Collect_def permute_fun_def ..
 
       
    99 
       
   100 lemma Collect_eqvt2:
 
    81   shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
 
   101   shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
 
    82   unfolding Collect_def permute_fun_def ..
 
   102   unfolding Collect_def permute_fun_def ..
 
    83 
   103 
    84 lemma empty_eqvt:
 
   104 lemma empty_eqvt:
 
    85   shows "p \<bullet> {} = {}"
 
   105   shows "p \<bullet> {} = {}"
 
    86   unfolding empty_def Collect_eqvt False_eqvt ..
 
   106   unfolding empty_def Collect_eqvt2 False_eqvt ..
 
    87 
   107 
    88 lemma supp_set_empty:
 
   108 lemma supp_set_empty:
 
    89   shows "supp {} = {}"
 
   109   shows "supp {} = {}"
 
    90   by (simp add: supp_def empty_eqvt)
 
   110   by (simp add: supp_def empty_eqvt)
 
    91 
   111 
    93   shows "a \<sharp> {}"
 
   113   shows "a \<sharp> {}"
 
    94   by (simp add: fresh_def supp_set_empty)
 
   114   by (simp add: fresh_def supp_set_empty)
 
    95 
   115 
    96 lemma UNIV_eqvt:
 
   116 lemma UNIV_eqvt:
 
    97   shows "p \<bullet> UNIV = UNIV"
 
   117   shows "p \<bullet> UNIV = UNIV"
 
    98   unfolding UNIV_def Collect_eqvt True_eqvt ..
 
   118   unfolding UNIV_def Collect_eqvt2 True_eqvt ..
 
    99 
   119 
   100 lemma union_eqvt:
 
   120 lemma union_eqvt:
 
   101   shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
 
   121   shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
 
   102   unfolding Un_def Collect_eqvt disj_eqvt mem_eqvt by simp
 
   122   unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp
 
   103 
   123 
   104 lemma inter_eqvt:
 
   124 lemma inter_eqvt:
 
   105   shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
 
   125   shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
 
   106   unfolding Int_def Collect_eqvt conj_eqvt mem_eqvt by simp
 
   126   unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp
 
   107 
   127 
   108 lemma Diff_eqvt:
 
   128 lemma Diff_eqvt:
 
   109   fixes A B :: "'a::pt set"
 
   129   fixes A B :: "'a::pt set"
 
   110   shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
 
   130   shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
 
   111   unfolding set_diff_eq Collect_eqvt conj_eqvt Not_eqvt mem_eqvt by simp
 
   131   unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp
 
   112 
   132 
   113 lemma Compl_eqvt:
 
   133 lemma Compl_eqvt:
 
   114   fixes A :: "'a::pt set"
 
   134   fixes A :: "'a::pt set"
 
   115   shows "p \<bullet> (- A) = - (p \<bullet> A)"
 
   135   shows "p \<bullet> (- A) = - (p \<bullet> A)"
 
   116   unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..
 
   136   unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..
 
   120   unfolding permute_set_eq_image image_insert ..
 
   140   unfolding permute_set_eq_image image_insert ..
 
   121 
   141 
   122 lemma vimage_eqvt:
 
   142 lemma vimage_eqvt:
 
   123   shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
 
   143   shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
 
   124   unfolding vimage_def permute_fun_def [where f=f]
 
   144   unfolding vimage_def permute_fun_def [where f=f]
 
   125   unfolding Collect_eqvt mem_eqvt ..
 
   145   unfolding Collect_eqvt2 mem_eqvt ..
 
   126 
   146 
   127 lemma image_eqvt:
 
   147 lemma image_eqvt:
 
   128   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
 
   148   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
 
   129   unfolding permute_set_eq_image
 
   149   unfolding permute_set_eq_image
 
   130   unfolding permute_fun_def [where f=f]
 
   150   unfolding permute_fun_def [where f=f]
 
   137 
   157 
   138 lemma finite_eqvt:
 
   158 lemma finite_eqvt:
 
   139   shows "p \<bullet> finite A = finite (p \<bullet> A)"
 
   159   shows "p \<bullet> finite A = finite (p \<bullet> A)"
 
   140   unfolding finite_permute_iff permute_bool_def ..
 
   160   unfolding finite_permute_iff permute_bool_def ..
 
   141 
   161 
   142 lemma supp_eqvt: "p \<bullet> supp S = supp (p \<bullet> S)"
 
       
   143   unfolding supp_def
 
       
   144   by (simp only: Collect_eqvt Not_eqvt finite_eqvt eq_eqvt
 
       
   145       permute_eqvt [of p] swap_eqvt permute_minus_cancel)
 
       
   146 
       
   147 
   162 
   148 section {* List Operations *}
 
   163 section {* List Operations *}
 
   149 
   164 
   150 lemma append_eqvt:
 
   165 lemma append_eqvt:
 
   151   shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
 
   166   shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
 
   203   shows "a \<sharp> ()"
 
   218   shows "a \<sharp> ()"
 
   204   by (simp add: fresh_def supp_unit)
 
   219   by (simp add: fresh_def supp_unit)
 
   205 
   220 
   206 section {* Equivariance automation *}
 
   221 section {* Equivariance automation *}
 
   207 
   222 
   208 text {* 
       
   209   below is a construction site for a conversion that  
       
   210   pushes permutations into a term as far as possible 
       
   211 *}
 
       
   212 
       
   213 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
 
   223 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
 
   214 
   224 
   215 use "nominal_thmdecls.ML"
 
   225 use "nominal_thmdecls.ML"
 
   216 setup "NominalThmDecls.setup"
 
   226 setup "Nominal_ThmDecls.setup"
 
   217 
   227 
   218 lemmas [eqvt] = 
   228 lemmas [eqvt] = 
   219   (* connectives *)
 
   229   (* connectives *)
 
   220   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
   230   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
   221   True_eqvt False_eqvt
 
   231   True_eqvt False_eqvt ex_eqvt all_eqvt
 
   222   imp_eqvt [folded induct_implies_def]
 
   232   imp_eqvt [folded induct_implies_def]
 
       
   233 
       
   234   (* nominal *)
 
       
   235   permute_eqvt supp_eqvt fresh_eqvt
 
   223 
   236 
   224   (* datatypes *)
 
   237   (* datatypes *)
 
   225   permute_prod.simps
 
   238   permute_prod.simps
 
   226   fst_eqvt snd_eqvt
 
   239   fst_eqvt snd_eqvt
 
   227 
   240 
   228   (* sets *)
 
   241   (* sets *)
 
   229   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
 
   242   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
 
   230   Diff_eqvt Compl_eqvt insert_eqvt
 
   243   Diff_eqvt Compl_eqvt insert_eqvt
 
   231 
   244 
   232 (* A simple conversion pushing permutations into a term *)
 
   245 declare permute_pure [eqvt]
 
   233 
   246 
   234 ML {*
 
   247 thm eqvt
 
   235 fun OF1 thm1 thm2 = thm2 RS thm1
 
   248 
   236 
   249 text {* helper lemmas for the eqvt_tac *}
 
   237 fun get_eqvt_thms ctxt =
 
       
   238   map (OF1 @{thm eq_reflection}) (NominalThmDecls.get_eqvt_thms ctxt)  
       
   239 *}
 
       
   240 
       
   241 ML {* 
       
   242 fun eqvt_conv ctxt ctrm =
 
       
   243   case (term_of ctrm) of
 
       
   244     (Const (@{const_name "permute"}, _) $ _ $ t) =>
 
       
   245        (if is_Const (head_of t)
 
       
   246         then (More_Conv.rewrs_conv (get_eqvt_thms ctxt) 
       
   247               then_conv eqvt_conv ctxt) ctrm
 
       
   248         else Conv.comb_conv (eqvt_conv ctxt) ctrm)
 
       
   249      | _ $ _ => Conv.comb_conv (eqvt_conv ctxt) ctrm
 
       
   250      | Abs _ => Conv.abs_conv (fn (_, ctxt) => eqvt_conv ctxt) ctxt ctrm
 
       
   251      | _ => Conv.all_conv ctrm
 
       
   252 *}
 
       
   253 
       
   254 ML {*
 
       
   255 fun eqvt_tac ctxt = 
       
   256   CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)
 
       
   257 *}
 
       
   258 
       
   259 lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"
 
       
   260 apply(tactic {* eqvt_tac @{context} 1 *}) 
       
   261 oops
 
       
   262 
       
   263 text {*
 
       
   264   Another conversion for pushing permutations into a term.
 
       
   265   It is designed not to apply rules like @{term permute_pure} to
 
       
   266   applications or abstractions, only to constants or free
 
       
   267   variables. Thus permutations are not removed too early, and they
 
       
   268   have a chance to cancel with bound variables.
 
       
   269 *}
 
       
   270 
   250 
   271 definition
 
   251 definition
 
   272   "unpermute p = permute (- p)"
 
   252   "unpermute p = permute (- p)"
 
   273 
   253 
   274 lemma push_apply:
 
   254 lemma eqvt_apply:
 
   275   fixes f :: "'a::pt \<Rightarrow> 'b::pt" and x :: "'a::pt"
 
   255   fixes f :: "'a::pt \<Rightarrow> 'b::pt" 
       
   256   and x :: "'a::pt"
 
   276   shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
 
   257   shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
 
   277   unfolding permute_fun_def by simp
 
   258   unfolding permute_fun_def by simp
 
   278 
   259 
   279 lemma push_lambda:
 
   260 lemma eqvt_lambda:
 
   280   fixes f :: "'a::pt \<Rightarrow> 'b::pt"
 
   261   fixes f :: "'a::pt \<Rightarrow> 'b::pt"
 
   281   shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
 
   262   shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
 
   282   unfolding permute_fun_def unpermute_def by simp
 
   263   unfolding permute_fun_def unpermute_def by simp
 
   283 
   264 
   284 lemma push_bound:
 
   265 lemma eqvt_bound:
 
   285   shows "p \<bullet> unpermute p x \<equiv> x"
 
   266   shows "p \<bullet> unpermute p x \<equiv> x"
 
   286   unfolding unpermute_def by simp
 
   267   unfolding unpermute_def by simp
 
   287 
   268 
   288 ML {*
 
   269 use "nominal_permeq.ML"
 
   289 structure PushData = Named_Thms
 
   270 
   290 (
 
   271 
   291   val name = "push"
 
   272 lemma "p \<bullet> (A \<longrightarrow> B = C)"
 
   292   val description = "push permutations"
 
   273 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) 
   293 )
 
   274 oops
 
   294 
   275 
   295 local
 
   276 lemma "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
 
   296 
   277 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
 
   297 fun push_apply_conv ctxt ct =
 
   278 oops
 
   298   case (term_of ct) of
 
   279 
   299     (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
 
   280 lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
 
   300       let
 
   281 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
 
   301         val (perm, t) = Thm.dest_comb ct
 
   282 oops
 
   302         val (_, p) = Thm.dest_comb perm
 
   283 
   303         val (f, x) = Thm.dest_comb t
 
   284 lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
 
   304         val a = ctyp_of_term x;
 
   285 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
 
   305         val b = ctyp_of_term t;
 
   286 oops
 
   306         val ty_insts = map SOME [b, a]
 
   287 
   307         val term_insts = map SOME [p, f, x]
 
   288 lemma "p \<bullet> (\<lambda>q. q \<bullet> (r \<bullet> x)) = foo"
 
   308       in
 
   289 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
 
   309         Drule.instantiate' ty_insts term_insts @{thm push_apply}
 
   290 oops
 
   310       end
 
   291 
   311   | _ => Conv.no_conv ct
 
   292 lemma "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
 
   312 
   293 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
 
   313 fun push_lambda_conv ctxt ct =
 
   294 oops
 
   314   case (term_of ct) of
 
   295 
   315     (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
 
       
   316       Conv.rewr_conv @{thm push_lambda} ct
 
       
   317   | _ => Conv.no_conv ct
 
       
   318 
       
   319 in
 
       
   320 
       
   321 fun push_conv ctxt ct =
 
       
   322   Conv.first_conv
 
       
   323     [ Conv.rewr_conv @{thm push_bound},
 
       
   324       push_apply_conv ctxt
 
       
   325         then_conv Conv.comb_conv (push_conv ctxt),
 
       
   326       push_lambda_conv ctxt
 
       
   327         then_conv Conv.abs_conv (fn (v, ctxt) => push_conv ctxt) ctxt,
 
       
   328       More_Conv.rewrs_conv (PushData.get ctxt),
 
       
   329       Conv.all_conv
 
       
   330     ] ct
 
       
   331 
       
   332 fun push_tac ctxt = 
       
   333   CONVERSION (More_Conv.bottom_conv (fn ctxt => push_conv ctxt) ctxt)
 
       
   334 
   296 
   335 end
 
   297 end
 
   336 *}
 
       
   337 
       
   338 setup PushData.setup
 
       
   339 
       
   340 declare permute_pure [THEN eq_reflection, push]
 
       
   341 
       
   342 lemma push_eq [THEN eq_reflection, push]:
 
       
   343   "p \<bullet> (op =) = (op =)"
 
       
   344   by (simp add: expand_fun_eq permute_fun_def eq_eqvt)
 
       
   345 
       
   346 lemma push_All [THEN eq_reflection, push]:
 
       
   347   "p \<bullet> All = All"
 
       
   348   by (simp add: expand_fun_eq permute_fun_def all_eqvt)
 
       
   349 
       
   350 lemma push_Ex [THEN eq_reflection, push]:
 
       
   351   "p \<bullet> Ex = Ex"
 
       
   352   by (simp add: expand_fun_eq permute_fun_def ex_eqvt)
 
       
   353 
       
   354 lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"
 
       
   355 apply (tactic {* push_tac @{context} 1 *}) 
       
   356 oops
 
       
   357 
       
   358 lemma "p \<bullet> (\<lambda>x. A \<longrightarrow> B x = (C::bool)) = foo"
 
       
   359 apply (tactic {* push_tac @{context} 1 *})
 
       
   360 oops
 
       
   361 
       
   362 lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
 
       
   363 apply (tactic {* push_tac @{context} 1 *})
 
       
   364 oops
 
       
   365 
       
   366 lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
 
       
   367 apply (tactic {* push_tac @{context} 1 *})
 
       
   368 oops
 
       
   369 
       
   370 end
nominal2