5 |
5 |
6 atom_decl name |
6 atom_decl name |
7 |
7 |
8 nominal_datatype lt = |
8 nominal_datatype lt = |
9 Var name ("_~" [150] 149) |
9 Var name ("_~" [150] 149) |
10 | Abs x::"name" t::"lt" binds x in t |
10 | Lam x::"name" t::"lt" binds x in t |
11 | App lt lt (infixl "$" 100) |
11 | App lt lt (infixl "$" 100) |
12 |
12 |
13 nominal_primrec |
13 nominal_primrec |
14 subst :: "lt \<Rightarrow> lt \<Rightarrow> name \<Rightarrow> lt" ("_[_'/_]" [200,0,0] 190) |
14 subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90) |
15 where |
15 where |
16 "(y~)[L/x] = (if y = x then L else y~)" |
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
17 | "atom y\<sharp>L \<Longrightarrow> atom y\<sharp>x \<Longrightarrow> (Abs y M)[L/x] = Abs y (M[L/x])" |
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
18 | "(M $ N)[L/x] = M[L/x] $ N[L/x]" |
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(perm_simp) |
20 apply (rule, perm_simp, rule) |
21 apply(auto) |
21 apply(rule TrueI) |
|
22 apply(auto simp add: lt.distinct lt.eq_iff) |
22 apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) |
23 apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) |
23 apply(simp_all add: fresh_star_def fresh_Pair) |
24 apply blast |
24 apply blast+ |
25 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
25 apply (erule Abs_lst1_fcb) |
26 apply blast |
26 apply (simp_all add: Abs_fresh_iff)[2] |
27 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
27 apply(drule_tac a="atom (ya)" in fresh_eqvt_at) |
28 apply(simp_all add: Abs_fresh_iff) |
28 apply(simp add: finite_supp fresh_Pair) |
29 apply(simp add: fresh_star_def fresh_Pair) |
29 apply(simp_all add: fresh_Pair Abs_fresh_iff) |
30 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)+ |
30 apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> La = La") |
31 done |
31 apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> xa = xa") |
|
32 apply(simp add: atom_eqvt eqvt_at_def Abs1_eq_iff swap_commute) |
|
33 apply (simp_all add: swap_fresh_fresh) |
|
34 done |
|
35 |
32 |
36 termination (eqvt) by lexicographic_order |
33 termination (eqvt) by lexicographic_order |
37 |
34 |
38 lemma forget[simp]: |
35 lemma forget[simp]: |
39 shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M" |
36 shows "atom x \<sharp> M \<Longrightarrow> M[x ::= s] = M" |
40 by (nominal_induct M avoiding: x s rule: lt.strong_induct) |
37 by (nominal_induct M avoiding: x s rule: lt.strong_induct) |
41 (auto simp add: lt.fresh fresh_at_base) |
38 (auto simp add: lt.fresh fresh_at_base) |
42 |
39 |
43 lemma [simp]: "supp ( M[V/(x::name)] ) <= (supp(M) - {atom x}) Un (supp V)" |
40 lemma [simp]: "supp (M[x ::= V]) <= (supp(M) - {atom x}) Un (supp V)" |
44 by (nominal_induct M avoiding: x V rule: lt.strong_induct) |
41 by (nominal_induct M avoiding: x V rule: lt.strong_induct) |
45 (auto simp add: lt.supp supp_at_base, blast, blast) |
42 (auto simp add: lt.supp supp_at_base, blast, blast) |
46 |
43 |
47 nominal_primrec |
44 nominal_primrec |
48 isValue:: "lt => bool" |
45 isValue:: "lt => bool" |
49 where |
46 where |
50 "isValue (Var x) = True" |
47 "isValue (Var x) = True" |
51 | "isValue (Abs y N) = True" |
48 | "isValue (Lam y N) = True" |
52 | "isValue (A $ B) = False" |
49 | "isValue (A $ B) = False" |
53 unfolding eqvt_def isValue_graph_def |
50 unfolding eqvt_def isValue_graph_def |
54 by (perm_simp, auto) |
51 by (perm_simp, auto) |
55 (erule lt.exhaust, auto) |
52 (erule lt.exhaust, auto) |
56 |
53 |
57 termination (eqvt) |
54 termination (eqvt) |
58 by (relation "measure size") (simp_all) |
55 by (relation "measure size") (simp_all) |
59 |
56 |
60 lemma is_Value_eqvt[eqvt]: |
|
61 shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)" |
|
62 by (induct M rule: lt.induct) (simp_all add: eqvts) |
|
63 |
|
64 inductive |
57 inductive |
65 eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
58 eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
66 where |
59 where |
67 evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Abs x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[V/x])" |
60 evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])" |
68 | ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $ M) \<longrightarrow>\<^isub>\<beta> (V $ M')" |
61 | ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $ M) \<longrightarrow>\<^isub>\<beta> (V $ M')" |
69 | ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $ N) \<longrightarrow>\<^isub>\<beta> (M' $ N)" |
62 | ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $ N) \<longrightarrow>\<^isub>\<beta> (M' $ N)" |
70 |
63 |
71 equivariance eval |
64 equivariance eval |
72 |
65 |