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 | App lt lt (infixl "$" 100) |
10 | App lt lt (infixl "$$" 100) |
11 | Lam x::"name" t::"lt" binds x in t |
11 | Lam x::"name" t::"lt" binds x in t |
12 |
12 |
13 nominal_primrec |
13 nominal_primrec |
14 subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90) |
14 subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90) |
15 where |
15 where |
47 nominal_primrec |
47 nominal_primrec |
48 isValue:: "lt => bool" |
48 isValue:: "lt => bool" |
49 where |
49 where |
50 "isValue (Var x) = True" |
50 "isValue (Var x) = True" |
51 | "isValue (Lam y N) = True" |
51 | "isValue (Lam y N) = True" |
52 | "isValue (A $ B) = False" |
52 | "isValue (A $$ B) = False" |
53 unfolding eqvt_def isValue_graph_def |
53 unfolding eqvt_def isValue_graph_def |
54 by (perm_simp, auto) |
54 by (perm_simp, auto) |
55 (erule lt.exhaust, auto) |
55 (erule lt.exhaust, auto) |
56 |
56 |
57 termination (eqvt) |
57 termination (eqvt) |
58 by (relation "measure size") (simp_all) |
58 by (relation "measure size") (simp_all) |
59 |
59 |
60 inductive |
60 inductive |
61 eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
61 eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
62 where |
62 where |
63 evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])" |
63 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')" |
64 | 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)" |
65 | ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $$ N) \<longrightarrow>\<^isub>\<beta> (M' $$ N)" |
66 |
66 |
67 equivariance eval |
67 equivariance eval |
68 |
68 |
69 nominal_inductive eval |
69 nominal_inductive eval |
70 done |
70 done |
109 equivariance eval_star |
109 equivariance eval_star |
110 |
110 |
111 lemma evbeta': |
111 lemma evbeta': |
112 fixes x :: name |
112 fixes x :: name |
113 assumes "isValue V" and "atom x\<sharp>V" and "N = (M[x ::= V])" |
113 assumes "isValue V" and "atom x\<sharp>V" and "N = (M[x ::= V])" |
114 shows "((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N" |
114 shows "((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N" |
115 using assms by simp (rule evs2, rule evbeta, simp_all add: evs1) |
115 using assms by simp (rule evs2, rule evbeta, simp_all add: evs1) |
116 |
116 |
117 end |
117 end |
118 |
118 |
119 |
119 |