30 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} |
30 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} |
31 thm permute_rtrm1_permute_bp.simps |
31 thm permute_rtrm1_permute_bp.simps |
32 |
32 |
33 local_setup {* |
33 local_setup {* |
34 snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") |
34 snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") |
35 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
35 [[[], [], [(NONE, 0, 1)], [(SOME @{term bv1}, 0, 2)]], |
36 [[], [[]], [[], []]]] *} |
36 [[], [], []]] *} |
37 |
37 |
38 notation |
38 notation |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
41 thm alpha_rtrm1_alpha_bp.intros |
41 thm alpha_rtrm1_alpha_bp.intros |
50 |
50 |
51 local_setup {* |
51 local_setup {* |
52 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} |
52 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} |
53 *} |
53 *} |
54 |
54 |
55 |
55 ML {* |
56 local_setup {* |
56 fun build_alpha_eqvts funs perms simps induct ctxt = |
57 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
57 let |
58 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) |
58 val pi = Free ("p", @{typ perm}); |
|
59 val types = map (domain_type o fastype_of) funs; |
|
60 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
|
61 val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); |
|
62 val args = map Free (indnames ~~ types); |
|
63 val args2 = map Free (indnames2 ~~ types); |
|
64 fun eqvtc ((alpha, perm), (arg, arg2)) = |
|
65 HOLogic.mk_imp (alpha $ arg $ arg2, |
|
66 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
|
67 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
|
68 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
|
69 (asm_full_simp_tac (HOL_ss addsimps |
|
70 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
|
71 THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
72 (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW |
|
73 (asm_full_simp_tac (HOL_ss addsimps |
|
74 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
|
75 ) 1 |
|
76 |
|
77 in |
|
78 gl |
|
79 end |
|
80 *}ye |
|
81 |
|
82 lemma alpha_gen_compose_eqvt: |
|
83 assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)" |
|
84 and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)" |
|
85 and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
|
86 shows "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s) \<and> P g pi d e t s R f pia" |
|
87 using b |
|
88 apply - |
|
89 sorry |
|
90 |
|
91 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (p \<bullet> pi)) \<Longrightarrow> \<exists>pi. Q pi" |
|
92 apply (erule exE) |
|
93 apply (rule_tac x="pia \<bullet> pi" in exI) |
|
94 by auto |
|
95 |
|
96 prove {* |
|
97 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} @{context} |
59 *} |
98 *} |
60 print_theorems |
99 apply(rule alpha_rtrm1_alpha_bp.induct) |
61 |
100 apply(simp_all add: atom_eqvt alpha1_inj) |
|
101 apply(erule exi) |
|
102 apply(simp add: alpha_gen.simps) |
|
103 apply(erule conjE)+ |
|
104 apply(rule conjI) |
|
105 apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric]) |
|
106 apply(subst empty_eqvt[symmetric]) |
|
107 apply(subst insert_eqvt[symmetric]) |
|
108 apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric]) |
|
109 apply(subst eqvts) |
|
110 apply(subst eqvts) |
|
111 apply(subst eqvts) |
|
112 apply(subst eqvts) |
|
113 apply(subst eqvts) |
|
114 apply simp |
|
115 apply(rule conjI) |
|
116 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) |
|
117 apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) |
|
118 thm eqvts |
|
119 apply(simp add:eqvts) |
|
120 |
|
121 thm insert_eqvt |
|
122 apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric]) |
|
123 |
|
124 apply(rule conjI) |
|
125 thm atom_eqvt |
|
126 apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) |
|
127 apply simp |
|
128 apply(rule conjI) |
|
129 apply(subst permute_eqvt[symmetric]) |
|
130 apply simp |
|
131 apply(rule conjI) |
|
132 apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) |
|
133 apply simp |
|
134 apply(subst permute_eqvt[symmetric]) |
|
135 apply simp |
|
136 apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1]) |
|
137 apply(simp) |
|
138 thm permute_eq_iff[THEN iffD1] |
|
139 apply(clarify) |
|
140 apply(rule conjI) |
|
141 |
|
142 apply(erule alpha_gen_compose_eqvt) |
|
143 |
|
144 prefer 2 |
|
145 apply(erule conj_forward) |
|
146 apply (simp add: eqvts) |
|
147 apply(erule alpha_gen_compose_eqvt) |
62 lemma alpha1_eqvt_proper[eqvt]: |
148 lemma alpha1_eqvt_proper[eqvt]: |
63 "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))" |
149 "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))" |
64 "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))" |
150 "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))" |
65 apply (simp_all only: eqvts) |
151 apply (simp_all only: eqvts) |
66 apply rule |
152 apply rule |