equal
deleted
inserted
replaced
8 nominal_datatype expr = |
8 nominal_datatype expr = |
9 eCnst nat |
9 eCnst nat |
10 | eVar nat |
10 | eVar nat |
11 |
11 |
12 inductive |
12 inductive |
13 eval :: "expr \<Rightarrow> nat \<Rightarrow> bool" |
13 eval :: "expr \<Rightarrow> nat list \<Rightarrow> bool" |
14 where |
14 where |
15 evCnst: "eval (eCnst c) 0" |
15 evCnst1: "eval (eCnst c) [2,1]" |
16 | evVar: "eval (eVar n) 2" |
16 | evCnst2: "eval (eCnst b) [1,2]" |
|
17 | evVar: "eval (eVar n) [1]" |
17 |
18 |
18 inductive_cases |
19 inductive_cases |
19 evInv_Cnst: "eval (eCnst c) m" |
20 evInv_Cnst: "eval (eCnst c) [1,2]" |
20 |
21 |
21 thm evInv_Cnst[simplified expr.distinct expr.eq_iff] |
22 thm evInv_Cnst |
|
23 |
22 |
24 |
23 |
25 |
24 atom_decl name |
26 atom_decl name |
25 |
27 |
26 nominal_datatype lam = |
28 nominal_datatype lam = |
141 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
143 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
142 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
144 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
143 defer |
145 defer |
144 apply(rule_tac y="x" in lam.exhaust) |
146 apply(rule_tac y="x" in lam.exhaust) |
145 apply(simp_all)[3] |
147 apply(simp_all)[3] |
146 apply(simp_all add: lam.distinct lam.eq_iff) |
148 apply(auto)[1] |
|
149 apply(simp_all) |
147 apply (erule Abs1_eq_fdest) |
150 apply (erule Abs1_eq_fdest) |
148 apply(simp add: supp_removeAll fresh_def) |
151 apply(simp add: supp_removeAll fresh_def) |
149 apply(drule supp_eqvt_at) |
152 apply(drule supp_eqvt_at) |
150 apply(simp add: finite_supp) |
153 apply(simp add: finite_supp) |
151 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
154 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |