diff -r 89715c48f728 -r f5057aabf5c0 Nominal/Manual/Term4.thy --- a/Nominal/Manual/Term4.thy Sat May 12 22:21:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,167 +0,0 @@ -theory Term4 -imports "../NewAlpha" "../Abs" "../Perm" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove" -begin - -atom_decl name - -section {*** lam with indirect list recursion ***} - -datatype rtrm4 = - rVr4 "name" -| rAp4 "rtrm4" "rtrm4 list" -| rLm4 "name" "rtrm4" --"bind (name) in (trm)" - -(* there cannot be a clause for lists, as *) -(* permutations are already defined in Nominal (also functions, options, and so on) *) -ML {* - val dtinfo = Datatype.the_info @{theory} "Term4.rtrm4"; - val {descr, sorts, ...} = dtinfo; -*} -setup {* snd o (define_raw_perms descr sorts @{thm rtrm4.induct} 1) *} -lemmas perm = permute_rtrm4_permute_rtrm4_list.simps(1-3) -lemma perm_fix: - fixes ts::"rtrm4 list" - shows "permute_rtrm4_list p ts = p \ ts" - by (induct ts) simp_all -lemmas perm_fixed = perm[simplified perm_fix] - -ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *} - -local_setup {* fn ctxt => let val (_, _, _, ctxt') = define_raw_fvs descr sorts [] bl ctxt in ctxt' end *} -lemmas fv = fv_rtrm4.simps (*fv_rtrm4_list.simps*) - -lemma fv_fix: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))" - by (rule ext) (induct_tac x, simp_all) -lemmas fv_fixed = fv[simplified fv_fix] - -(* TODO: check remove 2 *) -local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms perm_fixed fv_rtrm4.simps fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *} -thm eqvts(1-2) - -local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *} -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)) *} -lemmas alpha_inj = alpha4_inj(1-3) - -lemma alpha_fix: "alpha_rtrm4_list = list_all2 alpha_rtrm4" - apply (rule ext)+ - apply (induct_tac x xa rule: list_induct2') - apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) - apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) - apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) - apply rule - apply (erule alpha_rtrm4_list.cases) - apply simp_all - apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) - apply simp_all - done - -lemmas alpha_inj_fixed = alpha_inj[simplified alpha_fix (*fv_fix*)] - -notation - alpha_rtrm4 ("_ \4 _" [100, 100] 100) -and alpha_rtrm4_list ("_ \4l _" [100, 100] 100) - -declare perm_fixed[eqvt] -equivariance alpha_rtrm4 -lemmas alpha4_eqvt = eqvts(1-2) -lemmas alpha4_eqvt_fixed = alpha4_eqvt(2)[simplified alpha_fix (*fv_fix*)] - -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} ctxt) ctxt)) *} -thm alpha4_reflp - -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 alpha_fix fv_fix] - -quotient_type - trm4 = rtrm4 / alpha_rtrm4 - by (simp_all add: alpha4_equivp) - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4})) - |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4})) - |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4})) - |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4}))) -*} -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" - apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) - apply (simp_all add: alpha_gen) -done - -local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}] - (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *} -print_theorems - -local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}] - (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} -local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}] - (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} - -lemma [quot_respect]: - "(alpha_rtrm4 ===> list_all2 alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" - by (simp add: alpha_inj_fixed) - -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) *} - -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 [quot_respect]: "(op = ===> list_all2 alpha_rtrm4 ===> list_all2 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 - -ML {* - map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed} -*} - -ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} - -ML {* - map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fv_fix] fv_rtrm4_list.simps[simplified fv_fix]} -*} - -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 alpha_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"})])) -*} - -thm eqvts(6-7) -ML {* - map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(6-7)[simplified fv_fix]} -*} - -end