equal
deleted
inserted
replaced
1 theory LetRec |
1 theory LetRec |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 declare [[STEPS = 14]] |
|
6 |
|
7 atom_decl name |
5 atom_decl name |
8 |
6 |
9 nominal_datatype let_rec: |
7 nominal_datatype let_rec: |
10 lam = |
8 trm = |
11 Var "name" |
9 Var "name" |
12 | App "lam" "lam" |
10 | App "trm" "trm" |
13 | Lam x::"name" t::"lam" bind (set) x in t |
11 | Lam x::"name" t::"trm" bind (set) x in t |
14 | Let_Rec bp::"bp" t::"lam" bind (set) "bi bp" in bp t |
12 | Let_Rec bp::"bp" t::"trm" bind (set) "bn bp" in bp t |
15 and bp = |
13 and bp = |
16 Bp "name" "lam" |
14 Bp "name" "trm" |
17 binder |
15 binder |
18 bi::"bp \<Rightarrow> atom set" |
16 bn::"bp \<Rightarrow> atom set" |
19 where |
17 where |
20 "bi (Bp x t) = {atom x}" |
18 "bn (Bp x t) = {atom x}" |
21 |
19 |
22 thm let_rec.distinct |
20 thm let_rec.distinct |
23 thm let_rec.induct |
21 thm let_rec.induct |
24 thm let_rec.exhaust |
22 thm let_rec.exhaust |
25 thm let_rec.fv_defs |
23 thm let_rec.fv_defs |