equal
deleted
inserted
replaced
2 imports |
2 imports |
3 "../Nominal2" |
3 "../Nominal2" |
4 "~~/src/HOL/Library/Monad_Syntax" |
4 "~~/src/HOL/Library/Monad_Syntax" |
5 begin |
5 begin |
6 |
6 |
|
7 lemma perm_commute: |
|
8 "a \<sharp> p \<Longrightarrow> a' \<sharp> p \<Longrightarrow> (a \<rightleftharpoons> a') + p = p + (a \<rightleftharpoons> a')" |
|
9 apply(rule plus_perm_eq) |
|
10 apply(simp add: supp_swap fresh_def) |
|
11 done |
7 |
12 |
8 atom_decl name |
13 atom_decl name |
9 |
14 |
10 ML {* trace := true *} |
15 ML {* trace := true *} |
11 |
16 |
12 nominal_datatype lam = |
17 nominal_datatype lam = |
13 Var "name" |
18 Var "name" |
14 | App "lam" "lam" |
19 | App "lam" "lam" |
15 | 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 thm lam.strong_induct |
16 |
23 |
17 lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)" |
24 lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)" |
18 unfolding alpha_lam_raw_def |
25 unfolding alpha_lam_raw_def |
19 by perm_simp rule |
26 by perm_simp rule |
20 |
27 |
375 equivariance beta |
382 equivariance beta |
376 |
383 |
377 nominal_inductive beta |
384 nominal_inductive beta |
378 avoids b4: "x" |
385 avoids b4: "x" |
379 by (simp_all add: fresh_star_def fresh_Pair fresh_fact) |
386 by (simp_all add: fresh_star_def fresh_Pair fresh_fact) |
|
387 |
|
388 thm beta.strong_induct |
380 |
389 |
381 text {* One-Reduction *} |
390 text {* One-Reduction *} |
382 |
391 |
383 inductive |
392 inductive |
384 One :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>1 _" [80,80] 80) |
393 One :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>1 _" [80,80] 80) |