# HG changeset patch # User Cezary Kaliszyk # Date 1267524289 -3600 # Node ID 22a084c9316b6f9433b902fffe5ba344a8b3fed2 # Parent cbcd4997dac54b9adcf0930e9e97d7db607e4df9 Fixed eqvt code. diff -r cbcd4997dac5 -r 22a084c9316b Nominal/Abs.thy --- a/Nominal/Abs.thy Tue Mar 02 08:58:28 2010 +0100 +++ b/Nominal/Abs.thy Tue Mar 02 11:04:49 2010 +0100 @@ -114,14 +114,13 @@ done lemma alpha_gen_compose_eqvt: - assumes b: "\pia. (g d, t) \gen (\x1 x2. R x1 x2 \ R (pi \ x1) (pi \ x2)) f pia (g e, s)" + fixes pia + 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)" + shows "(g (pi \ d), pi \ t) \gen R f (pi \ pia) (g (pi \ e), pi \ s)" using b apply - - apply(erule exE) - apply(rule_tac x="pi \ pia" in exI) apply(simp add: alpha_gen.simps) apply(erule conjE)+ apply(rule conjI) @@ -419,6 +418,7 @@ apply(simp add: supp_swap) done +(* thm supp_perm lemma perm_induct_test: @@ -502,6 +502,6 @@ apply(simp) oops - +*) end diff -r cbcd4997dac5 -r 22a084c9316b Nominal/LFex.thy --- a/Nominal/LFex.thy Tue Mar 02 08:58:28 2010 +0100 +++ b/Nominal/LFex.thy Tue Mar 02 11:04:49 2010 +0100 @@ -24,9 +24,9 @@ local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind") - [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], - [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], - [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} + [[ [], [(NONE, 1, 2)]], + [ [], [], [(NONE, 1, 2)] ], + [ [], [], [], [(NONE, 1, 2)]]] *} notation alpha_rkind ("_ \ki _" [100, 100] 100) and alpha_rty ("_ \ty _" [100, 100] 100) diff -r cbcd4997dac5 -r 22a084c9316b Nominal/Rsp.thy --- a/Nominal/Rsp.thy Tue Mar 02 08:58:28 2010 +0100 +++ b/Nominal/Rsp.thy Tue Mar 02 11:04:49 2010 +0100 @@ -136,6 +136,10 @@ end *} +lemma exi: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (pi \ p)) \ \pi. Q pi" +apply (erule exE) +apply (rule_tac x="pi \ pia" in exI) +by auto ML {* fun build_alpha_eqvts funs perms simps induct ctxt = @@ -151,18 +155,20 @@ (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 + ( + (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 + THEN_ALL_NEW (etac @{thm exi[of _ _ "p"]} THEN' + REPEAT o etac conjE THEN' + (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW + (asm_full_simp_tac HOL_ss) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps - (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) -) 1 + (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))))) 1 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac in map (fn x => mp OF [x]) (HOLogic.conj_elims thm) end *} - end diff -r cbcd4997dac5 -r 22a084c9316b Nominal/Term1.thy --- a/Nominal/Term1.thy Tue Mar 02 08:58:28 2010 +0100 +++ b/Nominal/Term1.thy Tue Mar 02 11:04:49 2010 +0100 @@ -52,99 +52,10 @@ 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 - -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 +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)) *} -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} -*} -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))" diff -r cbcd4997dac5 -r 22a084c9316b Nominal/Term4.thy --- a/Nominal/Term4.thy Tue Mar 02 08:58:28 2010 +0100 +++ b/Nominal/Term4.thy Tue Mar 02 11:04:49 2010 +0100 @@ -30,7 +30,7 @@ thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} + [[[], [], [(NONE, 0,1)]], [[], []] ] *} print_theorems notation diff -r cbcd4997dac5 -r 22a084c9316b Nominal/Term6.thy --- a/Nominal/Term6.thy Tue Mar 02 08:58:28 2010 +0100 +++ b/Nominal/Term6.thy Tue Mar 02 11:04:49 2010 +0100 @@ -22,7 +22,7 @@ print_theorems local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [ - [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} + [[], [(NONE, 0, 1)], [(SOME @{term rbv6}, 0, 1)]]] *} notation alpha_rtrm6 ("_ \6 _" [100, 100] 100) thm alpha_rtrm6.intros @@ -41,7 +41,7 @@ (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) *} - +thm alpha6_eqvt local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} thm alpha6_equivp