equal
deleted
inserted
replaced
835 |
835 |
836 (***** axioms and theorems *****) |
836 (***** axioms and theorems *****) |
837 |
837 |
838 val proofs = ref 2; |
838 val proofs = ref 2; |
839 |
839 |
840 fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []); |
840 fun vars_of t = map Var (rev (Term.add_vars t [])); |
|
841 fun frees_of t = map Free (rev (Term.add_frees t [])); |
841 |
842 |
842 fun test_args _ [] = true |
843 fun test_args _ [] = true |
843 | test_args is (Bound i :: ts) = |
844 | test_args is (Bound i :: ts) = |
844 not (member (op =) is i) andalso test_args (i :: is) ts |
845 not (member (op =) is i) andalso test_args (i :: is) ts |
845 | test_args _ _ = false; |
846 | test_args _ _ = false; |
893 fun gen_axm_proof c name prop = |
894 fun gen_axm_proof c name prop = |
894 let |
895 let |
895 val nvs = needed_vars prop; |
896 val nvs = needed_vars prop; |
896 val args = map (fn (v as Var (ixn, _)) => |
897 val args = map (fn (v as Var (ixn, _)) => |
897 if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @ |
898 if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @ |
898 map SOME (sort Term.term_ord (term_frees prop)); |
899 map SOME (frees_of prop); |
899 in |
900 in |
900 proof_combt' (c (name, prop, NONE), args) |
901 proof_combt' (c (name, prop, NONE), args) |
901 end; |
902 end; |
902 |
903 |
903 val axm_proof = gen_axm_proof PAxm; |
904 val axm_proof = gen_axm_proof PAxm; |
1216 val PBody {oracles = oracles0, thms = thms0, proof = prf} = body; |
1217 val PBody {oracles = oracles0, thms = thms0, proof = prf} = body; |
1217 val prop = Logic.list_implies (hyps, prop); |
1218 val prop = Logic.list_implies (hyps, prop); |
1218 val nvs = needed_vars prop; |
1219 val nvs = needed_vars prop; |
1219 val args = map (fn (v as Var (ixn, _)) => |
1220 val args = map (fn (v as Var (ixn, _)) => |
1220 if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @ |
1221 if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @ |
1221 map SOME (sort Term.term_ord (term_frees prop)); |
1222 map SOME (frees_of prop); |
1222 |
1223 |
1223 val proof0 = |
1224 val proof0 = |
1224 if ! proofs = 2 then |
1225 if ! proofs = 2 then |
1225 #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf))) |
1226 #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf))) |
1226 else MinProof; |
1227 else MinProof; |