# HG changeset patch # User Christian Urban # Date 1266939124 -3600 # Node ID 06f40e1c6982909f5fe5d4bc21df74dc43d3b2bb # Parent c179ad9d2446874bee3a701a78290ba2d3b48113# Parent ec2e0116779e2197175a93813bd88366ab9f90e1 merged diff -r c179ad9d2446 -r 06f40e1c6982 Quot/Nominal/Rsp.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Nominal/Rsp.thy Tue Feb 23 16:32:04 2010 +0100 @@ -0,0 +1,88 @@ +theory Rsp +imports Abs +begin + +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 +*} + +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 +*} + +ML {* +fun remove_alls trm = +let + val vars = strip_all_vars trm + val fs = rev (map Free vars) +in + ((map fst vars), subst_bounds (fs, (strip_all_body trm))) +end +*} + +ML {* +fun get_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 +*} + +ML {* +fun prove_const_rsp bind const tac ctxt = +let + val rsp_goal = const_rsp const ctxt + val thy = ProofContext.theory_of ctxt + val (fixed, user_goal) = get_rsp_goal thy rsp_goal + val user_thm = Goal.prove ctxt fixed [] user_goal tac + fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' rtac user_thm THEN_ALL_NEW atac) 1 + val rsp_thm = Goal.prove ctxt [] [] rsp_goal tac +in + ctxt +|> snd o Local_Theory.note + ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), [rsp_thm]) +|> snd o Local_Theory.note ((bind, []), [user_thm]) +end +*} + +ML {* +fun fv_rsp_tac induct fv_simps = + eresolve_tac induct THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fv_simps)) +*} + +ML {* +fun constr_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 +*} + + +end diff -r c179ad9d2446 -r 06f40e1c6982 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Tue Feb 23 16:31:40 2010 +0100 +++ b/Quot/Nominal/Terms.thy Tue Feb 23 16:32:04 2010 +0100 @@ -1,5 +1,5 @@ theory Terms -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "../../Attic/Prove" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../../Attic/Prove" begin atom_decl name @@ -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)]]], [[], [[]], [[], []]]] *} @@ -120,20 +120,8 @@ (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 -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 {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] + (rtac @{thm alpha1_equivp(1)} 1) *} local_setup {* (fn ctxt => ctxt @@ -145,44 +133,18 @@ *} 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})) *} -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 (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})+ -done - +local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} @{term fv_rtrm1} + (fn _ => fv_rsp_tac @{thms alpha_rtrm1_alpha_bp.inducts} @{thms fv_rtrm1_fv_bp.simps} 1) *} +local_setup {* prove_const_rsp @{binding rVr1_rsp} @{term rVr1} + (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} +local_setup {* prove_const_rsp @{binding rAp1_rsp} @{term rAp1} + (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} +local_setup {* prove_const_rsp @{binding rLm1_rsp} @{term rLm1} + (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} +local_setup {* prove_const_rsp @{binding rLt1_rsp} @{term rLt1} + (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} +local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} @{term "permute :: perm \ rtrm1 \ rtrm1"} + (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] @@ -195,10 +157,6 @@ 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 @@ -209,11 +167,10 @@ end -lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] - -lemmas fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] - -lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] +lemmas + fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] +and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] +and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] lemma lm1_supp_pre: shows "(supp (atom x, t)) supports (Lm1 x t) " @@ -352,12 +309,10 @@ (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 (rule alpha2_equivp(1)) (rule alpha2_equivp(2)) +local_setup {* define_quotient_type + [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})), + (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))] + ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *} local_setup {* (fn ctxt => ctxt @@ -371,6 +326,22 @@ *} print_theorems +(*local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} @{term fv_rtrm2} + (fn _ => fv_rsp_tac @{thms alpha_rtrm2_alpha_rassign.inducts} @{thms fv_rtrm2_fv_rassign.simps} 1) *} *) +lemma fv_rtrm2_rsp: "x \2 y \ fv_rtrm2 x = fv_rtrm2 y" sorry +lemma bv2_rsp: "x \2b y \ rbv2 x = rbv2 y" sorry + +local_setup {* prove_const_rsp @{binding rVr2_rsp} @{term rVr2} + (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} +local_setup {* prove_const_rsp @{binding rAp2_rsp} @{term rAp2} + (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} +local_setup {* prove_const_rsp @{binding rLm2_rsp} @{term rLm2} + (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} +local_setup {* prove_const_rsp @{binding rLt2_rsp} @{term rLt2} + (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp bv2_rsp} @{thms alpha2_equivp} 1) *} +local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} @{term "permute :: perm \ rtrm2 \ rtrm2"} + (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} + section {*** lets with many assignments ***}