author  paulson 
Thu, 16 Dec 2010 20:14:04 +0000  
changeset 41214  8a341cf54a85 
parent 40832  4352ca878c41 
child 41296  6aaf80ea9715 
permissions  rwrr 
40040
3adb92ee2f22
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman
parents:
40029
diff
changeset

1 
(* Title: HOLCF/Tools/Domain/domain_induction.ML 
23152  2 
Author: David von Oheimb 
32740  3 
Author: Brian Huffman 
23152  4 

40040
3adb92ee2f22
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman
parents:
40029
diff
changeset

5 
Proofs of highlevel (co)induction rules for domain command. 
23152  6 
*) 
7 

40040
3adb92ee2f22
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman
parents:
40029
diff
changeset

8 
signature DOMAIN_INDUCTION = 
31005  9 
sig 
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset

10 
val comp_theorems : 
40097
429cd74f795f
remove legacy comp_dbind option from domain package
huffman
parents:
40040
diff
changeset

11 
binding list > 
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset

12 
Domain_Take_Proofs.take_induct_info > 
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

13 
Domain_Constructors.constr_info list > 
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset

14 
theory > thm list * theory 
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset

15 

40832  16 
val quiet_mode: bool Unsynchronized.ref 
17 
val trace_domain: bool Unsynchronized.ref 

18 
end 

31005  19 

40040
3adb92ee2f22
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman
parents:
40029
diff
changeset

20 
structure Domain_Induction :> DOMAIN_INDUCTION = 
31005  21 
struct 
23152  22 

40832  23 
val quiet_mode = Unsynchronized.ref false 
24 
val trace_domain = Unsynchronized.ref false 

29402  25 

40832  26 
fun message s = if !quiet_mode then () else writeln s 
27 
fun trace s = if !trace_domain then tracing s else () 

29402  28 

40832  29 
open HOLCF_Library 
23152  30 

40013  31 
(******************************************************************************) 
32 
(***************************** proofs about take ******************************) 

33 
(******************************************************************************) 

23152  34 

40013  35 
fun take_theorems 
40019
05cda34d36e7
put constructor argument specs in constr_info type
huffman
parents:
40018
diff
changeset

36 
(dbinds : binding list) 
35775
9b7e2e17be69
pass take_info as argument to Domain_Theorems.theorems
huffman
parents:
35774
diff
changeset

37 
(take_info : Domain_Take_Proofs.take_induct_info) 
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

38 
(constr_infos : Domain_Constructors.constr_info list) 
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

39 
(thy : theory) : thm list list * theory = 
23152  40 
let 
40832  41 
val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info 
42 
val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy 

23152  43 

40832  44 
val n = Free ("n", @{typ nat}) 
45 
val n' = @{const Suc} $ n 

35559  46 

40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

47 
local 
40832  48 
val newTs = map (#absT o #iso_info) constr_infos 
49 
val subs = newTs ~~ map (fn t => t $ n) take_consts 

40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

50 
fun is_ID (Const (c, _)) = (c = @{const_name ID}) 
40832  51 
 is_ID _ = false 
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

52 
in 
40488  53 
fun map_of_arg thy v T = 
40832  54 
let val m = Domain_Take_Proofs.map_of_typ thy subs T 
55 
in if is_ID m then v else mk_capply (m, v) end 

40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

56 
end 
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

57 

2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

58 
fun prove_take_apps 
40019
05cda34d36e7
put constructor argument specs in constr_info type
huffman
parents:
40018
diff
changeset

59 
((dbind, take_const), constr_info) thy = 
23152  60 
let 
41214  61 
val {iso_info, con_specs, con_betas, ...} : Domain_Constructors.constr_info = constr_info 
40832  62 
val {abs_inverse, ...} = iso_info 
40019
05cda34d36e7
put constructor argument specs in constr_info type
huffman
parents:
40018
diff
changeset

63 
fun prove_take_app (con_const, args) = 
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

64 
let 
40832  65 
val Ts = map snd args 
66 
val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts) 

67 
val vs = map Free (ns ~~ Ts) 

68 
val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs)) 

69 
val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts) 

70 
val goal = mk_trp (mk_eq (lhs, rhs)) 

40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

71 
val rules = 
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

72 
[abs_inverse] @ con_betas @ @{thms take_con_rules} 
40832  73 
@ take_Suc_thms @ deflation_thms @ deflation_take_thms 
74 
val tac = simp_tac (HOL_basic_ss addsimps rules) 1 

40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

75 
in 
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

76 
Goal.prove_global thy [] [] goal (K tac) 
40832  77 
end 
78 
val take_apps = map prove_take_app con_specs 

40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

79 
in 
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

80 
yield_singleton Global_Theory.add_thmss 
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

81 
((Binding.qualified true "take_rews" dbind, take_apps), 
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

82 
[Simplifier.simp_add]) thy 
40832  83 
end 
23152  84 
in 
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

85 
fold_map prove_take_apps 
40019
05cda34d36e7
put constructor argument specs in constr_info type
huffman
parents:
40018
diff
changeset

86 
(dbinds ~~ take_consts ~~ constr_infos) thy 
40832  87 
end 
23152  88 

40029  89 
(******************************************************************************) 
90 
(****************************** induction rules *******************************) 

91 
(******************************************************************************) 

40013  92 

40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

93 
val case_UU_allI = 
40832  94 
@{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis} 
40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

95 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

96 
fun prove_induction 
40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

97 
(comp_dbind : binding) 
40018  98 
(constr_infos : Domain_Constructors.constr_info list) 
99 
(take_info : Domain_Take_Proofs.take_induct_info) 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

100 
(take_rews : thm list) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

101 
(thy : theory) = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

102 
let 
40832  103 
val comp_dname = Binding.name_of comp_dbind 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

104 

40832  105 
val iso_infos = map #iso_info constr_infos 
106 
val exhausts = map #exhaust constr_infos 

107 
val con_rews = maps #con_rews constr_infos 

108 
val {take_consts, take_induct_thms, ...} = take_info 

35658  109 

40832  110 
val newTs = map #absT iso_infos 
111 
val P_names = Datatype_Prop.indexify_names (map (K "P") newTs) 

112 
val x_names = Datatype_Prop.indexify_names (map (K "x") newTs) 

113 
val P_types = map (fn T => T > HOLogic.boolT) newTs 

114 
val Ps = map Free (P_names ~~ P_types) 

115 
val xs = map Free (x_names ~~ newTs) 

116 
val n = Free ("n", HOLogic.natT) 

40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

117 

0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

118 
fun con_assm defined p (con, args) = 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

119 
let 
40832  120 
val Ts = map snd args 
121 
val ns = Name.variant_list P_names (Datatype_Prop.make_tnames Ts) 

122 
val vs = map Free (ns ~~ Ts) 

123 
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)) 

40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

124 
fun ind_hyp (v, T) t = 
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

125 
case AList.lookup (op =) (newTs ~~ Ps) T of NONE => t 
40832  126 
 SOME p' => Logic.mk_implies (mk_trp (p' $ v), t) 
127 
val t1 = mk_trp (p $ list_ccomb (con, vs)) 

128 
val t2 = fold_rev ind_hyp (vs ~~ Ts) t1 

129 
val t3 = Logic.list_implies (map (mk_trp o mk_defined) nonlazy, t2) 

130 
in fold_rev Logic.all vs (if defined then t3 else t2) end 

40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

131 
fun eq_assms ((p, T), cons) = 
40832  132 
mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons 
133 
val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos) 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

134 

40832  135 
val take_ss = HOL_ss addsimps (@{thm Rep_cfun_strict1} :: take_rews) 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

136 
fun quant_tac ctxt i = EVERY 
40832  137 
(map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names) 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

138 

40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

139 
(* FIXME: move this message to domain_take_proofs.ML *) 
40832  140 
val is_finite = #is_finite take_info 
40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

141 
val _ = if is_finite 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

142 
then message ("Proving finiteness rule for domain "^comp_dname^" ...") 
40832  143 
else () 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

144 

40832  145 
val _ = trace " Proving finite_ind..." 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

146 
val finite_ind = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

147 
let 
40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

148 
val concls = 
40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

149 
map (fn ((P, t), x) => P $ mk_capply (t $ n, x)) 
40832  150 
(Ps ~~ take_consts ~~ xs) 
151 
val goal = mk_trp (foldr1 mk_conj concls) 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

152 

555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

153 
fun tacf {prems, context} = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

154 
let 
40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

155 
(* Prove stronger prems, without definedness side conditions *) 
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

156 
fun con_thm p (con, args) = 
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

157 
let 
40832  158 
val subgoal = con_assm false p (con, args) 
159 
val rules = prems @ con_rews @ simp_thms 

160 
val simplify = asm_simp_tac (HOL_basic_ss addsimps rules) 

40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

161 
fun arg_tac (lazy, _) = 
40832  162 
rtac (if lazy then allI else case_UU_allI) 1 
40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

163 
val tacs = 
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

164 
rewrite_goals_tac @{thms atomize_all atomize_imp} :: 
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

165 
map arg_tac args @ 
40832  166 
[REPEAT (rtac impI 1), ALLGOALS simplify] 
40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

167 
in 
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

168 
Goal.prove context [] [] subgoal (K (EVERY tacs)) 
40832  169 
end 
170 
fun eq_thms (p, cons) = map (con_thm p) cons 

171 
val conss = map #con_specs constr_infos 

172 
val prems' = maps eq_thms (Ps ~~ conss) 

40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

173 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

174 
val tacs1 = [ 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

175 
quant_tac context 1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

176 
simp_tac HOL_ss 1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

177 
InductTacs.induct_tac context [[SOME "n"]] 1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

178 
simp_tac (take_ss addsimps prems) 1, 
40832  179 
TRY (safe_tac HOL_cs)] 
40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

180 
fun con_tac _ = 
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

181 
asm_simp_tac take_ss 1 THEN 
40832  182 
(resolve_tac prems' THEN_ALL_NEW etac spec) 1 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35777
diff
changeset

183 
fun cases_tacs (cons, exhaust) = 
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35777
diff
changeset

184 
res_inst_tac context [(("y", 0), "x")] exhaust 1 :: 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

185 
asm_simp_tac (take_ss addsimps prems) 1 :: 
40832  186 
map con_tac cons 
40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

187 
val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts) 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

188 
in 
40020
0cbb08bf18df
rewrite proof automation for finite_ind; get rid of case_UU_tac
huffman
parents:
40019
diff
changeset

189 
EVERY (map DETERM tacs) 
40832  190 
end 
191 
in Goal.prove_global thy [] assms goal tacf end 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

192 

40832  193 
val _ = trace " Proving ind..." 
35661
ede27eb8e94b
don't generate rule foo.finites for nonflat domains; use take_induct rule to prove induction rule
huffman
parents:
35660
diff
changeset

194 
val ind = 
40022  195 
let 
40832  196 
val concls = map (op $) (Ps ~~ xs) 
197 
val goal = mk_trp (foldr1 mk_conj concls) 

198 
val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps 

40022  199 
fun tacf {prems, context} = 
200 
let 

201 
fun finite_tac (take_induct, fin_ind) = 

202 
rtac take_induct 1 THEN 

203 
(if is_finite then all_tac else resolve_tac prems 1) THEN 

40832  204 
(rtac fin_ind THEN_ALL_NEW solve_tac prems) 1 
205 
val fin_inds = Project_Rule.projections context finite_ind 

40022  206 
in 
207 
TRY (safe_tac HOL_cs) THEN 

208 
EVERY (map finite_tac (take_induct_thms ~~ fin_inds)) 

40832  209 
end 
40022  210 
in Goal.prove_global thy [] (adms @ assms) goal tacf end 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

211 

40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

212 
(* case names for induction rules *) 
40832  213 
val dnames = map (fst o dest_Type) newTs 
40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

214 
val case_ns = 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

215 
let 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

216 
val adms = 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

217 
if is_finite then [] else 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

218 
if length dnames = 1 then ["adm"] else 
40832  219 
map (fn s => "adm_" ^ Long_Name.base_name s) dnames 
40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

220 
val bottoms = 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

221 
if length dnames = 1 then ["bottom"] else 
40832  222 
map (fn s => "bottom_" ^ Long_Name.base_name s) dnames 
41214  223 
fun one_eq bot (constr_info : Domain_Constructors.constr_info) = 
40832  224 
let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c)) 
225 
in bot :: map name_of (#con_specs constr_info) end 

226 
in adms @ flat (map2 one_eq bottoms constr_infos) end 

35630
8e562d56d404
add case_names attribute to casedist and ind rules
huffman
parents:
35601
diff
changeset

227 

40832  228 
val inducts = Project_Rule.projections (ProofContext.init_global thy) ind 
40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

229 
fun ind_rule (dname, rule) = 
40026
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40025
diff
changeset

230 
((Binding.empty, rule), 
40832  231 
[Rule_Cases.case_names case_ns, Induct.induct_type dname]) 
35630
8e562d56d404
add case_names attribute to casedist and ind rules
huffman
parents:
35601
diff
changeset

232 

35774  233 
in 
234 
thy 

40026
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40025
diff
changeset

235 
> snd o Global_Theory.add_thms [ 
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40025
diff
changeset

236 
((Binding.qualified true "finite_induct" comp_dbind, finite_ind), []), 
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40025
diff
changeset

237 
((Binding.qualified true "induct" comp_dbind, ind ), [])] 
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40025
diff
changeset

238 
> (snd o Global_Theory.add_thms (map ind_rule (dnames ~~ inducts))) 
40832  239 
end (* prove_induction *) 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

240 

555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

241 
(******************************************************************************) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

242 
(************************ bisimulation and coinduction ************************) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

243 
(******************************************************************************) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

244 

35574
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

245 
fun prove_coinduction 
40025  246 
(comp_dbind : binding, dbinds : binding list) 
247 
(constr_infos : Domain_Constructors.constr_info list) 

248 
(take_info : Domain_Take_Proofs.take_induct_info) 

249 
(take_rews : thm list list) 

35599
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

250 
(thy : theory) : theory = 
23152  251 
let 
40832  252 
val iso_infos = map #iso_info constr_infos 
253 
val newTs = map #absT iso_infos 

40025  254 

40832  255 
val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info 
23152  256 

40832  257 
val R_names = Datatype_Prop.indexify_names (map (K "R") newTs) 
258 
val R_types = map (fn T => T > T > boolT) newTs 

259 
val Rs = map Free (R_names ~~ R_types) 

260 
val n = Free ("n", natT) 

261 
val reserved = "x" :: "y" :: R_names 

35497  262 

40025  263 
(* declare bisimulation predicate *) 
40832  264 
val bisim_bind = Binding.suffix_name "_bisim" comp_dbind 
265 
val bisim_type = R_types > boolT 

35497  266 
val (bisim_const, thy) = 
40832  267 
Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy 
35497  268 

40025  269 
(* define bisimulation predicate *) 
270 
local 

271 
fun one_con T (con, args) = 

272 
let 

40832  273 
val Ts = map snd args 
274 
val ns1 = Name.variant_list reserved (Datatype_Prop.make_tnames Ts) 

275 
val ns2 = map (fn n => n^"'") ns1 

276 
val vs1 = map Free (ns1 ~~ Ts) 

277 
val vs2 = map Free (ns2 ~~ Ts) 

278 
val eq1 = mk_eq (Free ("x", T), list_ccomb (con, vs1)) 

279 
val eq2 = mk_eq (Free ("y", T), list_ccomb (con, vs2)) 

40025  280 
fun rel ((v1, v2), T) = 
281 
case AList.lookup (op =) (newTs ~~ Rs) T of 

40832  282 
NONE => mk_eq (v1, v2)  SOME r => r $ v1 $ v2 
283 
val eqs = foldr1 mk_conj (map rel (vs1 ~~ vs2 ~~ Ts) @ [eq1, eq2]) 

40025  284 
in 
285 
Library.foldr mk_ex (vs1 @ vs2, eqs) 

40832  286 
end 
40025  287 
fun one_eq ((T, R), cons) = 
288 
let 

40832  289 
val x = Free ("x", T) 
290 
val y = Free ("y", T) 

291 
val disj1 = mk_conj (mk_eq (x, mk_bottom T), mk_eq (y, mk_bottom T)) 

292 
val disjs = disj1 :: map (one_con T) cons 

40025  293 
in 
294 
mk_all (x, mk_all (y, mk_imp (R $ x $ y, foldr1 mk_disj disjs))) 

40832  295 
end 
296 
val conjs = map one_eq (newTs ~~ Rs ~~ map #con_specs constr_infos) 

297 
val bisim_rhs = lambdas Rs (Library.foldr1 mk_conj conjs) 

298 
val bisim_eqn = Logic.mk_equals (bisim_const, bisim_rhs) 

40025  299 
in 
300 
val (bisim_def_thm, thy) = thy > 

301 
yield_singleton (Global_Theory.add_defs false) 

40832  302 
((Binding.qualified true "bisim_def" comp_dbind, bisim_eqn), []) 
40025  303 
end (* local *) 
35497  304 

40025  305 
(* prove coinduction lemma *) 
306 
val coind_lemma = 

35497  307 
let 
40832  308 
val assm = mk_trp (list_comb (bisim_const, Rs)) 
40025  309 
fun one ((T, R), take_const) = 
310 
let 

40832  311 
val x = Free ("x", T) 
312 
val y = Free ("y", T) 

313 
val lhs = mk_capply (take_const $ n, x) 

314 
val rhs = mk_capply (take_const $ n, y) 

40025  315 
in 
316 
mk_all (x, mk_all (y, mk_imp (R $ x $ y, mk_eq (lhs, rhs)))) 

40832  317 
end 
40025  318 
val goal = 
40832  319 
mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts))) 
320 
val rules = @{thm Rep_cfun_strict1} :: take_0_thms 

40025  321 
fun tacf {prems, context} = 
322 
let 

40832  323 
val prem' = rewrite_rule [bisim_def_thm] (hd prems) 
324 
val prems' = Project_Rule.projections context prem' 

325 
val dests = map (fn th => th RS spec RS spec RS mp) prems' 

40025  326 
fun one_tac (dest, rews) = 
327 
dtac dest 1 THEN safe_tac HOL_cs THEN 

40832  328 
ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews)) 
40025  329 
in 
330 
rtac @{thm nat.induct} 1 THEN 

331 
simp_tac (HOL_ss addsimps rules) 1 THEN 

332 
safe_tac HOL_cs THEN 

333 
EVERY (map one_tac (dests ~~ take_rews)) 

334 
end 

35497  335 
in 
40025  336 
Goal.prove_global thy [] [assm] goal tacf 
40832  337 
end 
40025  338 

339 
(* prove individual coinduction rules *) 

340 
fun prove_coind ((T, R), take_lemma) = 

341 
let 

40832  342 
val x = Free ("x", T) 
343 
val y = Free ("y", T) 

344 
val assm1 = mk_trp (list_comb (bisim_const, Rs)) 

345 
val assm2 = mk_trp (R $ x $ y) 

346 
val goal = mk_trp (mk_eq (x, y)) 

40025  347 
fun tacf {prems, context} = 
348 
let 

40832  349 
val rule = hd prems RS coind_lemma 
40025  350 
in 
351 
rtac take_lemma 1 THEN 

352 
asm_simp_tac (HOL_basic_ss addsimps (rule :: prems)) 1 

40832  353 
end 
40025  354 
in 
355 
Goal.prove_global thy [] [assm1, assm2] goal tacf 

40832  356 
end 
357 
val coinds = map prove_coind (newTs ~~ Rs ~~ take_lemma_thms) 

358 
val coind_binds = map (Binding.qualified true "coinduct") dbinds 

35497  359 

360 
in 

40025  361 
thy > snd o Global_Theory.add_thms 
362 
(map Thm.no_attributes (coind_binds ~~ coinds)) 

40832  363 
end (* let *) 
35574
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

364 

40018  365 
(******************************************************************************) 
366 
(******************************* main function ********************************) 

367 
(******************************************************************************) 

368 

35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset

369 
fun comp_theorems 
40019
05cda34d36e7
put constructor argument specs in constr_info type
huffman
parents:
40018
diff
changeset

370 
(dbinds : binding list) 
35659  371 
(take_info : Domain_Take_Proofs.take_induct_info) 
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

372 
(constr_infos : Domain_Constructors.constr_info list) 
35657
0537c34c6067
pass take_induct_info as an argument to comp_theorems
huffman
parents:
35654
diff
changeset

373 
(thy : theory) = 
35574
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

374 
let 
40097
429cd74f795f
remove legacy comp_dbind option from domain package
huffman
parents:
40040
diff
changeset

375 

40832  376 
val comp_dname = space_implode "_" (map Binding.name_of dbinds) 
377 
val comp_dbind = Binding.name comp_dname 

35574
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

378 

40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

379 
(* Test for emptiness *) 
40026
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40025
diff
changeset

380 
(* FIXME: reimplement emptiness test 
40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

381 
local 
40832  382 
open Domain_Library 
383 
val dnames = map (fst o fst) eqs 

384 
val conss = map snd eqs 

40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

385 
fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

386 
is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

387 
((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

388 
rec_of arg <> n andalso rec_to (rec_of arg::ns) 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

389 
(lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) 
40832  390 
) o snd) cons 
40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

391 
fun warn (n,cons) = 
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

392 
if rec_to [] false (n,cons) 
40832  393 
then (warning ("domain "^List.nth(dnames,n)^" is empty!") true) 
394 
else false 

40023
a868e9d73031
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
huffman
parents:
40022
diff
changeset

395 
in 
40832  396 
val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs 
397 
val is_emptys = map warn n__eqs 

398 
end 

40026
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40025
diff
changeset

399 
*) 
23152  400 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

401 
(* Test for indirect recursion *) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

402 
local 
40832  403 
val newTs = map (#absT o #iso_info) constr_infos 
40026
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40025
diff
changeset

404 
fun indirect_typ (Type (_, Ts)) = 
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40025
diff
changeset

405 
exists (fn T => member (op =) newTs T orelse indirect_typ T) Ts 
40832  406 
 indirect_typ _ = false 
407 
fun indirect_arg (_, T) = indirect_typ T 

408 
fun indirect_con (_, args) = exists indirect_arg args 

409 
fun indirect_eq cons = exists indirect_con cons 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

410 
in 
40832  411 
val is_indirect = exists indirect_eq (map #con_specs constr_infos) 
35599
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

412 
val _ = 
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

413 
if is_indirect 
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

414 
then message "Indirect recursion detected, skipping proofs of (co)induction rules" 
40832  415 
else message ("Proving induction properties of domain "^comp_dname^" ...") 
416 
end 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

417 

555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

418 
(* theorems about take *) 
23152  419 

40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

420 
val (take_rewss, thy) = 
40832  421 
take_theorems dbinds take_info constr_infos thy 
23152  422 

40832  423 
val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info 
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
40014
diff
changeset

424 

40832  425 
val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss 
23152  426 

35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

427 
(* prove induction rules, unless definition is indirect recursive *) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

428 
val thy = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

429 
if is_indirect then thy else 
40832  430 
prove_induction comp_dbind constr_infos take_info take_rews thy 
23152  431 

35599
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

432 
val thy = 
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

433 
if is_indirect then thy else 
40832  434 
prove_coinduction (comp_dbind, dbinds) constr_infos take_info take_rewss thy 
23152  435 

35642
f478d5a9d238
generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents:
35630
diff
changeset

436 
in 
f478d5a9d238
generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents:
35630
diff
changeset

437 
(take_rews, thy) 
40832  438 
end (* let *) 
439 
end (* struct *) 