# HG changeset patch # User Christian Urban # Date 1267508589 -3600 # Node ID db1b5cb89aa4bf406aca1bcc8f602787484ee9f7 # Parent dca51a1f0c0de095b4b5ba6558a32496874d6814# Parent 2d17ed8aca6010779d627d7a7c66062f38f2171b merged diff -r dca51a1f0c0d -r db1b5cb89aa4 Nominal/Lift.thy --- a/Nominal/Lift.thy Tue Mar 02 06:42:43 2010 +0100 +++ b/Nominal/Lift.thy Tue Mar 02 06:43:09 2010 +0100 @@ -64,6 +64,8 @@ "rbv5 rLnil = {}" | "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" +ML Typedef.add_typedef + ML {* val thy1 = @{theory}; val info = Datatype.the_info @{theory} "Lift.rtrm5" @@ -135,9 +137,13 @@ val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9; val thy3 = Local_Theory.exit_global lthy10; +(* TODO: fix this hack... *) +val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5"); +(*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \ rtrm1 \ rtrm1"})] + @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*) val lthy11 = Theory_Target.init NONE thy3; val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct)); -val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11) +val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11); *} setup {* fn _ => Local_Theory.exit_global lthy12 *} diff -r dca51a1f0c0d -r db1b5cb89aa4 Nominal/Term1.thy --- a/Nominal/Term1.thy Tue Mar 02 06:42:43 2010 +0100 +++ b/Nominal/Term1.thy Tue Mar 02 06:43:09 2010 +0100 @@ -32,8 +32,8 @@ local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], - [[], [[]], [[], []]]] *} + [[[], [], [(NONE, 0, 1)], [(SOME @{term bv1}, 0, 2)]], + [[], [], []]] *} notation alpha_rtrm1 ("_ \1 _" [100, 100] 100) and @@ -52,13 +52,99 @@ snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \ rtrm1 \ rtrm1"},@{term "permute :: perm \ bp \ bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} *} +ML {* +fun build_alpha_eqvts funs perms simps induct ctxt = +let + val pi = Free ("p", @{typ perm}); + val types = map (domain_type o fastype_of) funs; + val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); + val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); + val args = map Free (indnames ~~ types); + val args2 = map Free (indnames2 ~~ types); + fun eqvtc ((alpha, perm), (arg, arg2)) = + HOLogic.mk_imp (alpha $ arg $ arg2, + (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) + val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) + fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW + (asm_full_simp_tac (HOL_ss addsimps + (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) + THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW + (asm_full_simp_tac (HOL_ss addsimps + (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) +) 1 + +in + gl +end +*}ye -local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), - build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \ rtrm1 \ rtrm1"},@{term "permute :: perm \ bp \ bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) +lemma alpha_gen_compose_eqvt: + assumes b: "(g d, t) \gen (\x1 x2. R x1 x2 \ R (pi \ x1) (pi \ x2)) f pia (g e, s)" + and c: "\y. pi \ (g y) = g (pi \ y)" + and a: "\x. pi \ (f x) = f (pi \ x)" + shows "\pia. (g (pi \ d), pi \ t) \gen R f pia (g (pi \ e), pi \ s) \ P g pi d e t s R f pia" + using b + apply - +sorry + +lemma exi: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (p \ pi)) \ \pi. Q pi" +apply (erule exE) +apply (rule_tac x="pia \ pi" in exI) +by auto + +prove {* + build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \ rtrm1 \ rtrm1"},@{term "permute :: perm \ bp \ bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} @{context} *} -print_theorems +apply(rule alpha_rtrm1_alpha_bp.induct) +apply(simp_all add: atom_eqvt alpha1_inj) +apply(erule exi) +apply(simp add: alpha_gen.simps) +apply(erule conjE)+ +apply(rule conjI) +apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric]) +apply(subst empty_eqvt[symmetric]) +apply(subst insert_eqvt[symmetric]) +apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric]) +apply(subst eqvts) +apply(subst eqvts) +apply(subst eqvts) +apply(subst eqvts) +apply(subst eqvts) +apply simp +apply(rule conjI) +apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) +apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) +thm eqvts +apply(simp add:eqvts) + +thm insert_eqvt +apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric]) +apply(rule conjI) +thm atom_eqvt +apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) +apply simp +apply(rule conjI) +apply(subst permute_eqvt[symmetric]) +apply simp +apply(rule conjI) +apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) +apply simp +apply(subst permute_eqvt[symmetric]) +apply simp +apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1]) +apply(simp) +thm permute_eq_iff[THEN iffD1] +apply(clarify) +apply(rule conjI) + +apply(erule alpha_gen_compose_eqvt) + +prefer 2 +apply(erule conj_forward) +apply (simp add: eqvts) +apply(erule alpha_gen_compose_eqvt) lemma alpha1_eqvt_proper[eqvt]: "pi \ (t \1 s) = ((pi \ t) \1 (pi \ s))" "pi \ (alpha_bp a b) = (alpha_bp (pi \ a) (pi \ b))"