equal
deleted
inserted
replaced
1 theory Term4 |
1 theory Term4 |
2 imports "../Abs" "../Perm" "../Fv" "../Rsp" "Quotient_List" |
2 imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 section {*** lam with indirect list recursion ***} |
7 section {*** lam with indirect list recursion ***} |
27 done |
27 done |
28 |
28 |
29 thm permute_rtrm4_permute_rtrm4_list.simps |
29 thm permute_rtrm4_permute_rtrm4_list.simps |
30 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
30 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
31 |
31 |
32 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") |
32 ML define_fv_alpha_export |
33 [[[], [], [(NONE, 0,1)]], [[], []] ] *} |
33 local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4") |
|
34 [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *} |
34 print_theorems |
35 print_theorems |
35 |
36 |
36 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" |
37 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" |
37 apply (rule ext)+ |
38 apply (rule ext)+ |
38 apply (induct_tac x xa rule: list_induct2') |
39 apply (induct_tac x xa rule: list_induct2') |
52 notation |
53 notation |
53 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
54 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
54 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
55 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
55 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] |
56 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] |
56 |
57 |
57 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} |
58 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} |
58 thm alpha4_inj |
59 thm alpha4_inj |
59 |
60 |
60 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
61 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
61 thm alpha4_inj_no |
62 thm alpha4_inj_no |
62 |
63 |
63 local_setup {* |
64 local_setup {* |
64 snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct} |
65 snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct} |
65 *} |
66 *} |