18 | "rbv8 (Bar1 v x b) = {atom v}" |
18 | "rbv8 (Bar1 v x b) = {atom v}" |
19 |
19 |
20 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *} |
20 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *} |
21 print_theorems |
21 print_theorems |
22 |
22 |
23 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [ |
23 ML define_fv_alpha_export |
24 [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
24 local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term8.rfoo8") [ |
|
25 [[], [(SOME (@{term rbv8}, false), 0, 1, AlphaGen)]], [[], [(NONE, 1, 2, AlphaGen)]]] |
|
26 [(@{term "rbv8"}, 1, [[], [(0, NONE), (2, SOME @{term rbv8})]])] *} |
25 notation |
27 notation |
26 alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and |
28 alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and |
27 alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100) |
29 alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100) |
28 thm alpha_rfoo8_alpha_rbar8.intros |
30 thm alpha_rfoo8_alpha_rbar8_alpha_rbv8.intros[no_vars] |
29 |
31 thm fv_rbar8.simps fv_rfoo8_fv_rbv8.simps |
30 |
32 |
31 inductive |
33 inductive |
32 alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100) |
34 alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100) |
33 and |
35 and |
34 alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100) |
36 alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100) |
|
37 and |
|
38 alpha8bv:: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>bv _" [100, 100] 100) |
35 where |
39 where |
36 a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)" |
40 "name = namea \<Longrightarrow> Foo0 name \<approx>f Foo0 namea" |
37 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)" |
41 | "\<exists>pi. rbar8 \<approx>bv rbar8a \<and> |
38 | a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2" |
42 (rbv8 rbar8, rfoo8) \<approx>gen alpha8f fv_rfoo8 pi (rbv8 rbar8a, rfoo8a) \<Longrightarrow> |
39 | a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2" |
43 Foo1 rbar8 rfoo8 \<approx>f Foo1 rbar8a rfoo8a" |
|
44 | "name = namea \<Longrightarrow> Bar0 name \<approx>b Bar0 namea" |
|
45 | "\<exists>pi. name1 = name1a \<and> ({atom name2}, rbar8) \<approx>gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \<Longrightarrow> |
|
46 Bar1 name1 name2 rbar8 \<approx>b Bar1 name1a name2a rbar8a" |
|
47 | "name = namea \<Longrightarrow> alpha8bv (Bar0 name) (Bar0 namea)" |
|
48 | "({atom name2}, rbar8) \<approx>gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \<Longrightarrow> |
|
49 alpha8bv (Bar1 name1 name2 rbar8) (Bar1 name1a name2a rbar8a)" |
40 |
50 |
41 lemma "(alpha8b ===> op =) rbv8 rbv8" |
51 lemma "(alpha8b ===> op =) rbv8 rbv8" |
42 apply simp apply clarify |
52 apply rule |
43 apply (erule alpha8f_alpha8b.inducts(2)) |
53 apply (induct_tac a b rule: alpha8f_alpha8b_alpha8bv.inducts(2)) |
44 apply (simp_all) |
54 apply (simp_all) |
45 done |
55 done |
46 |
56 |
47 lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y" |
57 lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y" |
48 apply (erule alpha8f_alpha8b.inducts(2)) |
58 apply (erule alpha8f_alpha8b_alpha8bv.inducts(2)) |
49 apply (simp_all add: alpha_gen) |
59 apply (simp_all add: alpha_gen) |
50 done |
60 apply clarify |
|
61 sorry |
|
62 |
51 lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8" |
63 lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8" |
52 apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp) |
64 apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp) |
53 done |
65 done |
54 |
66 |
55 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" |
67 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" |
56 apply simp apply clarify |
68 apply simp apply clarify |
57 apply (erule alpha8f_alpha8b.inducts(1)) |
69 apply (erule alpha8f_alpha8b_alpha8bv.inducts(1)) |
58 apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) |
70 apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) |
|
71 |
59 done |
72 done |
60 |
73 |
61 end |
74 end |