114 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
114 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
115 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
115 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
116 apply(simp add: permute_eqvt[symmetric]) |
116 apply(simp add: permute_eqvt[symmetric]) |
117 done |
117 done |
118 |
118 |
119 ML {* |
119 |
120 fun reflp_tac induct inj = |
|
121 rtac induct THEN_ALL_NEW |
|
122 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
|
123 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
|
124 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
|
125 asm_full_simp_tac (HOL_ss addsimps |
|
126 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
|
127 *} |
|
128 |
120 |
129 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
121 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
130 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) |
122 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) |
131 |
123 |
132 ML {* |
|
133 fun symp_tac induct inj = |
|
134 rtac induct THEN_ALL_NEW |
|
135 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
|
136 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
|
137 (etac @{thm alpha_gen_compose_sym} THEN' |
|
138 eresolve_tac @{thms alpha1_eqvt}) |
|
139 *} |
|
140 |
|
141 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
124 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
142 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} 1 *}) |
125 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *}) |
143 |
126 |
144 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
127 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} |
145 apply (tactic {* |
128 by (tactic {* transp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *}) |
146 (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW |
|
147 (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN' |
|
148 eresolve_tac @{thms alpha_rtrm1.cases alpha_bp.cases}) THEN_ALL_NEW |
|
149 ( |
|
150 asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj rtrm1.distinct rtrm1.inject bp.distinct bp.inject}) THEN' |
|
151 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
|
152 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac @{thms alpha1_eqvt}]) |
|
153 ) |
|
154 ) 1 *}) |
|
155 done |
|
156 |
129 |
157 lemma helper: "(\<forall>x y z. R x y \<and> R y z \<longrightarrow> R x z) = (\<forall>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z))" |
130 lemma helper: "(\<forall>x y z. R x y \<and> R y z \<longrightarrow> R x z) = (\<forall>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z))" |
158 by meson |
131 by meson |
159 |
132 |
160 lemma alpha1_equivp: |
133 lemma alpha1_equivp: |
510 thm alpha_rtrm5_alpha_rlts.intros |
483 thm alpha_rtrm5_alpha_rlts.intros |
511 |
484 |
512 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} |
485 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} |
513 thm alpha5_inj |
486 thm alpha5_inj |
514 |
487 |
515 lemma alpha5_equivps: |
|
516 shows "equivp alpha_rtrm5" |
|
517 and "equivp alpha_rlts" |
|
518 sorry |
|
519 |
|
520 quotient_type |
|
521 trm5 = rtrm5 / alpha_rtrm5 |
|
522 and |
|
523 lts = rlts / alpha_rlts |
|
524 by (auto intro: alpha5_equivps) |
|
525 |
|
526 local_setup {* |
|
527 (fn ctxt => ctxt |
|
528 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) |
|
529 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) |
|
530 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
|
531 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
|
532 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
|
533 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
|
534 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
|
535 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) |
|
536 *} |
|
537 print_theorems |
|
538 |
|
539 lemma rbv5_eqvt: |
488 lemma rbv5_eqvt: |
540 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
489 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
541 sorry |
490 sorry |
542 |
491 |
543 lemma fv_rtrm5_eqvt: |
492 lemma fv_rtrm5_eqvt: |
575 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
524 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
576 apply (subst permute_eqvt[symmetric]) |
525 apply (subst permute_eqvt[symmetric]) |
577 apply (simp) |
526 apply (simp) |
578 done |
527 done |
579 |
528 |
|
529 prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *} |
|
530 by (tactic {* reflp_tac @{thm rtrm5_rlts.induct} @{thms alpha5_inj} 1 *}) |
|
531 |
|
532 prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *} |
|
533 by (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} 1 *}) |
|
534 |
|
535 prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *} |
|
536 by (tactic {* transp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms rtrm5.inject rlts.inject} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} 1 *}) |
|
537 |
|
538 lemma alpha5_equivps: |
|
539 shows "equivp alpha_rtrm5" |
|
540 and "equivp alpha_rlts" |
|
541 ML_prf Goal.prove |
|
542 unfolding equivp_reflp_symp_transp reflp_def |
|
543 apply (simp_all add: alpha5_reflp_aux) |
|
544 unfolding symp_def |
|
545 apply (simp_all add: alpha5_symp_aux) |
|
546 unfolding transp_def |
|
547 apply (simp_all only: helper) |
|
548 apply (rule allI)+ |
|
549 apply (rule conjunct1[OF alpha5_transp_aux]) |
|
550 apply (rule allI)+ |
|
551 apply (rule conjunct2[OF alpha5_transp_aux]) |
|
552 done |
|
553 |
|
554 quotient_type |
|
555 trm5 = rtrm5 / alpha_rtrm5 |
|
556 and |
|
557 lts = rlts / alpha_rlts |
|
558 by (auto intro: alpha5_equivps) |
|
559 |
|
560 local_setup {* |
|
561 (fn ctxt => ctxt |
|
562 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) |
|
563 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) |
|
564 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
|
565 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
|
566 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
|
567 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
|
568 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
|
569 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) |
|
570 *} |
|
571 print_theorems |
|
572 |
580 lemma alpha5_rfv: |
573 lemma alpha5_rfv: |
581 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
574 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
582 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
575 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
583 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
576 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
584 apply(simp_all add: alpha_gen) |
577 apply(simp_all add: alpha_gen) |