equal
deleted
inserted
replaced
1 theory Term4 |
1 theory Term4 |
2 imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove" |
2 imports "../NewAlpha" "../Abs" "../Perm" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove" |
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 ***} |
29 done |
29 done |
30 |
30 |
31 thm permute_rtrm4_permute_rtrm4_list.simps |
31 thm permute_rtrm4_permute_rtrm4_list.simps |
32 lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
32 lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
33 |
33 |
|
34 ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *} |
34 |
35 |
35 local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4") |
36 local_setup {* fn ctxt => let val (_, _, ctxt') = define_raw_fv descr sorts [] bl ctxt in ctxt' end *} |
36 [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *} |
37 thm fv_rtrm4.simps fv_rtrm4_list.simps |
37 print_theorems |
38 |
|
39 local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *} |
|
40 thm alpha_rtrm4_alpha_rtrm4_list.intros |
38 |
41 |
39 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" |
42 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" |
40 apply (rule ext)+ |
43 apply (rule ext)+ |
41 apply (induct_tac x xa rule: list_induct2') |
44 apply (induct_tac x xa rule: list_induct2') |
42 apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) |
45 apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) |
46 apply (erule alpha_rtrm4_list.cases) |
49 apply (erule alpha_rtrm4_list.cases) |
47 apply simp_all |
50 apply simp_all |
48 apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) |
51 apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) |
49 apply simp_all |
52 apply simp_all |
50 done |
53 done |
51 |
|
52 ML {* @{term "\<Union>a"} *} |
|
53 |
54 |
54 lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))" |
55 lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))" |
55 apply (rule ext) |
56 apply (rule ext) |
56 apply (induct_tac x) |
57 apply (induct_tac x) |
57 apply simp_all |
58 apply simp_all |
65 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (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)) *} |
66 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (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)) *} |
66 thm alpha4_inj |
67 thm alpha4_inj |
67 |
68 |
68 lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3] |
69 lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3] |
69 |
70 |
70 local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *} |
71 local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4.simps fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *} |
71 thm eqvts(1-2) |
72 thm eqvts(1-2) |
72 |
73 |
73 local_setup {* |
74 local_setup {* |
74 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), |
75 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), |
75 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} ctxt 1) ctxt) ctxt)) |
76 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} ctxt 1) ctxt) ctxt)) |
152 *} |
153 *} |
153 |
154 |
154 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} |
155 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} |
155 |
156 |
156 ML {* |
157 ML {* |
157 map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4_fv_rtrm4_list.simps[simplified fix3]} |
158 map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fix3] fv_rtrm4_list.simps[simplified fix3]} |
158 *} |
159 *} |
159 |
160 |
160 ML {* |
161 ML {* |
161 val liftd = |
162 val liftd = |
162 map (Local_Defs.unfold @{context} @{thms id_simps}) ( |
163 map (Local_Defs.unfold @{context} @{thms id_simps}) ( |