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.
Nominal/Test.thy
changeset 1398 1f3c01345c9e
parent 1396 08294f4d6c08
child 1416 947e5f772a9c
equal deleted inserted replaced
1397:6e2dfe52b271 1398:1f3c01345c9e 
     1 theory Test
 
     1 theory Test
 
     2 imports "Parser" "../Attic/Prove"
 
     2 imports "Parser" "../Attic/Prove"
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 text {* weirdo example from Peter Sewell's bestiary *}
 
     5 text {* example 1, equivalent to example 2 from Terms *}
 
     6 
       
     7 nominal_datatype weird =
 
       
     8   WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
 
       
     9     bind x in p1, bind x in p2, bind y in p2, bind y in p3
 
       
    10 | WV "name"
 
       
    11 | WP "weird" "weird"
 
       
    12 
       
    13 thm permute_weird_raw.simps[no_vars]
 
       
    14 thm alpha_weird_raw.intros[no_vars]
 
       
    15 thm fv_weird_raw.simps[no_vars]
 
       
    16 
       
    17 
       
    18 text {* example 1 *}
 
       
    19 
       
    20 (* ML {* set show_hyps *} *)
 
       
    21 
     6 
    22 nominal_datatype lam =
 
     7 nominal_datatype lam =
 
    23   VAR "name"
 
     8   VAR "name"
 
    24 | APP "lam" "lam"
 
     9 | APP "lam" "lam"
 
    25 | LET bp::"bp" t::"lam"   bind "bi bp" in t
 
    10 | LET bp::"bp" t::"lam"   bind "bi bp" in t
 
    26 and bp = 
    11 and bp =
 
    27   BP "name" "lam" 
    12   BP "name" "lam"
 
    28 binder
 
    13 binder
 
    29   bi::"bp \<Rightarrow> atom set"
 
    14   bi::"bp \<Rightarrow> atom set"
 
    30 where
 
    15 where
 
    31   "bi (BP x t) = {atom x}"
 
    16   "bi (BP x t) = {atom x}"
 
    32 
    17 
    42 term Test.BP_raw
 
    27 term Test.BP_raw
 
    43 thm bi_raw.simps
 
    28 thm bi_raw.simps
 
    44 thm permute_lam_raw_permute_bp_raw.simps
 
    29 thm permute_lam_raw_permute_bp_raw.simps
 
    45 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars]
 
    30 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars]
 
    46 thm fv_lam_raw_fv_bp_raw.simps[no_vars]
 
    31 thm fv_lam_raw_fv_bp_raw.simps[no_vars]
 
    47 (*thm lam_bp_induct
 
       
    48 thm lam_bp_perm
 
       
    49 thm lam_bp_fv
 
       
    50 thm lam_bp_bn
 
       
    51 thm lam_bp_inject
 
       
    52 thm lam_bp_distinct*)
 
       
    53 
    32 
    54 text {* example 2 *}
 
    33 text {* example 2 *}
 
    55 
    34 
    56 nominal_datatype trm' =
 
    35 nominal_datatype trm' =
 
    57   Var "name"
 
    36   Var "name"
 
    58 | App "trm'" "trm'"
 
    37 | App "trm'" "trm'"
 
    59 | Lam x::"name" t::"trm'"          bind x in t 
    38 | Lam x::"name" t::"trm'"          bind x in t
 
    60 | Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
 
    39 | Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
 
    61 and pat' =
 
    40 and pat' =
 
    62   PN
 
    41   PN
 
    63 | PS "name"
 
    42 | PS "name"
 
    64 | PD "name" "name"
 
    43 | PD "name" "name"
 
    65 binder
 
    44 binder
 
    66   f::"pat' \<Rightarrow> atom set"
 
    45   f::"pat' \<Rightarrow> atom set"
 
    67 where 
    46 where
 
    68   "f PN = {}"
 
    47   "f PN = {}"
 
    69 | "f (PD x y) = {atom x, atom y}"
 
    48 | "f (PD x y) = {atom x, atom y}"
 
    70 | "f (PS x) = {atom x}"
 
    49 | "f (PS x) = {atom x}"
 
    71 
    50 
    72 
    51 
    87 thm trm'_pat'_inject*)
 
    66 thm trm'_pat'_inject*)
 
    88 
    67 
    89 nominal_datatype trm0 =
 
    68 nominal_datatype trm0 =
 
    90   Var0 "name"
 
    69   Var0 "name"
 
    91 | App0 "trm0" "trm0"
 
    70 | App0 "trm0" "trm0"
 
    92 | Lam0 x::"name" t::"trm0"          bind x in t 
    71 | Lam0 x::"name" t::"trm0"          bind x in t
 
    93 | Let0 p::"pat0" "trm0" t::"trm0"   bind "f0 p" in t
 
    72 | Let0 p::"pat0" "trm0" t::"trm0"   bind "f0 p" in t
 
    94 and pat0 =
 
    73 and pat0 =
 
    95   PN0
 
    74   PN0
 
    96 | PS0 "name"
 
    75 | PS0 "name"
 
    97 | PD0 "pat0" "pat0"
 
    76 | PD0 "pat0" "pat0"
 
    98 binder
 
    77 binder
 
    99   f0::"pat0 \<Rightarrow> atom set"
 
    78   f0::"pat0 \<Rightarrow> atom set"
 
   100 where 
    79 where
 
   101   "f0 PN0 = {}"
 
    80   "f0 PN0 = {}"
 
   102 | "f0 (PS0 x) = {atom x}"
 
    81 | "f0 (PS0 x) = {atom x}"
 
   103 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 
    82 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 
   104 
    83 
   105 thm f0_raw.simps
 
    84 thm f0_raw.simps
 
   108 thm trm0_pat0_fv
 
    87 thm trm0_pat0_fv
 
   109 thm trm0_pat0_bn*)
 
    88 thm trm0_pat0_bn*)
 
   110 
    89 
   111 text {* example type schemes *}
 
    90 text {* example type schemes *}
 
   112 
    91 
   113 (* does not work yet
 
       
   114 nominal_datatype t =
 
    92 nominal_datatype t =
 
   115   Var "name"
 
    93   Var "name"
 
   116 | Fun "t" "t"
 
    94 | Fun "t" "t"
 
   117 
    95 and  tyS =
 
   118 nominal_datatype tyS =
 
       
   119   All xs::"name list" ty::"t_raw" bind xs in ty
 
       
   120 *)
 
       
   121 
       
   122 
       
   123 nominal_datatype t = 
       
   124   Var "name" 
       
   125 | Fun "t" "t"
 
       
   126 and  tyS = 
       
   127   All xs::"name set" ty::"t" bind xs in ty
 
    96   All xs::"name set" ty::"t" bind xs in ty
 
   128 
    97 
   129 (* example 1 from Terms.thy *)
 
    98 (* example 1 from Terms.thy *)
 
   130 
    99 
   131 nominal_datatype trm1 =
 
   100 nominal_datatype trm1 =
 
   132   Vr1 "name"
 
   101   Vr1 "name"
 
   133 | Ap1 "trm1" "trm1"
 
   102 | Ap1 "trm1" "trm1"
 
   134 | Lm1 x::"name" t::"trm1"       bind x in t 
   103 | Lm1 x::"name" t::"trm1"       bind x in t
 
   135 | Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t 
   104 | Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t
 
   136 and bp1 =
 
   105 and bp1 =
 
   137   BUnit1
 
   106   BUnit1
 
   138 | BV1 "name"
 
   107 | BV1 "name"
 
   139 | BP1 "bp1" "bp1"
 
   108 | BP1 "bp1" "bp1"
 
   140 binder
 
   109 binder
 
   144 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 
   113 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 
   145 | "bv1 (BV1 x) = {atom x}"
 
   114 | "bv1 (BV1 x) = {atom x}"
 
   146 
   115 
   147 
   116 
   148 thm bv1_raw.simps
 
   117 thm bv1_raw.simps
 
   149 
       
   150 (* example 2 from Terms.thy *)
 
       
   151 
       
   152 nominal_datatype trm2 =
 
       
   153   Vr2 "name"
 
       
   154 | Ap2 "trm2" "trm2"
 
       
   155 | Lm2 x::"name" t::"trm2"       bind x in t
 
       
   156 | Lt2 r::"assign" t::"trm2"    bind "bv2 r" in t
 
       
   157 and assign = 
       
   158   As "name" "trm2"
 
       
   159 binder
 
       
   160   bv2
 
       
   161 where
 
       
   162   "bv2 (As x t) = {atom x}"
 
       
   163 
       
   164 (* compat should be
 
       
   165 compat (As x t) pi (As x' t') == pi o x = x' & alpha t t'
 
       
   166 *)
 
       
   167 
       
   168 
       
   169 thm fv_trm2_raw_fv_assign_raw.simps[no_vars]
 
       
   170 thm alpha_trm2_raw_alpha_assign_raw_alpha_bv2_raw.intros[no_vars]
 
       
   171 
       
   172 
       
   173 
   118 
   174 text {* example 3 from Terms.thy *}
 
   119 text {* example 3 from Terms.thy *}
 
   175 
   120 
   176 nominal_datatype trm3 =
 
   121 nominal_datatype trm3 =
 
   177   Vr3 "name"
 
   122   Vr3 "name"
 
   191 (* compat should be
 
   136 (* compat should be
 
   192 compat (ANil) pi (PNil) \<equiv> TRue
 
   137 compat (ANil) pi (PNil) \<equiv> TRue
 
   193 compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts'
 
   138 compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts'
 
   194 *)
 
   139 *)
 
   195 
   140 
   196 (* example 4 from Terms.thy *)
 
       
   197 
       
   198 (* fv_eqvt does not work, we need to repaire defined permute functions
 
       
   199    defined fv and defined alpha... *)
 
       
   200 nominal_datatype trm4 =
 
       
   201   Vr4 "name"
 
       
   202 | Ap4 "trm4" "trm4 list"
 
       
   203 | Lm4 x::"name" t::"trm4"  bind x in t
 
       
   204 
       
   205 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
 
       
   206 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 
       
   207 
       
   208 (* example 5 from Terms.thy *)
 
   141 (* example 5 from Terms.thy *)
 
   209 
   142 
   210 nominal_datatype trm5 =
 
   143 nominal_datatype trm5 =
 
   211   Vr5 "name"
 
   144   Vr5 "name"
 
   212 | Ap5 "trm5" "trm5"
 
   145 | Ap5 "trm5" "trm5"
 
   217 binder
 
   150 binder
 
   218   bv5
 
   151   bv5
 
   219 where
 
   152 where
 
   220   "bv5 Lnil = {}"
 
   153   "bv5 Lnil = {}"
 
   221 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
 
   154 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
 
   222 
       
   223 (* example 6 from Terms.thy *)
 
       
   224 
       
   225 (* BV is not respectful, needs to fail*)
 
       
   226 nominal_datatype trm6 =
 
       
   227   Vr6 "name"
 
       
   228 | Lm6 x::"name" t::"trm6"         bind x in t
 
       
   229 | Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
 
       
   230 binder
 
       
   231   bv6
 
       
   232 where
 
       
   233   "bv6 (Vr6 n) = {}"
 
       
   234 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
 
       
   235 | "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
 
       
   236 (* example 7 from Terms.thy *)
 
       
   237 
       
   238 (* BV is not respectful, needs to fail*)
 
       
   239 nominal_datatype trm7 =
 
       
   240   Vr7 "name"
 
       
   241 | Lm7 l::"name" r::"trm7"   bind l in r
 
       
   242 | Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
 
       
   243 binder 
       
   244   bv7 
       
   245 where
 
       
   246   "bv7 (Vr7 n) = {atom n}"
 
       
   247 | "bv7 (Lm7 n t) = bv7 t - {atom n}"
 
       
   248 | "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
 
       
   249 
       
   250 (* example 8 from Terms.thy *)
 
       
   251 
       
   252 nominal_datatype foo8 =
 
       
   253   Foo0 "name"
 
       
   254 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
 
       
   255 and bar8 =
 
       
   256   Bar0 "name"
 
       
   257 | Bar1 "name" s::"name" b::"bar8" bind s in b
 
       
   258 binder 
       
   259   bv8
 
       
   260 where
 
       
   261   "bv8 (Bar0 x) = {}"
 
       
   262 | "bv8 (Bar1 v x b) = {atom v}"
 
       
   263 
       
   264 (* example 9 from Terms.thy *)
 
       
   265 
       
   266 (* BV is not respectful, needs to fail*)
 
       
   267 nominal_datatype lam9 =
 
       
   268   Var9 "name"
 
       
   269 | Lam9 n::"name" l::"lam9" bind n in l
 
       
   270 and bla9 =
 
       
   271   Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
 
       
   272 binder
 
       
   273   bv9
 
       
   274 where
 
       
   275   "bv9 (Var9 x) = {}"
 
       
   276 | "bv9 (Lam9 x b) = {atom x}"
 
       
   277 
   155 
   278 (* example from my PHD *)
 
   156 (* example from my PHD *)
 
   279 
   157 
   280 atom_decl coname
 
   158 atom_decl coname
 
   281 
   159 
   301 | FApp "mexp" "path"
 
   179 | FApp "mexp" "path"
 
   302 | Ascr "mexp" "sexp"
 
   180 | Ascr "mexp" "sexp"
 
   303 and body =
 
   181 and body =
 
   304   Empty
 
   182   Empty
 
   305 | Seq c::defn d::"body"     bind "cbinders c" in d
 
   183 | Seq c::defn d::"body"     bind "cbinders c" in d
 
   306 and defn =  
   184 and defn =
 
   307   Type "name" "tyty"
 
   185   Type "name" "tyty"
 
   308 | Dty "name"
 
   186 | Dty "name"
 
   309 | DStru "name" "mexp"
 
   187 | DStru "name" "mexp"
 
   310 | Val "name" "trmtrm"
 
   188 | Val "name" "trmtrm"
 
   311 and sexp =
 
   189 and sexp =
 
   312   Sig sbody
 
   190   Sig sbody
 
   313 | SFunc "name" "sexp" "sexp"
 
   191 | SFunc "name" "sexp" "sexp"
 
   314 and sbody = 
   192 and sbody =
 
   315   SEmpty
 
   193   SEmpty
 
   316 | SSeq C::spec D::sbody    bind "Cbinders C" in D
 
   194 | SSeq C::spec D::sbody    bind "Cbinders C" in D
 
   317 and spec =
 
   195 and spec =
 
   318   Type1 "name" 
   196   Type1 "name"
 
   319 | Type2 "name" "tyty"
 
   197 | Type2 "name" "tyty"
 
   320 | SStru "name" "sexp"
 
   198 | SStru "name" "sexp"
 
   321 | SVal "name" "tyty"
 
   199 | SVal "name" "tyty"
 
   322 and tyty =
 
   200 and tyty =
 
   323   Tyref1 "name"
 
   201   Tyref1 "name"
 
   344 | "Cbinders (Type2 t T) = {atom t}"
 
   222 | "Cbinders (Type2 t T) = {atom t}"
 
   345 | "Cbinders (SStru x S) = {atom x}"
 
   223 | "Cbinders (SStru x S) = {atom x}"
 
   346 | "Cbinders (SVal v T) = {atom v}"
 
   224 | "Cbinders (SVal v T) = {atom v}"
 
   347 
   225 
   348 
   226 
       
   227 (* example 3 from Peter Sewell's bestiary *)
 
       
   228 nominal_datatype exp =
 
       
   229   VarP "name"
 
       
   230 | AppP "exp" "exp"
 
       
   231 | LamP x::"name" e::"exp" bind x in e
 
       
   232 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp' p" in e1
 
       
   233 and pat3 =
 
       
   234   PVar "name"
 
       
   235 | PUnit
 
       
   236 | PPair "pat3" "pat3"
 
       
   237 binder
 
       
   238   bp' :: "pat3 \<Rightarrow> atom set"
 
       
   239 where
 
       
   240   "bp' (PVar x) = {atom x}"
 
       
   241 | "bp' (PUnit) = {}"
 
       
   242 | "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
 
       
   243 thm alpha_exp_raw_alpha_pat3_raw_alpha_bp'_raw.intros
 
       
   244 
       
   245 (* example 6 from Peter Sewell's bestiary *)
 
       
   246 nominal_datatype exp6 =
 
       
   247   EVar name
 
       
   248 | EPair exp6 exp6
 
       
   249 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
 
       
   250 and pat6 =
 
       
   251   PVar' name
 
       
   252 | PUnit'
 
       
   253 | PPair' pat6 pat6
 
       
   254 binder
 
       
   255   bp6 :: "pat6 \<Rightarrow> atom set"
 
       
   256 where
 
       
   257   "bp6 (PVar' x) = {atom x}"
 
       
   258 | "bp6 (PUnit') = {}"
 
       
   259 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
 
       
   260 thm alpha_exp6_raw_alpha_pat6_raw_alpha_bp6_raw.intros
 
       
   261 
       
   262 (* THE REST ARE NOT SUPPOSED TO WORK YET *)
 
       
   263 
       
   264 (* example 7 from Peter Sewell's bestiary *)
 
       
   265 nominal_datatype exp7 =
 
       
   266   EVar name
 
       
   267 | EUnit
 
       
   268 | EPair exp7 exp7
 
       
   269 | ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
 
       
   270 and lrb =
 
       
   271   Assign name exp7
 
       
   272 and lrbs =
 
       
   273   Single lrb
 
       
   274 | More lrb lrbs
 
       
   275 binder
 
       
   276   b7 :: "lrb \<Rightarrow> atom set" and
 
       
   277   b7s :: "lrbs \<Rightarrow> atom set"
 
       
   278 where
 
       
   279   "b7 (Assign x e) = {atom x}"
 
       
   280 | "b7s (Single a) = b7 a"
 
       
   281 | "b7s (More a as) = (b7 a) \<union> (b7s as)"
 
       
   282 thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
 
       
   283 
       
   284 (* example 8 from Peter Sewell's bestiary *)
 
       
   285 nominal_datatype exp8 =
 
       
   286   EVar name
 
       
   287 | EUnit
 
       
   288 | EPair exp8 exp8
 
       
   289 | ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
 
       
   290 and fnclause =
 
       
   291   K x::name p::pat8 e::exp8 bind "b_pat p" in e
 
       
   292 and fnclauses =
 
       
   293   S fnclause
 
       
   294 | ORs fnclause fnclauses
 
       
   295 and lrb8 =
 
       
   296   Clause fnclauses
 
       
   297 and lrbs8 =
 
       
   298   Single lrb8
 
       
   299 | More lrb8 lrbs8
 
       
   300 and pat8 =
 
       
   301   PVar name
 
       
   302 | PUnit
 
       
   303 | PPair pat8 pat8
 
       
   304 binder
 
       
   305   b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
 
       
   306   b_pat :: "pat8 \<Rightarrow> atom set" and
 
       
   307   b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
 
       
   308   b_fnclause :: "fnclause \<Rightarrow> atom set" and
 
       
   309   b_lrb8 :: "lrb8 \<Rightarrow> atom set"
 
       
   310 where
 
       
   311   "b_lrbs8 (Single l) = b_lrb8 l"
 
       
   312 | "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
 
       
   313 | "b_pat (PVar x) = {atom x}"
 
       
   314 | "b_pat (PUnit) = {}"
 
       
   315 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
 
       
   316 | "b_fnclauses (S fc) = (b_fnclause fc)"
 
       
   317 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
 
       
   318 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
 
       
   319 | "b_fnclause (K x pat exp8) = {atom x}"
 
       
   320 thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros
 
       
   321 
       
   322 (* example 4 from Terms.thy *)
 
       
   323 (* fv_eqvt does not work, we need to repaire defined permute functions
 
       
   324    defined fv and defined alpha... *)
 
       
   325 nominal_datatype trm4 =
 
       
   326   Vr4 "name"
 
       
   327 | Ap4 "trm4" "trm4 list"
 
       
   328 | Lm4 x::"name" t::"trm4"  bind x in t
 
       
   329 
       
   330 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
 
       
   331 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 
       
   332 
   349 (* core haskell *)
 
   333 (* core haskell *)
 
   350 print_theorems
 
       
   351 
       
   352 atom_decl var
 
   334 atom_decl var
 
   353 atom_decl tvar
 
   335 atom_decl tvar
 
   354 
   336 
   355 
       
   356 (* there are types, coercion types and regular types *)
 
   337 (* there are types, coercion types and regular types *)
 
   357 nominal_datatype tkind = 
   338 nominal_datatype tkind =
 
   358   KStar
 
   339   KStar
 
   359 | KFun "tkind" "tkind"
 
   340 | KFun "tkind" "tkind"
 
   360 and ckind =
 
   341 and ckind =
 
   361   CKEq "ty" "ty" 
   342   CKEq "ty" "ty"
 
   362 and ty =
 
   343 and ty =
 
   363   TVar "tvar"
 
   344   TVar "tvar"
 
   364 | TC "string"
 
   345 | TC "string"
 
   365 | TApp "ty" "ty"
 
   346 | TApp "ty" "ty"
 
   366 | TFun "string" "ty list"
 
   347 | TFun "string" "ty list"
 
   386 typedecl kind
 
   367 typedecl kind
 
   387 
   368 
   388 instance ty and kind:: pt
 
   369 instance ty and kind:: pt
 
   389 sorry
 
   370 sorry
 
   390 
   371 
   391 abbreviation 
   372 abbreviation
 
   392   "atoms A \<equiv> atom ` A"
 
   373   "atoms A \<equiv> atom ` A"
 
   393 
   374 
   394 nominal_datatype trm =
 
   375 nominal_datatype trm =
 
   395   Var "var"
 
   376   Var "var"
 
   396 | C "string"
 
   377 | C "string"
 
   397 | LAM tv::"tvar" "kind" t::"trm"   bind tv in t 
   378 | LAM tv::"tvar" "kind" t::"trm"   bind tv in t
 
   398 | APP "trm" "ty"
 
   379 | APP "trm" "ty"
 
   399 | Lam v::"var" "ty" t::"trm"       bind v in t
 
   380 | Lam v::"var" "ty" t::"trm"       bind v in t
 
   400 | App "trm" "trm"
 
   381 | App "trm" "trm"
 
   401 | Let x::"var" "ty" "trm" t::"trm" bind x in t
 
   382 | Let x::"var" "ty" "trm" t::"trm" bind x in t
 
   402 | Case "trm" "assoc list"
 
   383 | Case "trm" "assoc list"
 
   403 | Cast "trm" "ty"                   --"ty is supposed to be a coercion type only"
 
   384 | Cast "trm" "ty"                   --"ty is supposed to be a coercion type only"
 
   404 and assoc = 
   385 and assoc =
 
   405   A p::"pat" t::"trm" bind "bv p" in t 
   386   A p::"pat" t::"trm" bind "bv p" in t
 
   406 and pat = 
   387 and pat =
 
   407   K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
 
   388   K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
 
   408 binder
 
   389 binder
 
   409  bv :: "pat \<Rightarrow> atom set"
 
   390  bv :: "pat \<Rightarrow> atom set"
 
   410 where
 
   391 where
 
   411  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
 
   392  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
 
   412 
   393 
   413 (*
 
   394 (*
 
   414 compat (K s ts vs) pi (K s' ts' vs') ==
 
   395 compat (K s ts vs) pi (K s' ts' vs') ==
 
   415   s = s' & 
   396   s = s' &
 
   416 
   397 
   417 *)
 
   398 *)
 
   418 
   399 
   419 
   400 
   420 (*thm bv_raw.simps*)
 
   401 
   421 
   402 text {* weirdo example from Peter Sewell's bestiary *}
 
   422 (* example 3 from Peter Sewell's bestiary *)
 
   403 
   423 nominal_datatype exp =
 
   404 nominal_datatype weird =
 
   424   VarP "name"
 
   405   WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
 
   425 | AppP "exp" "exp"
 
   406     bind x in p1, bind x in p2, bind y in p2, bind y in p3
 
   426 | LamP x::"name" e::"exp" bind x in e
 
   407 | WV "name"
 
   427 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp' p" in e1
 
   408 | WP "weird" "weird"
 
   428 and pat3 =
 
   409 
   429   PVar "name"
 
   410 thm permute_weird_raw.simps[no_vars]
 
   430 | PUnit
 
   411 thm alpha_weird_raw.intros[no_vars]
 
   431 | PPair "pat3" "pat3"
 
   412 thm fv_weird_raw.simps[no_vars]
 
   432 binder
 
   413 
   433   bp' :: "pat3 \<Rightarrow> atom set"
 
   414 (* example 6 from Terms.thy *)
 
   434 where
 
   415 
   435   "bp' (PVar x) = {atom x}"
 
   416 (* BV is not respectful, needs to fail*)
 
   436 | "bp' (PUnit) = {}"
 
   417 nominal_datatype trm6 =
 
   437 | "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
 
   418   Vr6 "name"
 
   438 thm alpha_exp_raw_alpha_pat3_raw_alpha_bp'_raw.intros
 
   419 | Lm6 x::"name" t::"trm6"         bind x in t
 
   439 
   420 | Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
 
   440 (* example 6 from Peter Sewell's bestiary *)
 
   421 binder
 
   441 nominal_datatype exp6 =
 
   422   bv6
 
   442   EVar name
 
   423 where
 
   443 | EPair exp6 exp6
 
   424   "bv6 (Vr6 n) = {}"
 
   444 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
 
   425 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
 
   445 and pat6 =
 
   426 | "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
 
   446   PVar' name
 
   427 (* example 7 from Terms.thy *)
 
   447 | PUnit'
 
   428 
   448 | PPair' pat6 pat6
 
   429 (* BV is not respectful, needs to fail*)
 
   449 binder
 
   430 nominal_datatype trm7 =
 
   450   bp6 :: "pat6 \<Rightarrow> atom set"
 
   431   Vr7 "name"
 
   451 where
 
   432 | Lm7 l::"name" r::"trm7"   bind l in r
 
   452   "bp6 (PVar' x) = {atom x}"
 
   433 | Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
 
   453 | "bp6 (PUnit') = {}"
 
   434 binder
 
   454 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
 
   435   bv7
 
   455 thm alpha_exp6_raw_alpha_pat6_raw_alpha_bp6_raw.intros
 
   436 where
 
   456 
   437   "bv7 (Vr7 n) = {atom n}"
 
   457 (* example 7 from Peter Sewell's bestiary *)
 
   438 | "bv7 (Lm7 n t) = bv7 t - {atom n}"
 
   458 nominal_datatype exp7 =
 
   439 | "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
 
   459   EVar name
 
   440 
   460 | EUnit
 
   441 (* example 8 from Terms.thy *)
 
   461 | EPair exp7 exp7
 
   442 
   462 | ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
 
   443 (* Binding in a term under a bn, needs to fail *)
 
   463 and lrb =
 
   444 nominal_datatype foo8 =
 
   464   Assign name exp7
 
   445   Foo0 "name"
 
   465 and lrbs =
 
   446 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
 
   466   Single lrb
 
   447 and bar8 =
 
   467 | More lrb lrbs
 
   448   Bar0 "name"
 
   468 binder
 
   449 | Bar1 "name" s::"name" b::"bar8" bind s in b
 
   469   b7 :: "lrb \<Rightarrow> atom set" and
 
   450 binder
 
   470   b7s :: "lrbs \<Rightarrow> atom set"
 
   451   bv8
 
   471 where
 
   452 where
 
   472   "b7 (Assign x e) = {atom x}"
 
   453   "bv8 (Bar0 x) = {}"
 
   473 | "b7s (Single a) = b7 a"
 
   454 | "bv8 (Bar1 v x b) = {atom v}"
 
   474 | "b7s (More a as) = (b7 a) \<union> (b7s as)"
 
   455 
   475 thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
 
   456 (* example 9 from Terms.thy *)
 
   476 
   457 
   477 (* example 8 from Peter Sewell's bestiary *)
 
   458 (* BV is not respectful, needs to fail*)
 
   478 nominal_datatype exp8 =
 
   459 nominal_datatype lam9 =
 
   479   EVar name
 
   460   Var9 "name"
 
   480 | EUnit
 
   461 | Lam9 n::"name" l::"lam9" bind n in l
 
   481 | EPair exp8 exp8
 
   462 and bla9 =
 
   482 | ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
 
   463   Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
 
   483 and fnclause =
 
   464 binder
 
   484   K x::name p::pat8 e::exp8 bind "b_pat p" in e
 
   465   bv9
 
   485 and fnclauses =
 
   466 where
 
   486   S fnclause
 
   467   "bv9 (Var9 x) = {}"
 
   487 | ORs fnclause fnclauses
 
   468 | "bv9 (Lam9 x b) = {atom x}"
 
   488 and lrb8 =
 
   469 
   489   Clause fnclauses
 
   470 
   490 and lrbs8 =
 
   471 (* Type schemes with separate datatypes *)
 
   491   Single lrb8
 
   472 nominal_datatype t =
 
   492 | More lrb8 lrbs8
 
   473   Var "name"
 
   493 and pat8 =
 
   474 | Fun "t" "t"
 
   494   PVar name
 
   475 
   495 | PUnit
 
   476 nominal_datatype tyS =
 
   496 | PPair pat8 pat8
 
   477   All xs::"name list" ty::"t_raw" bind xs in ty
 
   497 binder
 
       
   498   b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
 
       
   499   b_pat :: "pat8 \<Rightarrow> atom set" and
 
       
   500   b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
 
       
   501   b_fnclause :: "fnclause \<Rightarrow> atom set" and
 
       
   502   b_lrb8 :: "lrb8 \<Rightarrow> atom set"
 
       
   503 where
 
       
   504   "b_lrbs8 (Single l) = b_lrb8 l"
 
       
   505 | "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
 
       
   506 | "b_pat (PVar x) = {atom x}"
 
       
   507 | "b_pat (PUnit) = {}"
 
       
   508 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
 
       
   509 | "b_fnclauses (S fc) = (b_fnclause fc)"
 
       
   510 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
 
       
   511 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
 
       
   512 | "b_fnclause (K x pat exp8) = {atom x}"
 
       
   513 thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros
 
       
   514 
   478 
   515 
   479 
   516 
   480 
   517 
   481 
   518 (* example 9 from Peter Sewell's bestiary *)
 
   482 (* example 9 from Peter Sewell's bestiary *)
nominal2