|
1 theory Term7 |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 (* example with a respectful bn function defined over the type itself *) |
|
8 |
|
9 datatype rtrm7 = |
|
10 rVr7 "name" |
|
11 | rLm7 "name" "rtrm7" --"bind left in right" |
|
12 | rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)" |
|
13 |
|
14 primrec |
|
15 rbv7 |
|
16 where |
|
17 "rbv7 (rVr7 n) = {atom n}" |
|
18 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" |
|
19 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
|
20 |
|
21 setup {* snd o define_raw_perms ["rtrm7"] ["Term7.rtrm7"] *} |
|
22 thm permute_rtrm7.simps |
|
23 |
|
24 local_setup {* snd o define_fv_alpha "Term7.rtrm7" [ |
|
25 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} |
|
26 print_theorems |
|
27 notation |
|
28 alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100) |
|
29 thm alpha_rtrm7.intros |
|
30 thm fv_rtrm7.simps |
|
31 inductive |
|
32 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100) |
|
33 where |
|
34 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
|
35 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s" |
|
36 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2" |
|
37 |
|
38 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7" |
|
39 apply simp |
|
40 apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) |
|
41 apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) |
|
42 apply simp |
|
43 apply (rule a3) |
|
44 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
45 apply (simp_all add: alpha_gen fresh_star_def) |
|
46 apply (rule a1) |
|
47 apply (rule refl) |
|
48 done |
|
49 |
|
50 end |