# HG changeset patch # User Cezary Kaliszyk # Date 1266855568 -3600 # Node ID aec9576b39505da5c81ddea73931ac494e2edede # Parent 0f92257edeee2249998694914650da7fac084751 Testing auto equivp code. diff -r 0f92257edeee -r aec9576b3950 Quot/Nominal/Fv.thy --- a/Quot/Nominal/Fv.thy Mon Feb 22 16:44:58 2010 +0100 +++ b/Quot/Nominal/Fv.thy Mon Feb 22 17:19:28 2010 +0100 @@ -288,7 +288,7 @@ ML {* fun symp_tac induct inj eqvt = - rtac induct THEN_ALL_NEW + ((rtac @{thm impI} THEN' etac induct) ORELSE' 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 eqvt) @@ -296,7 +296,7 @@ ML {* fun transp_tac induct alpha_inj term_inj distinct cases eqvt = - rtac induct THEN_ALL_NEW + ((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 ( @@ -306,6 +306,21 @@ ) *} +lemma transp_aux: + "(\xa ya. R xa ya \ (\z. R ya z \ R xa z)) \ transp R" + unfolding transp_def + by blast + +ML {* +fun equivp_tac reflps symps transps = + 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 reflps THEN' + rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' + resolve_tac symps THEN' + rtac @{thm transp_aux} THEN' resolve_tac transps +*} + ML {* fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = let @@ -318,12 +333,19 @@ val symt = Goal.prove ctxt' [] [] symg symp_tac'; val transt = Goal.prove ctxt' [] [] transg transp_tac'; val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] + val reflts = HOLogic.conj_elims refltg + val symts = HOLogic.conj_elims symtg + val transts = HOLogic.conj_elims transtg fun equivp alpha = let - val goal = @{term Trueprop} $ (@{term equivp} $ alpha) - val tac = + val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) + val goal = @{term Trueprop} $ (equivp $ alpha) + fun tac _ = equivp_tac reflts symts transts 1 + in + Goal.prove ctxt [] [] goal tac + end in - (refltg, symtg, transtg) + map equivp alphas end *} diff -r 0f92257edeee -r aec9576b3950 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Mon Feb 22 16:44:58 2010 +0100 +++ b/Quot/Nominal/Terms.thy Mon Feb 22 17:19:28 2010 +0100 @@ -116,12 +116,11 @@ apply(simp add: permute_eqvt[symmetric]) done -ML {* -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} @{context} -*} -ML Variable.export +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), + (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")) *} +(*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")) *} @@ -130,11 +129,6 @@ 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 transp_aux: - "(\xa ya. R xa ya \ (\z. R ya z \ R xa z)) \ transp R" - unfolding transp_def - by blast - lemma alpha1_equivp: "equivp alpha_rtrm1" "equivp alpha_bp" @@ -147,7 +141,7 @@ THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) ) 1 *}) -done +done*) quotient_type trm1 = rtrm1 / alpha_rtrm1 by (rule alpha1_equivp(1)) @@ -345,17 +339,21 @@ local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *} thm alpha2_inj +lemma alpha2_eqvt: + "t \2 s \ (pi \ t) \2 (pi \ s)" + "a \2b b \ (pi \ a) \2b (pi \ b)" +sorry -lemma alpha2_equivp: - "equivp alpha_rtrm2" - "equivp alpha_rassign" - sorry +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []), + (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *} +thm alpha2_equivp + quotient_type trm2 = rtrm2 / alpha_rtrm2 and assign = rassign / alpha_rassign - by (auto intro: alpha2_equivp) + by (rule alpha2_equivp(1)) (rule alpha2_equivp(2)) local_setup {* (fn ctxt => ctxt @@ -400,16 +398,23 @@ alpha_rassigns ("_ \3a _" [100, 100] 100) thm alpha_rtrm3_alpha_rassigns.intros -lemma alpha3_equivp: - "equivp alpha_rtrm3" - "equivp alpha_rassigns" - sorry +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *} +thm alpha3_inj + +lemma alpha3_eqvt: + "t \3 s \ (pi \ t) \3 (pi \ s)" + "a \3a b \ (pi \ a) \3a (pi \ b)" +sorry + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []), + (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *} +thm alpha3_equivp quotient_type trm3 = rtrm3 / alpha_rtrm3 and assigns = rassigns / alpha_rassigns - by (auto intro: alpha3_equivp) + by (rule alpha3_equivp(1)) (rule alpha3_equivp(2)) section {*** lam with indirect list recursion ***} @@ -418,6 +423,7 @@ rVr4 "name" | rAp4 "rtrm4" "rtrm4 list" | rLm4 "name" "rtrm4" --"bind (name) in (trm)" +print_theorems thm rtrm4.recs @@ -445,6 +451,17 @@ alpha_rtrm4_list ("_ \4l _" [100, 100] 100) thm alpha_rtrm4_alpha_rtrm4_list.intros +(*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} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} *) + +lemma alpha4_eqvt: + "t \4 s \ (pi \ t) \4 (pi \ s)" + "a \4l b \ (pi \ a) \4l (pi \ b)" +sorry + +(*local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), + (build_equivps [@{term alpha_rtrm4}, @{term alpha_rassigns}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject rassigns.inject} @{thms alpha4_inj} @{thms rtrm4.distinct rassigns.distinct} @{thms alpha_rtrm4.cases alpha_rassigns.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}*) + + lemma alpha4_equivp: "equivp alpha_rtrm4" sorry lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry @@ -530,36 +547,15 @@ apply (simp) done -prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *} -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}] ("x","y","z")) *} -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}] ("x","y","z")) *} -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 +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), + (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *} +thm alpha5_equivp quotient_type trm5 = rtrm5 / alpha_rtrm5 and lts = rlts / alpha_rlts - by (auto intro: alpha5_equivps) + by (auto intro: alpha5_equivp) local_setup {* (fn ctxt => ctxt @@ -730,13 +726,17 @@ local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} thm alpha6_inj -lemma alpha6_equivps: - shows "equivp alpha6" +lemma alpha6_eqvt: + "xa \6 y \ (x \ xa) \6 (x \ y)" sorry +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), + (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} +thm alpha6_equivp + quotient_type trm6 = rtrm6 / alpha_rtrm6 - by (auto intro: alpha6_equivps) + by (auto intro: alpha6_equivp) local_setup {* (fn ctxt => ctxt @@ -750,8 +750,7 @@ lemma [quot_respect]: "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute" -apply auto (* will work with eqvt *) -sorry +by (auto simp add: alpha6_eqvt) (* Definitely not true , see lemma below *) lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6"