# HG changeset patch # User Christian Urban # Date 1266928381 -3600 # Node ID 20f76fde8ef177c7878d1923f54adab2e51ebfac # Parent 160343d86a6ff671ce8c31b5bfba08d2ca2b33e6# Parent 0d059450a3fa40c8bd457b5ed9fdd88fdebe2dd3 merged diff -r 160343d86a6f -r 20f76fde8ef1 FIXME-TODO --- a/FIXME-TODO Tue Feb 23 13:32:35 2010 +0100 +++ b/FIXME-TODO Tue Feb 23 13:33:01 2010 +0100 @@ -8,8 +8,13 @@ Higher Priority =============== -- Ask Markus how the files Quot* should be named. - (There is a HOL/Library/Quotient.thy --- seems to be an example. *) + +- Also, in the interest of making nicer generated documentation, you + might want to change all your "section" headings in Quotient.thy to + "subsection", and add a "header" statement to the top of the file. + Otherwise, each "section" gets its own chapter in the generated pdf, + when the rest of HOL has one chapter per theory file (the chapter + title comes from the "header" statement). - If the constant definition gives the wrong definition term, one gets a cryptic message about absrep_fun @@ -21,7 +26,6 @@ - The user should be able to give quotient_respects and preserves theorems in a more natural form. - Lower Priority ============== @@ -60,3 +64,6 @@ That means "qconst :: qty" is not read as a term, but as two entities. + +- Restrict automatic translation to particular quotient types + diff -r 160343d86a6f -r 20f76fde8ef1 Quot/Nominal/Abs.thy --- a/Quot/Nominal/Abs.thy Tue Feb 23 13:32:35 2010 +0100 +++ b/Quot/Nominal/Abs.thy Tue Feb 23 13:33:01 2010 +0100 @@ -74,11 +74,11 @@ apply(clarsimp) done -(* introduced for examples *) -lemma alpha_gen_atom_sym: - assumes a: "\pi t s. (R t s \ R (pi \ t) (pi \ s))" - shows "\pi. ({atom a}, t) \gen (\x1 x2. R x1 x2 \ R x2 x1) f pi ({atom b}, s) \ - \pi. ({atom b}, s) \gen R f pi ({atom a}, t)" +lemma alpha_gen_compose_sym: + assumes b: "\pi. (aa, t) \gen (\x1 x2. R x1 x2 \ R x2 x1) f pi (ab, s)" + and a: "\pi t s. (R t s \ R (pi \ t) (pi \ s))" + shows "\pi. (ab, s) \gen R f pi (aa, t)" + using b apply - apply(erule exE) apply(rule_tac x="- pi" in exI) apply(simp add: alpha_gen.simps) @@ -91,11 +91,12 @@ apply assumption done -lemma alpha_gen_atom_trans: - assumes a: "\pi t s. (R t s \ R (pi \ t) (pi \ s))" - shows "\\pi\perm. ({atom a}, t) \gen (\x1 x2. R x1 x2 \ (\x. R x2 x \ R x1 x)) f pi ({atom aa}, ta); - \pi\perm. ({atom aa}, ta) \gen R f pi ({atom ba}, sa)\ - \ \pi\perm. ({atom a}, t) \gen R f pi ({atom ba}, sa)" +lemma alpha_gen_compose_trans: + assumes b: "\pi\perm. (aa, t) \gen (\x1 x2. R x1 x2 \ (\x. R x2 x \ R x1 x)) f pi (ab, ta)" + and c: "\pi\perm. (ab, ta) \gen R f pi (ac, sa)" + and a: "\pi t s. (R t s \ R (pi \ t) (pi \ s))" + shows "\pi\perm. (aa, t) \gen R f pi (ac, sa)" + using b c apply - apply(simp add: alpha_gen.simps) apply(erule conjE)+ apply(erule exE)+ diff -r 160343d86a6f -r 20f76fde8ef1 Quot/Nominal/Fv.thy --- a/Quot/Nominal/Fv.thy Tue Feb 23 13:32:35 2010 +0100 +++ b/Quot/Nominal/Fv.thy Tue Feb 23 13:33:01 2010 +0100 @@ -90,6 +90,7 @@ *} +(* TODO: Notice datatypes without bindings and replace alpha with equality *) ML {* (* Currently needs just one full_tname to access Datatype *) fun define_fv_alpha full_tname bindsall lthy = @@ -219,11 +220,11 @@ ML {* fun alpha_inj_tac dist_inj intrs elims = SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' - rtac @{thm iffI} THEN' RANGE [ + (rtac @{thm iffI} THEN' RANGE [ (eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj) ), - (asm_full_simp_tac (HOL_ss addsimps intrs))] + asm_full_simp_tac (HOL_ss addsimps intrs)]) *} ML {* @@ -251,4 +252,148 @@ end *} +ML {* +fun build_alpha_refl_gl alphas (x, y, z) = +let + fun build_alpha alpha = + let + val ty = domain_type (fastype_of alpha); + val var = Free(x, ty); + val var2 = Free(y, ty); + val var3 = Free(z, ty); + val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); + val transp = HOLogic.mk_imp (alpha $ var $ var2, + HOLogic.mk_all (z, ty, + HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) + in + ((alpha $ var $ var), (symp, transp)) + end; + val (refl_eqs, eqs) = split_list (map build_alpha alphas) + val (sym_eqs, trans_eqs) = split_list eqs + fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l +in + (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) end +*} + +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 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})) +*} + +ML {* +fun symp_tac induct inj eqvt = + ((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 conjI) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) +*} + +ML {* +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 conjI) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) + ) +*} + +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 conjI THEN' rtac allI THEN' + resolve_tac reflps THEN' + rtac conjI THEN' rtac allI THEN' rtac 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 + val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; + 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 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'; + 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 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 + map equivp alphas +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 160343d86a6f -r 20f76fde8ef1 Quot/Nominal/LFex.thy --- a/Quot/Nominal/LFex.thy Tue Feb 23 13:32:35 2010 +0100 +++ b/Quot/Nominal/LFex.thy Tue Feb 23 13:33:01 2010 +0100 @@ -1,5 +1,5 @@ theory LFex -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" begin atom_decl name @@ -18,21 +18,6 @@ | App "trm" "trm" | Lam "ty" "name" "trm" -primrec - rfv_kind :: "kind \ atom set" -and rfv_ty :: "ty \ atom set" -and rfv_trm :: "trm \ atom set" -where - "rfv_kind (Type) = {}" -| "rfv_kind (KPi A x K) = (rfv_ty A) \ ((rfv_kind K) - {atom x})" -| "rfv_ty (TConst i) = {atom i}" -| "rfv_ty (TApp A M) = (rfv_ty A) \ (rfv_trm M)" -| "rfv_ty (TPi A x B) = (rfv_ty A) \ ((rfv_ty B) - {atom x})" -| "rfv_trm (Const i) = {atom i}" -| "rfv_trm (Var x) = {atom x}" -| "rfv_trm (App M N) = (rfv_trm M) \ (rfv_trm N)" -| "rfv_trm (Lam A x M) = (rfv_ty A) \ ((rfv_trm M) - {atom x})" - instantiation kind and ty and trm :: pt begin @@ -74,6 +59,52 @@ end +(* +setup {* snd o define_raw_perms ["kind", "ty", "trm"] ["LFex.kind", "LFex.ty", "LFex.trm"] *} +local_setup {* + snd o define_fv_alpha "LFex.kind" + [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], + [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], + [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} +notation + alpha_kind ("_ \ki _" [100, 100] 100) +and alpha_ty ("_ \ty _" [100, 100] 100) +and alpha_trm ("_ \tr _" [100, 100] 100) +thm fv_kind_fv_ty_fv_trm.simps alpha_kind_alpha_ty_alpha_trm.intros +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_kind_alpha_ty_alpha_trm.intros} @{thms kind.distinct ty.distinct trm.distinct kind.inject ty.inject trm.inject} @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} ctxt)) ctxt)) *} +thm alphas_inj + +lemma alphas_eqvt: + "t1 \ki s1 \ (pi \ t1) \ki (pi \ s1)" + "t2 \ty s2 \ (pi \ t2) \ty (pi \ s2)" + "t3 \tr s3 \ (pi \ t3) \tr (pi \ s3)" +sorry + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []), + (build_equivps [@{term alpha_kind}, @{term alpha_ty}, @{term alpha_trm}] + @{thm kind_ty_trm.induct} @{thm alpha_kind_alpha_ty_alpha_trm.induct} + @{thms kind.inject ty.inject trm.inject} @{thms alphas_inj} + @{thms kind.distinct ty.distinct trm.distinct} + @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} + @{thms alphas_eqvt} ctxt)) ctxt)) *} +thm alphas_equivp +*) + +primrec + rfv_kind :: "kind \ atom set" +and rfv_ty :: "ty \ atom set" +and rfv_trm :: "trm \ atom set" +where + "rfv_kind (Type) = {}" +| "rfv_kind (KPi A x K) = (rfv_ty A) \ ((rfv_kind K) - {atom x})" +| "rfv_ty (TConst i) = {atom i}" +| "rfv_ty (TApp A M) = (rfv_ty A) \ (rfv_trm M)" +| "rfv_ty (TPi A x B) = (rfv_ty A) \ ((rfv_ty B) - {atom x})" +| "rfv_trm (Const i) = {atom i}" +| "rfv_trm (Var x) = {atom x}" +| "rfv_trm (App M N) = (rfv_trm M) \ (rfv_trm N)" +| "rfv_trm (Lam A x M) = (rfv_ty A) \ ((rfv_trm M) - {atom x})" + inductive akind :: "kind \ kind \ bool" ("_ \ki _" [100, 100] 100) and aty :: "ty \ ty \ bool" ("_ \ty _" [100, 100] 100) @@ -185,15 +216,12 @@ apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts) apply(simp_all add: akind_aty_atrm.intros) apply (simp_all add: akind_aty_atrm_inj) - apply(rule alpha_gen_atom_sym) - apply(rule alpha_eqvt) - apply(assumption)+ - apply(rule alpha_gen_atom_sym) - apply(rule alpha_eqvt) - apply(assumption)+ - apply(rule alpha_gen_atom_sym) - apply(rule alpha_eqvt) - apply(assumption)+ + apply(erule alpha_gen_compose_sym) + apply(erule alpha_eqvt) + apply(erule alpha_gen_compose_sym) + apply(erule alpha_eqvt) + apply(erule alpha_gen_compose_sym) + apply(erule alpha_eqvt) done lemma al_trans: @@ -206,9 +234,9 @@ apply(erule akind.cases) apply(simp_all add: akind_aty_atrm.intros) apply(simp add: akind_aty_atrm_inj) - apply(rule alpha_gen_atom_trans) - apply(rule alpha_eqvt) - apply(assumption)+ + apply(erule alpha_gen_compose_trans) + apply(assumption) + apply(erule alpha_eqvt) apply(rotate_tac 4) apply(erule aty.cases) apply(simp_all add: akind_aty_atrm.intros) @@ -216,9 +244,9 @@ apply(erule aty.cases) apply(simp_all add: akind_aty_atrm.intros) apply(simp add: akind_aty_atrm_inj) - apply(rule alpha_gen_atom_trans) - apply(rule alpha_eqvt) - apply(assumption)+ + apply(erule alpha_gen_compose_trans) + apply(assumption) + apply(erule alpha_eqvt) apply(rotate_tac 4) apply(erule atrm.cases) apply(simp_all add: akind_aty_atrm.intros) @@ -226,9 +254,9 @@ apply(erule atrm.cases) apply(simp_all add: akind_aty_atrm.intros) apply(simp add: akind_aty_atrm_inj) - apply(rule alpha_gen_atom_trans) - apply(rule alpha_eqvt) - apply(assumption)+ + apply(erule alpha_gen_compose_trans) + apply(assumption) + apply(erule alpha_eqvt) done lemma alpha_equivps: diff -r 160343d86a6f -r 20f76fde8ef1 Quot/Nominal/LamEx2.thy --- a/Quot/Nominal/LamEx2.thy Tue Feb 23 13:32:35 2010 +0100 +++ b/Quot/Nominal/LamEx2.thy Tue Feb 23 13:33:01 2010 +0100 @@ -137,9 +137,8 @@ apply(simp add: a1) apply(simp add: a2) apply(rule a3) - apply(rule alpha_gen_atom_sym) - apply(rule alpha_eqvt) - apply(assumption)+ + apply(erule alpha_gen_compose_sym) + apply(erule alpha_eqvt) done lemma alpha_trans: @@ -152,9 +151,9 @@ apply(erule alpha.cases) apply(simp_all) apply(rule a3) -apply(rule alpha_gen_atom_trans) -apply(rule alpha_eqvt) -apply(assumption)+ +apply(erule alpha_gen_compose_trans) +apply(assumption) +apply(erule alpha_eqvt) done lemma alpha_equivp: diff -r 160343d86a6f -r 20f76fde8ef1 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Tue Feb 23 13:32:35 2010 +0100 +++ b/Quot/Nominal/Terms.thy Tue Feb 23 13:33:01 2010 +0100 @@ -116,11 +116,24 @@ apply(simp add: permute_eqvt[symmetric]) done -lemma alpha1_equivp: "equivp alpha_rtrm1" - sorry +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 -quotient_type trm1 = rtrm1 / alpha_rtrm1 - by (rule alpha1_equivp) +ML {* +fun define_quotient_type args tac ctxt = +let + val mthd = Method.SIMPLE_METHOD tac + val mthdt = Method.Basic (fn _ => mthd) + val bymt = Proof.global_terminal_proof (mthdt, NONE) +in + bymt (Quotient_Type.quotient_type args ctxt) +end +*} + +local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] + (rtac @{thm alpha1_equivp(1)} 1) +*} local_setup {* (fn ctxt => ctxt @@ -132,29 +145,44 @@ *} print_theorems -lemma alpha_rfv1: - shows "t \1 s \ fv_rtrm1 t = fv_rtrm1 s" - apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) - apply(simp_all add: alpha_gen.simps alpha_bp_eq) - done +prove fv_rtrm1_rsp': {* + (@{term Trueprop} $ (Quotient_Term.equiv_relation_chk @{context} (fastype_of @{term fv_rtrm1}, fastype_of @{term fv_trm1}) $ @{term fv_rtrm1} $ @{term fv_rtrm1})) *} +by (tactic {* + (rtac @{thm fun_rel_id} THEN' + eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fv_rtrm1_fv_bp.simps})) 1 *}) + + +lemmas fv_rtrm1_rsp = apply_rsp'[OF fv_rtrm1_rsp'] + +(* We need this since 'prove' doesn't support attributes *) +lemma [quot_respect]: "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1" + by (rule fv_rtrm1_rsp') + +ML {* +fun contr_rsp_tac inj rsp equivps = +let + val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps +in + REPEAT o rtac @{thm fun_rel_id} THEN' + simp_tac (HOL_ss addsimps inj) THEN' + (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW + (asm_simp_tac HOL_ss THEN_ALL_NEW ( + rtac @{thm exI[of _ "0 :: perm"]} THEN' + asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ + @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) + )) +end +*} lemma [quot_respect]: "(op = ===> alpha_rtrm1) rVr1 rVr1" "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" -apply (auto simp add: alpha1_inj alpha_bp_eq) -apply (rule_tac [!] x="0" in exI) -apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq) +apply (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})+ done -lemma [quot_respect]: - "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute" - by (simp add: alpha1_eqvt) - -lemma [quot_respect]: - "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1" - by (simp add: alpha_rfv1) lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] @@ -167,6 +195,10 @@ is "permute :: perm \ rtrm1 \ rtrm1" +lemma [quot_respect]: + "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute" + by (simp add: alpha1_eqvt) + lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] instance @@ -203,12 +235,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 @@ -232,7 +260,7 @@ apply(simp_all) done -lemma helper: "{b. \pi. pi \ (a \ b) \ bp \ bp} = {}" +lemma helper2: "{b. \pi. pi \ (a \ b) \ bp \ bp} = {}" apply auto apply (rule_tac x="(x \ a)" in exI) apply auto @@ -261,7 +289,7 @@ apply(simp add: Abs_eq_iff) apply(simp add: alpha_gen) apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) -apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper) +apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2) apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) apply(simp (no_asm) add: supp_def eqvts) apply(fold supp_def) @@ -315,17 +343,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 @@ -342,87 +374,103 @@ section {*** lets with many assignments ***} -datatype trm3 = - Vr3 "name" -| Ap3 "trm3" "trm3" -| Lm3 "name" "trm3" --"bind (name) in (trm3)" -| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)" -and assigns = - ANil -| ACons "name" "trm3" "assigns" +datatype rtrm3 = + rVr3 "name" +| rAp3 "rtrm3" "rtrm3" +| rLm3 "name" "rtrm3" --"bind (name) in (trm3)" +| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)" +and rassigns = + rANil +| rACons "name" "rtrm3" "rassigns" (* to be given by the user *) primrec bv3 where - "bv3 ANil = {}" -| "bv3 (ACons x t as) = {atom x} \ (bv3 as)" + "bv3 rANil = {}" +| "bv3 (rACons x t as) = {atom x} \ (bv3 as)" -setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} +setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *} -local_setup {* snd o define_fv_alpha "Terms.trm3" +local_setup {* snd o define_fv_alpha "Terms.rtrm3" [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], [[], [[], [], []]]] *} print_theorems notation - alpha_trm3 ("_ \3 _" [100, 100] 100) and - alpha_assigns ("_ \3a _" [100, 100] 100) -thm alpha_trm3_alpha_assigns.intros + alpha_rtrm3 ("_ \3 _" [100, 100] 100) and + alpha_rassigns ("_ \3a _" [100, 100] 100) +thm alpha_rtrm3_alpha_rassigns.intros + +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_equivp: - "equivp alpha_trm3" - "equivp alpha_assigns" - sorry +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 - qtrm3 = trm3 / alpha_trm3 + trm3 = rtrm3 / alpha_rtrm3 and - qassigns = assigns / alpha_assigns - by (auto intro: alpha3_equivp) + assigns = rassigns / alpha_rassigns + by (rule alpha3_equivp(1)) (rule alpha3_equivp(2)) section {*** lam with indirect list recursion ***} -datatype trm4 = - Vr4 "name" -| Ap4 "trm4" "trm4 list" -| Lm4 "name" "trm4" --"bind (name) in (trm)" +datatype rtrm4 = + rVr4 "name" +| rAp4 "rtrm4" "rtrm4 list" +| rLm4 "name" "rtrm4" --"bind (name) in (trm)" print_theorems -thm trm4.recs +thm rtrm4.recs (* there cannot be a clause for lists, as *) (* permutations are already defined in Nominal (also functions, options, and so on) *) -setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *} +setup {* snd o define_raw_perms ["rtrm4"] ["Terms.rtrm4"] *} (* "repairing" of the permute function *) lemma repaired: - fixes ts::"trm4 list" - shows "permute_trm4_list p ts = p \ ts" + fixes ts::"rtrm4 list" + shows "permute_rtrm4_list p ts = p \ ts" apply(induct ts) apply(simp_all) done -thm permute_trm4_permute_trm4_list.simps -thm permute_trm4_permute_trm4_list.simps[simplified repaired] +thm permute_rtrm4_permute_rtrm4_list.simps +thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] -local_setup {* snd o define_fv_alpha "Terms.trm4" [ +local_setup {* snd o define_fv_alpha "Terms.rtrm4" [ [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} print_theorems notation - alpha_trm4 ("_ \4 _" [100, 100] 100) and - alpha_trm4_list ("_ \4l _" [100, 100] 100) -thm alpha_trm4_alpha_trm4_list.intros + alpha_rtrm4 ("_ \4 _" [100, 100] 100) and + 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 list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} +thm alpha4_inj -lemma alpha4_equivp: "equivp alpha_trm4" sorry -lemma alpha4list_equivp: "equivp alpha_trm4_list" sorry +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_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 - qtrm4 = trm4 / alpha_trm4 and - qtrm4list = "trm4 list" / alpha_trm4_list - by (simp_all add: alpha4_equivp alpha4list_equivp) + qrtrm4 = rtrm4 / alpha_rtrm4 and + qrtrm4list = "rtrm4 list" / alpha_rtrm4_list + by (simp_all add: alpha4_equivp) datatype rtrm5 = @@ -460,30 +508,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 @@ -525,6 +549,29 @@ apply (simp) 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_equivp) + +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)" @@ -659,7 +706,7 @@ (* example with a bn function defined over the type itself *) datatype rtrm6 = rVr6 "name" -| rLm6 "name" "rtrm6" +| rLm6 "name" "rtrm6" --"bind name in rtrm6" | rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" primrec @@ -681,13 +728,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 @@ -701,8 +752,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" diff -r 160343d86a6f -r 20f76fde8ef1 Quot/quotient_info.ML --- a/Quot/quotient_info.ML Tue Feb 23 13:32:35 2010 +0100 +++ b/Quot/quotient_info.ML Tue Feb 23 13:33:01 2010 +0100 @@ -37,7 +37,9 @@ val equiv_rules_get: Proof.context -> thm list val equiv_rules_add: attribute val rsp_rules_get: Proof.context -> thm list + val rsp_rules_add: attribute val prs_rules_get: Proof.context -> thm list + val prs_rules_add: attribute val id_simps_get: Proof.context -> thm list val quotient_rules_get: Proof.context -> thm list val quotient_rules_add: attribute @@ -241,6 +243,7 @@ val description = "Respectfulness theorems.") val rsp_rules_get = RspRules.get +val rsp_rules_add = RspRules.add (* preservation theorems *) structure PrsRules = Named_Thms @@ -248,6 +251,7 @@ val description = "Preservation theorems.") val prs_rules_get = PrsRules.get +val prs_rules_add = PrsRules.add (* id simplification theorems *) structure IdSimps = Named_Thms