equal
deleted
inserted
replaced
1 theory Lambda |
1 theory Lambda |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
|
4 |
4 |
5 |
5 |
6 |
6 atom_decl name |
7 atom_decl name |
7 |
8 |
8 nominal_datatype lam = |
9 nominal_datatype lam = |
9 Var "name" |
10 Var "name" |
10 | App "lam" "lam" |
11 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
12 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
12 |
13 |
|
14 ML {* Method.SIMPLE_METHOD' *} |
|
15 ML {* Sign.intern_const *} |
|
16 |
|
17 ML {* |
|
18 val test:((Proof.context -> Method.method) context_parser) = |
|
19 Scan.succeed (fn ctxt => |
|
20 let |
|
21 val _ = Inductive.the_inductive ctxt "Lambda.frees_lst_graph" |
|
22 in |
|
23 Method.SIMPLE_METHOD' (K all_tac) |
|
24 end) |
|
25 *} |
|
26 |
|
27 method_setup test = {* test *} {* test *} |
13 |
28 |
14 section {* free name function *} |
29 section {* free name function *} |
15 |
30 |
16 text {* first returns an atom list *} |
31 text {* first returns an atom list *} |
|
32 |
|
33 ML Thm.implies_intr |
17 |
34 |
18 nominal_primrec |
35 nominal_primrec |
19 frees_lst :: "lam \<Rightarrow> atom list" |
36 frees_lst :: "lam \<Rightarrow> atom list" |
20 where |
37 where |
21 "frees_lst (Var x) = [atom x]" |
38 "frees_lst (Var x) = [atom x]" |