# HG changeset patch # User Cezary Kaliszyk # Date 1271834035 -7200 # Node ID 880fe1d2234e9e2fe2d264b23ba216a99b88c1f3 # Parent 7b74cf8439422062007a0caf4286ebf172db4b46# Parent 0dc61c2966da484e85ea8ab01363df5b083ea230 merge diff -r 7b74cf843942 -r 880fe1d2234e Nominal/Manual/Term4.thy --- a/Nominal/Manual/Term4.thy Wed Apr 21 09:13:32 2010 +0200 +++ b/Nominal/Manual/Term4.thy Wed Apr 21 09:13:55 2010 +0200 @@ -1,5 +1,5 @@ theory Term4 -imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" +imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove" begin atom_decl name @@ -28,7 +28,7 @@ done thm permute_rtrm4_permute_rtrm4_list.simps -lemmas rawperm=permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] +lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4") @@ -48,42 +48,45 @@ apply simp_all done -(* We need sth like: -lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *) +ML {* @{term "\a"} *} + +lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))" +apply (rule ext) +apply (induct_tac x) +apply simp_all +done notation alpha_rtrm4 ("_ \4 _" [100, 100] 100) and alpha_rtrm4_list ("_ \4l _" [100, 100] 100) thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_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 -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_rel_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_no +lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3] local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *} thm eqvts(1-2) local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []), - build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} ctxt 1) ctxt) ctxt)) +(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), + build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} ctxt 1) ctxt) ctxt)) *} -lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] +thm alpha4_eqvt +lemmas alpha4_eqvt_fixed = alpha4_eqvt[simplified fix2 fix3] local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []), - build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *} + build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *} thm alpha4_reflp -ML build_equivps +lemmas alpha4_reflp_fixed = alpha4_reflp[simplified fix2 fix3] -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), - (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} -lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), + (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{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)) *} +lemmas alpha4_equivp_fixed = alpha4_equivp[simplified fix2 fix3] quotient_type trm4 = rtrm4 / alpha_rtrm4 -(*and - trm4list = "rtrm4 list" / alpha_rtrm4_list*) by (simp_all add: alpha4_equivp) local_setup {* @@ -96,7 +99,6 @@ print_theorems - lemma fv_rtrm4_rsp: "xa \4 ya \ fv_rtrm4 xa = fv_rtrm4 ya" "x \4l y \ fv_rtrm4_list x = fv_rtrm4_list y" @@ -115,31 +117,61 @@ lemma [quot_respect]: "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" - by (simp add: alpha4_inj) + by (simp add: alpha4_inj_fixed) -(* Maybe also need: @{term "permute :: perm \ rtrm4 list \ rtrm4 list"} *) local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} [@{term "permute :: perm \ rtrm4 \ rtrm4"}] (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} -print_theorems -setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \ rtrm4 \ rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_append} *} +setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \ rtrm4 \ rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_plus} *} print_theorems - +(* Instead of permute for trm4_list we may need the following 2 lemmas: *) +lemma [quot_preserve]: "(id ---> map rep_trm4 ---> map abs_trm4) permute = permute" + apply (simp add: expand_fun_eq) + apply clarify + apply (rename_tac "pi" x) + apply (induct_tac x) + apply simp + apply simp + apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified]) + done -lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) = - (trm4 = trm4a \ list_rel (op =) list lista)" - by (lifting alpha4_inj(2)) +lemma [quot_respect]: "(op = ===> list_rel alpha_rtrm4 ===> list_rel alpha_rtrm4) permute permute" + apply simp + apply (rule allI)+ + apply (induct_tac xa y rule: list_induct2') + apply simp_all + apply clarify + apply (erule alpha4_eqvt) + done -thm bla[simplified list_rel_eq] +ML {* + map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed} +*} -ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *} -ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *} -ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *} ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} -. + +ML {* + map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4_fv_rtrm4_list.simps[simplified fix3]} +*} -(*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*) +ML {* +val liftd = + map (Local_Defs.unfold @{context} @{thms id_simps}) ( + map (Local_Defs.fold @{context} @{thms alphas}) ( + map (lift_thm [@{typ trm4}] @{context}) @{thms alpha4_inj_fixed[unfolded alphas]} + ) + ) +*} + +ML {* + map (lift_thm [@{typ trm4}] @{context}) + (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})])) +*} + +ML {* + map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fix3]} +*} end