126 (*lcp: curry the predicate of the induction rule*) |
126 (*lcp: curry the predicate of the induction rule*) |
127 fun curry_rule rl = |
127 fun curry_rule rl = |
128 Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl; |
128 Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl; |
129 |
129 |
130 (*lcp: put a theorem into Isabelle form, using meta-level connectives*) |
130 (*lcp: put a theorem into Isabelle form, using meta-level connectives*) |
131 val meta_outer = |
131 fun meta_outer ctxt = |
132 curry_rule o Drule.export_without_context o |
132 curry_rule o Drule.export_without_context o |
133 rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); |
133 rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); |
134 |
134 |
135 (*Strip off the outer !P*) |
135 (*Strip off the outer !P*) |
136 val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec; |
136 val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec; |
137 |
137 |
138 fun tracing true _ = () |
138 fun tracing true _ = () |
139 | tracing false msg = writeln msg; |
139 | tracing false msg = writeln msg; |
140 |
140 |
141 fun simplify_defn strict thy cs ss congs wfs id pats def0 = |
141 fun simplify_defn strict thy cs ss congs wfs id pats def0 = |
142 let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq |
142 let |
|
143 val ctxt = ProofContext.init thy |
|
144 val def = Thm.freezeT def0 RS meta_eq_to_obj_eq |
143 val {rules,rows,TCs,full_pats_TCs} = |
145 val {rules,rows,TCs,full_pats_TCs} = |
144 Prim.post_definition congs (thy, (def,pats)) |
146 Prim.post_definition congs (thy, (def,pats)) |
145 val {lhs=f,rhs} = S.dest_eq (concl def) |
147 val {lhs=f,rhs} = S.dest_eq (concl def) |
146 val (_,[R,_]) = S.strip_comb rhs |
148 val (_,[R,_]) = S.strip_comb rhs |
147 val dummy = Prim.trace_thms "congs =" congs |
149 val dummy = Prim.trace_thms "congs =" congs |
151 {f = f, R = R, rules = rules, |
153 {f = f, R = R, rules = rules, |
152 full_pats_TCs = full_pats_TCs, |
154 full_pats_TCs = full_pats_TCs, |
153 TCs = TCs} |
155 TCs = TCs} |
154 val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm) |
156 val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm) |
155 (R.CONJUNCTS rules) |
157 (R.CONJUNCTS rules) |
156 in {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')), |
158 in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')), |
157 rules = ListPair.zip(rules', rows), |
159 rules = ListPair.zip(rules', rows), |
158 tcs = (termination_goals rules') @ tcs} |
160 tcs = (termination_goals rules') @ tcs} |
159 end |
161 end |
160 handle U.ERR {mesg,func,module} => |
162 handle U.ERR {mesg,func,module} => |
161 error (mesg ^ |
163 error (mesg ^ |