author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46961  5c6955f487e5 
child 50771  2852f997bfb5 
permissions  rwrr 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Nominal/nominal_inductive.ML 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

2 
Author: Stefan Berghofer, TU Muenchen 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

3 

22530  4 
Infrastructure for proving equivariance and strong induction theorems 
5 
for inductive predicates involving nominal datatypes. 

22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

6 
*) 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

7 

1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

8 
signature NOMINAL_INDUCTIVE = 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

9 
sig 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

10 
val prove_strong_ind: string > (string * string list) list > local_theory > Proof.state 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

11 
val prove_eqvt: string > string list > local_theory > local_theory 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

12 
end 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

13 

1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

14 
structure NominalInductive : NOMINAL_INDUCTIVE = 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

15 
struct 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

16 

33772
b6a1feca2ac2
use of thmantiquotation
Christian Urban <urbanc@in.tum.de>
parents:
33671
diff
changeset

17 
val inductive_forall_def = @{thm induct_forall_def}; 
b6a1feca2ac2
use of thmantiquotation
Christian Urban <urbanc@in.tum.de>
parents:
33671
diff
changeset

18 
val inductive_atomize = @{thms induct_atomize}; 
b6a1feca2ac2
use of thmantiquotation
Christian Urban <urbanc@in.tum.de>
parents:
33671
diff
changeset

19 
val inductive_rulify = @{thms induct_rulify}; 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

20 

41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39557
diff
changeset

21 
fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify []; 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

22 

621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

23 
val atomize_conv = 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39557
diff
changeset

24 
Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

25 
(HOL_basic_ss addsimps inductive_atomize); 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

26 
val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); 
24832  27 
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 
26568  28 
(Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

29 

44929  30 
fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []); 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

31 

39159  32 
val fresh_prod = @{thm fresh_prod}; 
22530  33 

44689  34 
val perm_bool = mk_meta_eq @{thm perm_bool_def}; 
39159  35 
val perm_boolI = @{thm perm_boolI}; 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

36 
val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

37 
(Drule.strip_imp_concl (cprop_of perm_boolI)))); 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

38 

25824  39 
fun mk_perm_bool pi th = th RS Drule.cterm_instantiate 
40 
[(perm_boolI_pi, pi)] perm_boolI; 

41 

38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
38558
diff
changeset

42 
fun mk_perm_bool_simproc names = Simplifier.simproc_global_i 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

43 
(theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss => 
44868  44 
fn Const (@{const_name Nominal.perm}, _) $ _ $ t => 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36428
diff
changeset

45 
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

46 
then SOME perm_bool else NONE 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

47 
 _ => NONE); 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

48 

22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

49 
fun transp ([] :: _) = [] 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

50 
 transp xs = map hd xs :: transp (map tl xs); 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

51 

22530  52 
fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of 
53 
(Const (s, T), ts) => (case strip_type T of 

54 
(Ts, Type (tname, _)) => 

31938  55 
(case NominalDatatype.get_nominal_datatype thy tname of 
22530  56 
NONE => fold (add_binders thy i) ts bs 
57 
 SOME {descr, index, ...} => (case AList.lookup op = 

58 
(#3 (the (AList.lookup op = descr index))) s of 

59 
NONE => fold (add_binders thy i) ts bs 

60 
 SOME cargs => fst (fold (fn (xs, x) => fn (bs', cargs') => 

61 
let val (cargs1, (u, _) :: cargs2) = chop (length xs) cargs' 

62 
in (add_binders thy i u 

63 
(fold (fn (u, T) => 

64 
if exists (fn j => j < i) (loose_bnos u) then I 

65 
else insert (op aconv o pairself fst) 

66 
(incr_boundvars (~i) u, T)) cargs1 bs'), cargs2) 

67 
end) cargs (bs, ts ~~ Ts)))) 

68 
 _ => fold (add_binders thy i) ts bs) 

69 
 (u, ts) => add_binders thy i u (fold (add_binders thy i) ts bs)) 

70 
 add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs 

71 
 add_binders thy i _ bs = bs; 

72 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38715
diff
changeset

73 
fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

74 
Const (name, _) => 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36428
diff
changeset

75 
if member (op =) names name then SOME (f p q) else NONE 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

76 
 _ => NONE) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

77 
 split_conj _ _ _ _ = NONE; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

78 

621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

79 
fun strip_all [] t = t 
38558  80 
 strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t; 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

81 

621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

82 
(*********************************************************************) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

83 
(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *) 
27722
d657036e26c5
 corrected bogus comment for function inst_conj_all
berghofe
parents:
27449
diff
changeset

84 
(* or ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t) *) 
d657036e26c5
 corrected bogus comment for function inst_conj_all
berghofe
parents:
27449
diff
changeset

85 
(* to R ... & id (ALL z. P z (pi_1 o ... o pi_n o t)) *) 
d657036e26c5
 corrected bogus comment for function inst_conj_all
berghofe
parents:
27449
diff
changeset

86 
(* or id (ALL z. P z (pi_1 o ... o pi_n o t)) *) 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

87 
(* *) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

88 
(* where "id" protects the subformula from simplification *) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

89 
(*********************************************************************) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

90 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38715
diff
changeset

91 
fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ = 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

92 
(case head_of p of 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

93 
Const (name, _) => 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36428
diff
changeset

94 
if member (op =) names name then SOME (HOLogic.mk_conj (p, 
44868  95 
Const (@{const_name Fun.id}, HOLogic.boolT > HOLogic.boolT) $ 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

96 
(subst_bounds (pis, strip_all pis q)))) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

97 
else NONE 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

98 
 _ => NONE) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

99 
 inst_conj_all names ps pis t u = 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

100 
if member (op aconv) ps (head_of u) then 
44868  101 
SOME (Const (@{const_name Fun.id}, HOLogic.boolT > HOLogic.boolT) $ 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

102 
(subst_bounds (pis, strip_all pis t))) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

103 
else NONE 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

104 
 inst_conj_all _ _ _ _ _ = NONE; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

105 

621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

106 
fun inst_conj_all_tac k = EVERY 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

107 
[TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]), 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

108 
REPEAT_DETERM_N k (etac allE 1), 
26359  109 
simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1]; 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

110 

621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

111 
fun map_term f t u = (case f t u of 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

112 
NONE => map_term' f t u  x => x) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

113 
and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u u') of 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

114 
(NONE, NONE) => NONE 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

115 
 (SOME t'', NONE) => SOME (t'' $ u) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

116 
 (NONE, SOME u'') => SOME (t $ u'') 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

117 
 (SOME t'', SOME u'') => SOME (t'' $ u'')) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

118 
 map_term' f (Abs (s, T, t)) (Abs (s', T', t')) = (case map_term f t t' of 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

119 
NONE => NONE 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

120 
 SOME t'' => SOME (Abs (s, T, t''))) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

121 
 map_term' _ _ _ = NONE; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

122 

621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

123 
(*********************************************************************) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

124 
(* Prove F[f t] from F[t], where F is monotone *) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

125 
(*********************************************************************) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

126 

621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

127 
fun map_thm ctxt f tac monos opt th = 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

128 
let 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

129 
val prop = prop_of th; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

130 
fun prove t = 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

131 
Goal.prove ctxt [] [] t (fn _ => 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

132 
EVERY [cut_facts_tac [th] 1, etac rev_mp 1, 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

133 
REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)), 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

134 
REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

135 
in Option.map prove (map_term f prop (the_default prop opt)) end; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

136 

27352
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

137 
val eta_contract_cterm = Thm.dest_arg o Thm.cprop_of o Thm.eta_conversion; 
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

138 

25824  139 
fun first_order_matchs pats objs = Thm.first_order_match 
27352
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

140 
(eta_contract_cterm (Conjunction.mk_conjunction_balanced pats), 
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

141 
eta_contract_cterm (Conjunction.mk_conjunction_balanced objs)); 
25824  142 

143 
fun first_order_mrs ths th = ths MRS 

144 
Thm.instantiate (first_order_matchs (cprems_of th) (map cprop_of ths)) th; 

145 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

146 
fun prove_strong_ind s avoids ctxt = 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

147 
let 
42361  148 
val thy = Proof_Context.theory_of ctxt; 
25824  149 
val ({names, ...}, {raw_induct, intrs, elims, ...}) = 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

150 
Inductive.the_inductive ctxt (Sign.intern_const thy s); 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

151 
val ind_params = Inductive.params_of raw_induct; 
24832  152 
val raw_induct = atomize_induct ctxt raw_induct; 
25824  153 
val elims = map (atomize_induct ctxt) elims; 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

154 
val monos = Inductive.get_monos ctxt; 
24571  155 
val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt; 
33040  156 
val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of 
22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

157 
[] => () 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

158 
 xs => error ("Missing equivariance theorem for predicate(s): " ^ 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

159 
commas_quote xs)); 
44045
2814ff2a6e3e
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents:
43326
diff
changeset

160 
val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

161 
(Induct.lookup_inductP ctxt (hd names))))); 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

162 
val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt; 
22530  163 
val concls = raw_induct' > Logic.strip_imp_concl > HOLogic.dest_Trueprop > 
164 
HOLogic.dest_conj > map (HOLogic.dest_imp ##> strip_comb); 

165 
val ps = map (fst o snd) concls; 

166 

167 
val _ = (case duplicates (op = o pairself fst) avoids of 

168 
[] => () 

169 
 xs => error ("Duplicate case names: " ^ commas_quote (map fst xs))); 

170 
val _ = assert_all (null o duplicates op = o snd) avoids 

171 
(fn (a, _) => error ("Duplicate variable names for case " ^ quote a)); 

33040  172 
val _ = (case subtract (op =) induct_cases (map fst avoids) of 
22530  173 
[] => () 
174 
 xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs)); 

25824  175 
val avoids' = if null induct_cases then replicate (length intrs) ("", []) 
176 
else map (fn name => 

177 
(name, the_default [] (AList.lookup op = avoids name))) induct_cases; 

22530  178 
fun mk_avoids params (name, ps) = 
179 
let val k = length params  1 

180 
in map (fn x => case find_index (equal x o fst) params of 

181 
~1 => error ("No such variable in case " ^ quote name ^ 

182 
" of inductive definition: " ^ quote x) 

183 
 i => (Bound (k  i), snd (nth params i))) ps 

184 
end; 

185 

186 
val prems = map (fn (prem, avoid) => 

187 
let 

188 
val prems = map (incr_boundvars 1) (Logic.strip_assums_hyp prem); 

189 
val concl = incr_boundvars 1 (Logic.strip_assums_concl prem); 

190 
val params = Logic.strip_params prem 

191 
in 

192 
(params, 

193 
fold (add_binders thy 0) (prems @ [concl]) [] @ 

194 
map (apfst (incr_boundvars 1)) (mk_avoids params avoid), 

195 
prems, strip_comb (HOLogic.dest_Trueprop concl)) 

196 
end) (Logic.strip_imp_prems raw_induct' ~~ avoids'); 

197 

198 
val atomTs = distinct op = (maps (map snd o #2) prems); 

199 
val ind_sort = if null atomTs then HOLogic.typeS 

36428
874843c1e96e
really minimize sorts after certification  looks like this is intended here;
wenzelm
parents:
36323
diff
changeset

200 
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy 
874843c1e96e
really minimize sorts after certification  looks like this is intended here;
wenzelm
parents:
36323
diff
changeset

201 
("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs)); 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
42361
diff
changeset

202 
val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt'); 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

203 
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt'; 
22530  204 
val fsT = TFree (fs_ctxt_tyname, ind_sort); 
205 

24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

206 
val inductive_forall_def' = Drule.instantiate' 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

207 
[SOME (ctyp_of thy fsT)] [] inductive_forall_def; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

208 

22530  209 
fun lift_pred' t (Free (s, T)) ts = 
210 
list_comb (Free (s, fsT > T), t :: ts); 

211 
val lift_pred = lift_pred' (Bound 0); 

212 

24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

213 
fun lift_prem (t as (f $ u)) = 
22530  214 
let val (p, ts) = strip_comb t 
215 
in 

44868  216 
if member (op =) ps p then HOLogic.mk_induct_forall fsT $ 
217 
Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) 

22530  218 
else lift_prem f $ lift_prem u 
219 
end 

220 
 lift_prem (Abs (s, T, t)) = Abs (s, T, lift_prem t) 

221 
 lift_prem t = t; 

222 

223 
fun mk_distinct [] = [] 

32952  224 
 mk_distinct ((x, T) :: xs) = map_filter (fn (y, U) => 
22530  225 
if T = U then SOME (HOLogic.mk_Trueprop 
226 
(HOLogic.mk_not (HOLogic.eq_const T $ x $ y))) 

227 
else NONE) xs @ mk_distinct xs; 

228 

229 
fun mk_fresh (x, T) = HOLogic.mk_Trueprop 

31938  230 
(NominalDatatype.fresh_const T fsT $ x $ Bound 0); 
22530  231 

232 
val (prems', prems'') = split_list (map (fn (params, bvars, prems, (p, ts)) => 

233 
let 

234 
val params' = params @ [("y", fsT)]; 

235 
val prem = Logic.list_implies 

236 
(map mk_fresh bvars @ mk_distinct bvars @ 

237 
map (fn prem => 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

238 
if null (preds_of ps prem) then prem 
22530  239 
else lift_prem prem) prems, 
240 
HOLogic.mk_Trueprop (lift_pred p ts)); 

29276  241 
val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params') 
22530  242 
in 
46218
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
44929
diff
changeset

243 
(Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem))) 
22530  244 
end) prems); 
245 

246 
val ind_vars = 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33772
diff
changeset

247 
(Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~ 
22530  248 
map NominalAtoms.mk_permT atomTs) @ [("z", fsT)]; 
249 
val ind_Ts = rev (map snd ind_vars); 

250 

251 
val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 

252 
(map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, 

253 
HOLogic.list_all (ind_vars, lift_pred p 

31938  254 
(map (fold_rev (NominalDatatype.mk_perm ind_Ts) 
22530  255 
(map Bound (length atomTs downto 1))) ts)))) concls)); 
256 

257 
val concl' = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 

258 
(map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem, 

259 
lift_pred' (Free (fs_ctxt_name, fsT)) p ts)) concls)); 

260 

261 
val vc_compat = map (fn (params, bvars, prems, (p, ts)) => 

46218
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
44929
diff
changeset

262 
map (fn q => Logic.list_all (params, incr_boundvars ~1 (Logic.list_implies 
32952  263 
(map_filter (fn prem => 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

264 
if null (preds_of ps prem) then SOME prem 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

265 
else map_term (split_conj (K o I) names) prem prem) prems, q)))) 
22530  266 
(mk_distinct bvars @ 
267 
maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop 

31938  268 
(NominalDatatype.fresh_const U T $ u $ t)) bvars) 
22530  269 
(ts ~~ binder_types (fastype_of p)))) prems; 
270 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

271 
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

272 
val pt2_atoms = map (fn aT => Global_Theory.get_thm thy 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

273 
("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; 
35232
f588e1169c8b
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents:
33968
diff
changeset

274 
val eqvt_ss = Simplifier.global_context thy HOL_basic_ss 
27352
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

275 
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) 
44868  276 
addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}], 
27352
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

277 
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

278 
val fresh_bij = Global_Theory.get_thms thy "fresh_bij"; 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

279 
val perm_bij = Global_Theory.get_thms thy "perm_bij"; 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

280 
val fs_atoms = map (fn aT => Global_Theory.get_thm thy 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

281 
("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

282 
val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'"; 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

283 
val fresh_atm = Global_Theory.get_thms thy "fresh_atm"; 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

284 
val swap_simps = Global_Theory.get_thms thy "swap_simps"; 
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

285 
val perm_fresh_fresh = Global_Theory.get_thms thy "perm_fresh_fresh"; 
22530  286 

287 
fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) = 

288 
let 

27722
d657036e26c5
 corrected bogus comment for function inst_conj_all
berghofe
parents:
27449
diff
changeset

289 
(** protect terms to avoid that fresh_prod interferes with **) 
22530  290 
(** pairs used in introduction rules of inductive predicate **) 
291 
fun protect t = 

44868  292 
let val T = fastype_of t in Const (@{const_name Fun.id}, T > T) $ t end; 
22530  293 
val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1); 
294 
val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop 

295 
(HOLogic.exists_const T $ Abs ("x", T, 

31938  296 
NominalDatatype.fresh_const T (fastype_of p) $ 
22530  297 
Bound 0 $ p))) 
298 
(fn _ => EVERY 

299 
[resolve_tac exists_fresh' 1, 

27722
d657036e26c5
 corrected bogus comment for function inst_conj_all
berghofe
parents:
27449
diff
changeset

300 
resolve_tac fs_atoms 1]); 
32202  301 
val (([(_, cx)], ths), ctxt') = Obtain.result 
22530  302 
(fn _ => EVERY 
303 
[etac exE 1, 

304 
full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1, 

26359  305 
full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1, 
22530  306 
REPEAT (etac conjE 1)]) 
307 
[ex] ctxt 

308 
in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end; 

309 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

310 
fun mk_ind_proof ctxt' thss = 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

311 
Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} => 
22530  312 
let val th = Goal.prove ctxt [] [] concl (fn {context, ...} => 
313 
rtac raw_induct 1 THEN 

314 
EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) => 

315 
[REPEAT (rtac allI 1), simp_tac eqvt_ss 1, 

316 
SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} => 

317 
let 

318 
val (params', (pis, z)) = 

32202  319 
chop (length params  length atomTs  1) (map (term_of o #2) params) > 
22530  320 
split_last; 
321 
val bvars' = map 

322 
(fn (Bound i, T) => (nth params' (length params'  i), T) 

323 
 (t, T) => (t, T)) bvars; 

324 
val pi_bvars = map (fn (t, _) => 

31938  325 
fold_rev (NominalDatatype.mk_perm []) pis t) bvars'; 
22530  326 
val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl)); 
327 
val (freshs1, freshs2, ctxt'') = fold 

328 
(obtain_fresh_name (ts @ pi_bvars)) 

329 
(map snd bvars') ([], [], ctxt'); 

31938  330 
val freshs2' = NominalDatatype.mk_not_sym freshs2; 
331 
val pis' = map NominalDatatype.perm_of_pair (pi_bvars ~~ freshs1); 

24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

332 
fun concat_perm pi1 pi2 = 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

333 
let val T = fastype_of pi1 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

334 
in if T = fastype_of pi2 then 
44868  335 
Const (@{const_name List.append}, T > T > T) $ pi1 $ pi2 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

336 
else pi2 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

337 
end; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

338 
val pis'' = fold (concat_perm #> map) pis' pis; 
22530  339 
val env = Pattern.first_order_match thy (ihypt, prop_of ihyp) 
340 
(Vartab.empty, Vartab.empty); 

341 
val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy)) 

32035  342 
(map (Envir.subst_term env) vs ~~ 
31938  343 
map (fold_rev (NominalDatatype.mk_perm []) 
22530  344 
(rev pis' @ pis)) params' @ [z])) ihyp; 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

345 
fun mk_pi th = 
26359  346 
Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}] 
31938  347 
addsimprocs [NominalDatatype.perm_simproc]) 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

348 
(Simplifier.simplify eqvt_ss 
25824  349 
(fold_rev (mk_perm_bool o cterm_of thy) 
350 
(rev pis' @ pis) th)); 

24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

351 
val (gprems1, gprems2) = split_list 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

352 
(map (fn (th, t) => 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

353 
if null (preds_of ps t) then (SOME th, mk_pi th) 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

354 
else 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

355 
(map_thm ctxt (split_conj (K o I) names) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

356 
(etac conjunct1 1) monos NONE th, 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

357 
mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis'')) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

358 
(inst_conj_all_tac (length pis'')) monos (SOME t) th)))) 
32952  359 
(gprems ~~ oprems)) >> map_filter I; 
22530  360 
val vc_compat_ths' = map (fn th => 
361 
let 

25824  362 
val th' = first_order_mrs gprems1 th; 
22530  363 
val (bop, lhs, rhs) = (case concl_of th' of 
364 
_ $ (fresh $ lhs $ rhs) => 

365 
(fn t => fn u => fresh $ t $ u, lhs, rhs) 

366 
 _ $ (_ $ (_ $ lhs $ rhs)) => 

367 
(curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs)); 

368 
val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop 

31938  369 
(bop (fold_rev (NominalDatatype.mk_perm []) pis lhs) 
370 
(fold_rev (NominalDatatype.mk_perm []) pis rhs))) 

22530  371 
(fn _ => simp_tac (HOL_basic_ss addsimps 
372 
(fresh_bij @ perm_bij)) 1 THEN rtac th' 1) 

373 
in Simplifier.simplify (eqvt_ss addsimps fresh_atm) th'' end) 

374 
vc_compat_ths; 

31938  375 
val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths'; 
27449
4880da911af0
Rewrote code to use swap_simps rather than calc_atm (which tends to
berghofe
parents:
27353
diff
changeset

376 
(** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **) 
4880da911af0
Rewrote code to use swap_simps rather than calc_atm (which tends to
berghofe
parents:
27353
diff
changeset

377 
(** we have to presimplify the rewrite rules **) 
4880da911af0
Rewrote code to use swap_simps rather than calc_atm (which tends to
berghofe
parents:
27353
diff
changeset

378 
val swap_simps_ss = HOL_ss addsimps swap_simps @ 
4880da911af0
Rewrote code to use swap_simps rather than calc_atm (which tends to
berghofe
parents:
27353
diff
changeset

379 
map (Simplifier.simplify (HOL_ss addsimps swap_simps)) 
22530  380 
(vc_compat_ths'' @ freshs2'); 
381 
val th = Goal.prove ctxt'' [] [] 

382 
(HOLogic.mk_Trueprop (list_comb (P $ hd ts, 

31938  383 
map (fold (NominalDatatype.mk_perm []) pis') (tl ts)))) 
22530  384 
(fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1, 
385 
REPEAT_DETERM_N (nprems_of ihyp  length gprems) 

27449
4880da911af0
Rewrote code to use swap_simps rather than calc_atm (which tends to
berghofe
parents:
27353
diff
changeset

386 
(simp_tac swap_simps_ss 1), 
22530  387 
REPEAT_DETERM_N (length gprems) 
27847
0dffedf9aff5
Changed proof of strong induction rule to avoid infinite loop
berghofe
parents:
27722
diff
changeset

388 
(simp_tac (HOL_basic_ss 
0dffedf9aff5
Changed proof of strong induction rule to avoid infinite loop
berghofe
parents:
27722
diff
changeset

389 
addsimps [inductive_forall_def'] 
31938  390 
addsimprocs [NominalDatatype.perm_simproc]) 1 THEN 
27847
0dffedf9aff5
Changed proof of strong induction rule to avoid infinite loop
berghofe
parents:
27722
diff
changeset

391 
resolve_tac gprems2 1)])); 
22530  392 
val final = Goal.prove ctxt'' [] [] (term_of concl) 
393 
(fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss 

394 
addsimps vc_compat_ths'' @ freshs2' @ 

395 
perm_fresh_fresh @ fresh_atm) 1); 

42361  396 
val final' = Proof_Context.export ctxt'' ctxt' [final]; 
22530  397 
in resolve_tac final' 1 end) context 1]) 
398 
(prems ~~ thss ~~ ihyps ~~ prems''))) 

399 
in 

400 
cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN 

401 
REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN 

27228
4f7976a6ffc3
allE_Nil: only one copy, proven in regular theory source;
wenzelm
parents:
27153
diff
changeset

402 
etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32035
diff
changeset

403 
asm_full_simp_tac (simpset_of ctxt) 1) 
42361  404 
end) > singleton (Proof_Context.export ctxt' ctxt); 
22530  405 

25824  406 
(** strong case analysis rule **) 
407 

408 
val cases_prems = map (fn ((name, avoids), rule) => 

409 
let 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

410 
val ([rule'], ctxt') = Variable.import_terms false [prop_of rule] ctxt; 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

411 
val prem :: prems = Logic.strip_imp_prems rule'; 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

412 
val concl = Logic.strip_imp_concl rule' 
25824  413 
in 
414 
(prem, 

415 
List.drop (snd (strip_comb (HOLogic.dest_Trueprop prem)), length ind_params), 

416 
concl, 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

417 
fold_map (fn (prem, (_, avoid)) => fn ctxt => 
25824  418 
let 
419 
val prems = Logic.strip_assums_hyp prem; 

420 
val params = Logic.strip_params prem; 

421 
val bnds = fold (add_binders thy 0) prems [] @ mk_avoids params avoid; 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

422 
fun mk_subst (p as (s, T)) (i, j, ctxt, ps, qs, is, ts) = 
25824  423 
if member (op = o apsnd fst) bnds (Bound i) then 
424 
let 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

425 
val ([s'], ctxt') = Variable.variant_fixes [s] ctxt; 
25824  426 
val t = Free (s', T) 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

427 
in (i + 1, j, ctxt', ps, (t, T) :: qs, i :: is, t :: ts) end 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

428 
else (i + 1, j + 1, ctxt, p :: ps, qs, is, Bound j :: ts); 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

429 
val (_, _, ctxt', ps, qs, is, ts) = fold_rev mk_subst params 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

430 
(0, 0, ctxt, [], [], [], []) 
25824  431 
in 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

432 
((ps, qs, is, map (curry subst_bounds (rev ts)) prems), ctxt') 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

433 
end) (prems ~~ avoids) ctxt') 
25824  434 
end) 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

435 
(Inductive.partition_rules' raw_induct (intrs ~~ avoids') ~~ 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

436 
elims); 
25824  437 

438 
val cases_prems' = 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

439 
map (fn (prem, args, concl, (prems, _)) => 
25824  440 
let 
441 
fun mk_prem (ps, [], _, prems) = 

46218
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
44929
diff
changeset

442 
Logic.list_all (ps, Logic.list_implies (prems, concl)) 
25824  443 
 mk_prem (ps, qs, _, prems) = 
46218
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
44929
diff
changeset

444 
Logic.list_all (ps, Logic.mk_implies 
25824  445 
(Logic.list_implies 
446 
(mk_distinct qs @ 

447 
maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop 

31938  448 
(NominalDatatype.fresh_const T (fastype_of u) $ t $ u)) 
25824  449 
args) qs, 
450 
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 

451 
(map HOLogic.dest_Trueprop prems))), 

452 
concl)) 

453 
in map mk_prem prems end) cases_prems; 

454 

35232
f588e1169c8b
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents:
33968
diff
changeset

455 
val cases_eqvt_ss = Simplifier.global_context thy HOL_ss 
27449
4880da911af0
Rewrote code to use swap_simps rather than calc_atm (which tends to
berghofe
parents:
27353
diff
changeset

456 
addsimps eqvt_thms @ swap_simps @ perm_pi_simp 
27352
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

457 
addsimprocs [NominalPermeq.perm_simproc_app, 
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

458 
NominalPermeq.perm_simproc_fun]; 
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

459 

8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

460 
val simp_fresh_atm = map 
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

461 
(Simplifier.simplify (HOL_basic_ss addsimps fresh_atm)); 
25824  462 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

463 
fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))), 
25824  464 
prems') = 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

465 
(name, Goal.prove ctxt' [] (prem :: prems') concl 
26711  466 
(fn {prems = hyp :: hyps, context = ctxt1} => 
25824  467 
EVERY (rtac (hyp RS elim) 1 :: 
468 
map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) => 

469 
SUBPROOF (fn {prems = case_hyps, params, context = ctxt2, concl, ...} => 

470 
if null qs then 

471 
rtac (first_order_mrs case_hyps case_hyp) 1 

472 
else 

473 
let 

32202  474 
val params' = map (term_of o #2 o nth (rev params)) is; 
25824  475 
val tab = params' ~~ map fst qs; 
476 
val (hyps1, hyps2) = chop (length args) case_hyps; 

477 
(* turns a = t and [x1 # t, ..., xn # t] *) 

478 
(* into [x1 # a, ..., xn # a] *) 

479 
fun inst_fresh th' ths = 

480 
let val (ths1, ths2) = chop (length qs) ths 

481 
in 

482 
(map (fn th => 

483 
let 

484 
val (cf, ct) = 

485 
Thm.dest_comb (Thm.dest_arg (cprop_of th)); 

486 
val arg_cong' = Drule.instantiate' 

487 
[SOME (ctyp_of_term ct)] 

488 
[NONE, SOME ct, SOME cf] (arg_cong RS iffD2); 

489 
val inst = Thm.first_order_match (ct, 

490 
Thm.dest_arg (Thm.dest_arg (cprop_of th'))) 

491 
in [th', th] MRS Thm.instantiate inst arg_cong' 

492 
end) ths1, 

493 
ths2) 

494 
end; 

495 
val (vc_compat_ths1, vc_compat_ths2) = 

496 
chop (length vc_compat_ths  length args * length qs) 

497 
(map (first_order_mrs hyps2) vc_compat_ths); 

498 
val vc_compat_ths' = 

31938  499 
NominalDatatype.mk_not_sym vc_compat_ths1 @ 
25824  500 
flat (fst (fold_map inst_fresh hyps1 vc_compat_ths2)); 
501 
val (freshs1, freshs2, ctxt3) = fold 

502 
(obtain_fresh_name (args @ map fst qs @ params')) 

503 
(map snd qs) ([], [], ctxt2); 

31938  504 
val freshs2' = NominalDatatype.mk_not_sym freshs2; 
505 
val pis = map (NominalDatatype.perm_of_pair) 

25824  506 
((freshs1 ~~ map fst qs) @ (params' ~~ freshs1)); 
507 
val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis); 

508 
val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms 

509 
(fn x as Free _ => 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36428
diff
changeset

510 
if member (op =) args x then x 
25824  511 
else (case AList.lookup op = tab x of 
512 
SOME y => y 

31938  513 
 NONE => fold_rev (NominalDatatype.mk_perm []) pis x) 
25824  514 
 x => x) o HOLogic.dest_Trueprop o prop_of) case_hyps)); 
515 
val inst = Thm.first_order_match (Thm.dest_arg 

516 
(Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj); 

517 
val th = Goal.prove ctxt3 [] [] (term_of concl) 

518 
(fn {context = ctxt4, ...} => 

519 
rtac (Thm.instantiate inst case_hyp) 1 THEN 

520 
SUBPROOF (fn {prems = fresh_hyps, ...} => 

521 
let 

31938  522 
val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps; 
27352
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

523 
val case_ss = cases_eqvt_ss addsimps freshs2' @ 
8adeff7fd4bc
 Equivariance simpset used in proofs of strong induction and inversion
berghofe
parents:
27228
diff
changeset

524 
simp_fresh_atm (vc_compat_ths' @ fresh_hyps'); 
25824  525 
val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh; 
526 
val hyps1' = map 

527 
(mk_pis #> Simplifier.simplify fresh_fresh_ss) hyps1; 

528 
val hyps2' = map 

529 
(mk_pis #> Simplifier.simplify case_ss) hyps2; 

27449
4880da911af0
Rewrote code to use swap_simps rather than calc_atm (which tends to
berghofe
parents:
27353
diff
changeset

530 
val case_hyps' = hyps1' @ hyps2' 
25824  531 
in 
27449
4880da911af0
Rewrote code to use swap_simps rather than calc_atm (which tends to
berghofe
parents:
27353
diff
changeset

532 
simp_tac case_ss 1 THEN 
25824  533 
REPEAT_DETERM (TRY (rtac conjI 1) THEN 
534 
resolve_tac case_hyps' 1) 

535 
end) ctxt4 1) 

42361  536 
val final = Proof_Context.export ctxt3 ctxt2 [th] 
25824  537 
in resolve_tac final 1 end) ctxt1 1) 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

538 
(thss ~~ hyps ~~ prems))) > 
42361  539 
singleton (Proof_Context.export ctxt' ctxt)) 
25824  540 

22530  541 
in 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

542 
ctxt'' > 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35232
diff
changeset

543 
Proof.theorem NONE (fn thss => fn ctxt => 
22530  544 
let 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

545 
val rec_name = space_implode "_" (map Long_Name.base_name names); 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30087
diff
changeset

546 
val rec_qualified = Binding.qualify false rec_name; 
33368  547 
val ind_case_names = Rule_Cases.case_names induct_cases; 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

548 
val induct_cases' = Inductive.partition_rules' raw_induct 
25824  549 
(intrs ~~ induct_cases); 
550 
val thss' = map (map atomize_intr) thss; 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

551 
val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss'); 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

552 
val strong_raw_induct = 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

553 
mk_ind_proof ctxt thss' > Inductive.rulify; 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

554 
val strong_cases = map (mk_cases_proof ##> Inductive.rulify) 
25824  555 
(thsss ~~ elims ~~ cases_prems ~~ cases_prems'); 
22530  556 
val strong_induct = 
557 
if length names > 1 then 

33368  558 
(strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0]) 
22530  559 
else (strong_raw_induct RSN (2, rev_mp), 
33368  560 
[ind_case_names, Rule_Cases.consumes 1]); 
33671  561 
val ((_, [strong_induct']), ctxt') = ctxt > Local_Theory.note 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

562 
((rec_qualified (Binding.name "strong_induct"), 
33670
02b7738aef6a
eliminated slightly odd kind argument of LocalTheory.note(s);
wenzelm
parents:
33666
diff
changeset

563 
map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]); 
22530  564 
val strong_inducts = 
33670
02b7738aef6a
eliminated slightly odd kind argument of LocalTheory.note(s);
wenzelm
parents:
33666
diff
changeset

565 
Project_Rule.projects ctxt (1 upto length names) strong_induct'; 
22530  566 
in 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

567 
ctxt' > 
33671  568 
Local_Theory.note 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

569 
((rec_qualified (Binding.name "strong_inducts"), 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

570 
[Attrib.internal (K ind_case_names), 
33368  571 
Attrib.internal (K (Rule_Cases.consumes 1))]), 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

572 
strong_inducts) > snd > 
33671  573 
Local_Theory.notes (map (fn ((name, elim), (_, cases)) => 
30435
e62d6ecab6ad
explicit Binding.qualified_name  prevents implicitly qualified bstring;
wenzelm
parents:
30364
diff
changeset

574 
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"), 
33368  575 
[Attrib.internal (K (Rule_Cases.case_names (map snd cases))), 
576 
Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])])) 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

577 
(strong_cases ~~ induct_cases')) > snd 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

578 
end) 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

579 
(map (map (rulify_term thy #> rpair [])) vc_compat) 
22530  580 
end; 
581 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

582 
fun prove_eqvt s xatoms ctxt = 
22530  583 
let 
42361  584 
val thy = Proof_Context.theory_of ctxt; 
22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

585 
val ({names, ...}, {raw_induct, intrs, elims, ...}) = 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

586 
Inductive.the_inductive ctxt (Sign.intern_const thy s); 
24832  587 
val raw_induct = atomize_induct ctxt raw_induct; 
588 
val elims = map (atomize_induct ctxt) elims; 

24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

589 
val intrs = map atomize_intr intrs; 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

590 
val monos = Inductive.get_monos ctxt; 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

591 
val intrs' = Inductive.unpartition_rules intrs 
22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

592 
(map (fn (((s, ths), (_, k)), th) => 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

593 
(s, ths ~~ Inductive.infer_intro_vars th k ths)) 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

594 
(Inductive.partition_rules raw_induct intrs ~~ 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

595 
Inductive.arities_of raw_induct ~~ elims)); 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

596 
val k = length (Inductive.params_of raw_induct); 
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

597 
val atoms' = NominalAtoms.atoms_of thy; 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

598 
val atoms = 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

599 
if null xatoms then atoms' else 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

600 
let val atoms = map (Sign.intern_type thy) xatoms 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

601 
in 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

602 
(case duplicates op = atoms of 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

603 
[] => () 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

604 
 xs => error ("Duplicate atoms: " ^ commas xs); 
33040  605 
case subtract (op =) atoms' atoms of 
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

606 
[] => () 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

607 
 xs => error ("No such atoms: " ^ commas xs); 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

608 
atoms) 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

609 
end; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39159
diff
changeset

610 
val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; 
35232
f588e1169c8b
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents:
33968
diff
changeset

611 
val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps 
24571  612 
(NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs 
26364
cb6f360ab425
Equivariance prover now uses permutation simprocs as well.
berghofe
parents:
26359
diff
changeset

613 
[mk_perm_bool_simproc names, 
cb6f360ab425
Equivariance prover now uses permutation simprocs as well.
berghofe
parents:
26359
diff
changeset

614 
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

615 
val (([t], [pi]), ctxt') = ctxt > 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

616 
Variable.import_terms false [concl_of raw_induct] >> 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

617 
Variable.variant_fixes ["pi"]; 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

618 
val ps = map (fst o HOLogic.dest_imp) 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

619 
(HOLogic.dest_conj (HOLogic.dest_Trueprop t)); 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

620 
fun eqvt_tac ctxt'' pi (intr, vs) st = 
22544  621 
let 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

622 
fun eqvt_err s = 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

623 
let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

624 
in error ("Could not prove equivariance for introduction rule\n" ^ 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

625 
Syntax.string_of_term ctxt''' t ^ "\n" ^ s) 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

626 
end; 
22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

627 
val res = SUBPROOF (fn {prems, params, ...} => 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

628 
let 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

629 
val prems' = map (fn th => the_default th (map_thm ctxt' 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

630 
(split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; 
25824  631 
val prems'' = map (fn th => Simplifier.simplify eqvt_ss 
632 
(mk_perm_bool (cterm_of thy pi) th)) prems'; 

22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

633 
val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~ 
32202  634 
map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of o #2) params) 
22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

635 
intr 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

636 
in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

637 
end) ctxt' 1 st 
22544  638 
in 
639 
case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of 

640 
NONE => eqvt_err ("Rule does not match goal\n" ^ 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

641 
Syntax.string_of_term ctxt'' (hd (prems_of st))) 
22544  642 
 SOME (th, _) => Seq.single th 
643 
end; 

22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

644 
val thss = map (fn atom => 
25824  645 
let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, []))) 
22530  646 
in map (fn th => zero_var_indexes (th RS mp)) 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33772
diff
changeset

647 
(Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

648 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p => 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

649 
let 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

650 
val (h, ts) = strip_comb p; 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

651 
val (ts1, ts2) = chop k ts 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

652 
in 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

653 
HOLogic.mk_imp (p, list_comb (h, ts1 @ 
31938  654 
map (NominalDatatype.mk_perm [] pi') ts2)) 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

655 
end) ps))) 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

656 
(fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs => 
22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

657 
full_simp_tac eqvt_ss 1 THEN 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

658 
eqvt_tac context pi' intr_vs) intrs')) > 
42361  659 
singleton (Proof_Context.export ctxt' ctxt))) 
22544  660 
end) atoms 
661 
in 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

662 
ctxt > 
33671  663 
Local_Theory.notes (map (fn (name, ths) => 
30435
e62d6ecab6ad
explicit Binding.qualified_name  prevents implicitly qualified bstring;
wenzelm
parents:
30364
diff
changeset

664 
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"), 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

665 
[Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])])) 
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

666 
(names ~~ transp thss)) > snd 
22544  667 
end; 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

668 

1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

669 

1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

670 
(* outer syntax *) 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

671 

24867  672 
val _ = 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

673 
Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"} 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36692
diff
changeset

674 
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" 
46949  675 
(Parse.xname  Scan.optional (@{keyword "avoids"}  Parse.and_list1 (Parse.name  
676 
(@{keyword ":"}  Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) => 

30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

677 
prove_strong_ind name avoids)); 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

678 

24867  679 
val _ = 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

680 
Outer_Syntax.local_theory @{command_spec "equivariance"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

681 
"prove equivariance for inductive predicate involving nominal datatypes" 
46949  682 
(Parse.xname  Scan.optional (@{keyword "["}  Parse.list1 Parse.name  @{keyword "]"}) [] >> 
30087
a780642a9c9c
nominal_inductive and equivariance now work on local_theory.
berghofe
parents:
29585
diff
changeset

683 
(fn (name, atoms) => prove_eqvt name atoms)); 
22530  684 

22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

685 
end 