1 theory LetSimple1 |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 nominal_datatype trm = |
|
8 Var "name" |
|
9 | App "trm" "trm" |
|
10 | Let x::"name" "trm" t::"trm" binds x in t |
|
11 |
|
12 print_theorems |
|
13 |
|
14 thm trm.fv_defs |
|
15 thm trm.eq_iff |
|
16 thm trm.bn_defs |
|
17 thm trm.bn_inducts |
|
18 thm trm.perm_simps |
|
19 thm trm.induct |
|
20 thm trm.inducts |
|
21 thm trm.distinct |
|
22 thm trm.supp |
|
23 thm trm.fresh |
|
24 thm trm.exhaust |
|
25 thm trm.strong_exhaust |
|
26 thm trm.perm_bn_simps |
|
27 |
|
28 nominal_primrec |
|
29 height_trm :: "trm \<Rightarrow> nat" |
|
30 where |
|
31 "height_trm (Var x) = 1" |
|
32 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
|
33 | "height_trm (Let x t s) = max (height_trm t) (height_trm s)" |
|
34 apply (simp only: eqvt_def height_trm_graph_def) |
|
35 apply (rule, perm_simp, rule, rule TrueI) |
|
36 apply (case_tac x rule: trm.exhaust(1)) |
|
37 apply (auto)[3] |
|
38 apply(simp_all)[5] |
|
39 apply (subgoal_tac "height_trm_sumC t = height_trm_sumC ta") |
|
40 apply (subgoal_tac "height_trm_sumC s = height_trm_sumC sa") |
|
41 apply simp |
|
42 apply(simp) |
|
43 apply(erule conjE) |
|
44 apply(erule_tac c="()" in Abs_lst1_fcb2) |
|
45 apply(simp_all add: fresh_star_def pure_fresh)[2] |
|
46 apply(simp_all add: eqvt_at_def)[2] |
|
47 apply(simp) |
|
48 done |
|
49 |
|
50 termination |
|
51 by lexicographic_order |
|
52 |
|
53 |
|
54 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
|
55 frees_set :: "trm \<Rightarrow> atom set" |
|
56 where |
|
57 "frees_set (Var x) = {atom x}" |
|
58 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
|
59 | "frees_set (Let x t s) = (frees_set s) - {atom x} \<union> (frees_set t)" |
|
60 apply(simp add: eqvt_def frees_set_graph_def) |
|
61 apply(rule, perm_simp, rule) |
|
62 apply(erule frees_set_graph.induct) |
|
63 apply(auto)[3] |
|
64 apply(rule_tac y="x" in trm.exhaust) |
|
65 apply(auto)[3] |
|
66 apply(simp_all)[5] |
|
67 apply(simp) |
|
68 apply(erule conjE) |
|
69 apply(subgoal_tac "frees_set_sumC s - {atom x} = frees_set_sumC sa - {atom xa}") |
|
70 apply(simp) |
|
71 apply(erule_tac c="()" in Abs_lst1_fcb2) |
|
72 apply(simp add: fresh_minus_atom_set) |
|
73 apply(simp add: fresh_star_def fresh_Unit) |
|
74 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
|
75 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
|
76 done |
|
77 |
|
78 termination |
|
79 by lexicographic_order |
|
80 |
|
81 |
|
82 nominal_primrec |
|
83 subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90) |
|
84 where |
|
85 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
86 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
|
87 | "atom x \<sharp> (y, s) \<Longrightarrow> (Let x t t')[y ::= s] = Let x (t[y ::= s]) (t'[y ::= s])" |
|
88 apply(simp add: eqvt_def subst_graph_def) |
|
89 apply (rule, perm_simp, rule) |
|
90 apply(rule TrueI) |
|
91 apply(auto)[1] |
|
92 apply(rule_tac y="a" and c="(aa, b)" in trm.strong_exhaust) |
|
93 apply(blast)+ |
|
94 apply(simp_all add: fresh_star_def fresh_Pair_elim)[1] |
|
95 apply(blast) |
|
96 apply(simp_all)[5] |
|
97 apply(simp (no_asm_use)) |
|
98 apply(simp) |
|
99 apply(erule conjE)+ |
|
100 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
|
101 apply(simp add: Abs_fresh_iff) |
|
102 apply(simp add: fresh_star_def fresh_Pair) |
|
103 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
104 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
105 done |
|
106 |
|
107 termination |
|
108 by lexicographic_order |
|
109 |
|
110 |
|
111 end |
|