equal
deleted
inserted
replaced
85 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
85 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
86 @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) |
86 @{thms split_conv alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) |
87 )) |
87 )) |
88 *} |
88 *} |
89 |
89 |
90 ML {* |
|
91 fun perm_arg arg = |
|
92 let |
|
93 val ty = fastype_of arg |
|
94 in |
|
95 Const (@{const_name permute}, @{typ perm} --> ty --> ty) |
|
96 end |
|
97 *} |
|
98 |
90 |
99 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
91 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
100 apply (erule exE) |
92 apply (erule exE) |
101 apply (rule_tac x="pi \<bullet> pia" in exI) |
93 apply (rule_tac x="pi \<bullet> pia" in exI) |
102 by auto |
94 by auto |
121 let |
113 let |
122 val pi = Free ("p", @{typ perm}); |
114 val pi = Free ("p", @{typ perm}); |
123 val (tys, _) = strip_type (fastype_of alpha) |
115 val (tys, _) = strip_type (fastype_of alpha) |
124 val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys)); |
116 val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys)); |
125 val args = map Free (indnames ~~ tys); |
117 val args = map Free (indnames ~~ tys); |
126 val perm_args = map (fn x => perm_arg x $ pi $ x) args |
118 val perm_args = map (fn x => mk_perm pi x) args |
127 in |
119 in |
128 (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names) |
120 (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names) |
129 end |
121 end |
130 *} |
122 *} |
131 |
123 |