|
1 theory Lambda_add |
|
2 imports "Lambda" |
|
3 begin |
|
4 |
|
5 nominal_primrec |
|
6 addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
|
7 where |
|
8 "fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)" |
|
9 | "addlam_pre (Var x) (App t1 t2) = Var x" |
|
10 | "addlam_pre (Var x) (Var v) = Var x" |
|
11 | "addlam_pre (App t1 t2) it = App t1 t2" |
|
12 | "addlam_pre (Lam [x]. t) it = Lam [x].t" |
|
13 apply (subgoal_tac "\<And>p a x. addlam_pre_graph a x \<Longrightarrow> addlam_pre_graph (p \<bullet> a) (p \<bullet> x)") |
|
14 apply (simp add: eqvt_def) |
|
15 apply (intro allI) |
|
16 apply(simp add: permute_fun_def) |
|
17 apply(rule ext) |
|
18 apply(rule ext) |
|
19 apply(simp add: permute_bool_def) |
|
20 apply rule |
|
21 apply(drule_tac x="p" in meta_spec) |
|
22 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
23 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
24 apply simp |
|
25 apply(drule_tac x="-p" in meta_spec) |
|
26 apply(drule_tac x="x" in meta_spec) |
|
27 apply(drule_tac x="xa" in meta_spec) |
|
28 apply simp |
|
29 apply (erule addlam_pre_graph.induct) |
|
30 apply (simp_all add: addlam_pre_graph.intros) |
|
31 apply (simp_all add:lam.distinct) |
|
32 apply clarify |
|
33 apply simp |
|
34 apply (rule_tac y="a" in lam.exhaust) |
|
35 apply(auto simp add: lam.distinct lam.eq_iff) |
|
36 prefer 2 apply blast |
|
37 prefer 2 apply blast |
|
38 apply (rule_tac y="b" and c="name" in lam.strong_exhaust) |
|
39 apply(auto simp add: lam.distinct lam.eq_iff)[3] |
|
40 apply blast |
|
41 apply(drule_tac x="namea" in meta_spec) |
|
42 apply(drule_tac x="name" in meta_spec) |
|
43 apply(drule_tac x="lam" in meta_spec) |
|
44 apply (auto simp add: fresh_star_def atom_name_def fresh_at_base)[1] |
|
45 apply (auto simp add: lam.eq_iff Abs1_eq_iff fresh_def lam.supp supp_at_base) |
|
46 done |
|
47 |
|
48 termination |
|
49 by (relation "measure (\<lambda>(t,_). size t)") |
|
50 (simp_all add: lam.size) |
|
51 |
|
52 function |
|
53 addlam :: "lam \<Rightarrow> lam" |
|
54 where |
|
55 "addlam (Var x) = addlam_pre (Var x) (Lam [x]. (Var x))" |
|
56 | "addlam (App t1 t2) = App t1 t2" |
|
57 | "addlam (Lam [x]. t) = Lam [x].t" |
|
58 apply (simp_all add:lam.distinct) |
|
59 apply (rule_tac y="x" in lam.exhaust) |
|
60 apply auto |
|
61 apply (simp add:lam.eq_iff) |
|
62 done |
|
63 |
|
64 termination |
|
65 by (relation "measure (\<lambda>(t). size t)") |
|
66 (simp_all add: lam.size) |
|
67 |
|
68 lemma addlam': |
|
69 "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)" |
|
70 apply simp |
|
71 apply (subgoal_tac "Lam [x]. Var x = Lam [fv]. Var fv") |
|
72 apply simp |
|
73 apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base) |
|
74 done |
|
75 |
|
76 end |
|
77 |
|
78 |
|
79 |