author  wenzelm 
Thu, 17 Apr 2008 22:22:21 +0200  
changeset 26711  3a478bfa1650 
parent 26568  3a3a83493f00 
child 26939  1035c89b4c02 
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 
ID: $Id$ 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

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

4 

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

22313
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 

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

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

10 
sig 
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

11 
val prove_strong_ind: string > (string * string list) list > theory > Proof.state 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

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

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

14 

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

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

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

17 

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

18 
val inductive_forall_name = "HOL.induct_forall"; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

19 
val inductive_forall_def = thm "induct_forall_def"; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

20 
val inductive_atomize = thms "induct_atomize"; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

21 
val inductive_rulify = thms "induct_rulify"; 
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 
fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify []; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

24 

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

25 
val atomize_conv = 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

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

28 
val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); 
24832  29 
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 
26568  30 
(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

31 

22530  32 
val finite_Un = thm "finite_Un"; 
33 
val supp_prod = thm "supp_prod"; 

34 
val fresh_prod = thm "fresh_prod"; 

35 

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

36 
val perm_bool = mk_meta_eq (thm "perm_bool"); 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

37 
val perm_boolI = thm "perm_boolI"; 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

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

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

40 

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

43 

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

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

45 
(theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss => 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

46 
fn Const ("Nominal.perm", _) $ _ $ t => 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

47 
if the_default "" (try (head_of #> dest_Const #> fst) t) mem names 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

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

50 

22530  51 
val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE; 
52 

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

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

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

55 

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

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

59 
(case NominalPackage.get_nominal_datatype thy tname of 

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

61 
 SOME {descr, index, ...} => (case AList.lookup op = 

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

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

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

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

66 
in (add_binders thy i u 

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

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

69 
else insert (op aconv o pairself fst) 

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

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

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

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

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

75 
 add_binders thy i _ bs = bs; 

76 

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

77 
fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

78 
Const (name, _) => 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

79 
if name mem names then SOME (f p q) else NONE 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

81 
 split_conj _ _ _ _ = NONE; 
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 
fun strip_all [] t = t 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

84 
 strip_all (_ :: xs) (Const ("All", _) $ Abs (s, T, t)) = strip_all xs t; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

85 

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

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

87 
(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

89 
(* to R ... & id (ALL z. (pi_1 o ... o pi_n o t)) *) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

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

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

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

94 

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

95 
fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ = 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

97 
Const (name, _) => 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

98 
if name mem names then SOME (HOLogic.mk_conj (p, 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

99 
Const ("Fun.id", HOLogic.boolT > HOLogic.boolT) $ 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

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

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

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

104 
if member (op aconv) ps (head_of u) then 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

105 
SOME (Const ("Fun.id", HOLogic.boolT > HOLogic.boolT) $ 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

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

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

109 

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

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

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

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

114 

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

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

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

117 
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

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

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

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

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

122 
 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

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

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

125 
 map_term' _ _ _ = NONE; 
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 
(*********************************************************************) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

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

130 

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

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

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

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

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

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

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

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

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

139 
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

140 

25824  141 
fun first_order_matchs pats objs = Thm.first_order_match 
142 
(Conjunction.mk_conjunction_balanced pats, 

143 
Conjunction.mk_conjunction_balanced objs); 

144 

145 
fun first_order_mrs ths th = ths MRS 

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

147 

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

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

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

150 
val ctxt = ProofContext.init thy; 
25824  151 
val ({names, ...}, {raw_induct, intrs, elims, ...}) = 
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

152 
InductivePackage.the_inductive ctxt (Sign.intern_const thy s); 
25824  153 
val ind_params = InductivePackage.params_of raw_induct; 
24832  154 
val raw_induct = atomize_induct ctxt raw_induct; 
25824  155 
val elims = map (atomize_induct ctxt) elims; 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

156 
val monos = InductivePackage.get_monos ctxt; 
24571  157 
val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt; 
22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

158 
val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

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

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

161 
commas_quote xs)); 
22530  162 
val induct_cases = map fst (fst (RuleCases.get (the 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24832
diff
changeset

163 
(Induct.lookup_inductP ctxt (hd names))))); 
22530  164 
val raw_induct' = Logic.unvarify (prop_of raw_induct); 
25824  165 
val elims' = map (Logic.unvarify o prop_of) elims; 
22530  166 
val concls = raw_induct' > Logic.strip_imp_concl > HOLogic.dest_Trueprop > 
167 
HOLogic.dest_conj > map (HOLogic.dest_imp ##> strip_comb); 

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

169 

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

171 
[] => () 

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

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

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

175 
val _ = (case map fst avoids \\ induct_cases of 

176 
[] => () 

177 
 xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs)); 

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

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

22530  181 
fun mk_avoids params (name, ps) = 
182 
let val k = length params  1 

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

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

185 
" of inductive definition: " ^ quote x) 

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

187 
end; 

188 

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

190 
let 

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

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

193 
val params = Logic.strip_params prem 

194 
in 

195 
(params, 

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

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

198 
prems, strip_comb (HOLogic.dest_Trueprop concl)) 

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

200 

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

202 
val ind_sort = if null atomTs then HOLogic.typeS 

203 
else Sign.certify_sort thy (map (fn T => Sign.intern_class thy 

204 
("fs_" ^ Sign.base_name (fst (dest_Type T)))) atomTs); 

205 
val fs_ctxt_tyname = Name.variant (map fst (term_tfrees raw_induct')) "'n"; 

206 
val fs_ctxt_name = Name.variant (add_term_names (raw_induct', [])) "z"; 

207 
val fsT = TFree (fs_ctxt_tyname, ind_sort); 

208 

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

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

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

211 

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

214 
val lift_pred = lift_pred' (Bound 0); 

215 

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

216 
fun lift_prem (t as (f $ u)) = 
22530  217 
let val (p, ts) = strip_comb t 
218 
in 

219 
if p mem ps then 

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

220 
Const (inductive_forall_name, 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

221 
(fsT > HOLogic.boolT) > HOLogic.boolT) $ 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

222 
Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) 
22530  223 
else lift_prem f $ lift_prem u 
224 
end 

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

226 
 lift_prem t = t; 

227 

228 
fun mk_distinct [] = [] 

229 
 mk_distinct ((x, T) :: xs) = List.mapPartial (fn (y, U) => 

230 
if T = U then SOME (HOLogic.mk_Trueprop 

231 
(HOLogic.mk_not (HOLogic.eq_const T $ x $ y))) 

232 
else NONE) xs @ mk_distinct xs; 

233 

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

25824  235 
(NominalPackage.fresh_const T fsT $ x $ Bound 0); 
22530  236 

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

238 
let 

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

240 
val prem = Logic.list_implies 

241 
(map mk_fresh bvars @ mk_distinct bvars @ 

242 
map (fn prem => 

243 
if null (term_frees prem inter ps) then prem 

244 
else lift_prem prem) prems, 

245 
HOLogic.mk_Trueprop (lift_pred p ts)); 

246 
val vs = map (Var o apfst (rpair 0)) (rename_wrt_term prem params') 

247 
in 

248 
(list_all (params', prem), (rev vs, subst_bounds (vs, prem))) 

249 
end) prems); 

250 

251 
val ind_vars = 

252 
(DatatypeProp.indexify_names (replicate (length atomTs) "pi") ~~ 

253 
map NominalAtoms.mk_permT atomTs) @ [("z", fsT)]; 

254 
val ind_Ts = rev (map snd ind_vars); 

255 

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

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

258 
HOLogic.list_all (ind_vars, lift_pred p 

259 
(map (fold_rev (NominalPackage.mk_perm ind_Ts) 

260 
(map Bound (length atomTs downto 1))) ts)))) concls)); 

261 

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

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

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

265 

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

267 
map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies 

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

268 
(List.mapPartial (fn prem => 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

269 
if null (ps inter term_frees prem) then SOME prem 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

25824  273 
(NominalPackage.fresh_const U T $ u $ t)) bvars) 
22530  274 
(ts ~~ binder_types (fastype_of p)))) prems; 
275 

26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

276 
val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

277 
val pt2_atoms = map (fn aT => PureThy.get_thm thy 
26337  278 
("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs; 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

279 
val eqvt_ss = HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

280 
addsimprocs [mk_perm_bool_simproc ["Fun.id"]]; 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

281 
val fresh_bij = PureThy.get_thms thy "fresh_bij"; 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

282 
val perm_bij = PureThy.get_thms thy "perm_bij"; 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

283 
val fs_atoms = map (fn aT => PureThy.get_thm thy 
26337  284 
("fs_" ^ Sign.base_name (fst (dest_Type aT)) ^ "1")) atomTs; 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

285 
val exists_fresh' = PureThy.get_thms thy "exists_fresh'"; 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

286 
val fresh_atm = PureThy.get_thms thy "fresh_atm"; 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

287 
val calc_atm = PureThy.get_thms thy "calc_atm"; 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

288 
val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh"; 
22530  289 

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

291 
let 

292 
(** protect terms to avoid that supp_prod interferes with **) 

293 
(** pairs used in introduction rules of inductive predicate **) 

294 
fun protect t = 

295 
let val T = fastype_of t in Const ("Fun.id", T > T) $ t end; 

296 
val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1); 

297 
val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop 

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

25824  299 
NominalPackage.fresh_const T (fastype_of p) $ 
22530  300 
Bound 0 $ p))) 
301 
(fn _ => EVERY 

302 
[resolve_tac exists_fresh' 1, 

303 
simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]); 

304 
val (([cx], ths), ctxt') = Obtain.result 

305 
(fn _ => EVERY 

306 
[etac exE 1, 

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

26359  308 
full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1, 
22530  309 
REPEAT (etac conjE 1)]) 
310 
[ex] ctxt 

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

312 

25824  313 
fun mk_ind_proof thy thss = 
26711  314 
Goal.prove_global thy [] prems' concl' (fn {prems = ihyps, context = ctxt} => 
22530  315 
let val th = Goal.prove ctxt [] [] concl (fn {context, ...} => 
316 
rtac raw_induct 1 THEN 

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

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

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

320 
let 

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

322 
chop (length params  length atomTs  1) (map term_of params) > 

323 
split_last; 

324 
val bvars' = map 

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

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

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

328 
fold_rev (NominalPackage.mk_perm []) pis t) bvars'; 

329 
val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl)); 

330 
val (freshs1, freshs2, ctxt'') = fold 

331 
(obtain_fresh_name (ts @ pi_bvars)) 

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

333 
val freshs2' = NominalPackage.mk_not_sym freshs2; 

334 
val pis' = map NominalPackage.perm_of_pair (pi_bvars ~~ freshs1); 

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

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

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

337 
in if T = fastype_of pi2 then 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

338 
Const ("List.append", T > T > T) $ pi1 $ pi2 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

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

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

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

345 
(map (Envir.subst_vars env) vs ~~ 

346 
map (fold_rev (NominalPackage.mk_perm []) 

347 
(rev pis' @ pis)) params' @ [z])) ihyp; 

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

348 
fun mk_pi th = 
26359  349 
Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}] 
24570
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

350 
addsimprocs [NominalPackage.perm_simproc]) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

351 
(Simplifier.simplify eqvt_ss 
25824  352 
(fold_rev (mk_perm_bool o cterm_of thy) 
353 
(rev pis' @ pis) th)); 

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

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

355 
(map (fn (th, t) => 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

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

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

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

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

360 
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

361 
(inst_conj_all_tac (length pis'')) monos (SOME t) th)))) 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

362 
(gprems ~~ oprems)) >> List.mapPartial I; 
22530  363 
val vc_compat_ths' = map (fn th => 
364 
let 

25824  365 
val th' = first_order_mrs gprems1 th; 
22530  366 
val (bop, lhs, rhs) = (case concl_of th' of 
367 
_ $ (fresh $ lhs $ rhs) => 

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

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

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

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

372 
(bop (fold_rev (NominalPackage.mk_perm []) pis lhs) 

373 
(fold_rev (NominalPackage.mk_perm []) pis rhs))) 

374 
(fn _ => simp_tac (HOL_basic_ss addsimps 

375 
(fresh_bij @ perm_bij)) 1 THEN rtac th' 1) 

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

377 
vc_compat_ths; 

378 
val vc_compat_ths'' = NominalPackage.mk_not_sym vc_compat_ths'; 

379 
(** Since calc_atm simplifies (pi :: 'a prm) o (x :: 'b) to x **) 

380 
(** we have to presimplify the rewrite rules **) 

381 
val calc_atm_ss = HOL_ss addsimps calc_atm @ 

382 
map (Simplifier.simplify (HOL_ss addsimps calc_atm)) 

383 
(vc_compat_ths'' @ freshs2'); 

384 
val th = Goal.prove ctxt'' [] [] 

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

386 
map (fold (NominalPackage.mk_perm []) pis') (tl ts)))) 

387 
(fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1, 

388 
REPEAT_DETERM_N (nprems_of ihyp  length gprems) 

389 
(simp_tac calc_atm_ss 1), 

390 
REPEAT_DETERM_N (length gprems) 

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

391 
(simp_tac (HOL_ss 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

392 
addsimps inductive_forall_def' :: gprems2 
22530  393 
addsimprocs [NominalPackage.perm_simproc]) 1)])); 
394 
val final = Goal.prove ctxt'' [] [] (term_of concl) 

395 
(fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss 

396 
addsimps vc_compat_ths'' @ freshs2' @ 

397 
perm_fresh_fresh @ fresh_atm) 1); 

398 
val final' = ProofContext.export ctxt'' ctxt' [final]; 

399 
in resolve_tac final' 1 end) context 1]) 

400 
(prems ~~ thss ~~ ihyps ~~ prems''))) 

401 
in 

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

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

404 
etac impE 1 THEN atac 1 THEN REPEAT (etac allE_Nil 1) THEN 

405 
asm_full_simp_tac (simpset_of thy) 1) 

26711  406 
end); 
22530  407 

25824  408 
(** strong case analysis rule **) 
409 

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

411 
let 

412 
val prem :: prems = Logic.strip_imp_prems rule; 

413 
val concl = Logic.strip_imp_concl rule; 

414 
val used = add_term_free_names (rule, []) 

415 
in 

416 
(prem, 

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

418 
concl, 

419 
fst (fold_map (fn (prem, (_, avoid)) => fn used => 

420 
let 

421 
val prems = Logic.strip_assums_hyp prem; 

422 
val params = Logic.strip_params prem; 

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

424 
fun mk_subst (p as (s, T)) (i, j, used, ps, qs, is, ts) = 

425 
if member (op = o apsnd fst) bnds (Bound i) then 

426 
let 

427 
val s' = Name.variant used s; 

428 
val t = Free (s', T) 

429 
in (i + 1, j, s' :: used, ps, (t, T) :: qs, i :: is, t :: ts) end 

430 
else (i + 1, j + 1, used, p :: ps, qs, is, Bound j :: ts); 

431 
val (_, _, used', ps, qs, is, ts) = fold_rev mk_subst params 

432 
(0, 0, used, [], [], [], []) 

433 
in 

434 
((ps, qs, is, map (curry subst_bounds (rev ts)) prems), used') 

435 
end) (prems ~~ avoids) used)) 

436 
end) 

437 
(InductivePackage.partition_rules' raw_induct (intrs ~~ avoids') ~~ 

438 
elims'); 

439 

440 
val cases_prems' = 

441 
map (fn (prem, args, concl, prems) => 

442 
let 

443 
fun mk_prem (ps, [], _, prems) = 

444 
list_all (ps, Logic.list_implies (prems, concl)) 

445 
 mk_prem (ps, qs, _, prems) = 

446 
list_all (ps, Logic.mk_implies 

447 
(Logic.list_implies 

448 
(mk_distinct qs @ 

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

450 
(NominalPackage.fresh_const T (fastype_of u) $ t $ u)) 

451 
args) qs, 

452 
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 

453 
(map HOLogic.dest_Trueprop prems))), 

454 
concl)) 

455 
in map mk_prem prems end) cases_prems; 

456 

457 
val cases_eqvt_ss = HOL_ss addsimps eqvt_thms @ calc_atm delsplits [split_if]; 

458 

459 
fun mk_cases_proof thy ((((name, thss), elim), (prem, args, concl, prems)), 

460 
prems') = 

26711  461 
(name, Goal.prove_global thy [] (prem :: prems') concl 
462 
(fn {prems = hyp :: hyps, context = ctxt1} => 

25824  463 
EVERY (rtac (hyp RS elim) 1 :: 
464 
map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) => 

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

466 
if null qs then 

467 
rtac (first_order_mrs case_hyps case_hyp) 1 

468 
else 

469 
let 

470 
val params' = map (term_of o nth (rev params)) is; 

471 
val tab = params' ~~ map fst qs; 

472 
val (hyps1, hyps2) = chop (length args) case_hyps; 

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

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

475 
fun inst_fresh th' ths = 

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

477 
in 

478 
(map (fn th => 

479 
let 

480 
val (cf, ct) = 

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

482 
val arg_cong' = Drule.instantiate' 

483 
[SOME (ctyp_of_term ct)] 

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

485 
val inst = Thm.first_order_match (ct, 

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

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

488 
end) ths1, 

489 
ths2) 

490 
end; 

491 
val (vc_compat_ths1, vc_compat_ths2) = 

492 
chop (length vc_compat_ths  length args * length qs) 

493 
(map (first_order_mrs hyps2) vc_compat_ths); 

494 
val vc_compat_ths' = 

495 
NominalPackage.mk_not_sym vc_compat_ths1 @ 

496 
flat (fst (fold_map inst_fresh hyps1 vc_compat_ths2)); 

497 
val (freshs1, freshs2, ctxt3) = fold 

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

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

500 
val freshs2' = NominalPackage.mk_not_sym freshs2; 

501 
val pis = map (NominalPackage.perm_of_pair) 

502 
((freshs1 ~~ map fst qs) @ (params' ~~ freshs1)); 

503 
val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis); 

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

505 
(fn x as Free _ => 

506 
if x mem args then x 

507 
else (case AList.lookup op = tab x of 

508 
SOME y => y 

509 
 NONE => fold_rev (NominalPackage.mk_perm []) pis x) 

510 
 x => x) o HOLogic.dest_Trueprop o prop_of) case_hyps)); 

511 
val inst = Thm.first_order_match (Thm.dest_arg 

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

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

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

515 
rtac (Thm.instantiate inst case_hyp) 1 THEN 

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

517 
let 

518 
val fresh_hyps' = NominalPackage.mk_not_sym fresh_hyps; 

519 
val case_ss = cases_eqvt_ss addsimps 

520 
vc_compat_ths' @ freshs2' @ fresh_hyps' 

521 
val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh; 

522 
val hyps1' = map 

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

524 
val hyps2' = map 

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

526 
val case_hyps' = hyps1' @ hyps2' 

527 
in 

528 
simp_tac case_ss 1 THEN 

529 
REPEAT_DETERM (TRY (rtac conjI 1) THEN 

530 
resolve_tac case_hyps' 1) 

531 
end) ctxt4 1) 

532 
val final = ProofContext.export ctxt3 ctxt2 [th] 

533 
in resolve_tac final 1 end) ctxt1 1) 

534 
(thss ~~ hyps ~~ prems)))) 

535 

22530  536 
in 
537 
thy > 

538 
ProofContext.init > 

539 
Proof.theorem_i NONE (fn thss => ProofContext.theory (fn thy => 

540 
let 

541 
val ctxt = ProofContext.init thy; 

542 
val rec_name = space_implode "_" (map Sign.base_name names); 

543 
val ind_case_names = RuleCases.case_names induct_cases; 

25824  544 
val induct_cases' = InductivePackage.partition_rules' raw_induct 
545 
(intrs ~~ induct_cases); 

546 
val thss' = map (map atomize_intr) thss; 

547 
val thsss = InductivePackage.partition_rules' raw_induct (intrs ~~ thss'); 

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

548 
val strong_raw_induct = 
25824  549 
mk_ind_proof thy thss' > InductivePackage.rulify; 
550 
val strong_cases = map (mk_cases_proof thy ##> InductivePackage.rulify) 

551 
(thsss ~~ elims ~~ cases_prems ~~ cases_prems'); 

22530  552 
val strong_induct = 
553 
if length names > 1 then 

554 
(strong_raw_induct, [ind_case_names, RuleCases.consumes 0]) 

555 
else (strong_raw_induct RSN (2, rev_mp), 

556 
[ind_case_names, RuleCases.consumes 1]); 

557 
val ([strong_induct'], thy') = thy > 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24571
diff
changeset

558 
Sign.add_path rec_name > 
22530  559 
PureThy.add_thms [(("strong_induct", #1 strong_induct), #2 strong_induct)]; 
560 
val strong_inducts = 

561 
ProjectRule.projects ctxt (1 upto length names) strong_induct' 

562 
in 

563 
thy' > 

564 
PureThy.add_thmss [(("strong_inducts", strong_inducts), 

565 
[ind_case_names, RuleCases.consumes 1])] > snd > 

25824  566 
Sign.parent_path > 
567 
fold (fn ((name, elim), (_, cases)) => 

568 
Sign.add_path (Sign.base_name name) #> 

569 
PureThy.add_thms [(("strong_cases", elim), 

570 
[RuleCases.case_names (map snd cases), 

571 
RuleCases.consumes 1])] #> snd #> 

572 
Sign.parent_path) (strong_cases ~~ induct_cases') 

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

574 
(map (map (rulify_term thy #> rpair [])) vc_compat) 
22530  575 
end; 
576 

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

577 
fun prove_eqvt s xatoms thy = 
22530  578 
let 
579 
val ctxt = ProofContext.init thy; 

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

580 
val ({names, ...}, {raw_induct, intrs, elims, ...}) = 
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

581 
InductivePackage.the_inductive ctxt (Sign.intern_const thy s); 
24832  582 
val raw_induct = atomize_induct ctxt raw_induct; 
583 
val elims = map (atomize_induct ctxt) elims; 

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

584 
val intrs = map atomize_intr intrs; 
621b60b1df00
Generalized equivariance and nominal_inductive commands to
berghofe
parents:
23531
diff
changeset

585 
val monos = InductivePackage.get_monos ctxt; 
22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

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

587 
(map (fn (((s, ths), (_, k)), th) => 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

588 
(s, ths ~~ InductivePackage.infer_intro_vars th k ths)) 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

589 
(InductivePackage.partition_rules raw_induct intrs ~~ 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

590 
InductivePackage.arities_of raw_induct ~~ elims)); 
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

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

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

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

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

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

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

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

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

599 
case atoms \\ atoms' of 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

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

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

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

603 
end; 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset

604 
val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; 
26364
cb6f360ab425
Equivariance prover now uses permutation simprocs as well.
berghofe
parents:
26359
diff
changeset

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

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

608 
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

609 
val t = Logic.unvarify (concl_of raw_induct); 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

610 
val pi = Name.variant (add_term_names (t, [])) "pi"; 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

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

612 
(HOLogic.dest_conj (HOLogic.dest_Trueprop t)); 
25824  613 
fun eqvt_tac pi (intr, vs) st = 
22544  614 
let 
615 
fun eqvt_err s = error 

616 
("Could not prove equivariance for introduction rule\n" ^ 

617 
Sign.string_of_term (theory_of_thm intr) 

618 
(Logic.unvarify (prop_of intr)) ^ "\n" ^ s); 

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

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

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

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

622 
(split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; 
25824  623 
val prems'' = map (fn th => Simplifier.simplify eqvt_ss 
624 
(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

625 
val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~ 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

626 
map (cterm_of thy o NominalPackage.mk_perm [] pi o term_of) params) 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

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

628 
in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1 
22544  629 
end) ctxt 1 st 
630 
in 

631 
case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of 

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

633 
Sign.string_of_term (theory_of_thm st) (hd (prems_of st))) 

634 
 SOME (th, _) => Seq.single th 

635 
end; 

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

636 
val thss = map (fn atom => 
25824  637 
let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, []))) 
22530  638 
in map (fn th => zero_var_indexes (th RS mp)) 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

639 
(DatatypeAux.split_conj_thm (Goal.prove_global thy [] [] 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

640 
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p => 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

641 
HOLogic.mk_imp (p, list_comb 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

642 
(apsnd (map (NominalPackage.mk_perm [] pi')) (strip_comb p)))) ps))) 
22788
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

643 
(fn _ => EVERY (rtac raw_induct 1 :: map (fn intr_vs => 
3038bd211582
eqvt_tac now instantiates introduction rules before applying them.
berghofe
parents:
22755
diff
changeset

644 
full_simp_tac eqvt_ss 1 THEN 
25824  645 
eqvt_tac pi' intr_vs) intrs')))) 
22544  646 
end) atoms 
647 
in 

648 
fold (fn (name, ths) => 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24571
diff
changeset

649 
Sign.add_path (Sign.base_name name) #> 
22544  650 
PureThy.add_thmss [(("eqvt", ths), [NominalThmDecls.eqvt_add])] #> snd #> 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24571
diff
changeset

651 
Sign.parent_path) (names ~~ transp thss) thy 
22544  652 
end; 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

653 

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

654 

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

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

656 

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

657 
local structure P = OuterParse and K = OuterKeyword in 
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

658 

24867  659 
val _ = OuterSyntax.keywords ["avoids"]; 
660 

661 
val _ = 

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

662 
OuterSyntax.command "nominal_inductive" 
22530  663 
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal 
664 
(P.name  Scan.optional (P.$$$ "avoids"  P.and_list1 (P.name  

665 
(P.$$$ ":"  Scan.repeat1 P.name))) [] >> (fn (name, avoids) => 

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

666 
Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids))); 
22313
1a507b463f50
First steps towards strengthening of induction rules for
berghofe
parents:
diff
changeset

667 

24867  668 
val _ = 
22530  669 
OuterSyntax.command "equivariance" 
670 
"prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl 

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

671 
(P.name  Scan.optional (P.$$$ "["  P.list1 P.name  P.$$$ "]") [] >> 
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22544
diff
changeset

672 
(fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms))); 
22530  673 

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

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

675 

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

676 
end 