134 | oras_of (tabs, AbsP (_, _, prf)) = oras_of (tabs, prf) |
134 | oras_of (tabs, AbsP (_, _, prf)) = oras_of (tabs, prf) |
135 | oras_of (tabs, prf % _) = oras_of (tabs, prf) |
135 | oras_of (tabs, prf % _) = oras_of (tabs, prf) |
136 | oras_of (tabs, prf1 %% prf2) = oras_of (oras_of (tabs, prf1), prf2) |
136 | oras_of (tabs, prf1 %% prf2) = oras_of (oras_of (tabs, prf1), prf2) |
137 | oras_of (tabs as (thms, oras), PThm ((name, _), prf, prop, _)) = |
137 | oras_of (tabs as (thms, oras), PThm ((name, _), prf, prop, _)) = |
138 (case Symtab.lookup (thms, name) of |
138 (case Symtab.lookup (thms, name) of |
139 None => oras_of ((Symtab.update ((name, [prop]), thms), oras), prf) |
139 NONE => oras_of ((Symtab.update ((name, [prop]), thms), oras), prf) |
140 | Some ps => if prop mem ps then tabs else |
140 | SOME ps => if prop mem ps then tabs else |
141 oras_of ((Symtab.update ((name, prop::ps), thms), oras), prf)) |
141 oras_of ((Symtab.update ((name, prop::ps), thms), oras), prf)) |
142 | oras_of ((thms, oras), prf as Oracle _) = (thms, prf ins oras) |
142 | oras_of ((thms, oras), prf as Oracle _) = (thms, prf ins oras) |
143 | oras_of (tabs, MinProof prfs) = foldl oras_of (tabs, prfs) |
143 | oras_of (tabs, MinProof prfs) = foldl oras_of (tabs, prfs) |
144 | oras_of (tabs, _) = tabs |
144 | oras_of (tabs, _) = tabs |
145 in |
145 in |
150 | thms_of_proof tab (AbsP (_, _, prf)) = thms_of_proof tab prf |
150 | thms_of_proof tab (AbsP (_, _, prf)) = thms_of_proof tab prf |
151 | thms_of_proof tab (prf1 %% prf2) = thms_of_proof (thms_of_proof tab prf1) prf2 |
151 | thms_of_proof tab (prf1 %% prf2) = thms_of_proof (thms_of_proof tab prf1) prf2 |
152 | thms_of_proof tab (prf % _) = thms_of_proof tab prf |
152 | thms_of_proof tab (prf % _) = thms_of_proof tab prf |
153 | thms_of_proof tab (prf' as PThm ((s, _), prf, prop, _)) = |
153 | thms_of_proof tab (prf' as PThm ((s, _), prf, prop, _)) = |
154 (case Symtab.lookup (tab, s) of |
154 (case Symtab.lookup (tab, s) of |
155 None => thms_of_proof (Symtab.update ((s, [(prop, prf')]), tab)) prf |
155 NONE => thms_of_proof (Symtab.update ((s, [(prop, prf')]), tab)) prf |
156 | Some ps => if exists (equal prop o fst) ps then tab else |
156 | SOME ps => if exists (equal prop o fst) ps then tab else |
157 thms_of_proof (Symtab.update ((s, (prop, prf')::ps), tab)) prf) |
157 thms_of_proof (Symtab.update ((s, (prop, prf')::ps), tab)) prf) |
158 | thms_of_proof tab (MinProof prfs) = foldl (uncurry thms_of_proof) (tab, prfs) |
158 | thms_of_proof tab (MinProof prfs) = foldl (uncurry thms_of_proof) (tab, prfs) |
159 | thms_of_proof tab _ = tab; |
159 | thms_of_proof tab _ = tab; |
160 |
160 |
161 fun axms_of_proof tab (Abst (_, _, prf)) = axms_of_proof tab prf |
161 fun axms_of_proof tab (Abst (_, _, prf)) = axms_of_proof tab prf |
235 handle SAME => AbsP (s, t, mapp prf)) |
235 handle SAME => AbsP (s, t, mapp prf)) |
236 | mapp (prf % t) = (mapp prf % apsome f t |
236 | mapp (prf % t) = (mapp prf % apsome f t |
237 handle SAME => prf % apsome' (same f) t) |
237 handle SAME => prf % apsome' (same f) t) |
238 | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2 |
238 | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2 |
239 handle SAME => prf1 %% mapp prf2) |
239 handle SAME => prf1 %% mapp prf2) |
240 | mapp (PThm (a, prf, prop, Some Ts)) = |
240 | mapp (PThm (a, prf, prop, SOME Ts)) = |
241 PThm (a, prf, prop, Some (same (map g) Ts)) |
241 PThm (a, prf, prop, SOME (same (map g) Ts)) |
242 | mapp (PAxm (a, prop, Some Ts)) = |
242 | mapp (PAxm (a, prop, SOME Ts)) = |
243 PAxm (a, prop, Some (same (map g) Ts)) |
243 PAxm (a, prop, SOME (same (map g) Ts)) |
244 | mapp _ = raise SAME |
244 | mapp _ = raise SAME |
245 and mapph prf = (mapp prf handle SAME => prf) |
245 and mapph prf = (mapp prf handle SAME => prf) |
246 |
246 |
247 in mapph end; |
247 in mapph end; |
248 |
248 |
249 fun fold_proof_terms f g (a, Abst (_, Some T, prf)) = fold_proof_terms f g (g (T, a), prf) |
249 fun fold_proof_terms f g (a, Abst (_, SOME T, prf)) = fold_proof_terms f g (g (T, a), prf) |
250 | fold_proof_terms f g (a, Abst (_, None, prf)) = fold_proof_terms f g (a, prf) |
250 | fold_proof_terms f g (a, Abst (_, NONE, prf)) = fold_proof_terms f g (a, prf) |
251 | fold_proof_terms f g (a, AbsP (_, Some t, prf)) = fold_proof_terms f g (f (t, a), prf) |
251 | fold_proof_terms f g (a, AbsP (_, SOME t, prf)) = fold_proof_terms f g (f (t, a), prf) |
252 | fold_proof_terms f g (a, AbsP (_, None, prf)) = fold_proof_terms f g (a, prf) |
252 | fold_proof_terms f g (a, AbsP (_, NONE, prf)) = fold_proof_terms f g (a, prf) |
253 | fold_proof_terms f g (a, prf % Some t) = f (t, fold_proof_terms f g (a, prf)) |
253 | fold_proof_terms f g (a, prf % SOME t) = f (t, fold_proof_terms f g (a, prf)) |
254 | fold_proof_terms f g (a, prf % None) = fold_proof_terms f g (a, prf) |
254 | fold_proof_terms f g (a, prf % NONE) = fold_proof_terms f g (a, prf) |
255 | fold_proof_terms f g (a, prf1 %% prf2) = fold_proof_terms f g |
255 | fold_proof_terms f g (a, prf1 %% prf2) = fold_proof_terms f g |
256 (fold_proof_terms f g (a, prf1), prf2) |
256 (fold_proof_terms f g (a, prf1), prf2) |
257 | fold_proof_terms _ g (a, PThm (_, _, _, Some Ts)) = foldr g (Ts, a) |
257 | fold_proof_terms _ g (a, PThm (_, _, _, SOME Ts)) = foldr g (Ts, a) |
258 | fold_proof_terms _ g (a, PAxm (_, prop, Some Ts)) = foldr g (Ts, a) |
258 | fold_proof_terms _ g (a, PAxm (_, prop, SOME Ts)) = foldr g (Ts, a) |
259 | fold_proof_terms _ _ (a, _) = a; |
259 | fold_proof_terms _ _ (a, _) = a; |
260 |
260 |
261 val add_prf_names = fold_proof_terms add_term_names ((uncurry K) o swap); |
261 val add_prf_names = fold_proof_terms add_term_names ((uncurry K) o swap); |
262 val add_prf_tfree_names = fold_proof_terms add_term_tfree_names add_typ_tfree_names; |
262 val add_prf_tfree_names = fold_proof_terms add_term_tfree_names add_typ_tfree_names; |
263 val add_prf_tvar_ixns = fold_proof_terms add_term_tvar_ixns (add_typ_ixns o swap); |
263 val add_prf_tvar_ixns = fold_proof_terms add_term_tvar_ixns (add_typ_ixns o swap); |
340 fun incr_pboundvars 0 0 prf = prf |
340 fun incr_pboundvars 0 0 prf = prf |
341 | incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf; |
341 | incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf; |
342 |
342 |
343 |
343 |
344 fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k |
344 fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k |
345 | prf_loose_bvar1 (prf % Some t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k) |
345 | prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k) |
346 | prf_loose_bvar1 (_ % None) _ = true |
346 | prf_loose_bvar1 (_ % NONE) _ = true |
347 | prf_loose_bvar1 (AbsP (_, Some t, prf)) k = loose_bvar1 (t, k) orelse prf_loose_bvar1 prf k |
347 | prf_loose_bvar1 (AbsP (_, SOME t, prf)) k = loose_bvar1 (t, k) orelse prf_loose_bvar1 prf k |
348 | prf_loose_bvar1 (AbsP (_, None, _)) k = true |
348 | prf_loose_bvar1 (AbsP (_, NONE, _)) k = true |
349 | prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1) |
349 | prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1) |
350 | prf_loose_bvar1 _ _ = false; |
350 | prf_loose_bvar1 _ _ = false; |
351 |
351 |
352 fun prf_loose_Pbvar1 (PBound i) k = i = k |
352 fun prf_loose_Pbvar1 (PBound i) k = i = k |
353 | prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k |
353 | prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k |
361 | prf_add_loose_bnos plev tlev (prf1 %% prf2) p = |
361 | prf_add_loose_bnos plev tlev (prf1 %% prf2) p = |
362 prf_add_loose_bnos plev tlev prf2 |
362 prf_add_loose_bnos plev tlev prf2 |
363 (prf_add_loose_bnos plev tlev prf1 p) |
363 (prf_add_loose_bnos plev tlev prf1 p) |
364 | prf_add_loose_bnos plev tlev (prf % opt) (is, js) = |
364 | prf_add_loose_bnos plev tlev (prf % opt) (is, js) = |
365 prf_add_loose_bnos plev tlev prf (case opt of |
365 prf_add_loose_bnos plev tlev prf (case opt of |
366 None => (is, ~1 ins js) |
366 NONE => (is, ~1 ins js) |
367 | Some t => (is, add_loose_bnos (t, tlev, js))) |
367 | SOME t => (is, add_loose_bnos (t, tlev, js))) |
368 | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) = |
368 | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) = |
369 prf_add_loose_bnos (plev+1) tlev prf (case opt of |
369 prf_add_loose_bnos (plev+1) tlev prf (case opt of |
370 None => (is, ~1 ins js) |
370 NONE => (is, ~1 ins js) |
371 | Some t => (is, add_loose_bnos (t, tlev, js))) |
371 | SOME t => (is, add_loose_bnos (t, tlev, js))) |
372 | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = |
372 | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = |
373 prf_add_loose_bnos plev (tlev+1) prf p |
373 prf_add_loose_bnos plev (tlev+1) prf p |
374 | prf_add_loose_bnos _ _ _ _ = ([], []); |
374 | prf_add_loose_bnos _ _ _ _ = ([], []); |
375 |
375 |
376 |
376 |
631 |
631 |
632 fun mk_app (b, (i, j, prf)) = |
632 fun mk_app (b, (i, j, prf)) = |
633 if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j); |
633 if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j); |
634 |
634 |
635 fun lift Us bs i j (Const ("==>", _) $ A $ B) = |
635 fun lift Us bs i j (Const ("==>", _) $ A $ B) = |
636 AbsP ("H", None (*A*), lift Us (true::bs) (i+1) j B) |
636 AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B) |
637 | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = |
637 | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = |
638 Abst (a, None (*T*), lift (T::Us) (false::bs) i (j+1) t) |
638 Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t) |
639 | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf, |
639 | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf, |
640 map (fn k => (#3 (foldr mk_app (bs, (i-1, j-1, PBound k))))) |
640 map (fn k => (#3 (foldr mk_app (bs, (i-1, j-1, PBound k))))) |
641 (i + k - 1 downto i)); |
641 (i + k - 1 downto i)); |
642 in |
642 in |
643 mk_AbsP (k, lift [] [] 0 0 Bi) |
643 mk_AbsP (k, lift [] [] 0 0 Bi) |
644 end; |
644 end; |
645 |
645 |
646 |
646 |
647 (***** proof by assumption *****) |
647 (***** proof by assumption *****) |
648 |
648 |
649 fun mk_asm_prf (Const ("==>", _) $ A $ B) i = AbsP ("H", None (*A*), mk_asm_prf B (i+1)) |
649 fun mk_asm_prf (Const ("==>", _) $ A $ B) i = AbsP ("H", NONE (*A*), mk_asm_prf B (i+1)) |
650 | mk_asm_prf (Const ("all", _) $ Abs (a, T, t)) i = Abst (a, None (*T*), mk_asm_prf t i) |
650 | mk_asm_prf (Const ("all", _) $ Abs (a, T, t)) i = Abst (a, NONE (*T*), mk_asm_prf t i) |
651 | mk_asm_prf _ i = PBound i; |
651 | mk_asm_prf _ i = PBound i; |
652 |
652 |
653 fun assumption_proof Bs Bi n prf = |
653 fun assumption_proof Bs Bi n prf = |
654 mk_AbsP (length Bs, proof_combP (prf, |
654 mk_AbsP (length Bs, proof_combP (prf, |
655 map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi (~n)])); |
655 map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi (~n)])); |
656 |
656 |
657 |
657 |
658 (***** Composition of object rule with proof state *****) |
658 (***** Composition of object rule with proof state *****) |
659 |
659 |
660 fun flatten_params_proof i j n (Const ("==>", _) $ A $ B, k) = |
660 fun flatten_params_proof i j n (Const ("==>", _) $ A $ B, k) = |
661 AbsP ("H", None (*A*), flatten_params_proof (i+1) j n (B, k)) |
661 AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k)) |
662 | flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) = |
662 | flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) = |
663 Abst (a, None (*T*), flatten_params_proof i (j+1) n (t, k)) |
663 Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k)) |
664 | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), |
664 | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), |
665 map Bound (j-1 downto 0)), map PBound (i-1 downto 0 \ i-n)); |
665 map Bound (j-1 downto 0)), map PBound (i-1 downto 0 \ i-n)); |
666 |
666 |
667 fun bicompose_proof Bs oldAs newAs A n rprf sprf = |
667 fun bicompose_proof Bs oldAs newAs A n rprf sprf = |
668 let |
668 let |
704 ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], |
704 ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], |
705 Logic.mk_equals (f $ x, g $ y)))]; |
705 Logic.mk_equals (f $ x, g $ y)))]; |
706 |
706 |
707 val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, |
707 val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, |
708 equal_elim_axm, abstract_rule_axm, combination_axm] = |
708 equal_elim_axm, abstract_rule_axm, combination_axm] = |
709 map (fn (s, t) => PAxm ("ProtoPure." ^ s, varify t, None)) equality_axms; |
709 map (fn (s, t) => PAxm ("ProtoPure." ^ s, varify t, NONE)) equality_axms; |
710 |
710 |
711 end; |
711 end; |
712 |
712 |
713 val reflexive = reflexive_axm % None; |
713 val reflexive = reflexive_axm % NONE; |
714 |
714 |
715 fun symmetric (prf as PAxm ("ProtoPure.reflexive", _, _) % _) = prf |
715 fun symmetric (prf as PAxm ("ProtoPure.reflexive", _, _) % _) = prf |
716 | symmetric prf = symmetric_axm % None % None %% prf; |
716 | symmetric prf = symmetric_axm % NONE % NONE %% prf; |
717 |
717 |
718 fun transitive _ _ (PAxm ("ProtoPure.reflexive", _, _) % _) prf2 = prf2 |
718 fun transitive _ _ (PAxm ("ProtoPure.reflexive", _, _) % _) prf2 = prf2 |
719 | transitive _ _ prf1 (PAxm ("ProtoPure.reflexive", _, _) % _) = prf1 |
719 | transitive _ _ prf1 (PAxm ("ProtoPure.reflexive", _, _) % _) = prf1 |
720 | transitive u (Type ("prop", [])) prf1 prf2 = |
720 | transitive u (Type ("prop", [])) prf1 prf2 = |
721 transitive_axm % None % Some (remove_types u) % None %% prf1 %% prf2 |
721 transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2 |
722 | transitive u T prf1 prf2 = |
722 | transitive u T prf1 prf2 = |
723 transitive_axm % None % None % None %% prf1 %% prf2; |
723 transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; |
724 |
724 |
725 fun abstract_rule x a prf = |
725 fun abstract_rule x a prf = |
726 abstract_rule_axm % None % None %% forall_intr_proof x a prf; |
726 abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf; |
727 |
727 |
728 fun check_comb (PAxm ("ProtoPure.combination", _, _) % f % g % _ % _ %% prf %% _) = |
728 fun check_comb (PAxm ("ProtoPure.combination", _, _) % f % g % _ % _ %% prf %% _) = |
729 is_some f orelse check_comb prf |
729 is_some f orelse check_comb prf |
730 | check_comb (PAxm ("ProtoPure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = |
730 | check_comb (PAxm ("ProtoPure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = |
731 check_comb prf1 andalso check_comb prf2 |
731 check_comb prf1 andalso check_comb prf2 |
735 fun combination f g t u (Type (_, [T, U])) prf1 prf2 = |
735 fun combination f g t u (Type (_, [T, U])) prf1 prf2 = |
736 let |
736 let |
737 val f = Envir.beta_norm f; |
737 val f = Envir.beta_norm f; |
738 val g = Envir.beta_norm g; |
738 val g = Envir.beta_norm g; |
739 val prf = if check_comb prf1 then |
739 val prf = if check_comb prf1 then |
740 combination_axm % None % None |
740 combination_axm % NONE % NONE |
741 else (case prf1 of |
741 else (case prf1 of |
742 PAxm ("ProtoPure.reflexive", _, _) % _ => |
742 PAxm ("ProtoPure.reflexive", _, _) % _ => |
743 combination_axm %> remove_types f % None |
743 combination_axm %> remove_types f % NONE |
744 | _ => combination_axm %> remove_types f %> remove_types g) |
744 | _ => combination_axm %> remove_types f %> remove_types g) |
745 in |
745 in |
746 (case T of |
746 (case T of |
747 Type ("fun", _) => prf % |
747 Type ("fun", _) => prf % |
748 (case head_of f of |
748 (case head_of f of |
749 Abs _ => Some (remove_types t) |
749 Abs _ => SOME (remove_types t) |
750 | Var _ => Some (remove_types t) |
750 | Var _ => SOME (remove_types t) |
751 | _ => None) % |
751 | _ => NONE) % |
752 (case head_of g of |
752 (case head_of g of |
753 Abs _ => Some (remove_types u) |
753 Abs _ => SOME (remove_types u) |
754 | Var _ => Some (remove_types u) |
754 | Var _ => SOME (remove_types u) |
755 | _ => None) %% prf1 %% prf2 |
755 | _ => NONE) %% prf1 %% prf2 |
756 | _ => prf % None % None %% prf1 %% prf2) |
756 | _ => prf % NONE % NONE %% prf1 %% prf2) |
757 end; |
757 end; |
758 |
758 |
759 fun equal_intr A B prf1 prf2 = |
759 fun equal_intr A B prf1 prf2 = |
760 equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; |
760 equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; |
761 |
761 |
819 |
819 |
820 fun gen_axm_proof c name prop = |
820 fun gen_axm_proof c name prop = |
821 let |
821 let |
822 val nvs = needed_vars prop; |
822 val nvs = needed_vars prop; |
823 val args = map (fn (v as Var (ixn, _)) => |
823 val args = map (fn (v as Var (ixn, _)) => |
824 if ixn mem nvs then Some v else None) (vars_of prop) @ |
824 if ixn mem nvs then SOME v else NONE) (vars_of prop) @ |
825 map Some (sort (make_ord atless) (term_frees prop)); |
825 map SOME (sort (make_ord atless) (term_frees prop)); |
826 in |
826 in |
827 proof_combt' (c (name, prop, None), args) |
827 proof_combt' (c (name, prop, NONE), args) |
828 end; |
828 end; |
829 |
829 |
830 val axm_proof = gen_axm_proof PAxm; |
830 val axm_proof = gen_axm_proof PAxm; |
831 val oracle_proof = gen_axm_proof Oracle; |
831 val oracle_proof = gen_axm_proof Oracle; |
832 |
832 |
833 fun shrink ls lev (prf as Abst (a, T, body)) = |
833 fun shrink ls lev (prf as Abst (a, T, body)) = |
834 let val (b, is, ch, body') = shrink ls (lev+1) body |
834 let val (b, is, ch, body') = shrink ls (lev+1) body |
835 in (b, is, ch, if ch then Abst (a, T, body') else prf) end |
835 in (b, is, ch, if ch then Abst (a, T, body') else prf) end |
836 | shrink ls lev (prf as AbsP (a, t, body)) = |
836 | shrink ls lev (prf as AbsP (a, t, body)) = |
837 let val (b, is, ch, body') = shrink (lev::ls) lev body |
837 let val (b, is, ch, body') = shrink (lev::ls) lev body |
838 in (b orelse 0 mem is, mapfilter (fn 0 => None | i => Some (i-1)) is, |
838 in (b orelse 0 mem is, mapfilter (fn 0 => NONE | i => SOME (i-1)) is, |
839 ch, if ch then AbsP (a, t, body') else prf) |
839 ch, if ch then AbsP (a, t, body') else prf) |
840 end |
840 end |
841 | shrink ls lev prf = |
841 | shrink ls lev prf = |
842 let val (is, ch, _, prf') = shrink' ls lev [] [] prf |
842 let val (is, ch, _, prf') = shrink' ls lev [] [] prf |
843 in (false, is, ch, prf') end |
843 in (false, is, ch, prf') end |
850 end |
850 end |
851 | shrink' ls lev ts prfs (prf as prf1 % t) = |
851 | shrink' ls lev ts prfs (prf as prf1 % t) = |
852 let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1 |
852 let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1 |
853 in (is, ch orelse ch', ts', if ch orelse ch' then prf' % t' else prf) end |
853 in (is, ch orelse ch', ts', if ch orelse ch' then prf' % t' else prf) end |
854 | shrink' ls lev ts prfs (prf as PBound i) = |
854 | shrink' ls lev ts prfs (prf as PBound i) = |
855 (if exists (fn Some (Bound j) => lev-j <= nth_elem (i, ls) | _ => true) ts |
855 (if exists (fn SOME (Bound j) => lev-j <= nth_elem (i, ls) | _ => true) ts |
856 orelse not (null (duplicates |
856 orelse not (null (duplicates |
857 (foldl (fn (js, Some (Bound j)) => j :: js | (js, _) => js) ([], ts)))) |
857 (foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts)))) |
858 orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf) |
858 orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf) |
859 | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf) |
859 | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf) |
860 | shrink' ls lev ts prfs (prf as MinProof _) = |
860 | shrink' ls lev ts prfs (prf as MinProof _) = |
861 ([], false, map (pair false) ts, prf) |
861 ([], false, map (pair false) ts, prf) |
862 | shrink' ls lev ts prfs prf = |
862 | shrink' ls lev ts prfs prf = |
866 val vs = vars_of prop; |
866 val vs = vars_of prop; |
867 val (ts', ts'') = splitAt (length vs, ts) |
867 val (ts', ts'') = splitAt (length vs, ts) |
868 val insts = take (length ts', map (fst o dest_Var) vs) ~~ ts'; |
868 val insts = take (length ts', map (fst o dest_Var) vs) ~~ ts'; |
869 val nvs = foldl (fn (ixns', (ixn, ixns)) => |
869 val nvs = foldl (fn (ixns', (ixn, ixns)) => |
870 ixn ins (case assoc (insts, ixn) of |
870 ixn ins (case assoc (insts, ixn) of |
871 Some (Some t) => if is_proj t then ixns union ixns' else ixns' |
871 SOME (SOME t) => if is_proj t then ixns union ixns' else ixns' |
872 | _ => ixns union ixns')) |
872 | _ => ixns union ixns')) |
873 (needed prop ts'' prfs, add_npvars false true [] ([], prop)); |
873 (needed prop ts'' prfs, add_npvars false true [] ([], prop)); |
874 val insts' = map |
874 val insts' = map |
875 (fn (ixn, x as Some _) => if ixn mem nvs then (false, x) else (true, None) |
875 (fn (ixn, x as SOME _) => if ixn mem nvs then (false, x) else (true, NONE) |
876 | (_, x) => (false, x)) insts |
876 | (_, x) => (false, x)) insts |
877 in ([], false, insts' @ map (pair false) ts'', prf) end |
877 in ([], false, insts' @ map (pair false) ts'', prf) end |
878 and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) = |
878 and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) = |
879 (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs |
879 (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs |
880 | needed (Var (ixn, _)) (_::_) _ = [ixn] |
880 | needed (Var (ixn, _)) (_::_) _ = [ixn] |
971 | subst plev tlev (Abst (a, T, body)) = |
971 | subst plev tlev (Abst (a, T, body)) = |
972 Abst (a, apsome substT T, subst plev (tlev+1) body) |
972 Abst (a, apsome substT T, subst plev (tlev+1) body) |
973 | subst plev tlev (prf %% prf') = subst plev tlev prf %% subst plev tlev prf' |
973 | subst plev tlev (prf %% prf') = subst plev tlev prf %% subst plev tlev prf' |
974 | subst plev tlev (prf % t) = subst plev tlev prf % apsome (subst' tlev) t |
974 | subst plev tlev (prf % t) = subst plev tlev prf % apsome (subst' tlev) t |
975 | subst plev tlev (prf as Hyp (Var (ixn, _))) = (case assoc (pinst, ixn) of |
975 | subst plev tlev (prf as Hyp (Var (ixn, _))) = (case assoc (pinst, ixn) of |
976 None => prf |
976 NONE => prf |
977 | Some prf' => incr_pboundvars plev tlev prf') |
977 | SOME prf' => incr_pboundvars plev tlev prf') |
978 | subst _ _ (PThm (id, prf, prop, Ts)) = |
978 | subst _ _ (PThm (id, prf, prop, Ts)) = |
979 PThm (id, prf, prop, apsome (map substT) Ts) |
979 PThm (id, prf, prop, apsome (map substT) Ts) |
980 | subst _ _ (PAxm (id, prop, Ts)) = |
980 | subst _ _ (PAxm (id, prop, Ts)) = |
981 PAxm (id, prop, apsome (map substT) Ts) |
981 PAxm (id, prop, apsome (map substT) Ts) |
982 | subst _ _ t = t |
982 | subst _ _ t = t |
1015 |
1015 |
1016 val skel0 = PBound 0; |
1016 val skel0 = PBound 0; |
1017 |
1017 |
1018 fun rewrite_prf tymatch (rules, procs) prf = |
1018 fun rewrite_prf tymatch (rules, procs) prf = |
1019 let |
1019 let |
1020 fun rew _ (Abst (_, _, body) % Some t) = Some (prf_subst_bounds [t] body, skel0) |
1020 fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, skel0) |
1021 | rew _ (AbsP (_, _, body) %% prf) = Some (prf_subst_pbounds [prf] body, skel0) |
1021 | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, skel0) |
1022 | rew Ts prf = (case get_first (fn (_, r) => r Ts prf) procs of |
1022 | rew Ts prf = (case get_first (fn (_, r) => r Ts prf) procs of |
1023 Some prf' => Some (prf', skel0) |
1023 SOME prf' => SOME (prf', skel0) |
1024 | None => get_first (fn (prf1, prf2) => Some (prf_subst |
1024 | NONE => get_first (fn (prf1, prf2) => SOME (prf_subst |
1025 (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2) |
1025 (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2) |
1026 handle PMatch => None) (filter (could_unify prf o fst) rules)); |
1026 handle PMatch => NONE) (filter (could_unify prf o fst) rules)); |
1027 |
1027 |
1028 fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) = |
1028 fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) = |
1029 if prf_loose_Pbvar1 prf' 0 then rew Ts prf |
1029 if prf_loose_Pbvar1 prf' 0 then rew Ts prf |
1030 else |
1030 else |
1031 let val prf'' = incr_pboundvars (~1) 0 prf' |
1031 let val prf'' = incr_pboundvars (~1) 0 prf' |
1032 in Some (if_none (rew Ts prf'') (prf'', skel0)) end |
1032 in SOME (if_none (rew Ts prf'') (prf'', skel0)) end |
1033 | rew0 Ts (prf as Abst (_, _, prf' % Some (Bound 0))) = |
1033 | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) = |
1034 if prf_loose_bvar1 prf' 0 then rew Ts prf |
1034 if prf_loose_bvar1 prf' 0 then rew Ts prf |
1035 else |
1035 else |
1036 let val prf'' = incr_pboundvars 0 (~1) prf' |
1036 let val prf'' = incr_pboundvars 0 (~1) prf' |
1037 in Some (if_none (rew Ts prf'') (prf'', skel0)) end |
1037 in SOME (if_none (rew Ts prf'') (prf'', skel0)) end |
1038 | rew0 Ts prf = rew Ts prf; |
1038 | rew0 Ts prf = rew Ts prf; |
1039 |
1039 |
1040 fun rew1 _ (Hyp (Var _)) _ = None |
1040 fun rew1 _ (Hyp (Var _)) _ = NONE |
1041 | rew1 Ts skel prf = (case rew2 Ts skel prf of |
1041 | rew1 Ts skel prf = (case rew2 Ts skel prf of |
1042 Some prf1 => (case rew0 Ts prf1 of |
1042 SOME prf1 => (case rew0 Ts prf1 of |
1043 Some (prf2, skel') => Some (if_none (rew1 Ts skel' prf2) prf2) |
1043 SOME (prf2, skel') => SOME (if_none (rew1 Ts skel' prf2) prf2) |
1044 | None => Some prf1) |
1044 | NONE => SOME prf1) |
1045 | None => (case rew0 Ts prf of |
1045 | NONE => (case rew0 Ts prf of |
1046 Some (prf1, skel') => Some (if_none (rew1 Ts skel' prf1) prf1) |
1046 SOME (prf1, skel') => SOME (if_none (rew1 Ts skel' prf1) prf1) |
1047 | None => None)) |
1047 | NONE => NONE)) |
1048 |
1048 |
1049 and rew2 Ts skel (prf % Some t) = (case prf of |
1049 and rew2 Ts skel (prf % SOME t) = (case prf of |
1050 Abst (_, _, body) => |
1050 Abst (_, _, body) => |
1051 let val prf' = prf_subst_bounds [t] body |
1051 let val prf' = prf_subst_bounds [t] body |
1052 in Some (if_none (rew2 Ts skel0 prf') prf') end |
1052 in SOME (if_none (rew2 Ts skel0 prf') prf') end |
1053 | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf of |
1053 | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf of |
1054 Some prf' => Some (prf' % Some t) |
1054 SOME prf' => SOME (prf' % SOME t) |
1055 | None => None)) |
1055 | NONE => NONE)) |
1056 | rew2 Ts skel (prf % None) = apsome (fn prf' => prf' % None) |
1056 | rew2 Ts skel (prf % NONE) = apsome (fn prf' => prf' % NONE) |
1057 (rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf) |
1057 (rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf) |
1058 | rew2 Ts skel (prf1 %% prf2) = (case prf1 of |
1058 | rew2 Ts skel (prf1 %% prf2) = (case prf1 of |
1059 AbsP (_, _, body) => |
1059 AbsP (_, _, body) => |
1060 let val prf' = prf_subst_pbounds [prf2] body |
1060 let val prf' = prf_subst_pbounds [prf2] body |
1061 in Some (if_none (rew2 Ts skel0 prf') prf') end |
1061 in SOME (if_none (rew2 Ts skel0 prf') prf') end |
1062 | _ => |
1062 | _ => |
1063 let val (skel1, skel2) = (case skel of |
1063 let val (skel1, skel2) = (case skel of |
1064 skel1 %% skel2 => (skel1, skel2) |
1064 skel1 %% skel2 => (skel1, skel2) |
1065 | _ => (skel0, skel0)) |
1065 | _ => (skel0, skel0)) |
1066 in case rew1 Ts skel1 prf1 of |
1066 in case rew1 Ts skel1 prf1 of |
1067 Some prf1' => (case rew1 Ts skel2 prf2 of |
1067 SOME prf1' => (case rew1 Ts skel2 prf2 of |
1068 Some prf2' => Some (prf1' %% prf2') |
1068 SOME prf2' => SOME (prf1' %% prf2') |
1069 | None => Some (prf1' %% prf2)) |
1069 | NONE => SOME (prf1' %% prf2)) |
1070 | None => (case rew1 Ts skel2 prf2 of |
1070 | NONE => (case rew1 Ts skel2 prf2 of |
1071 Some prf2' => Some (prf1 %% prf2') |
1071 SOME prf2' => SOME (prf1 %% prf2') |
1072 | None => None) |
1072 | NONE => NONE) |
1073 end) |
1073 end) |
1074 | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (if_none T dummyT :: Ts) |
1074 | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (if_none T dummyT :: Ts) |
1075 (case skel of Abst (_, _, skel') => skel' | _ => skel0) prf of |
1075 (case skel of Abst (_, _, skel') => skel' | _ => skel0) prf of |
1076 Some prf' => Some (Abst (s, T, prf')) |
1076 SOME prf' => SOME (Abst (s, T, prf')) |
1077 | None => None) |
1077 | NONE => NONE) |
1078 | rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts |
1078 | rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts |
1079 (case skel of AbsP (_, _, skel') => skel' | _ => skel0) prf of |
1079 (case skel of AbsP (_, _, skel') => skel' | _ => skel0) prf of |
1080 Some prf' => Some (AbsP (s, t, prf')) |
1080 SOME prf' => SOME (AbsP (s, t, prf')) |
1081 | None => None) |
1081 | NONE => NONE) |
1082 | rew2 _ _ _ = None |
1082 | rew2 _ _ _ = NONE |
1083 |
1083 |
1084 in if_none (rew1 [] skel0 prf) prf end; |
1084 in if_none (rew1 [] skel0 prf) prf end; |
1085 |
1085 |
1086 fun rewrite_proof tsig = rewrite_prf (fn (tab, f) => |
1086 fun rewrite_proof tsig = rewrite_prf (fn (tab, f) => |
1087 Type.typ_match tsig (tab, f ()) handle Type.TYPE_MATCH => raise PMatch); |
1087 Type.typ_match tsig (tab, f ()) handle Type.TYPE_MATCH => raise PMatch); |
1121 fun thm_proof sign (name, tags) hyps prop prf = |
1121 fun thm_proof sign (name, tags) hyps prop prf = |
1122 let |
1122 let |
1123 val prop = Logic.list_implies (hyps, prop); |
1123 val prop = Logic.list_implies (hyps, prop); |
1124 val nvs = needed_vars prop; |
1124 val nvs = needed_vars prop; |
1125 val args = map (fn (v as Var (ixn, _)) => |
1125 val args = map (fn (v as Var (ixn, _)) => |
1126 if ixn mem nvs then Some v else None) (vars_of prop) @ |
1126 if ixn mem nvs then SOME v else NONE) (vars_of prop) @ |
1127 map Some (sort (make_ord atless) (term_frees prop)); |
1127 map SOME (sort (make_ord atless) (term_frees prop)); |
1128 val opt_prf = if ! proofs = 2 then |
1128 val opt_prf = if ! proofs = 2 then |
1129 #4 (shrink [] 0 (rewrite_prf fst (ProofData.get_sg sign) |
1129 #4 (shrink [] 0 (rewrite_prf fst (ProofData.get_sg sign) |
1130 (foldr (uncurry implies_intr_proof) (hyps, prf)))) |
1130 (foldr (uncurry implies_intr_proof) (hyps, prf)))) |
1131 else MinProof (mk_min_proof ([], prf)); |
1131 else MinProof (mk_min_proof ([], prf)); |
1132 val head = (case strip_combt (fst (strip_combP prf)) of |
1132 val head = (case strip_combt (fst (strip_combP prf)) of |
1133 (PThm ((old_name, _), prf', prop', None), args') => |
1133 (PThm ((old_name, _), prf', prop', NONE), args') => |
1134 if (old_name="" orelse old_name=name) andalso |
1134 if (old_name="" orelse old_name=name) andalso |
1135 prop = prop' andalso args = args' then |
1135 prop = prop' andalso args = args' then |
1136 PThm ((name, tags), prf', prop, None) |
1136 PThm ((name, tags), prf', prop, NONE) |
1137 else |
1137 else |
1138 PThm ((name, tags), opt_prf, prop, None) |
1138 PThm ((name, tags), opt_prf, prop, NONE) |
1139 | _ => PThm ((name, tags), opt_prf, prop, None)) |
1139 | _ => PThm ((name, tags), opt_prf, prop, NONE)) |
1140 in |
1140 in |
1141 proof_combP (proof_combt' (head, args), map Hyp hyps) |
1141 proof_combP (proof_combt' (head, args), map Hyp hyps) |
1142 end; |
1142 end; |
1143 |
1143 |
1144 fun get_name_tags hyps prop prf = |
1144 fun get_name_tags hyps prop prf = |