equal
deleted
inserted
replaced
9 ML {* val _ = recursive := false *} |
9 ML {* val _ = recursive := false *} |
10 nominal_datatype exp = |
10 nominal_datatype exp = |
11 VarP "name" |
11 VarP "name" |
12 | AppP "exp" "exp" |
12 | AppP "exp" "exp" |
13 | LamP x::"name" e::"exp" bind x in e |
13 | LamP x::"name" e::"exp" bind x in e |
14 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1 |
14 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 |
15 and pat3 = |
15 and pat3 = |
16 PVar "name" |
16 PVar "name" |
17 | PUnit |
17 | PUnit |
18 | PPair "pat3" "pat3" |
18 | PPair "pat3" "pat3" |
19 binder |
19 binder |
20 bp'' :: "pat3 \<Rightarrow> atom set" |
20 bp :: "pat3 \<Rightarrow> atom set" |
21 where |
21 where |
22 "bp'' (PVar x) = {atom x}" |
22 "bp (PVar x) = {atom x}" |
23 | "bp'' (PUnit) = {}" |
23 | "bp (PUnit) = {}" |
24 | "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2" |
24 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
25 |
25 |
26 thm exp_pat3.fv |
26 thm exp_pat3.fv |
27 thm exp_pat3.eq_iff |
27 thm exp_pat3.eq_iff |
28 thm exp_pat3.bn |
28 thm exp_pat3.bn |
29 thm exp_pat3.perm |
29 thm exp_pat3.perm |
30 thm exp_pat3.induct |
30 thm exp_pat3.induct |
31 thm exp_pat3.distinct |
31 thm exp_pat3.distinct |
32 thm exp_pat3.fv |
32 thm exp_pat3.fv |
33 thm exp_pat3.supp (* The bindings are too complicated *) |
33 thm exp_pat3.supp |
34 |
34 |
35 end |
35 end |
36 |
36 |
37 |
37 |
38 |
38 |