16 |
16 |
17 nominal_datatype lam = |
17 nominal_datatype lam = |
18 Var "name" |
18 Var "name" |
19 | App "lam" "lam" |
19 | App "lam" "lam" |
20 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
20 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
21 |
|
22 lemma |
|
23 "Lam [x]. Var x = Lam [y]. Var y" |
|
24 proof - |
|
25 obtain c::name where fresh: "atom c \<sharp> (Lam [x]. Var x, Lam [y]. Var y)" |
|
26 by (metis obtain_fresh) |
|
27 have "Lam [x]. Var x = (c \<leftrightarrow> x) \<bullet> Lam [x]. Var x" |
|
28 using fresh by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: fresh_Pair) |
|
29 also have "... = Lam [c].Var c" by simp |
|
30 also have "... = (c \<leftrightarrow> y) \<bullet> Lam [c]. Var c" |
|
31 using fresh by (rule_tac flip_fresh_fresh[symmetric]) (auto simp add: fresh_Pair) |
|
32 also have "... = Lam [y]. Var y" by simp |
|
33 finally show "Lam [x]. Var x = Lam [y]. Var y" . |
|
34 qed |
|
35 |
|
36 definition |
|
37 Name :: "nat \<Rightarrow> name" |
|
38 where |
|
39 "Name n = Abs_name (Atom (Sort ''name'' []) n)" |
|
40 |
|
41 definition |
|
42 "Ident2 = Lam [Name 1].(Var (Name 1))" |
|
43 |
|
44 definition |
|
45 "Ident x = Lam [x].(Var x)" |
|
46 |
|
47 lemma "Ident2 = Ident x" |
|
48 unfolding Ident_def Ident2_def |
|
49 by simp |
|
50 |
|
51 lemma "Ident x = Ident y" |
|
52 unfolding Ident_def |
|
53 by simp |
21 |
54 |
22 thm lam.strong_induct |
55 thm lam.strong_induct |
23 |
56 |
24 lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)" |
57 lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)" |
25 unfolding alpha_lam_raw_def |
58 unfolding alpha_lam_raw_def |
43 is_app :: "lam \<Rightarrow> bool" |
76 is_app :: "lam \<Rightarrow> bool" |
44 where |
77 where |
45 "is_app (Var x) = False" |
78 "is_app (Var x) = False" |
46 | "is_app (App t1 t2) = True" |
79 | "is_app (App t1 t2) = True" |
47 | "is_app (Lam [x]. t) = False" |
80 | "is_app (Lam [x]. t) = False" |
|
81 thm is_app_graph_def is_app_graph_aux_def |
48 apply(simp add: eqvt_def is_app_graph_aux_def) |
82 apply(simp add: eqvt_def is_app_graph_aux_def) |
49 apply(rule TrueI) |
83 apply(rule TrueI) |
50 apply(rule_tac y="x" in lam.exhaust) |
84 apply(rule_tac y="x" in lam.exhaust) |
51 apply(auto)[3] |
85 apply(auto)[3] |
52 apply(all_trivials) |
86 apply(all_trivials) |