66 Const("==",_)$_$_ => r |
66 Const("==",_)$_$_ => r |
67 | _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection |
67 | _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection |
68 | _ => r RS P_imp_P_eq_True |
68 | _ => r RS P_imp_P_eq_True |
69 |
69 |
70 (*Is this the best way to invoke the simplifier??*) |
70 (*Is this the best way to invoke the simplifier??*) |
71 fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L)) |
71 fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L)) |
72 |
72 |
73 fun join_assums th = |
73 fun join_assums th = |
74 let val thy = Thm.theory_of_thm th |
74 let val thy = Thm.theory_of_thm th |
|
75 val ctxt = Proof_Context.init_global thy |
75 val tych = cterm_of thy |
76 val tych = cterm_of thy |
76 val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th))) |
77 val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th))) |
77 val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *) |
78 val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *) |
78 val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *) |
79 val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *) |
79 val cntxt = union (op aconv) cntxtl cntxtr |
80 val cntxt = union (op aconv) cntxtl cntxtr |
80 in |
81 in |
81 Rules.GEN_ALL |
82 Rules.GEN_ALL |
82 (Rules.DISCH_ALL |
83 (Rules.DISCH_ALL |
83 (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th))) |
84 (rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th))) |
84 end |
85 end |
85 val gen_all = USyntax.gen_all |
86 val gen_all = USyntax.gen_all |
86 in |
87 in |
87 fun proof_stage strict ctxt wfs theory {f, R, rules, full_pats_TCs, TCs} = |
88 fun proof_stage strict ctxt wfs theory {f, R, rules, full_pats_TCs, TCs} = |
88 let |
89 let |
137 |
138 |
138 fun simplify_defn strict thy ctxt congs wfs id pats def0 = |
139 fun simplify_defn strict thy ctxt congs wfs id pats def0 = |
139 let |
140 let |
140 val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq |
141 val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq |
141 val {rules,rows,TCs,full_pats_TCs} = |
142 val {rules,rows,TCs,full_pats_TCs} = |
142 Prim.post_definition congs (thy, (def, pats)) |
143 Prim.post_definition congs thy ctxt (def, pats) |
143 val {lhs=f,rhs} = USyntax.dest_eq (concl def) |
144 val {lhs=f,rhs} = USyntax.dest_eq (concl def) |
144 val (_,[R,_]) = USyntax.strip_comb rhs |
145 val (_,[R,_]) = USyntax.strip_comb rhs |
145 val dummy = Prim.trace_thms "congs =" congs |
146 val dummy = Prim.trace_thms "congs =" congs |
146 (*the next step has caused simplifier looping in some cases*) |
147 (*the next step has caused simplifier looping in some cases*) |
147 val {induction, rules, tcs} = |
148 val {induction, rules, tcs} = |
148 proof_stage strict ctxt wfs thy |
149 proof_stage strict ctxt wfs thy |
149 {f = f, R = R, rules = rules, |
150 {f = f, R = R, rules = rules, |
150 full_pats_TCs = full_pats_TCs, |
151 full_pats_TCs = full_pats_TCs, |
151 TCs = TCs} |
152 TCs = TCs} |
152 val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm) |
153 val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt) |
153 (Rules.CONJUNCTS rules) |
154 (Rules.CONJUNCTS rules) |
154 in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')), |
155 in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')), |
155 rules = ListPair.zip(rules', rows), |
156 rules = ListPair.zip(rules', rows), |
156 tcs = (termination_goals rules') @ tcs} |
157 tcs = (termination_goals rules') @ tcs} |
157 end |
158 end |
158 handle Utils.ERR {mesg,func,module} => |
159 handle Utils.ERR {mesg,func,module} => |
159 error (mesg ^ |
160 error (mesg ^ |
168 |
169 |
169 fun solve_eq _ (th, [], i) = error "derive_init_eqs: missing rules" |
170 fun solve_eq _ (th, [], i) = error "derive_init_eqs: missing rules" |
170 | solve_eq _ (th, [a], i) = [(a, i)] |
171 | solve_eq _ (th, [a], i) = [(a, i)] |
171 | solve_eq ctxt (th, splitths, i) = |
172 | solve_eq ctxt (th, splitths, i) = |
172 (writeln "Proving unsplit equation..."; |
173 (writeln "Proving unsplit equation..."; |
173 [((Drule.export_without_context o Object_Logic.rulify_no_asm) |
174 [((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt) |
174 (CaseSplit.splitto ctxt splitths th), i)]) |
175 (CaseSplit.splitto ctxt splitths th), i)]) |
175 handle ERROR s => |
176 handle ERROR s => |
176 (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths); |
177 (warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths); |
177 in |
178 in |
178 fun derive_init_eqs ctxt rules eqs = |
179 fun derive_init_eqs ctxt rules eqs = |