31 |
31 |
32 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") |
32 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") |
33 [[[], [], [(NONE, 0,1)]], [[], []] ] *} |
33 [[[], [], [(NONE, 0,1)]], [[], []] ] *} |
34 print_theorems |
34 print_theorems |
35 |
35 |
|
36 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" |
|
37 apply (rule ext)+ |
|
38 apply (induct_tac x xa rule: list_induct2') |
|
39 apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) |
|
40 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
|
41 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
|
42 apply rule |
|
43 apply (erule alpha_rtrm4_list.cases) |
|
44 apply simp_all |
|
45 apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) |
|
46 apply simp_all |
|
47 done |
|
48 |
|
49 (* We need sth like: |
|
50 lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *) |
|
51 |
36 notation |
52 notation |
37 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
53 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
38 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
54 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
39 thm alpha_rtrm4_alpha_rtrm4_list.intros |
55 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] |
40 |
56 |
41 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (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)) *} |
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)) *} |
42 thm alpha4_inj |
58 thm alpha4_inj |
43 thm alpha_rtrm4_alpha_rtrm4_list.induct |
59 |
|
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 thm alpha4_inj_no |
44 |
62 |
45 local_setup {* |
63 local_setup {* |
46 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} |
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} |
47 *} |
65 *} |
48 print_theorems |
66 print_theorems |
49 |
67 |
50 local_setup {* |
68 local_setup {* |
51 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), |
69 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []), |
52 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) |
70 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) |
|
71 *} |
|
72 lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] |
|
73 |
|
74 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), |
|
75 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} |
|
76 lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] |
|
77 |
|
78 (*lemma fv_rtrm4_rsp: |
|
79 "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya" |
|
80 "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y" |
|
81 apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) |
|
82 apply (simp_all add: alpha_gen) |
|
83 done*) |
|
84 |
|
85 |
|
86 quotient_type |
|
87 trm4 = rtrm4 / alpha_rtrm4 |
|
88 (*and |
|
89 trm4list = "rtrm4 list" / alpha_rtrm4_list*) |
|
90 by (simp_all add: alpha4_equivp) |
|
91 |
|
92 local_setup {* |
|
93 (fn ctxt => ctxt |
|
94 |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4})) |
|
95 |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4})) |
|
96 |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4}))) |
53 *} |
97 *} |
54 print_theorems |
98 print_theorems |
55 |
99 |
56 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
100 local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}] |
57 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} |
101 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *} |
58 thm alpha4_equivp |
102 print_theorems |
59 |
103 |
60 quotient_type |
104 local_setup {* snd o prove_const_rsp @{binding rVr4_rsp} [@{term rVr4}] |
61 qrtrm4 = rtrm4 / alpha_rtrm4 and |
105 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} |
62 qrtrm4list = "rtrm4 list" / alpha_rtrm4_list |
106 lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" |
63 by (simp_all add: alpha4_equivp) |
107 apply simp |
|
108 apply clarify |
|
109 apply (simp add: alpha4_inj) |
|
110 |
|
111 |
|
112 local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}] |
|
113 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} |
|
114 local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp} |
|
115 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}, @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] |
|
116 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
|
117 |
|
118 thm rtrm4.induct |
|
119 lemmas trm1_bp_induct = rtrm4.induct[quot_lifted] |
64 |
120 |
65 end |
121 end |