improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type
1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Apr 28 15:42:10 2010 +0200
1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Apr 28 16:45:48 2010 +0200
1.3 @@ -531,14 +531,17 @@
1.4 let
1.5 val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
1.6 val case_th = MetaSimplifier.simplify true
1.7 - (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs)
1.8 - (nth cases (i - 1))
1.9 + (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
1.10 val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
1.11 val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
1.12 val (_, tenv) = fold (Pattern.match thy) pats (Vartab.empty, Vartab.empty)
1.13 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
1.14 val inst = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
1.15 - val thesis = Thm.instantiate ([], inst) case_th OF (replicate nargs @{thm refl}) OF prems'
1.16 + val case_th' = Thm.instantiate ([], inst) case_th OF (replicate nargs @{thm refl})
1.17 + val (_, tenv) = fold (Pattern.match thy) (prems_of case_th' ~~ map prop_of prems') (Vartab.empty, Vartab.empty)
1.18 + val inst' = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
1.19 + val case_th'' = Thm.instantiate ([], inst') case_th'
1.20 + val thesis = case_th'' OF prems'
1.21 in
1.22 (rtac thesis 1)
1.23 end