2436
|
1 |
theory LetRec
|
2454
|
2 |
imports "../Nominal2"
|
1596
|
3 |
begin
|
|
4 |
|
2311
|
5 |
atom_decl name
|
2056
|
6 |
|
2436
|
7 |
nominal_datatype let_rec:
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
8 |
trm =
|
2056
|
9 |
Var "name"
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
| App "trm" "trm"
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
11 |
| Lam x::"name" t::"trm" binds (set) x in t
|
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
12 |
| Let_Rec bp::"bp" t::"trm" binds (set) "bn bp" in bp t
|
1946
|
13 |
and bp =
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
Bp "name" "trm"
|
1596
|
15 |
binder
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
bn::"bp \<Rightarrow> atom set"
|
1596
|
17 |
where
|
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
"bn (Bp x t) = {atom x}"
|
1596
|
19 |
|
2436
|
20 |
thm let_rec.distinct
|
|
21 |
thm let_rec.induct
|
|
22 |
thm let_rec.exhaust
|
|
23 |
thm let_rec.fv_defs
|
|
24 |
thm let_rec.bn_defs
|
|
25 |
thm let_rec.perm_simps
|
|
26 |
thm let_rec.eq_iff
|
|
27 |
thm let_rec.fv_bn_eqvt
|
|
28 |
thm let_rec.size_eqvt
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
|
2877
|
30 |
|
|
31 |
nominal_primrec
|
|
32 |
height_trm :: "trm \<Rightarrow> nat"
|
|
33 |
and height_bp :: "bp \<Rightarrow> nat"
|
|
34 |
where
|
|
35 |
"height_trm (Var x) = 1"
|
|
36 |
| "height_trm (App l r) = max (height_trm l) (height_trm r)"
|
|
37 |
| "height_trm (Lam v b) = 1 + (height_trm b)"
|
|
38 |
| "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)"
|
|
39 |
| "height_bp (Bp v t) = height_trm t"
|
|
40 |
apply (simp only: eqvt_def height_trm_height_bp_graph_def)
|
|
41 |
apply (rule, perm_simp, rule, rule TrueI)
|
|
42 |
apply auto
|
|
43 |
apply (case_tac x)
|
|
44 |
apply (case_tac a rule: let_rec.exhaust(1))
|
|
45 |
apply auto
|
|
46 |
apply (case_tac b rule: let_rec.exhaust(2))
|
|
47 |
apply blast
|
|
48 |
apply (erule Abs_set_fcb)
|
|
49 |
apply (simp_all add: pure_fresh)
|
|
50 |
apply (simp add: eqvt_at_def)
|
|
51 |
apply (simp add: Abs_eq_iff2)
|
|
52 |
apply (simp add: alphas)
|
|
53 |
apply clarify
|
|
54 |
apply (rule trans)
|
|
55 |
apply(rule_tac p="p" in supp_perm_eq[symmetric])
|
|
56 |
apply (simp add: pure_supp fresh_star_def)
|
2971
|
57 |
apply(simp add: eqvt_at_def)
|
|
58 |
apply(perm_simp)
|
|
59 |
apply (simp add: permute_fun_def)
|
2877
|
60 |
done
|
|
61 |
|
2974
|
62 |
ML {*
|
|
63 |
let
|
|
64 |
val [t1, t2] = Item_Net.content (Nominal_Function_Common.get_function @{context})
|
|
65 |
in
|
|
66 |
(#eqvts (snd t1),
|
|
67 |
#eqvts (snd t2))
|
|
68 |
end
|
|
69 |
*}
|
|
70 |
|
|
71 |
|
2973
d1038e67923a
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
thm height_trm_def height_bp_def
|
d1038e67923a
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
|
d1038e67923a
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
termination (eqvt) by lexicographic_order
|
2067
|
75 |
|
1596
|
76 |
end
|
|
77 |
|
|
78 |
|
|
79 |
|