author  huffman 
Fri, 05 Mar 2010 15:59:48 0800  
changeset 35601  50ba5010b876 
parent 35599  20670f5564e9 
child 35630  8e562d56d404 
permissions  rwrr 
32126  1 
(* Title: HOLCF/Tools/Domain/domain_theorems.ML 
23152  2 
Author: David von Oheimb 
32740  3 
Author: Brian Huffman 
23152  4 

5 
Proof generator for domain command. 

6 
*) 

7 

26342  8 
val HOLCF_ss = @{simpset}; 
23152  9 

31005  10 
signature DOMAIN_THEOREMS = 
11 
sig 

35444  12 
val theorems: 
13 
Domain_Library.eq * Domain_Library.eq list 

14 
> typ * (binding * (bool * binding option * typ) list * mixfix) list 

35558
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35557
diff
changeset

15 
> Domain_Take_Proofs.iso_info 
35444  16 
> theory > thm list * theory; 
17 

31005  18 
val comp_theorems: bstring * Domain_Library.eq list > theory > thm list * theory; 
32740  19 
val quiet_mode: bool Unsynchronized.ref; 
20 
val trace_domain: bool Unsynchronized.ref; 

31005  21 
end; 
22 

31023  23 
structure Domain_Theorems :> DOMAIN_THEOREMS = 
31005  24 
struct 
23152  25 

32740  26 
val quiet_mode = Unsynchronized.ref false; 
27 
val trace_domain = Unsynchronized.ref false; 

29402  28 

29 
fun message s = if !quiet_mode then () else writeln s; 

30 
fun trace s = if !trace_domain then tracing s else (); 

31 

23152  32 
open Domain_Library; 
33 
infixr 0 ===>; 

34 
infixr 0 ==>; 

35 
infix 0 == ; 

36 
infix 1 ===; 

37 
infix 1 ~= ; 

38 
infix 1 <<; 

39 
infix 1 ~<<; 

40 
infix 9 ` ; 

41 
infix 9 `% ; 

42 
infix 9 `%%; 

43 
infixr 9 oo; 

44 

45 
(*  general proof facilities  *) 

46 

24503  47 
fun legacy_infer_term thy t = 
48 
let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy) 

49 
in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end; 

50 

23152  51 
fun pg'' thy defs t tacs = 
52 
let 

24503  53 
val t' = legacy_infer_term thy t; 
23152  54 
val asms = Logic.strip_imp_prems t'; 
55 
val prop = Logic.strip_imp_concl t'; 

26711  56 
fun tac {prems, context} = 
23152  57 
rewrite_goals_tac defs THEN 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27153
diff
changeset

58 
EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context}) 
23152  59 
in Goal.prove_global thy [] asms prop tac end; 
60 

61 
fun pg' thy defs t tacsf = 

62 
let 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27153
diff
changeset

63 
fun tacs {prems, context} = 
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27153
diff
changeset

64 
if null prems then tacsf context 
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27153
diff
changeset

65 
else cut_facts_tac prems 1 :: tacsf context; 
23152  66 
in pg'' thy defs t tacs end; 
67 

35443
2e0f9516947e
change domain package's treatment of variable names in theorems to be like datatype package
huffman
parents:
35288
diff
changeset

68 
(* FIXME!!!!!!!!! *) 
2e0f9516947e
change domain package's treatment of variable names in theorems to be like datatype package
huffman
parents:
35288
diff
changeset

69 
(* We should NEVER reparse variable names as strings! *) 
2e0f9516947e
change domain package's treatment of variable names in theorems to be like datatype package
huffman
parents:
35288
diff
changeset

70 
(* The names can conflict with existing constants or other syntax! *) 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27153
diff
changeset

71 
fun case_UU_tac ctxt rews i v = 
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27153
diff
changeset

72 
InductTacs.case_tac ctxt (v^"=UU") i THEN 
23152  73 
asm_simp_tac (HOLCF_ss addsimps rews) i; 
74 

75 
(*  general proofs  *) 

76 

29064  77 
val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp} 
23152  78 

35444  79 
fun theorems 
80 
(((dname, _), cons) : eq, eqs : eq list) 

81 
(dom_eqn : typ * (binding * (bool * binding option * typ) list * mixfix) list) 

35558
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35557
diff
changeset

82 
(iso_info : Domain_Take_Proofs.iso_info) 
35444  83 
(thy : theory) = 
23152  84 
let 
85 

29402  86 
val _ = message ("Proving isomorphism properties of domain "^dname^" ..."); 
35514
a2cfa413eaab
move takerelated definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
35512
diff
changeset

87 
val map_tab = Domain_Take_Proofs.get_map_tab thy; 
33801  88 

23152  89 

90 
(*  getting the axioms and definitions  *) 

91 

35558
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35557
diff
changeset

92 
val ax_abs_iso = #abs_inverse iso_info; 
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35557
diff
changeset

93 
val ax_rep_iso = #rep_inverse iso_info; 
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35557
diff
changeset

94 

bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35557
diff
changeset

95 
val abs_const = #abs_const iso_info; 
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35557
diff
changeset

96 
val rep_const = #rep_const iso_info; 
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35557
diff
changeset

97 

23152  98 
local 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26342
diff
changeset

99 
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); 
23152  100 
in 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

101 
val ax_take_0 = ga "take_0" dname; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

102 
val ax_take_Suc = ga "take_Suc" dname; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

103 
val ax_take_strict = ga "take_strict" dname; 
23152  104 
end; (* local *) 
105 

35444  106 
(*  define constructors  *) 
107 

108 
val (result, thy) = 

109 
Domain_Constructors.add_domain_constructors 

35486
c91854705b1d
move definition of case combinator to domain_constructors.ML
huffman
parents:
35482
diff
changeset

110 
(Long_Name.base_name dname) (snd dom_eqn) iso_info thy; 
35444  111 

35451  112 
val con_appls = #con_betas result; 
35457
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

113 
val {exhaust, casedist, ...} = result; 
35458
deaf221c4a59
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman
parents:
35457
diff
changeset

114 
val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result; 
35457
d63655b88369
move proofs of casedist into domain_constructors.ML
huffman
parents:
35456
diff
changeset

115 
val {sel_rews, ...} = result; 
35459
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

116 
val when_rews = #cases result; 
3d8acfae6fb8
move proofs of when_rews intro domain_constructors.ML
huffman
parents:
35458
diff
changeset

117 
val when_strict = hd when_rews; 
35461
34360a1e3537
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
huffman
parents:
35460
diff
changeset

118 
val dis_rews = #dis_rews result; 
35466
9fcfd5763181
move proofs of match_rews to domain_constructors.ML
huffman
parents:
35464
diff
changeset

119 
val mat_rews = #match_rews result; 
35482
d756837b708d
move proofs of pat_rews to domain_constructors.ML
huffman
parents:
35481
diff
changeset

120 
val pat_rews = #pat_rews result; 
35444  121 

23152  122 
(*  theorems concerning the isomorphism  *) 
123 

35444  124 
val pg = pg' thy; 
125 

35560  126 
val retraction_strict = @{thm retraction_strict}; 
23152  127 
val abs_strict = ax_rep_iso RS (allI RS retraction_strict); 
128 
val rep_strict = ax_abs_iso RS (allI RS retraction_strict); 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34974
diff
changeset

129 
val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict]; 
23152  130 

131 
(*  theorems concerning one induction step  *) 

132 

35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

133 
local 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

134 
fun dc_take dn = %%:(dn^"_take"); 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

135 
val dnames = map (fst o fst) eqs; 
35523
cc57f4a274a3
fix proof script for take_apps so it works with indirect recursion
huffman
parents:
35521
diff
changeset

136 
val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy; 
cc57f4a274a3
fix proof script for take_apps so it works with indirect recursion
huffman
parents:
35521
diff
changeset

137 
fun get_deflation_take dn = PureThy.get_thm thy (dn ^ ".deflation_take"); 
cc57f4a274a3
fix proof script for take_apps so it works with indirect recursion
huffman
parents:
35521
diff
changeset

138 
val axs_deflation_take = map get_deflation_take dnames; 
23152  139 

35559  140 
fun copy_of_dtyp tab r dt = 
141 
if Datatype_Aux.is_rec_type dt then copy tab r dt else ID 

142 
and copy tab r (Datatype_Aux.DtRec i) = r i 

143 
 copy tab r (Datatype_Aux.DtTFree a) = ID 

144 
 copy tab r (Datatype_Aux.DtType (c, ds)) = 

145 
case Symtab.lookup tab c of 

146 
SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds) 

147 
 NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); 

148 

35521  149 
fun one_take_app (con, args) = 
23152  150 
let 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

151 
fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; 
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31160
diff
changeset

152 
fun one_rhs arg = 
33971  153 
if Datatype_Aux.is_rec_type (dtyp_of arg) 
35559  154 
then copy_of_dtyp map_tab 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

155 
mk_take (dtyp_of arg) ` (%# arg) 
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31160
diff
changeset

156 
else (%# arg); 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

157 
val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args); 
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
31160
diff
changeset

158 
val rhs = con_app2 con one_rhs args; 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

159 
val goal = mk_trp (lhs === rhs); 
35590  160 
val rules = 
161 
[ax_take_Suc, ax_abs_iso, @{thm cfcomp2}] 

162 
@ @{thms take_con_rules ID1 deflation_strict} 

35523
cc57f4a274a3
fix proof script for take_apps so it works with indirect recursion
huffman
parents:
35521
diff
changeset

163 
@ deflation_thms @ axs_deflation_take; 
35590  164 
val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

165 
in pg con_appls goal (K tacs) end; 
35557
5da670d57118
uniformly use variable names m and n in takerelated lemmas; use export_without_context where appropriate
huffman
parents:
35528
diff
changeset

166 
val take_apps = map one_take_app cons; 
23152  167 
in 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

168 
val take_rews = ax_take_0 :: ax_take_strict :: take_apps; 
23152  169 
end; 
170 

171 
in 

172 
thy 

30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

173 
> Sign.add_path (Long_Name.base_name dname) 
31004  174 
> snd o PureThy.add_thmss [ 
175 
((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]), 

176 
((Binding.name "exhaust" , [exhaust] ), []), 

177 
((Binding.name "casedist" , [casedist] ), [Induct.cases_type dname]), 

178 
((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]), 

179 
((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]), 

33427  180 
((Binding.name "con_rews" , con_rews ), 
181 
[Simplifier.simp_add, Fixrec.fixrec_simp_add]), 

31004  182 
((Binding.name "sel_rews" , sel_rews ), [Simplifier.simp_add]), 
183 
((Binding.name "dis_rews" , dis_rews ), [Simplifier.simp_add]), 

184 
((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]), 

185 
((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]), 

186 
((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]), 

187 
((Binding.name "inverts" , inverts ), [Simplifier.simp_add]), 

188 
((Binding.name "injects" , injects ), [Simplifier.simp_add]), 

35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

189 
((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]), 
33427  190 
((Binding.name "match_rews", mat_rews ), 
191 
[Simplifier.simp_add, Fixrec.fixrec_simp_add])] 

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

192 
> Sign.parent_path 
28536  193 
> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

194 
pat_rews @ dist_les @ dist_eqs) 
23152  195 
end; (* let *) 
196 

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

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

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

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

200 

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

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

202 
(comp_dnam, eqs : eq list) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

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

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

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

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

208 
val dnames = map (fst o fst) eqs; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

209 
val conss = map snd eqs; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

210 
fun dc_take dn = %%:(dn^"_take"); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

211 
val x_name = idx_name dnames "x"; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

212 
val P_name = idx_name dnames "P"; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

214 

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

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

216 
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

217 
fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

218 
in 
35597
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

219 
val axs_rep_iso = map (ga "rep_iso") dnames; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

220 
val axs_abs_iso = map (ga "abs_iso") dnames; 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

221 
val axs_chain_take = map (ga "chain_take") dnames; 
35597
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

222 
val lub_take_thms = map (ga "lub_take") dnames; 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

223 
val axs_finite_def = map (ga "finite_def") dnames; 
35597
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

224 
val take_0_thms = map (ga "take_0") dnames; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

225 
val take_Suc_thms = map (ga "take_Suc") dnames; 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

226 
val cases = map (ga "casedist" ) dnames; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

227 
val con_rews = maps (gts "con_rews" ) dnames; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

229 

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

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

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

232 
val P_names = map P_name (1 upto (length dnames)); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

233 
val vns = Name.variant_list P_names (map vname args); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

234 
val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns)); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

235 
fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

236 
val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

237 
val t2 = lift ind_hyp (filter is_rec args, t1); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

238 
val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

239 
in Library.foldr mk_All (vns, t3) end; 
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 
fun one_eq ((p, cons), concl) = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

242 
mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); 
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 
fun ind_term concf = Library.foldr one_eq 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

245 
(mapn (fn n => fn x => (P_name n, x)) 1 conss, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

246 
mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

248 
fun quant_tac ctxt i = EVERY 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

249 
(mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

250 

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

251 
fun ind_prems_tac prems = EVERY 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

252 
(maps (fn cons => 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

253 
(resolve_tac prems 1 :: 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

254 
maps (fn (_,args) => 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

256 
map (K(atac 1)) (nonlazy args) @ 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

257 
map (K(atac 1)) (filter is_rec args)) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

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

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

261 
(* check whether every/exists constructor of the nth part of the equation: 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

262 
it has a possibly indirectly recursive argument that isn't/is possibly 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

263 
indirectly lazy *) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

264 
fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

265 
is_rec arg andalso not(rec_of arg mem ns) andalso 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

266 
((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

267 
rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

268 
(lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

269 
) o snd) cons; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

270 
fun all_rec_to ns = rec_to forall not all_rec_to ns; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

271 
fun warn (n,cons) = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

272 
if all_rec_to [] false (n,cons) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

273 
then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

275 
fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

276 

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

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

278 
val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

279 
val is_emptys = map warn n__eqs; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

280 
val is_finite = forall (not o lazy_rec_to [] false) n__eqs; 
35601
50ba5010b876
print message when finiteness of domain definition is detected
huffman
parents:
35599
diff
changeset

281 
val _ = if is_finite 
50ba5010b876
print message when finiteness of domain definition is detected
huffman
parents:
35599
diff
changeset

282 
then message ("Proving finiteness rule for domain "^comp_dnam^" ...") 
50ba5010b876
print message when finiteness of domain definition is detected
huffman
parents:
35599
diff
changeset

283 
else (); 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

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

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

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

288 
fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n)); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

289 
val goal = ind_term concf; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

290 

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

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

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

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

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

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

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

297 
simp_tac (take_ss addsimps prems) 1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

298 
TRY (safe_tac HOL_cs)]; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

299 
fun arg_tac arg = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

301 
case_UU_tac context (prems @ con_rews) 1 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

302 
(List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

303 
fun con_tacs (con, args) = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

305 
map arg_tac (filter is_nonlazy_rec args) @ 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

306 
[resolve_tac prems 1] @ 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

307 
map (K (atac 1)) (nonlazy args) @ 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

308 
map (K (etac spec 1)) (filter is_rec args); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

309 
fun cases_tacs (cons, cases) = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

311 
asm_simp_tac (take_ss addsimps prems) 1 :: 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

312 
maps con_tacs cons; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

314 
tacs1 @ maps cases_tacs (conss ~~ cases) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

316 
in pg'' thy [] goal tacf 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

317 
handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

319 

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

320 
(*  theorems concerning finiteness and induction  *) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

321 

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

322 
val global_ctxt = ProofContext.init thy; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

323 

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

324 
val _ = trace " Proving finites, ind..."; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

325 
val (finites, ind) = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

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

328 
then (* finite case *) 
35597
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

329 
let 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

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

331 
let 
35597
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

332 
val iso_locale_thms = 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

333 
map2 (fn x => fn y => @{thm iso.intro} OF [x, y]) 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

334 
axs_abs_iso axs_rep_iso; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

335 
val decisive_abs_rep_thms = 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

336 
map (fn x => @{thm decisive_abs_rep} OF [x]) 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

337 
iso_locale_thms; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

338 
val n = Free ("n", @{typ nat}); 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

339 
fun mk_decisive t = %%: @{const_name decisive} $ t; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

340 
fun f dn = mk_decisive (dc_take dn $ n); 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

341 
val goal = mk_trp (foldr1 mk_conj (map f dnames)); 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

342 
val rules0 = @{thm decisive_bottom} :: take_0_thms; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

343 
val rules1 = 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

344 
take_Suc_thms @ decisive_abs_rep_thms 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

345 
@ @{thms decisive_ID decisive_ssum_map decisive_sprod_map}; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

346 
val tacs = [ 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

347 
rtac @{thm nat.induct} 1, 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

348 
simp_tac (HOL_ss addsimps rules0) 1, 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

349 
asm_simp_tac (HOL_ss addsimps rules1) 1]; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

350 
in pg [] goal (K tacs) end; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

351 
fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x"); 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

352 
fun one_finite (dn, decisive_thm) = 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

354 
val goal = mk_trp (%%:(dn^"_finite") $ %:"x"); 
35597
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

355 
val tacs = [ 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

356 
rtac @{thm lub_ID_finite} 1, 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

357 
resolve_tac axs_chain_take 1, 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

358 
resolve_tac lub_take_thms 1, 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

359 
rtac decisive_thm 1]; 
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

360 
in pg axs_finite_def goal (K tacs) end; 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

361 

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

362 
val _ = trace " Proving finites"; 
35597
e4331b99b03f
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
huffman
parents:
35590
diff
changeset

363 
val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma); 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

364 
val _ = trace " Proving ind"; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

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

367 
fun concf n dn = %:(P_name n) $ %:(x_name n); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

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

370 
fun finite_tacs (finite, fin_ind) = [ 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

371 
rtac(rewrite_rule axs_finite_def finite RS exE)1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

372 
etac subst 1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

373 
rtac fin_ind 1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

374 
ind_prems_tac prems]; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

376 
TRY (safe_tac HOL_cs) :: 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

377 
maps finite_tacs (finites ~~ atomize global_ctxt finite_ind) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

379 
in pg'' thy [] (ind_term concf) tacf end; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

380 
in (finites, ind) end (* let *) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

381 

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

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

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

384 
fun one_finite n dn = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

385 
read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

386 
val finites = mapn one_finite 1 dnames; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

387 

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

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

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

390 
fun one_adm n _ = mk_trp (mk_adm (%:(P_name n))); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

391 
fun concf n dn = %:(P_name n) $ %:(x_name n); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

392 
in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

394 
@{thms cont_id cont_const cont2cont_Rep_CFun 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

395 
cont2cont_fst cont2cont_snd}; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

397 
let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n)); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

398 
in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

399 
val subgoal' = legacy_infer_term thy subgoal; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

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

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

403 
EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems]; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

404 
val subthm = Goal.prove context [] [] subgoal' (K subtac); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

406 
map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

407 
cut_facts_tac (subthm :: take (length dnames) prems) 1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

408 
REPEAT (rtac @{thm conjI} 1 ORELSE 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

409 
EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

410 
resolve_tac axs_chain_take 1, 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

411 
asm_simp_tac HOL_basic_ss 1]) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

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

414 
val ind = (pg'' thy [] goal tacf 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

415 
handle ERROR _ => 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

416 
(warning "Cannot prove infinite induction rule"; TrueI) 
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 
in (finites, ind) end 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

420 
handle THM _ => 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

421 
(warning "Induction proofs failed (THM raised)."; ([], TrueI)) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

422 
 ERROR _ => 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

423 
(warning "Cannot prove induction rule"; ([], TrueI)); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

424 

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

425 
val inducts = Project_Rule.projections (ProofContext.init thy) ind; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

426 
fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

427 
val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

428 

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

429 
in thy > Sign.add_path comp_dnam 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

430 
> snd o PureThy.add_thmss [ 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

431 
((Binding.name "finites" , finites ), []), 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

432 
((Binding.name "finite_ind" , [finite_ind]), []), 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

433 
((Binding.name "ind" , [ind] ), [])] 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

434 
> (if induct_failed then I 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

435 
else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))) 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

436 
> Sign.parent_path 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

438 

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

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

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

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

442 

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

443 
fun prove_coinduction 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

444 
(comp_dnam, eqs : eq list) 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

445 
(take_lemmas : thm list) 
35599
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

446 
(thy : theory) : theory = 
23152  447 
let 
27232  448 

23152  449 
val dnames = map (fst o fst) eqs; 
28965  450 
val comp_dname = Sign.full_bname thy comp_dnam; 
35574
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

451 
fun dc_take dn = %%:(dn^"_take"); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

452 
val x_name = idx_name dnames "x"; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

453 
val n_eqs = length eqs; 
23152  454 

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

455 
val take_rews = 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

456 
maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; 
35497  457 

458 
(*  define bisimulation predicate  *) 

459 

460 
local 

461 
open HOLCF_Library 

462 
val dtypes = map (Type o fst) eqs; 

463 
val relprod = mk_tupleT (map (fn tp => tp > tp > boolT) dtypes); 

464 
val bisim_bind = Binding.name (comp_dnam ^ "_bisim"); 

465 
val bisim_type = relprod > boolT; 

466 
in 

467 
val (bisim_const, thy) = 

468 
Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy; 

469 
end; 

470 

471 
local 

472 

473 
fun legacy_infer_term thy t = 

474 
singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); 

475 
fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); 

476 
fun infer_props thy = map (apsnd (legacy_infer_prop thy)); 

477 
fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x); 

478 
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; 

479 

480 
val comp_dname = Sign.full_bname thy comp_dnam; 

481 
val dnames = map (fst o fst) eqs; 

482 
val x_name = idx_name dnames "x"; 

483 

35521  484 
fun one_con (con, args) = 
35497  485 
let 
486 
val nonrec_args = filter_out is_rec args; 

487 
val rec_args = filter is_rec args; 

488 
val recs_cnt = length rec_args; 

489 
val allargs = nonrec_args @ rec_args 

490 
@ map (upd_vname (fn s=> s^"'")) rec_args; 

491 
val allvns = map vname allargs; 

492 
fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; 

493 
val vns1 = map (vname_arg "" ) args; 

494 
val vns2 = map (vname_arg "'") args; 

495 
val allargs_cnt = length nonrec_args + 2*recs_cnt; 

496 
val rec_idxs = (recs_cnt1) downto 0; 

497 
val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) 

498 
(allargs~~((allargs_cnt1) downto 0))); 

499 
fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 

500 
Bound (2*recs_cnti) $ Bound (recs_cnti); 

501 
val capps = 

502 
List.foldr 

503 
mk_conj 

504 
(mk_conj( 

505 
Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), 

506 
Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) 

507 
(mapn rel_app 1 rec_args); 

508 
in 

509 
List.foldr 

510 
mk_ex 

511 
(Library.foldr mk_conj 

512 
(map (defined o Bound) nonlazy_idxs,capps)) allvns 

513 
end; 

514 
fun one_comp n (_,cons) = 

515 
mk_all (x_name(n+1), 

516 
mk_all (x_name(n+1)^"'", 

517 
mk_imp (proj (Bound 2) eqs n $ Bound 1 $ Bound 0, 

518 
foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) 

519 
::map one_con cons)))); 

520 
val bisim_eqn = 

521 
%%:(comp_dname^"_bisim") == 

522 
mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs)); 

523 

524 
in 

525 
val ([ax_bisim_def], thy) = 

526 
thy 

527 
> Sign.add_path comp_dnam 

528 
> add_defs_infer [(Binding.name "bisim_def", bisim_eqn)] 

529 
> Sign.parent_path; 

530 
end; (* local *) 

531 

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

532 
(*  theorem concerning coinduction  *) 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

533 

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

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

535 
val pg = pg' thy; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

536 
val xs = mapn (fn n => K (x_name n)) 1 dnames; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

537 
fun bnd_arg n i = Bound(2*(n_eqs  n)i1); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

538 
val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

539 
val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

540 
val _ = trace " Proving coind_lemma..."; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

541 
val coind_lemma = 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

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

543 
fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

544 
fun mk_eqn n dn = 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

545 
(dc_take dn $ %:"n" ` bnd_arg n 0) === 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

546 
(dc_take dn $ %:"n" ` bnd_arg n 1); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

547 
fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t)); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

548 
val goal = 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

549 
mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R", 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

550 
Library.foldr mk_all2 (xs, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

551 
Library.foldr mk_imp (mapn mk_prj 0 dnames, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

552 
foldr1 mk_conj (mapn mk_eqn 0 dnames))))); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

553 
fun x_tacs ctxt n x = [ 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

554 
rotate_tac (n+1) 1, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

555 
etac all2E 1, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

556 
eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

557 
TRY (safe_tac HOL_cs), 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

558 
REPEAT (CHANGED (asm_simp_tac take_ss 1))]; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

559 
fun tacs ctxt = [ 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

560 
rtac impI 1, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

561 
InductTacs.induct_tac ctxt [[SOME "n"]] 1, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

562 
simp_tac take_ss 1, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

563 
safe_tac HOL_cs] @ 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

564 
flat (mapn (x_tacs ctxt) 0 xs); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

565 
in pg [ax_bisim_def] goal tacs end; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

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

567 
val _ = trace " Proving coind..."; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

568 
val coind = 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

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

570 
fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'")); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

571 
fun mk_eqn x = %:x === %:(x^"'"); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

572 
val goal = 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

573 
mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===> 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

574 
Logic.list_implies (mapn mk_prj 0 xs, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

575 
mk_trp (foldr1 mk_conj (map mk_eqn xs))); 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

576 
val tacs = 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

577 
TRY (safe_tac HOL_cs) :: 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

578 
maps (fn take_lemma => [ 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

579 
rtac take_lemma 1, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

580 
cut_facts_tac [coind_lemma] 1, 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

581 
fast_tac HOL_cs 1]) 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

582 
take_lemmas; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

583 
in pg [] goal (K tacs) end; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

584 
end; (* local *) 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

585 

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

586 
in thy > Sign.add_path comp_dnam 
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

587 
> snd o PureThy.add_thmss [((Binding.name "coind", [coind]), [])] 
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

588 
> Sign.parent_path 
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

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

590 

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

591 
fun comp_theorems (comp_dnam, eqs: eq list) thy = 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

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

593 
val map_tab = Domain_Take_Proofs.get_map_tab thy; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

594 

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

595 
val dnames = map (fst o fst) eqs; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

596 
val comp_dname = Sign.full_bname thy comp_dnam; 
ee5df989b7c4
move coinductionrelated stuff into function prove_coindunction
huffman
parents:
35560
diff
changeset

597 

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

598 
(*  getting the composite axiom and definitions  *) 
23152  599 

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

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

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

602 
fun indirect_arg arg = 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

603 
rec_of arg = ~1 andalso Datatype_Aux.is_rec_type (dtyp_of arg); 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

604 
fun indirect_con (_, args) = exists indirect_arg args; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

605 
fun indirect_eq (_, cons) = exists indirect_con cons; 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

607 
val is_indirect = exists indirect_eq eqs; 
35599
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

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

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

610 
then message "Indirect recursion detected, skipping proofs of (co)induction rules" 
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

611 
else message ("Proving induction properties of domain "^comp_dname^" ..."); 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

613 

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

614 
(* theorems about take *) 
23152  615 

616 
local 

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

617 
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

618 
val axs_chain_take = map (ga "chain_take") dnames; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

619 
val axs_lub_take = map (ga "lub_take" ) dnames; 
23152  620 
in 
29402  621 
val _ = trace " Proving take_lemmas..."; 
23152  622 
val take_lemmas = 
623 
let 

35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

624 
fun take_lemma (ax_chain_take, ax_lub_take) = 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

626 
(@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]); 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

627 
in map take_lemma (axs_chain_take ~~ axs_lub_take) end; 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

628 
val axs_reach = 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

629 
let 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

630 
fun reach (ax_chain_take, ax_lub_take) = 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

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

632 
(@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]); 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35486
diff
changeset

633 
in map reach (axs_chain_take ~~ axs_lub_take) end; 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

634 
end; 
23152  635 

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

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

637 
maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames; 
23152  638 

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

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

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

641 
if is_indirect then thy else 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35574
diff
changeset

642 
prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews thy; 
23152  643 

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

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

645 
if is_indirect then thy else 
20670f5564e9
skip coinduction proofs for indirectrecursive domain definitions
huffman
parents:
35597
diff
changeset

646 
prove_coinduction (comp_dnam, eqs) take_lemmas thy; 
23152  647 

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

648 
in thy > Sign.add_path comp_dnam 
31004  649 
> snd o PureThy.add_thmss [ 
650 
((Binding.name "take_lemmas", take_lemmas ), []), 

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

651 
((Binding.name "reach" , axs_reach ), [])] 
28536  652 
> Sign.parent_path > pair take_rews 
23152  653 
end; (* let *) 
654 
end; (* struct *) 