equal
deleted
inserted
replaced
378 | CLeftc "co" |
378 | CLeftc "co" |
379 | CCoe "co" "co" |
379 | CCoe "co" "co" |
380 |
380 |
381 |
381 |
382 typedecl ty --"hack since ty is not yet defined" |
382 typedecl ty --"hack since ty is not yet defined" |
|
383 typedecl kind |
|
384 |
|
385 instance ty and kind:: pt |
|
386 sorry |
383 |
387 |
384 abbreviation |
388 abbreviation |
385 "atoms A \<equiv> atom ` A" |
389 "atoms A \<equiv> atom ` A" |
386 |
390 |
387 nominal_datatype trm = |
391 nominal_datatype trm = |
415 (* example 3 from Peter Sewell's bestiary *) |
419 (* example 3 from Peter Sewell's bestiary *) |
416 nominal_datatype exp = |
420 nominal_datatype exp = |
417 VarP "name" |
421 VarP "name" |
418 | AppP "exp" "exp" |
422 | AppP "exp" "exp" |
419 | LamP x::"name" e::"exp" bind x in e |
423 | LamP x::"name" e::"exp" bind x in e |
420 | LetP x::"name" p::"pat" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 |
424 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 |
421 and pat = |
425 and pat3 = |
422 PVar "name" |
426 PVar "name" |
423 | PUnit |
427 | PUnit |
424 | PPair "pat" "pat" |
428 | PPair "pat3" "pat3" |
425 binder |
429 binder |
426 bp :: "pat \<Rightarrow> atom set" |
430 bp :: "pat3 \<Rightarrow> atom set" |
427 where |
431 where |
428 "bp (PVar x) = {atom x}" |
432 "bp (PVar x) = {atom x}" |
429 | "bp (PUnit) = {}" |
433 | "bp (PUnit) = {}" |
430 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
434 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
431 thm alpha_exp_raw_alpha_pat_raw.intros |
435 thm alpha_exp_raw_alpha_pat3_raw.intros |
432 |
436 |
433 (* example 6 from Peter Sewell's bestiary *) |
437 (* example 6 from Peter Sewell's bestiary *) |
434 nominal_datatype exp6 = |
438 nominal_datatype exp6 = |
435 EVar name |
439 EVar name |
436 | EPair exp6 exp6 |
440 | EPair exp6 exp6 |