2684
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Lambda
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../Nominal/Nominal2"
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
section {* Definitions for Lambda Terms *}
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
2686
|
7 |
|
2684
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
text {* type of variables *}
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
atom_decl name
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
subsection {* Alpha-Equated Lambda Terms *}
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
nominal_datatype lam =
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
Var "name"
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
| App "lam" "lam"
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
text {* some automatically derived theorems *}
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
thm lam.distinct
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
thm lam.eq_iff
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
thm lam.fresh
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
thm lam.size
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
thm lam.exhaust
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
thm lam.strong_exhaust
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
thm lam.induct
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
thm lam.strong_induct
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
subsection {* Height Function *}
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
nominal_primrec
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
height :: "lam \<Rightarrow> int"
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
where
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
"height (Var x) = 1"
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
| "height (App t1 t2) = max (height t1) (height t2) + 1"
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
| "height (Lam [x].t) = height t + 1"
|
2718
|
41 |
apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)")
|
|
42 |
unfolding eqvt_def
|
|
43 |
apply(rule allI)
|
|
44 |
apply(simp add: permute_fun_def)
|
|
45 |
apply(rule ext)
|
|
46 |
apply(rule ext)
|
|
47 |
apply(simp add: permute_bool_def)
|
|
48 |
apply(rule iffI)
|
|
49 |
apply(drule_tac x="p" in meta_spec)
|
|
50 |
apply(drule_tac x="- p \<bullet> x" in meta_spec)
|
|
51 |
apply(drule_tac x="- p \<bullet> xa" in meta_spec)
|
|
52 |
apply(simp)
|
|
53 |
apply(drule_tac x="-p" in meta_spec)
|
|
54 |
apply(drule_tac x="x" in meta_spec)
|
|
55 |
apply(drule_tac x="xa" in meta_spec)
|
|
56 |
apply(simp)
|
|
57 |
apply(erule height_graph.induct)
|
|
58 |
apply(perm_simp)
|
|
59 |
apply(rule height_graph.intros)
|
|
60 |
apply(perm_simp)
|
|
61 |
apply(rule height_graph.intros)
|
|
62 |
apply(assumption)
|
|
63 |
apply(assumption)
|
|
64 |
apply(perm_simp)
|
|
65 |
apply(rule height_graph.intros)
|
|
66 |
apply(assumption)
|
2684
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
apply(rule_tac y="x" in lam.exhaust)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
apply(auto simp add: lam.distinct lam.eq_iff)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
apply(simp add: Abs_eq_iff alphas)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
apply(clarify)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
apply(subst (4) supp_perm_eq[where p="p", symmetric])
|
2718
|
72 |
apply(simp add: pure_supp fresh_star_def)
|
2684
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
apply(simp add: eqvt_at_def)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
done
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
termination
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
by (relation "measure size") (simp_all add: lam.size)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
|
2686
|
80 |
subsection {* Capture-Avoiding Substitution *}
|
2684
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
82 |
nominal_primrec
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
83 |
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
where
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
"(Var x)[y ::= s] = (if x = y then s else (Var x))"
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
87 |
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
|
2718
|
88 |
apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)")
|
|
89 |
unfolding eqvt_def
|
|
90 |
apply(rule allI)
|
|
91 |
apply(simp add: permute_fun_def)
|
|
92 |
apply(rule ext)
|
|
93 |
apply(rule ext)
|
|
94 |
apply(simp add: permute_bool_def)
|
|
95 |
apply(rule iffI)
|
|
96 |
apply(drule_tac x="p" in meta_spec)
|
|
97 |
apply(drule_tac x="- p \<bullet> x" in meta_spec)
|
|
98 |
apply(drule_tac x="- p \<bullet> xa" in meta_spec)
|
|
99 |
apply(simp)
|
|
100 |
apply(drule_tac x="-p" in meta_spec)
|
|
101 |
apply(drule_tac x="x" in meta_spec)
|
|
102 |
apply(drule_tac x="xa" in meta_spec)
|
|
103 |
apply(simp)
|
|
104 |
apply(erule subst_graph.induct)
|
|
105 |
apply(perm_simp)
|
|
106 |
apply(rule subst_graph.intros)
|
|
107 |
apply(perm_simp)
|
|
108 |
apply(rule subst_graph.intros)
|
|
109 |
apply(assumption)
|
|
110 |
apply(assumption)
|
|
111 |
apply(perm_simp)
|
|
112 |
apply(rule subst_graph.intros)
|
|
113 |
apply(simp add: fresh_Pair)
|
|
114 |
apply(assumption)
|
2684
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
115 |
apply(auto simp add: lam.distinct lam.eq_iff)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
116 |
apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
apply(blast)+
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
118 |
apply(simp add: fresh_star_def)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
120 |
apply(subst (asm) Abs_eq_iff2)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
121 |
apply(simp add: alphas atom_eqvt)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
122 |
apply(clarify)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
123 |
apply(rule trans)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
124 |
apply(rule_tac p="p" in supp_perm_eq[symmetric])
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
125 |
apply(rule fresh_star_supp_conv)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
126 |
apply(drule fresh_star_perm_set_conv)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
127 |
apply(simp add: finite_supp)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
128 |
apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))")
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
129 |
apply(auto simp add: fresh_star_def)[1]
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
130 |
apply(simp (no_asm) add: fresh_star_def)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
131 |
apply(rule conjI)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
132 |
apply(simp (no_asm) add: Abs_fresh_iff)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
133 |
apply(clarify)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
134 |
apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
135 |
apply(simp add: finite_supp)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
136 |
apply(simp (no_asm_use) add: fresh_Pair)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
137 |
apply(simp add: Abs_fresh_iff)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
138 |
apply(simp)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
139 |
apply(simp add: Abs_fresh_iff)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
140 |
apply(subgoal_tac "p \<bullet> ya = ya")
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
141 |
apply(subgoal_tac "p \<bullet> sa = sa")
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
142 |
apply(simp add: atom_eqvt eqvt_at_def)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
143 |
apply(rule perm_supp_eq)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
144 |
apply(auto simp add: fresh_star_def fresh_Pair)[1]
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
145 |
apply(rule perm_supp_eq)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
146 |
apply(auto simp add: fresh_star_def fresh_Pair)[1]
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
147 |
apply(rule conjI)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
148 |
apply(simp add: Abs_fresh_iff)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
149 |
apply(drule sym)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
150 |
apply(simp add: Abs_fresh_iff)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
151 |
done
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
152 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
153 |
termination
|
2686
|
154 |
by (relation "measure (\<lambda>(t, _, _). size t)")
|
2684
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
155 |
(simp_all add: lam.size)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
156 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
157 |
lemma subst_eqvt[eqvt]:
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
158 |
shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
159 |
by (induct t x s rule: subst.induct) (simp_all)
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
160 |
|
2701
|
161 |
lemma fresh_fact:
|
|
162 |
assumes a: "atom z \<sharp> s"
|
|
163 |
and b: "z = y \<or> atom z \<sharp> t"
|
|
164 |
shows "atom z \<sharp> t[y ::= s]"
|
|
165 |
using a b
|
|
166 |
by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
|
|
167 |
(auto simp add: lam.fresh fresh_at_base)
|
2684
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
168 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
169 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
170 |
end
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
171 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
172 |
|
d72a7168f1cb
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
173 |
|