equal
deleted
inserted
replaced
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
19 unfolding eqvt_def subst_graph_def |
19 unfolding eqvt_def subst_graph_def |
20 apply (simp) |
20 apply (simp) |
21 apply(rule TrueI) |
21 apply(rule TrueI) |
|
22 using [[simproc del: alpha_lst]] |
22 apply(auto simp add: lt.distinct lt.eq_iff) |
23 apply(auto simp add: lt.distinct lt.eq_iff) |
23 apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) |
24 apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) |
24 apply blast |
25 apply blast |
25 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
26 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
26 apply blast |
27 apply blast |
58 by (relation "measure size") (simp_all) |
59 by (relation "measure size") (simp_all) |
59 |
60 |
60 inductive |
61 inductive |
61 eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
62 eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
62 where |
63 where |
63 evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])" |
64 evbeta: "\<lbrakk>atom x \<sharp> V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])" |
64 | ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $$ M) \<longrightarrow>\<^isub>\<beta> (V $$ M')" |
65 | ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $$ M) \<longrightarrow>\<^isub>\<beta> (V $$ M')" |
65 | ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $$ N) \<longrightarrow>\<^isub>\<beta> (M' $$ N)" |
66 | ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $$ N) \<longrightarrow>\<^isub>\<beta> (M' $$ N)" |
66 |
67 |
67 equivariance eval |
68 equivariance eval |
68 |
69 |