--- a/Nominal/Ex/ExCoreHaskell.thy	Tue May 04 13:52:40 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Tue May 04 14:13:18 2010 +0200
@@ -1,23 +1,15 @@
 theory ExCoreHaskell
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* core haskell *)
 
-ML {* val _ = recursive := false *}
-(* this should not be an equivariance rule *)
-(* for the moment, we force it to be       *)
-setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
-thm eqvts
-(*declare permute_pure[eqvt]*)
-
 atom_decl var
 atom_decl cvar
 atom_decl tvar
 
 (* there are types, coercion types and regular types list-data-structure *)
 
-ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype tkind =
   KStar
 | KFun "tkind" "tkind"
@@ -28,7 +20,7 @@
 | TC "string"
 | TApp "ty" "ty"
 | TFun "string" "ty_lst"
-| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
+| TAll tv::"tvar" "tkind" T::"ty"  bind_set tv in T
 | TEq "ckind" "ty"
 and ty_lst =
   TsNil
@@ -38,7 +30,7 @@
 | CConst "string"
 | CApp "co" "co"
 | CFun "string" "co_lst"
-| CAll cv::"cvar" "ckind" C::"co"  bind cv in C
+| CAll cv::"cvar" "ckind" C::"co"  bind_set cv in C
 | CEq "ckind" "co"
 | CRefl "ty"
 | CSym "co"
@@ -56,13 +48,13 @@
 and trm =
   Var "var"
 | K "string"
-| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
-| LAMC cv::"cvar" "ckind" t::"trm" bind cv in t
+| LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t
+| LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t
 | AppT "trm" "ty"
 | AppC "trm" "co"
-| Lam v::"var" "ty" t::"trm"       bind v in t
+| Lam v::"var" "ty" t::"trm"       bind_set v in t
 | App "trm" "trm"
-| Let x::"var" "ty" "trm" t::"trm" bind x in t
+| Let x::"var" "ty" "trm" t::"trm" bind_set x in t
 | Case "trm" "assoc_lst"
 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 and assoc_lst =
@@ -93,86 +85,6 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
-(*
-function
-rfv_tkind_raw and rfv_ckind_raw and rfv_ty_raw and rfv_ty_lst_raw and rfv_co_raw and rfv_co_lst_raw and rfv_trm_raw and rfv_assoc_lst_raw and rfv_bv_raw and rfv_bv_vs_raw and rfv_bv_tvs_raw and rfv_bv_cvs_raw and rfv_pat_raw and rfv_vars_raw and rfv_tvars_raw and rfv_cvars_raw
-where
-  "rfv_tkind_raw KStar_raw = {}"
-| "rfv_tkind_raw (KFun_raw tkind_raw1 tkind_raw2) = rfv_tkind_raw tkind_raw1 \<union> rfv_tkind_raw tkind_raw2"
-| "rfv_ckind_raw (CKEq_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2"
-| "rfv_ty_raw (TVar_raw tvar) = {atom tvar}"
-| "rfv_ty_raw (TC_raw list) = {}"
-| "rfv_ty_raw (TApp_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2"
-| "rfv_ty_raw (TFun_raw list ty_lst_raw) = rfv_ty_lst_raw ty_lst_raw"
-| "rfv_ty_raw (TAll_raw tvar tkind_raw ty_raw) =
- rfv_tkind_raw tkind_raw \<union> (rfv_ty_raw ty_raw - {atom tvar})"
-| "rfv_ty_raw (TEq_raw ckind_raw ty_raw) = rfv_ckind_raw ckind_raw \<union> rfv_ty_raw ty_raw"
-| "rfv_ty_lst_raw TsNil_raw = {}"
-| "rfv_ty_lst_raw (TsCons_raw ty_raw ty_lst_raw) = rfv_ty_raw ty_raw \<union> rfv_ty_lst_raw ty_lst_raw"
-| "rfv_co_raw (CVar_raw cvar) = {atom cvar}"
-| "rfv_co_raw (CConst_raw list) = {}"
-| "rfv_co_raw (CApp_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"
-| "rfv_co_raw (CFun_raw list co_lst_raw) = rfv_co_lst_raw co_lst_raw"
-| "rfv_co_raw (CAll_raw cvar ckind_raw co_raw) =
- rfv_ckind_raw ckind_raw \<union> (rfv_co_raw co_raw - {atom cvar})"
-| "rfv_co_raw (CEq_raw ckind_raw co_raw) = rfv_ckind_raw ckind_raw \<union> rfv_co_raw co_raw"
-| "rfv_co_raw (CRefl_raw ty_raw) = rfv_ty_raw ty_raw"
-| "rfv_co_raw (CSym_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CCir_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"
-| "rfv_co_raw (CAt_raw co_raw ty_raw) = rfv_co_raw co_raw \<union> rfv_ty_raw ty_raw"
-| "rfv_co_raw (CLeft_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CRight_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CSim_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"
-| "rfv_co_raw (CRightc_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CLeftc_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CCoe_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"
-| "rfv_co_lst_raw CsNil_raw = {}"
-| "rfv_co_lst_raw (CsCons_raw co_raw co_lst_raw) = rfv_co_raw co_raw \<union> rfv_co_lst_raw co_lst_raw"
-| "rfv_trm_raw (Var_raw var) = {atom var}"
-| "rfv_trm_raw (K_raw list) = {}"
-| "rfv_trm_raw (LAMT_raw tvar tkind_raw trm_raw) =
- rfv_tkind_raw tkind_raw \<union> (rfv_trm_raw trm_raw - {atom tvar})"
-| "rfv_trm_raw (LAMC_raw cvar ckind_raw trm_raw) =
- rfv_ckind_raw ckind_raw \<union> (rfv_trm_raw trm_raw - {atom cvar})"
-| "rfv_trm_raw (AppT_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw"
-| "rfv_trm_raw (AppC_raw trm_raw co_raw) = rfv_trm_raw trm_raw \<union> rfv_co_raw co_raw"
-| "rfv_trm_raw (Lam_raw var ty_raw trm_raw) = rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw - {atom var})"
-| "rfv_trm_raw (App_raw trm_raw1 trm_raw2) = rfv_trm_raw trm_raw1 \<union> rfv_trm_raw trm_raw2"
-| "rfv_trm_raw (Let_raw var ty_raw trm_raw1 trm_raw2) =
- rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw1 \<union> (rfv_trm_raw trm_raw2 - {atom var}))"
-| "rfv_trm_raw (Case_raw trm_raw assoc_lst_raw) = rfv_trm_raw trm_raw \<union> rfv_assoc_lst_raw assoc_lst_raw"
-| "rfv_trm_raw (Cast_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw"
-| "rfv_assoc_lst_raw ANil_raw = {}"
-| "rfv_assoc_lst_raw (ACons_raw pat_raw trm_raw assoc_lst_raw) =
- rfv_bv_raw pat_raw \<union> (rfv_trm_raw trm_raw - set (bv_raw pat_raw) \<union> rfv_assoc_lst_raw assoc_lst_raw)"
-| "rfv_bv_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) =
- rfv_bv_tvs_raw tvars_raw \<union> (rfv_bv_cvs_raw cvars_raw \<union> rfv_bv_vs_raw vars_raw)"
-| "rfv_bv_vs_raw VsNil_raw = {}"
-| "rfv_bv_vs_raw (VsCons_raw var ty_raw vars_raw) = rfv_ty_raw ty_raw \<union> rfv_bv_vs_raw vars_raw"
-| "rfv_bv_tvs_raw TvsNil_raw = {}"
-| "rfv_bv_tvs_raw (TvsCons_raw tvar tkind_raw tvars_raw) =
- rfv_tkind_raw tkind_raw \<union> rfv_bv_tvs_raw tvars_raw"
-| "rfv_bv_cvs_raw CvsNil_raw = {}"
-| "rfv_bv_cvs_raw (CvsCons_raw cvar ckind_raw cvars_raw) =
- rfv_ckind_raw ckind_raw \<union> rfv_bv_cvs_raw cvars_raw"
-| "rfv_pat_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) =
- rfv_tvars_raw tvars_raw \<union> (rfv_cvars_raw cvars_raw \<union> rfv_vars_raw vars_raw)"
-| "rfv_vars_raw VsNil_raw = {}"
-| "rfv_vars_raw (VsCons_raw var ty_raw vars_raw) =
- {atom var} \<union> (rfv_ty_raw ty_raw \<union> rfv_vars_raw vars_raw)"
-| "rfv_tvars_raw TvsNil_raw = {}"
-| "rfv_tvars_raw (TvsCons_raw tvar tkind_raw tvars_raw) =
- {atom tvar} \<union> (rfv_tkind_raw tkind_raw \<union> rfv_tvars_raw tvars_raw)"
-| "rfv_cvars_raw CvsNil_raw = {}"
-| "rfv_cvars_raw (CvsCons_raw cvar ckind_raw cvars_raw) =
- {atom cvar} \<union> (rfv_ckind_raw ckind_raw \<union> rfv_cvars_raw cvars_raw)"
-apply pat_completeness
-apply auto
-done
-termination
-by lexicographic_order
-*)
-
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
@@ -213,9 +125,7 @@
  "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"
  "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"
  apply (erule_tac [!] alpha_inducts)
- apply simp_all
- apply (rule_tac [!] alpha_intros)
- apply simp_all
+ apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)
  done
 
 lemma [quot_respect]:
@@ -252,27 +162,23 @@
   "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"
   "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"
   apply(induct b rule: inducts(12))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   apply(induct c rule: inducts(11))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   apply(induct d rule: inducts(10))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   done
 
 lemma perm_bv2:
   "p \<bullet> bv l = bv (permute_bv p l)"
   apply(induct l rule: inducts(9))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv)
   apply(simp add: perm_bv1[symmetric])
   apply(simp add: eqvts)
   done
 
 lemma alpha_perm_bn1:
- " alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
+ "alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
  "alpha_bv_cvs cvars (permute_bv_cvs q cvars)"
  "alpha_bv_vs vars (permute_bv_vs q vars)"
   apply(induct tvars rule: inducts(11))
@@ -292,13 +198,13 @@
 lemma ACons_subst:
   "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
   apply (simp only: eq_iff)
+  apply (simp add: alpha_perm_bn)
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
   apply (simp add: perm_bv2[symmetric])
   apply (simp add: eqvts[symmetric])
   apply (simp add: supp_abs)
   apply (simp add: fv_supp)
-  apply (simp add: alpha_perm_bn)
   apply (rule supp_perm_eq[symmetric])
   apply (subst supp_finite_atom_set)
   apply (rule finite_Diff)
@@ -311,34 +217,27 @@
   "permute_bv_tvs 0 c = c"
   "permute_bv_vs 0 d = d"
   apply(induct b rule: inducts(12))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   apply(induct c rule: inducts(11))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   apply(induct d rule: inducts(10))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   done
 
 lemma permute_bv_zero2:
   "permute_bv 0 a = a"
   apply(induct a rule: inducts(9))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts permute_bv_zero1)
   done
 
 lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"
-apply (induct x rule: inducts(11))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: eq_iff fresh_star_union)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
+  apply (induct x rule: inducts(11))
+  apply (simp_all add: eq_iff fresh_star_union)
+  done
 
 lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"
 apply (induct x rule: inducts(12))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (rule TrueI)+
 apply (simp_all add: eq_iff fresh_star_union)
 apply (subst supp_perm_eq)
 apply (simp_all add: fv_supp)
@@ -346,70 +245,65 @@
 
 lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"
 apply (induct x rule: inducts(10))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: eq_iff fresh_star_union)
+apply (rule TrueI)+
+apply (simp_all add: fresh_star_union eq_iff)
 apply (subst supp_perm_eq)
 apply (simp_all add: fv_supp)
 done
 
 lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
 apply (induct x rule: inducts(9))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (rule TrueI)+
 apply (simp_all add: eq_iff fresh_star_union)
 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
-apply (simp add: eqvts)
+apply (subst supp_perm_eq)
+apply (simp_all add: fv_supp)
 done
 
 lemma fin1: "finite (fv_bv_tvs x)"
 apply (induct x rule: inducts(11))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma fin2: "finite (fv_bv_cvs x)"
 apply (induct x rule: inducts(12))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma fin3: "finite (fv_bv_vs x)"
 apply (induct x rule: inducts(10))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma fin_fv_bv: "finite (fv_bv x)"
 apply (induct x rule: inducts(9))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (rule TrueI)+
+defer
+apply (rule TrueI)+
 apply (simp add: fin1 fin2 fin3)
+apply (rule finite_supp)
 done
 
 lemma finb1: "finite (set (bv_tvs x))"
 apply (induct x rule: inducts(11))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma finb2: "finite (set (bv_cvs x))"
 apply (induct x rule: inducts(12))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma finb3: "finite (set (bv_vs x))"
 apply (induct x rule: inducts(10))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma fin_bv: "finite (set (bv x))"
 apply (induct x rule: inducts(9))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp add: finb1 finb2 finb3)
+apply (simp_all add: finb1 finb2 finb3)
 done
 
-thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct
-
 lemma strong_induction_principle:
   assumes a01: "\<And>b. P1 b KStar"
   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
@@ -494,7 +388,7 @@
     apply (simp only: perm)
     apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
                and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
@@ -534,7 +428,7 @@
     apply (simp only: perm)
     apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"
                and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
@@ -575,7 +469,7 @@
     apply (simp only: perm)
     apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
                and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
@@ -615,7 +509,7 @@
     apply (simp only: perm)
     apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"
                and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
@@ -656,7 +550,7 @@
     apply (simp only: perm)
     apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
                and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
@@ -697,7 +591,7 @@
     apply (simp only: perm)
     apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
                and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
@@ -760,6 +654,12 @@
 
 section {* test about equivariance for alpha *}
 
+(* this should not be an equivariance rule *)
+(* for the moment, we force it to be       *)
+
+(*declare permute_pure[eqvt]*)
+(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
+
 thm eqvts
 thm eqvts_raw
 
@@ -769,7 +669,7 @@
 equivariance alpha_tkind_raw
 
 thm eqvts
-thm eqvts_raw
+thm eqvts_raw*)
 
 end