diff -r 5a60977f932b -r 43bd70786f9f Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Mon Feb 22 15:41:30 2010 +0100 +++ b/Quot/Nominal/Terms.thy Mon Feb 22 16:16:04 2010 +0100 @@ -116,43 +116,16 @@ apply(simp add: permute_eqvt[symmetric]) done -ML {* -fun reflp_tac induct inj = - rtac induct THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW - TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW - (rtac @{thm exI[of _ "0 :: perm"]} THEN' - asm_full_simp_tac (HOL_ss addsimps - @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) -*} + prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) -ML {* -fun symp_tac induct inj = - rtac induct THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW - TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_sym} THEN' - eresolve_tac @{thms alpha1_eqvt}) -*} - prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} -by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} 1 *}) +by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *}) prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *} -apply (tactic {* - (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW - (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN' - eresolve_tac @{thms alpha_rtrm1.cases alpha_bp.cases}) THEN_ALL_NEW - ( - asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj rtrm1.distinct rtrm1.inject bp.distinct bp.inject}) THEN' - TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac @{thms alpha1_eqvt}]) - ) -) 1 *}) -done +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 *}) lemma helper: "(\x y z. R x y \ R y z \ R x z) = (\xa ya. R xa ya \ (\z. R ya z \ R xa z))" by meson @@ -512,30 +485,6 @@ 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)) *} thm alpha5_inj -lemma alpha5_equivps: - shows "equivp alpha_rtrm5" - and "equivp alpha_rlts" -sorry - -quotient_type - trm5 = rtrm5 / alpha_rtrm5 -and - lts = rlts / alpha_rlts - by (auto intro: alpha5_equivps) - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) - |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) - |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) - |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) - |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) - |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) -*} -print_theorems - lemma rbv5_eqvt: "pi \ (rbv5 x) = rbv5 (pi \ x)" sorry @@ -577,6 +526,50 @@ apply (simp) done +prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *} +by (tactic {* reflp_tac @{thm rtrm5_rlts.induct} @{thms alpha5_inj} 1 *}) + +prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *} +by (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} 1 *}) + +prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *} +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 *}) + +lemma alpha5_equivps: + shows "equivp alpha_rtrm5" + and "equivp alpha_rlts" +ML_prf Goal.prove +unfolding equivp_reflp_symp_transp reflp_def +apply (simp_all add: alpha5_reflp_aux) +unfolding symp_def +apply (simp_all add: alpha5_symp_aux) +unfolding transp_def +apply (simp_all only: helper) +apply (rule allI)+ +apply (rule conjunct1[OF alpha5_transp_aux]) +apply (rule allI)+ +apply (rule conjunct2[OF alpha5_transp_aux]) +done + +quotient_type + trm5 = rtrm5 / alpha_rtrm5 +and + lts = rlts / alpha_rlts + by (auto intro: alpha5_equivps) + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) + |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) + |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) + |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) + |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) + |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) +*} +print_theorems + lemma alpha5_rfv: "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" "(l \l m \ fv_rlts l = fv_rlts m)"