71 lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] |
71 lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] |
72 |
72 |
73 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []), |
73 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []), |
74 build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *} |
74 build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *} |
75 thm alpha4_reflp |
75 thm alpha4_reflp |
|
76 ML build_equivps |
76 |
77 |
77 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), |
78 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), |
78 (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)) *} |
79 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{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)) *} |
79 lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] |
80 lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] |
80 |
81 |
81 (*lemma fv_rtrm4_rsp: |
82 (*lemma fv_rtrm4_rsp: |
82 "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya" |
83 "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya" |
83 "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y" |
84 "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y" |
92 trm4list = "rtrm4 list" / alpha_rtrm4_list*) |
93 trm4list = "rtrm4 list" / alpha_rtrm4_list*) |
93 by (simp_all add: alpha4_equivp) |
94 by (simp_all add: alpha4_equivp) |
94 |
95 |
95 local_setup {* |
96 local_setup {* |
96 (fn ctxt => ctxt |
97 (fn ctxt => ctxt |
97 |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4})) |
98 |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4})) |
98 |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4})) |
99 |> snd o (Quotient_Def.quotient_lift_const [] ("Ap4", @{term rAp4})) |
99 |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4}))) |
100 |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4}))) |
100 *} |
101 *} |
101 print_theorems |
102 print_theorems |
102 |
103 |
103 local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}] |
104 local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}] |
104 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *} |
105 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *} |