# HG changeset patch # User Cezary Kaliszyk # Date 1266913919 -3600 # Node ID 74e2b9b95adde9002c94dbf376ab6708df18dc24 # Parent 06ace3a1eedd9658b76cb9ee23b4a3705597503e Fixes for auxiliary datatypes. diff -r 06ace3a1eedd -r 74e2b9b95add Quot/Nominal/Fv.thy --- a/Quot/Nominal/Fv.thy Mon Feb 22 18:09:44 2010 +0100 +++ b/Quot/Nominal/Fv.thy Tue Feb 23 09:31:59 2010 +0100 @@ -295,10 +295,32 @@ *} ML {* -fun transp_tac induct alpha_inj term_inj distinct cases eqvt = - ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW - (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN' - eresolve_tac cases) THEN_ALL_NEW +fun imp_elim_tac case_rules = + Subgoal.FOCUS (fn {concl, context, ...} => + case term_of concl of + _ $ (_ $ asm $ _) => + let + fun filter_fn case_rule = ( + case Logic.strip_assums_hyp (prop_of case_rule) of + ((_ $ asmc) :: _) => + let + val thy = ProofContext.theory_of context + in + Pattern.matches thy (asmc, asm) + end + | _ => false) + val matching_rules = filter filter_fn case_rules + in + (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1 + end + | _ => no_tac + ) +*} + +ML {* +fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = + ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW + (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW ( asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW @@ -328,7 +350,7 @@ val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1; fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; - fun transp_tac' _ = transp_tac alpha_induct alpha_inj term_inj distinct cases eqvt 1; + fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; val symt = Goal.prove ctxt' [] [] symg symp_tac'; val transt = Goal.prove ctxt' [] [] transg transp_tac'; @@ -349,4 +371,29 @@ end *} +(* +Tests: +prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} +by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) + +prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} +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}] ("x","y","z")) *} +by (tactic {* transp_tac @{context} @{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 alpha1_equivp: + "equivp alpha_rtrm1" + "equivp alpha_bp" +apply (tactic {* + (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) + THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' + resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux}) + THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' + resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux} + THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) +) +1 *}) +done*) + end diff -r 06ace3a1eedd -r 74e2b9b95add Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Mon Feb 22 18:09:44 2010 +0100 +++ b/Quot/Nominal/Terms.thy Tue Feb 23 09:31:59 2010 +0100 @@ -120,29 +120,6 @@ (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} thm alpha1_equivp -(*prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} -by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) - -prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} -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}] ("x","y","z")) *} -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 alpha1_equivp: - "equivp alpha_rtrm1" - "equivp alpha_bp" -apply (tactic {* - (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) - THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' - resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux}) - THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' - resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux} - THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) -) -1 *}) -done*) - quotient_type trm1 = rtrm1 / alpha_rtrm1 by (rule alpha1_equivp(1)) @@ -227,12 +204,8 @@ lemma bp_supp: "finite (supp (bp :: bp))" apply (induct bp) apply(simp_all add: supp_def) - apply (fold supp_def) - apply (simp add: supp_at_base) - apply(simp add: Collect_imp_eq) - apply(simp add: Collect_neg_eq[symmetric]) - apply (fold supp_def) - apply (simp) + apply(simp add: supp_at_base supp_def[symmetric]) + apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric] supp_def) done instance trm1 :: fs @@ -459,24 +432,14 @@ "a \4l b \ (pi \ a) \4l (pi \ b)" sorry -(* -prove alpha4_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] ("x","y","z")) *} -apply (tactic {* -transp_tac @{thm rtrm4.induct} @{thms alpha4_inj} @{thms rtrm4.inject list.inject} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha1_eqvt} 1 *}) local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), - (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 list.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} -*) - - - - -lemma alpha4_equivp: "equivp alpha_rtrm4" sorry -lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry + (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)) *} +thm alpha4_equivp quotient_type qrtrm4 = rtrm4 / alpha_rtrm4 and qrtrm4list = "rtrm4 list" / alpha_rtrm4_list - by (simp_all add: alpha4_equivp alpha4list_equivp) + by (simp_all add: alpha4_equivp) datatype rtrm5 =