# HG changeset patch # User Cezary Kaliszyk # Date 1266931184 -3600 # Node ID 28aaf6d01e10fe978919da7889c6358c6d65acce # Parent 0d059450a3fa40c8bd457b5ed9fdd88fdebe2dd3 Progress towards automatic rsp of constants and fv. diff -r 0d059450a3fa -r 28aaf6d01e10 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Tue Feb 23 12:49:45 2010 +0100 +++ b/Quot/Nominal/Terms.thy Tue Feb 23 14:19:44 2010 +0100 @@ -32,7 +32,7 @@ setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} thm permute_rtrm1_permute_bp.simps -local_setup {* +local_setup {* snd o define_fv_alpha "Terms.rtrm1" [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], [[], [[]], [[], []]]] *} @@ -145,8 +145,21 @@ *} print_theorems -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})) *} + +ML {* +fun const_rsp const lthy = +let + val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy) + val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); +in + HOLogic.mk_Trueprop (rel $ const $ const) +end +*} + +(*local_setup {* +snd o Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), @{thms refl}) *} *) + +prove fv_rtrm1_rsp': {* const_rsp @{term fv_rtrm1} @{context} *} by (tactic {* (rtac @{thm fun_rel_id} THEN' eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW @@ -175,6 +188,33 @@ end *} +ML {* +fun remove_alls trm = +let + val fs = rev (map Free (strip_all_vars trm)) +in + subst_bounds (fs, (strip_all_body trm)) +end +*} + +ML {* +fun rsp_goal thy trm = +let + val goalstate = Goal.init (cterm_of thy trm); + val tac = REPEAT o rtac @{thm fun_rel_id}; +in + case (SINGLE (tac 1) goalstate) of + NONE => error "rsp_goal failed" + | SOME th => remove_alls (term_of (cprem_of th 1)) +end +*} + +prove rAp1_rsp': {* rsp_goal @{theory} (const_rsp @{term rAp1} @{context}) *} +by (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *}) + +thm apply_rsp'[OF apply_rsp'[OF rAp1_rsp']] + + lemma [quot_respect]: "(op = ===> alpha_rtrm1) rVr1 rVr1" "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"