diff --git a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy @@ -1,826 +1,817 @@ (* Title: HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Author: Nik Sultana, Cambridge University Computer Laboratory Various tests for the proof reconstruction module. NOTE - looks for THF proofs in the path indicated by $THF_PROOFS - these proofs are generated using LEO-II with the following configuration choices: -po 1 -nux -nuc --expand_extuni You can simply filter LEO-II's output using the filter_proof script which is distributed with LEO-II. *) theory TPTP_Proof_Reconstruction_Test imports TPTP_Test TPTP_Proof_Reconstruction begin section "Main function" text "This function wraps all the reconstruction-related functions. Simply point it at a THF proof produced by LEO-II (using the configuration described above), and it will try to reconstruct it into an Isabelle/HOL theorem. It also returns the theory (into which the axioms and definitions used in the proof have been imported), but note that you can get the theory value from the theorem value." ML \ reconstruct_leo2 (Path.explode "$THF_PROOFS/NUM667^1.p.out") @{theory} \ section "Prep for testing the component functions" declare [[ tptp_trace_reconstruction = false, tptp_test_all = false, (* tptp_test_all = true, *) tptp_test_timeout = 30, (* tptp_max_term_size = 200 *) tptp_max_term_size = 0 ]] declare [[ML_exception_trace, ML_print_depth = 200]] section "Importing proofs" ML \ val probs = (* "$THF_PROOFS/SYN991^1.p.out" *) (*lacks conjecture*) (* "$THF_PROOFS/SYO040^2.p.out" *) (* "$THF_PROOFS/NUM640^1.p.out" *) (* "$THF_PROOFS/SEU553^2.p.out" *) (* "$THF_PROOFS/NUM665^1.p.out" *) (* "$THF_PROOFS/SEV161^5.p.out" *) (* "$THF_PROOFS/SET014^4.p.out" *) "$THF_PROOFS/NUM667^1.p.out" |> Path.explode |> single val prob_names = probs |> map (Path.file_name #> TPTP_Problem_Name.Nonstandard) \ setup \ if test_all @{context} then I else fold (fn path => TPTP_Reconstruct.import_thm true [Path.dir path, Path.explode "$THF_PROOFS"] path leo2_on_load) probs \ text "Display nicely." ML \ fun display_nicely ctxt (fms : TPTP_Reconstruct.formula_meaning list) = List.app (fn ((n, data) : TPTP_Reconstruct.formula_meaning) => Pretty.writeln (Pretty.block [Pretty.str (n ^ " "), Syntax.pretty_term ctxt (#fmla data), Pretty.str ( if is_none (#source_inf_opt data) then "" else ("\n\tannotation: " ^ @{make_string} (the (#source_inf_opt data : TPTP_Proof.source_info option))))]) ) (rev fms); (*FIXME hack for testing*) fun test_fmla thy = TPTP_Reconstruct.get_fmlas_of_prob thy (hd prob_names); fun test_pannot thy = TPTP_Reconstruct.get_pannot_of_prob thy (hd prob_names); if test_all @{context} orelse prob_names = [] then () else display_nicely @{context} (#meta (test_pannot @{theory})) (* To look at the original proof (i.e., before the proof transformations applied when the proof is loaded) replace previous line with: (test_fmla @{theory} |> map TPTP_Reconstruct.structure_fmla_meaning) *) \ ML \ fun step_range_tester f_x f_exn ctxt prob_name from until = let val max = case until of SOME x => x | NONE => if is_some Int.maxInt then the Int.maxInt else 999999 fun test_step x = if x > max then () else (f_x x; (interpret_leo2_inference ctxt prob_name (Int.toString x); ()) handle e => f_exn e; (*FIXME naive. should let Interrupt through*) (*assumes that inferences are numbered consecutively*) test_step (x + 1)) in test_step from end val step_range_tester_tracing = step_range_tester (fn x => tracing ("@step " ^ Int.toString x)) (fn e => tracing ("!!" ^ @{make_string} e)) \ ML \ (*try to reconstruct each inference step*) if test_all @{context} orelse prob_names = [] orelse true (*NOTE currently disabled*) then () else let (*FIXME not guaranteed to be the right nodes*) val heur_start = 3 val heur_end = hd (#meta (test_pannot @{theory})) |> #1 |> Int.fromString in step_range_tester_tracing @{context} (hd prob_names) heur_start heur_end end \ section "Building metadata and tactics" subsection "Building the skeleton" ML \ if test_all @{context} orelse prob_names = [] then [] else TPTP_Reconstruct.make_skeleton @{context} (test_pannot @{theory}); length it \ subsection "The 'one shot' tactic approach" ML \ val the_tactic = if test_all @{context} then [] else map (fn prob_name => (TPTP_Reconstruct.naive_reconstruct_tac @{context} interpret_leo2_inference (* auto_based_reconstruction_tac *) (* oracle_based_reconstruction_tac *) prob_name)) prob_names; \ subsection "The 'piecemeal' approach" ML \ val the_tactics = if test_all @{context} then [] else map (fn prob_name => TPTP_Reconstruct.naive_reconstruct_tacs interpret_leo2_inference (* auto_based_reconstruction_tac *) (* oracle_based_reconstruction_tac *) prob_name @{context}) prob_names; \ declare [[ML_print_depth = 2000]] ML \ the_tactics |> map (filter (fn (_, _, x) => is_none x) #> map (fn (x, SOME y, _) => (x, cterm_of @{theory} y))) \ section "Using metadata and tactics" text "There are various ways of testing the two ways (whole tactics or lists of tactics) of representing 'reconstructors'." subsection "The 'one shot' tactic approach" text "First we test whole tactics." ML \ (*produce thm*) if test_all @{context} then [] else map ( (* try *) (TPTP_Reconstruct.reconstruct @{context} (fn prob_name => TPTP_Reconstruct.naive_reconstruct_tac @{context} interpret_leo2_inference prob_name (* oracle_based_reconstruction_tac *)))) prob_names \ subsection "The 'piecemeal' approach" ML \ fun attac n = List.nth (List.nth (the_tactics, 0), n) |> #3 |> the |> snd fun attac_to n 0 = attac n | attac_to n m = attac n THEN attac_to (n + 1) (m - 1) fun shotac n = List.nth (List.nth (the_tactics, 0), n) |> #3 |> the |> fst \ ML \ (*Given a list of reconstructed inferences (as in "the_tactics" above, count the number of failures and successes, and list the failed inference reconstructions.*) fun evaluate_the_tactics [] acc = acc | evaluate_the_tactics ((node_no, (inf_name, inf_fmla, NONE)) :: xs) ((fai, suc), inf_list) = let val score = (fai + 1, suc) val index_info = get_index (fn (x, _) => if x = node_no then SOME true else NONE) inf_list val inf_list' = case index_info of NONE => (node_no, (inf_name, inf_fmla, 1)) :: inf_list | SOME (idx, _) => nth_map idx (fn (node_no, (inf_name, inf_fmla, count)) => (node_no, (inf_name, inf_fmla, count + 1))) inf_list in evaluate_the_tactics xs (score, inf_list') end | evaluate_the_tactics ((_, (_, _, SOME _)) :: xs) ((fai, suc), inf_list) = evaluate_the_tactics xs ((fai, suc + 1), inf_list) \ text "Now we build a tactic by combining lists of tactics" ML \ (*given a list of tactics to be applied in sequence (i.e., they follow a skeleton), we build a single tactic, interleaving some tracing info to help with debugging.*) fun step_by_step_tacs ctxt verbose (thm_tacs : (thm * tactic) list) : tactic = let fun interleave_tacs [] [] = all_tac | interleave_tacs (tac1 :: tacs1) (tac2 :: tacs2) = EVERY [tac1, tac2] THEN interleave_tacs tacs1 tacs2 val thms_to_traceprint = map (fn thm => fn st => (*FIXME uses makestring*) print_tac ctxt (@{make_string} thm) st) in if verbose then ListPair.unzip thm_tacs |> apfst (fn thms => enumerate 1 thms) |> apfst thms_to_traceprint |> uncurry interleave_tacs else EVERY (map #2 thm_tacs) end \ ML \ (*apply step_by_step_tacs to all problems under test*) fun narrated_tactics ctxt = map (map (#3 #> the) #> step_by_step_tacs ctxt false) the_tactics; (*produce thm*) (*use narrated_tactics to reconstruct all problems under test*) if test_all @{context} then [] else map (fn (prob_name, tac) => TPTP_Reconstruct.reconstruct @{context} (fn _ => tac) prob_name) (ListPair.zip (prob_names, narrated_tactics @{context})) \ subsection "Manually using 'piecemeal' approach" text "Another testing possibility involves manually creating a lemma and running through the list of tactics generating to prove that lemma. The following code shows the goal of each problem under test, and then for each problem returns the list of tactics which can be invoked individually as shown below." ML \ fun show_goal ctxt prob_name = let val thy = Proof_Context.theory_of ctxt val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name in #meta pannot |> filter (fn (_, info) => #role info = TPTP_Syntax.Role_Conjecture) |> hd |> snd |> #fmla |> cterm_of thy end; if test_all @{context} then [] else map (show_goal @{context}) prob_names; \ ML \ (*project out the list of tactics from "the_tactics"*) val just_the_tacs = map (map (#3 #> the #> #2)) the_tactics; map length just_the_tacs \ ML \ (*like just_the_tacs, but extract the thms, to inspect their thys*) val just_the_thms = map (map (#3 #> the #> #1)) the_tactics; map length just_the_thms; \ ML \ -val axms_of_thy = - `Theory.axioms_of - #> apsnd cterm_of - #> swap - #> apsnd (map snd) - #> uncurry map -\ - -ML \ (*Show the skeleton-level inference which is done by each element of just_the_tacs. This is useful when debugging using the technique shown next*) if test_all @{context} orelse prob_names = [] then () else the_tactics |> hd |> map #1 |> TPTP_Reconstruct_Library.enumerate 0 |> List.app (@{make_string} #> writeln) \ ML \ fun leo2_tac_wrap ctxt prob_name step i st = rtac (interpret_leo2_inference ctxt prob_name step) i st \ (*FIXME move these examples elsewhere*) (* lemma "\(Xj::TPTP_Interpret.ind) Xk::TPTP_Interpret.ind. bnd_cCKB6_BLACK Xj Xk \ bnd_cCKB6_BLACK (bnd_s (bnd_s (bnd_s Xj))) (bnd_s Xk)" apply (tactic {*nth (nth just_the_tacs 0) 0*}) apply (tactic {*nth (nth just_the_tacs 0) 1*}) apply (tactic {*nth (nth just_the_tacs 0) 2*}) apply (tactic {*nth (nth just_the_tacs 0) 3*}) apply (tactic {*nth (nth just_the_tacs 0) 4*}) apply (tactic {*nth (nth just_the_tacs 0) 5*}) ML_prf "nth (hd the_tactics) 6" apply (tactic {*nth (nth just_the_tacs 0) 6*}) apply (tactic {*nth (nth just_the_tacs 0) 7*}) apply (tactic {*nth (nth just_the_tacs 0) 8*}) apply (tactic {*nth (nth just_the_tacs 0) 9*}) apply (tactic {*nth (nth just_the_tacs 0) 10*}) apply (tactic {*nth (nth just_the_tacs 0) 11*}) apply (tactic {*nth (nth just_the_tacs 0) 12*}) apply (tactic {*nth (nth just_the_tacs 0) 13*}) apply (tactic {*nth (nth just_the_tacs 0) 14*}) apply (tactic {*nth (nth just_the_tacs 0) 15*}) apply (tactic {*nth (nth just_the_tacs 0) 16*}) (* apply (tactic {* rtac (interpret_leo2_inference @{context} (hd prob_names) "8") 1 *}) apply (tactic {* rtac (interpret_leo2_inference @{context} (hd prob_names) "7") 1 *}) apply (tactic {* rtac (interpret_leo2_inference @{context} (hd prob_names) "6") 1 *}) (* apply (tactic {* rtac (interpret_leo2_inference @{context} (hd prob_names) "4") 1 *}) *) *) apply (tactic {*nth (nth just_the_tacs 0) 17*}) apply (tactic {*nth (nth just_the_tacs 0) 18*}) apply (tactic {*nth (nth just_the_tacs 0) 19*}) apply (tactic {*nth (nth just_the_tacs 0) 20*}) apply (tactic {*nth (nth just_the_tacs 0) 21*}) ML_prf "nth (hd the_tactics) 21" ML_prf "nth (hd the_tactics) 22" apply (tactic {*nth (nth just_the_tacs 0) 22*}) apply (tactic {*nth (nth just_the_tacs 0) 23*}) apply (tactic {*nth (nth just_the_tacs 0) 24*}) apply (tactic {*nth (nth just_the_tacs 0) 25*}) ML_prf "nth (hd the_tactics) 19" apply (tactic {* interpret_leo2_inference_wrap (hd prob_names) "8" 1 *}) apply (tactic {* interpret_leo2_inference_wrap (hd prob_names) "7" 1 *}) apply (tactic {* interpret_leo2_inference_wrap (hd prob_names) "6" 1 *}) apply (tactic {* interpret_leo2_inference_wrap (hd prob_names) "4" 1 *}) ML_prf "nth (hd the_tactics) 20" ML_prf "nth (hd the_tactics) 21" ML_prf "nth (hd the_tactics) 22" *) (* lemma "bnd_powersetE1 \ bnd_sepInPowerset \ (\A Xphi. bnd_subset (bnd_dsetconstr A Xphi) A)" apply (tactic {*nth (nth just_the_tacs 0) 0*}) apply (tactic {*nth (nth just_the_tacs 0) 1*}) apply (tactic {*nth (nth just_the_tacs 0) 2*}) apply (tactic {*nth (nth just_the_tacs 0) 3*}) apply (tactic {*nth (nth just_the_tacs 0) 4*}) apply (tactic {*nth (nth just_the_tacs 0) 5*}) ML_prf "nth (hd the_tactics) 6" apply (tactic {*nth (nth just_the_tacs 0) 6*}) apply (tactic {*nth (nth just_the_tacs 0) 7*}) apply (tactic {*nth (nth just_the_tacs 0) 8*}) apply (tactic {*nth (nth just_the_tacs 0) 9*}) apply (tactic {*nth (nth just_the_tacs 0) 10*}) apply (tactic {*nth (nth just_the_tacs 0) 11*}) apply (tactic {*nth (nth just_the_tacs 0) 12*}) apply (tactic {*nth (nth just_the_tacs 0) 13*}) apply (tactic {*nth (nth just_the_tacs 0) 14*}) apply (tactic {*nth (nth just_the_tacs 0) 15*}) apply (tactic {*nth (nth just_the_tacs 0) 16*}) apply (tactic {*nth (nth just_the_tacs 0) 17*}) apply (tactic {*nth (nth just_the_tacs 0) 18*}) apply (tactic {*nth (nth just_the_tacs 0) 19*}) apply (tactic {*nth (nth just_the_tacs 0) 20*}) apply (tactic {*nth (nth just_the_tacs 0) 21*}) apply (tactic {*nth (nth just_the_tacs 0) 22*}) apply (tactic {*nth (nth just_the_tacs 0) 23*}) apply (tactic {*nth (nth just_the_tacs 0) 24*}) apply (tactic {*nth (nth just_the_tacs 0) 25*}) (* apply (tactic {*nth (nth just_the_tacs 0) 26*}) *) ML_prf "nth (hd the_tactics) 26" apply (subgoal_tac "(\ (\A Xphi. bnd_subset (bnd_dsetconstr A Xphi) A)) = True \ (\ bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True") prefer 2 apply (thin_tac "(bnd_powersetE1 \ bnd_sepInPowerset \ (\A Xphi. bnd_subset (bnd_dsetconstr A Xphi) A)) = False") apply (tactic {*extcnf_combined_simulator_tac (hd prob_names) 1*}) apply (tactic {*extcnf_combined_simulator_tac (hd prob_names) 1*}) apply (tactic {*extcnf_combined_simulator_tac (hd prob_names) 1*}) apply (tactic {*extcnf_combined_simulator_tac (hd prob_names) 1*}) apply simp (* apply (tactic {*nth (nth just_the_tacs 0) 26*}) *) apply (tactic {*nth (nth just_the_tacs 0) 27*}) apply (tactic {*nth (nth just_the_tacs 0) 28*}) apply (tactic {*nth (nth just_the_tacs 0) 29*}) apply (tactic {*nth (nth just_the_tacs 0) 30*}) apply (tactic {*nth (nth just_the_tacs 0) 31*}) apply (tactic {*nth (nth just_the_tacs 0) 32*}) apply (tactic {*nth (nth just_the_tacs 0) 33*}) apply (tactic {*nth (nth just_the_tacs 0) 34*}) apply (tactic {*nth (nth just_the_tacs 0) 35*}) apply (tactic {*nth (nth just_the_tacs 0) 36*}) apply (tactic {*nth (nth just_the_tacs 0) 37*}) apply (tactic {*nth (nth just_the_tacs 0) 38*}) apply (tactic {*nth (nth just_the_tacs 0) 39*}) apply (tactic {*nth (nth just_the_tacs 0) 40*}) apply (tactic {*nth (nth just_the_tacs 0) 41*}) apply (tactic {*nth (nth just_the_tacs 0) 42*}) apply (tactic {*nth (nth just_the_tacs 0) 43*}) apply (tactic {*nth (nth just_the_tacs 0) 44*}) apply (tactic {*nth (nth just_the_tacs 0) 45*}) apply (tactic {*nth (nth just_the_tacs 0) 46*}) apply (tactic {*nth (nth just_the_tacs 0) 47*}) apply (tactic {*nth (nth just_the_tacs 0) 48*}) apply (tactic {*nth (nth just_the_tacs 0) 49*}) apply (tactic {*nth (nth just_the_tacs 0) 50*}) apply (tactic {*nth (nth just_the_tacs 0) 51*}) done *) (* We can use just_the_tacs as follows: (this is from SEV012^5.p.out) lemma "((\(Xx :: bool) (Xy :: bool). True \ True) \ (\(Xx :: bool) (Xy :: bool) (Xz :: bool). True \ True \ True)) \ (\(Xx :: bool) (Xy :: bool). True) = (\Xx Xy. True)" apply (tactic {*nth (nth just_the_tacs 0) 0*}) apply (tactic {*nth (nth just_the_tacs 0) 1*}) apply (tactic {*nth (nth just_the_tacs 0) 2*}) apply (tactic {*nth (nth just_the_tacs 0) 3*}) apply (tactic {*nth (nth just_the_tacs 0) 4*}) apply (tactic {*nth (nth just_the_tacs 0) 5*}) ML_prf "nth (hd the_tactics) 6" apply (tactic {*nth (nth just_the_tacs 0) 6*}) apply (tactic {*nth (nth just_the_tacs 0) 7*}) apply (tactic {*nth (nth just_the_tacs 0) 8*}) apply (tactic {*nth (nth just_the_tacs 0) 9*}) apply (tactic {*nth (nth just_the_tacs 0) 10*}) apply (tactic {*nth (nth just_the_tacs 0) 11*}) apply (tactic {*nth (nth just_the_tacs 0) 12*}) apply (tactic {*nth (nth just_the_tacs 0) 13*}) apply (tactic {*nth (nth just_the_tacs 0) 14*}) apply (tactic {*nth (nth just_the_tacs 0) 15*}) apply (tactic {*nth (nth just_the_tacs 0) 16*}) apply (tactic {*nth (nth just_the_tacs 0) 17*}) apply (tactic {*nth (nth just_the_tacs 0) 18*}) apply (tactic {*nth (nth just_the_tacs 0) 19*}) apply (tactic {*nth (nth just_the_tacs 0) 20*}) apply (tactic {*nth (nth just_the_tacs 0) 21*}) apply (tactic {*nth (nth just_the_tacs 0) 22*}) done (* We could also use previous definitions directly, e.g. the following should prove the goal at a go: - apply (tactic {*narrated_tactics |> hd |> hd*}) - apply (tactic {* TPTP_Reconstruct.naive_reconstruct_tac interpret_leo2_inference (hd prob_names) @{context}*}) (Note that the previous two methods don't work in this "lemma" testing mode, not sure why. The previous methods (producing the thm values directly) should work though.) *) *) section "Testing against benchmark" ML \ (*if reconstruction_info value is NONE then a big error must have occurred*) type reconstruction_info = ((int(*no of failures*) * int(*no of successes*)) * (TPTP_Reconstruct.rolling_stock * term option(*inference formula*) * int (*number of times the inference occurs in the skeleton*)) list) option datatype proof_contents = No_info | Empty | Nonempty of reconstruction_info (*To make output less cluttered in whole-run tests*) fun erase_inference_fmlas (Nonempty (SOME (outline, inf_info))) = Nonempty (SOME (outline, map (fn (inf_name, _, count) => (inf_name, NONE, count)) inf_info)) | erase_inference_fmlas x = x \ ML \ (*Report on how many inferences in a proof are reconstructed, and give some info about the inferences for which reconstruction failed.*) fun test_partial_reconstruction thy prob_file = let val prob_name = prob_file |> Path.file_name |> TPTP_Problem_Name.Nonstandard val thy' = try (TPTP_Reconstruct.import_thm true [Path.dir prob_file, Path.explode "$TPTP"] prob_file leo2_on_load) thy val ctxt' = if is_some thy' then SOME (Proof_Context.init_global (the thy')) else NONE (*to test if proof is empty*) val fms = if is_some thy' then SOME (TPTP_Reconstruct.get_fmlas_of_prob (the thy') prob_name) else NONE val the_tactics = if is_some thy' then SOME (TPTP_Reconstruct.naive_reconstruct_tacs (* metis_based_reconstruction_tac *) interpret_leo2_inference (* auto_based_reconstruction_tac *) (* oracle_based_reconstruction_tac *) prob_name (the ctxt')) else NONE (* val _ = tracing ("tt=" ^ @{make_string} the_tactics) *) val skeleton = if is_some thy' then SOME (TPTP_Reconstruct.make_skeleton (the ctxt') (TPTP_Reconstruct.get_pannot_of_prob (the thy') prob_name)) else NONE val skeleton_and_tactics = if is_some thy' then SOME (ListPair.zip (the skeleton, the the_tactics)) else NONE val result = if is_some thy' then SOME (evaluate_the_tactics (the skeleton_and_tactics) ((0, 0), [])) else NONE (*strip node names*) val result' = if is_some result then SOME (apsnd (map #2) (the result)) else NONE in if is_some fms andalso List.null (the fms) then Empty else Nonempty result' end \ ML \ (*default timeout is 1 min*) fun reconstruct timeout light_output file thy = let val timer = Timer.startRealTimer () in Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout)) (test_partial_reconstruction thy #> light_output ? erase_inference_fmlas #> @{make_string} (* FIXME *) #> (fn s => report (Proof_Context.init_global thy) (@{make_string} file ^ " === " ^ s ^ " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> @{make_string})))) file end \ ML \ (*this version of "reconstruct" builds theorems, instead of lists of reconstructed inferences*) (*default timeout is 1 min*) fun reconstruct timeout file thy = let val timer = Timer.startRealTimer () val thy' = TPTP_Reconstruct.import_thm true [Path.dir file, Path.explode "$TPTP"] file leo2_on_load thy val ctxt = Proof_Context.init_global thy' (*FIXME pass ctxt instead of thy*) val prob_name = file |> Path.file_name |> TPTP_Problem_Name.Nonstandard in Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout)) (fn prob_name => (can (TPTP_Reconstruct.reconstruct ctxt (fn prob_name => TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference prob_name (* oracle_based_reconstruction_tac *))) prob_name ) |> (fn s => report ctxt (Path.print file ^ " === " ^ Bool.toString s ^ " t=" ^ (Timer.checkRealTimer timer |> Time.toMilliseconds |> @{make_string})))) prob_name end \ ML \ fun reconstruction_test timeout ctxt = test_fn ctxt (fn file => reconstruct timeout file (Proof_Context.theory_of ctxt)) "reconstructor" () \ ML \ datatype examination_results = Whole_proof of string(*filename*) * proof_contents | Specific_rule of string(*filename*) * string(*inference rule*) * term option list (*Look out for failures reconstructing a particular inference rule*) fun filter_failures inference_name (Whole_proof (filename, results)) = let val filtered_results = case results of Nonempty (SOME results') => #2 results' |> maps (fn (stock as TPTP_Reconstruct.Annotated_step (_, inf_name), inf_fmla, _) => if inf_name = inference_name then [inf_fmla] else []) | _ => [] in Specific_rule (filename, inference_name, filtered_results) end (*Returns detailed info about a proof-reconstruction attempt. If rule_name is specified then the related failed inferences are returned, otherwise all failed inferences are returned.*) fun examine_failed_inferences ctxt filename rule_name = let val thy = Proof_Context.theory_of ctxt val prob_file = Path.explode filename val results = if test_all ctxt then No_info else test_partial_reconstruction thy prob_file in Whole_proof (filename, results) |> is_some rule_name ? (fn x => filter_failures (the rule_name) x) end \ ML \ exception NONSENSE fun annotation_or_id (TPTP_Reconstruct.Step n) = n | annotation_or_id (TPTP_Reconstruct.Annotated_step (n, anno)) = anno | annotation_or_id TPTP_Reconstruct.Assumed = "assumption" | annotation_or_id TPTP_Reconstruct.Unconjoin = "conjI" | annotation_or_id TPTP_Reconstruct.Caboose = "(end)" | annotation_or_id (TPTP_Reconstruct.Synth_step s) = s | annotation_or_id (TPTP_Reconstruct.Split (split_node, soln_node, _)) = "split_at " ^ split_node ^ " " ^ soln_node; fun count_failures (Whole_proof (_, No_info)) = raise NONSENSE | count_failures (Whole_proof (_, Empty)) = raise NONSENSE | count_failures (Whole_proof (_, Nonempty NONE)) = raise NONSENSE | count_failures (Whole_proof (_, Nonempty (SOME (((n, _), _))))) = n | count_failures (Specific_rule (_, _, t)) = length t fun pre_classify_failures [] alist = alist | pre_classify_failures ((stock, _, _) :: xs) alist = let val inf = annotation_or_id stock val count = AList.lookup (=) alist inf in if is_none count then pre_classify_failures xs ((inf, 1) :: alist) else pre_classify_failures xs (AList.update (=) (inf, the count + 1) alist) end fun classify_failures (Whole_proof (_, Nonempty (SOME (((_, _), inferences))))) = pre_classify_failures inferences [] | classify_failures (Specific_rule (_, rule, t)) = [(rule, length t)] | classify_failures _ = raise NONSENSE \ ML \ val regressions = map (fn s => "$THF_PROOFS/" ^ s) ["SEV405^5.p.out", (*"SYO377^5.p.out", Always seems to raise Interrupt on my laptop -- probably because node 475 has lots of premises*) "PUZ031^5.p.out", "ALG001^5.p.out", "SYO238^5.p.out", (*"SEV158^5.p.out", This is big*) "SYO285^5.p.out", "../SYO285^5.p.out_reduced", (* "SYO225^5.p.out", This is big*) "SYO291^5.p.out", "SET669^3.p.out", "SEV233^5.p.out", (*"SEU511^1.p.out", This is big*) "SEV161^5.p.out", "SEV012^5.p.out", "SYO035^1.p.out", "SYO291^5.p.out", "SET741^4.p.out", (*involves both definitions and contorted splitting. has nice graph.*) "SEU548^2.p.out", "SEU513^2.p.out", "SYO006^1.p.out", "SYO371^5.p.out" (*has contorted splitting, like SYO006^1.p.out, but doesn't involve definitions*) ] \ ML \ val experiment = examine_failed_inferences @{context} (List.last regressions) NONE; (* val experiment_focus = filter_failures "extcnf_combined" experiment; *) (* count_failures experiment_focus classify_failures experiment *) \ text "Run reconstruction on all problems in a benchmark (provided via a script) and report on partial success." declare [[ tptp_test_all = true, tptp_test_timeout = 10 ]] ML \ (*problem source*) val tptp_probs_dir = Path.explode "$THF_PROOFS" |> Path.expand; \ ML \ if test_all @{context} then (report @{context} "Reconstructing proofs"; S timed_test (reconstruction_test (get_timeout @{context})) @{context} (TPTP_Syntax.get_file_list tptp_probs_dir)) else () \ (* Debugging strategy: 1) get list of all proofs 2) order by size 3) try to construct each in turn, given some timeout Use this to find the smallest failure, then debug that. *) end diff --git a/src/HOL/Tools/Nitpick/nitpick_hol.ML b/src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML @@ -1,2430 +1,2429 @@ (* Title: HOL/Tools/Nitpick/nitpick_hol.ML Author: Jasmin Blanchette, TU Muenchen Copyright 2008, 2009, 2010 Auxiliary HOL-related functions used by Nitpick. *) signature NITPICK_HOL = sig type const_table = term list Symtab.table type special_fun = ((string * typ) * int list * term list) * (string * typ) type unrolled = (string * typ) * (string * typ) type wf_cache = ((string * typ) * (bool * bool)) list type hol_context = {thy: theory, ctxt: Proof.context, max_bisim_depth: int, boxes: (typ option * bool option) list, wfs: ((string * typ) option * bool option) list, user_axioms: bool option, debug: bool, whacks: term list, binary_ints: bool option, destroy_constrs: bool, specialize: bool, star_linear_preds: bool, total_consts: bool option, needs: term list option, tac_timeout: Time.time, evals: term list, case_names: (string * int) list, def_tables: const_table * const_table, nondef_table: const_table, nondefs: term list, simp_table: const_table Unsynchronized.ref, psimp_table: const_table, choice_spec_table: const_table, intro_table: const_table, ground_thm_table: term list Inttab.table, ersatz_table: (string * string) list, skolems: (string * string list) list Unsynchronized.ref, special_funs: special_fun list Unsynchronized.ref, unrolled_preds: unrolled list Unsynchronized.ref, wf_cache: wf_cache Unsynchronized.ref, constr_cache: (typ * (string * typ) list) list Unsynchronized.ref} datatype fixpoint_kind = Lfp | Gfp | NoFp datatype boxability = InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2 val name_sep : string val numeral_prefix : string val base_prefix : string val step_prefix : string val unrolled_prefix : string val ubfp_prefix : string val lbfp_prefix : string val quot_normal_prefix : string val skolem_prefix : string val special_prefix : string val uncurry_prefix : string val eval_prefix : string val iter_var_prefix : string val strip_first_name_sep : string -> string * string val original_name : string -> string val abs_var : indexname * typ -> term -> term val s_conj : term * term -> term val s_disj : term * term -> term val strip_any_connective : term -> term list * term val conjuncts_of : term -> term list val disjuncts_of : term -> term list val unarize_unbox_etc_type : typ -> typ val uniterize_unarize_unbox_etc_type : typ -> typ val string_for_type : Proof.context -> typ -> string val pretty_for_type : Proof.context -> typ -> Pretty.T val prefix_name : string -> string -> string val shortest_name : string -> string val short_name : string -> string val shorten_names_in_term : term -> term val strict_type_match : theory -> typ * typ -> bool val type_match : theory -> typ * typ -> bool val const_match : theory -> (string * typ) * (string * typ) -> bool val term_match : theory -> term * term -> bool val frac_from_term_pair : typ -> term -> term -> term val is_fun_type : typ -> bool val is_set_type : typ -> bool val is_fun_or_set_type : typ -> bool val is_set_like_type : typ -> bool val is_pair_type : typ -> bool val is_lfp_iterator_type : typ -> bool val is_gfp_iterator_type : typ -> bool val is_fp_iterator_type : typ -> bool val is_iterator_type : typ -> bool val is_boolean_type : typ -> bool val is_integer_type : typ -> bool val is_bit_type : typ -> bool val is_word_type : typ -> bool val is_integer_like_type : typ -> bool val is_number_type : Proof.context -> typ -> bool val is_higher_order_type : typ -> bool val elem_type : typ -> typ val pseudo_domain_type : typ -> typ val pseudo_range_type : typ -> typ val const_for_iterator_type : typ -> string * typ val strip_n_binders : int -> typ -> typ list * typ val nth_range_type : int -> typ -> typ val num_factors_in_type : typ -> int val curried_binder_types : typ -> typ list val mk_flat_tuple : typ -> term list -> term val dest_n_tuple : int -> term -> term list val is_codatatype : Proof.context -> typ -> bool val is_quot_type : Proof.context -> typ -> bool val is_pure_typedef : Proof.context -> typ -> bool val is_univ_typedef : Proof.context -> typ -> bool val is_data_type : Proof.context -> typ -> bool val is_record_get : theory -> string * typ -> bool val is_record_update : theory -> string * typ -> bool val is_abs_fun : Proof.context -> string * typ -> bool val is_rep_fun : Proof.context -> string * typ -> bool val is_quot_abs_fun : Proof.context -> string * typ -> bool val is_quot_rep_fun : Proof.context -> string * typ -> bool val mate_of_rep_fun : Proof.context -> string * typ -> string * typ val is_nonfree_constr : Proof.context -> string * typ -> bool val is_free_constr : Proof.context -> string * typ -> bool val is_constr : Proof.context -> string * typ -> bool val is_sel : string -> bool val is_sel_like_and_no_discr : string -> bool val box_type : hol_context -> boxability -> typ -> typ val binarize_nat_and_int_in_type : typ -> typ val binarize_nat_and_int_in_term : term -> term val discr_for_constr : string * typ -> string * typ val num_sels_for_constr_type : typ -> int val nth_sel_name_for_constr_name : string -> int -> string val nth_sel_for_constr : string * typ -> int -> string * typ val binarized_and_boxed_nth_sel_for_constr : hol_context -> bool -> string * typ -> int -> string * typ val sel_no_from_name : string -> int val close_form : term -> term val distinctness_formula : typ -> term list -> term val register_frac_type : string -> (string * string) list -> morphism -> Context.generic -> Context.generic val register_frac_type_global : string -> (string * string) list -> theory -> theory val unregister_frac_type : string -> morphism -> Context.generic -> Context.generic val unregister_frac_type_global : string -> theory -> theory val register_ersatz : (string * string) list -> morphism -> Context.generic -> Context.generic val register_ersatz_global : (string * string) list -> theory -> theory val register_codatatype : typ -> string -> (string * typ) list -> morphism -> Context.generic -> Context.generic val register_codatatype_global : typ -> string -> (string * typ) list -> theory -> theory val unregister_codatatype : typ -> morphism -> Context.generic -> Context.generic val unregister_codatatype_global : typ -> theory -> theory val binarized_and_boxed_data_type_constrs : hol_context -> bool -> typ -> (string * typ) list val constr_name_for_sel_like : string -> string val binarized_and_boxed_constr_for_sel : hol_context -> bool -> string * typ -> string * typ val card_of_type : (typ * int) list -> typ -> int val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int val bounded_exact_card_of_type : hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int val typical_card_of_type : typ -> int val is_finite_type : hol_context -> typ -> bool val is_special_eligible_arg : bool -> typ list -> term -> bool val s_let : typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term val s_betapply : typ list -> term * term -> term val s_betapplys : typ list -> term * term list -> term val discriminate_value : hol_context -> string * typ -> term -> term val select_nth_constr_arg : Proof.context -> string * typ -> term -> int -> typ -> term val construct_value : Proof.context -> string * typ -> term list -> term val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term val special_bounds : term list -> (indexname * typ) list val is_funky_typedef : Proof.context -> typ -> bool val all_defs_of : theory -> (term * term) list -> term list val all_nondefs_of : Proof.context -> (term * term) list -> term list val arity_of_built_in_const : string * typ -> int option val is_built_in_const : string * typ -> bool val term_under_def : term -> term val case_const_names : Proof.context -> (string * int) list val unfold_defs_in_term : hol_context -> term -> term val const_def_tables : Proof.context -> (term * term) list -> term list -> const_table * const_table val const_nondef_table : term list -> const_table val const_simp_table : Proof.context -> (term * term) list -> const_table val const_psimp_table : Proof.context -> (term * term) list -> const_table val const_choice_spec_table : Proof.context -> (term * term) list -> const_table val inductive_intro_table : Proof.context -> (term * term) list -> const_table * const_table -> const_table val ground_theorem_table : theory -> term list Inttab.table val ersatz_table : Proof.context -> (string * string) list val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit val inverse_axioms_for_rep_fun : Proof.context -> string * typ -> term list val optimized_typedef_axioms : Proof.context -> string * typ list -> term list val optimized_quot_type_axioms : Proof.context -> string * typ list -> term list val def_of_const : theory -> const_table * const_table -> string * typ -> term option val fixpoint_kind_of_rhs : term -> fixpoint_kind val fixpoint_kind_of_const : theory -> const_table * const_table -> string * typ -> fixpoint_kind val is_raw_inductive_pred : hol_context -> string * typ -> bool val is_constr_pattern : Proof.context -> term -> bool val is_constr_pattern_lhs : Proof.context -> term -> bool val is_constr_pattern_formula : Proof.context -> term -> bool val nondef_props_for_const : theory -> bool -> const_table -> string * typ -> term list val is_choice_spec_fun : hol_context -> string * typ -> bool val is_choice_spec_axiom : Proof.context -> const_table -> term -> bool val is_raw_equational_fun : hol_context -> string * typ -> bool val is_equational_fun : hol_context -> string * typ -> bool val codatatype_bisim_axioms : hol_context -> typ -> term list val is_well_founded_inductive_pred : hol_context -> string * typ -> bool val unrolled_inductive_pred_const : hol_context -> bool -> string * typ -> term val equational_fun_axioms : hol_context -> string * typ -> term list val is_equational_fun_surely_complete : hol_context -> string * typ -> bool val merged_type_var_table_for_terms : theory -> term list -> (sort * string) list val merge_type_vars_in_term : theory -> bool -> (sort * string) list -> term -> term val ground_types_in_type : hol_context -> bool -> typ -> typ list val ground_types_in_terms : hol_context -> bool -> term list -> typ list end; structure Nitpick_HOL : NITPICK_HOL = struct open Nitpick_Util type const_table = term list Symtab.table type special_fun = ((string * typ) * int list * term list) * (string * typ) type unrolled = (string * typ) * (string * typ) type wf_cache = ((string * typ) * (bool * bool)) list type hol_context = {thy: theory, ctxt: Proof.context, max_bisim_depth: int, boxes: (typ option * bool option) list, wfs: ((string * typ) option * bool option) list, user_axioms: bool option, debug: bool, whacks: term list, binary_ints: bool option, destroy_constrs: bool, specialize: bool, star_linear_preds: bool, total_consts: bool option, needs: term list option, tac_timeout: Time.time, evals: term list, case_names: (string * int) list, def_tables: const_table * const_table, nondef_table: const_table, nondefs: term list, simp_table: const_table Unsynchronized.ref, psimp_table: const_table, choice_spec_table: const_table, intro_table: const_table, ground_thm_table: term list Inttab.table, ersatz_table: (string * string) list, skolems: (string * string list) list Unsynchronized.ref, special_funs: special_fun list Unsynchronized.ref, unrolled_preds: unrolled list Unsynchronized.ref, wf_cache: wf_cache Unsynchronized.ref, constr_cache: (typ * (string * typ) list) list Unsynchronized.ref} datatype fixpoint_kind = Lfp | Gfp | NoFp datatype boxability = InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2 (* FIXME: Get rid of 'codatatypes' and related functionality *) structure Data = Generic_Data ( type T = {frac_types: (string * (string * string) list) list, ersatz_table: (string * string) list, codatatypes: (string * (string * (string * typ) list)) list} val empty = {frac_types = [], ersatz_table = [], codatatypes = []} val extend = I fun merge ({frac_types = fs1, ersatz_table = et1, codatatypes = cs1}, {frac_types = fs2, ersatz_table = et2, codatatypes = cs2}) : T = {frac_types = AList.merge (op =) (K true) (fs1, fs2), ersatz_table = AList.merge (op =) (K true) (et1, et2), codatatypes = AList.merge (op =) (K true) (cs1, cs2)} ) val name_sep = "$" val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep val sel_prefix = nitpick_prefix ^ "sel" val discr_prefix = nitpick_prefix ^ "is" ^ name_sep val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep val base_prefix = nitpick_prefix ^ "base" ^ name_sep val step_prefix = nitpick_prefix ^ "step" ^ name_sep val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep val skolem_prefix = nitpick_prefix ^ "sk" val special_prefix = nitpick_prefix ^ "sp" val uncurry_prefix = nitpick_prefix ^ "unc" val eval_prefix = nitpick_prefix ^ "eval" val iter_var_prefix = "i" (** Constant/type information and term/type manipulation **) fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep fun quot_normal_name_for_type ctxt T = quot_normal_prefix ^ YXML.content_of (Syntax.string_of_typ ctxt T) val strip_first_name_sep = Substring.full #> Substring.position name_sep ##> Substring.triml 1 #> apply2 Substring.string fun original_name s = if String.isPrefix nitpick_prefix s then case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2 else s fun s_conj (t1, \<^const>\True\) = t1 | s_conj (\<^const>\True\, t2) = t2 | s_conj (t1, t2) = if t1 = \<^const>\False\ orelse t2 = \<^const>\False\ then \<^const>\False\ else HOLogic.mk_conj (t1, t2) fun s_disj (t1, \<^const>\False\) = t1 | s_disj (\<^const>\False\, t2) = t2 | s_disj (t1, t2) = if t1 = \<^const>\True\ orelse t2 = \<^const>\True\ then \<^const>\True\ else HOLogic.mk_disj (t1, t2) fun strip_connective conn_t (t as (t0 $ t1 $ t2)) = if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t] | strip_connective _ t = [t] fun strip_any_connective (t as (t0 $ _ $ _)) = if t0 = \<^const>\HOL.conj\ orelse t0 = \<^const>\HOL.disj\ then (strip_connective t0 t, t0) else ([t], \<^const>\Not\) | strip_any_connective t = ([t], \<^const>\Not\) val conjuncts_of = strip_connective \<^const>\HOL.conj\ val disjuncts_of = strip_connective \<^const>\HOL.disj\ (* When you add constants to these lists, make sure to handle them in "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as well. *) val built_in_consts = [(\<^const_name>\Pure.all\, 1), (\<^const_name>\Pure.eq\, 2), (\<^const_name>\Pure.imp\, 2), (\<^const_name>\Pure.conjunction\, 2), (\<^const_name>\Trueprop\, 1), (\<^const_name>\Not\, 1), (\<^const_name>\False\, 0), (\<^const_name>\True\, 0), (\<^const_name>\All\, 1), (\<^const_name>\Ex\, 1), (\<^const_name>\HOL.eq\, 1), (\<^const_name>\HOL.conj\, 2), (\<^const_name>\HOL.disj\, 2), (\<^const_name>\HOL.implies\, 2), (\<^const_name>\If\, 3), (\<^const_name>\Let\, 2), (\<^const_name>\Pair\, 2), (\<^const_name>\fst\, 1), (\<^const_name>\snd\, 1), (\<^const_name>\Set.member\, 2), (\<^const_name>\Collect\, 1), (\<^const_name>\Id\, 0), (\<^const_name>\converse\, 1), (\<^const_name>\trancl\, 1), (\<^const_name>\relcomp\, 2), (\<^const_name>\finite\, 1), (\<^const_name>\unknown\, 0), (\<^const_name>\is_unknown\, 1), (\<^const_name>\safe_The\, 1), (\<^const_name>\Frac\, 0), (\<^const_name>\norm_frac\, 0), (\<^const_name>\Suc\, 0), (\<^const_name>\nat\, 0), (\<^const_name>\nat_gcd\, 0), (\<^const_name>\nat_lcm\, 0)] val built_in_typed_consts = [((\<^const_name>\zero_class.zero\, nat_T), 0), ((\<^const_name>\one_class.one\, nat_T), 0), ((\<^const_name>\plus_class.plus\, nat_T --> nat_T --> nat_T), 0), ((\<^const_name>\minus_class.minus\, nat_T --> nat_T --> nat_T), 0), ((\<^const_name>\times_class.times\, nat_T --> nat_T --> nat_T), 0), ((\<^const_name>\Rings.divide\, nat_T --> nat_T --> nat_T), 0), ((\<^const_name>\ord_class.less\, nat_T --> nat_T --> bool_T), 2), ((\<^const_name>\ord_class.less_eq\, nat_T --> nat_T --> bool_T), 2), ((\<^const_name>\of_nat\, nat_T --> int_T), 0), ((\<^const_name>\zero_class.zero\, int_T), 0), ((\<^const_name>\one_class.one\, int_T), 0), ((\<^const_name>\plus_class.plus\, int_T --> int_T --> int_T), 0), ((\<^const_name>\minus_class.minus\, int_T --> int_T --> int_T), 0), ((\<^const_name>\times_class.times\, int_T --> int_T --> int_T), 0), ((\<^const_name>\Rings.divide\, int_T --> int_T --> int_T), 0), ((\<^const_name>\uminus_class.uminus\, int_T --> int_T), 0), ((\<^const_name>\ord_class.less\, int_T --> int_T --> bool_T), 2), ((\<^const_name>\ord_class.less_eq\, int_T --> int_T --> bool_T), 2)] fun unarize_type \<^typ>\unsigned_bit word\ = nat_T | unarize_type \<^typ>\signed_bit word\ = int_T | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts) | unarize_type T = T fun unarize_unbox_etc_type (Type (\<^type_name>\fun_box\, Ts)) = unarize_unbox_etc_type (Type (\<^type_name>\fun\, Ts)) | unarize_unbox_etc_type (Type (\<^type_name>\pair_box\, Ts)) = Type (\<^type_name>\prod\, map unarize_unbox_etc_type Ts) | unarize_unbox_etc_type \<^typ>\unsigned_bit word\ = nat_T | unarize_unbox_etc_type \<^typ>\signed_bit word\ = int_T | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_unbox_etc_type Ts) | unarize_unbox_etc_type T = T fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts) | uniterize_type \<^typ>\bisim_iterator\ = nat_T | uniterize_type T = T val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type fun pretty_for_type ctxt = Syntax.pretty_typ ctxt o unarize_unbox_etc_type val prefix_name = Long_Name.qualify o Long_Name.base_name val shortest_name = Long_Name.base_name val prefix_abs_vars = Term.map_abs_vars o prefix_name fun short_name s = case space_explode name_sep s of [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix | ss => map shortest_name ss |> space_implode "_" fun shorten_names_in_type (Type (s, Ts)) = Type (short_name s, map shorten_names_in_type Ts) | shorten_names_in_type T = T val shorten_names_in_term = map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t) #> map_types shorten_names_in_type fun strict_type_match thy (T1, T2) = (Sign.typ_match thy (T2, T1) Vartab.empty; true) handle Type.TYPE_MATCH => false fun type_match thy = strict_type_match thy o apply2 unarize_unbox_etc_type fun const_match thy ((s1, T1), (s2, T2)) = s1 = s2 andalso type_match thy (T1, T2) fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2) | term_match thy (Free (s1, T1), Free (s2, T2)) = const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) | term_match _ (t1, t2) = t1 aconv t2 fun frac_from_term_pair T t1 t2 = case snd (HOLogic.dest_number t1) of 0 => HOLogic.mk_number T 0 | n1 => case snd (HOLogic.dest_number t2) of 1 => HOLogic.mk_number T n1 | n2 => Const (\<^const_name>\divide\, T --> T --> T) $ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2 fun is_fun_type (Type (\<^type_name>\fun\, _)) = true | is_fun_type _ = false fun is_set_type (Type (\<^type_name>\set\, _)) = true | is_set_type _ = false val is_fun_or_set_type = is_fun_type orf is_set_type fun is_set_like_type (Type (\<^type_name>\fun\, [_, T'])) = (body_type T' = bool_T) | is_set_like_type (Type (\<^type_name>\set\, _)) = true | is_set_like_type _ = false fun is_pair_type (Type (\<^type_name>\prod\, _)) = true | is_pair_type _ = false fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s | is_lfp_iterator_type _ = false fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s | is_gfp_iterator_type _ = false val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type fun is_iterator_type T = (T = \<^typ>\bisim_iterator\ orelse is_fp_iterator_type T) fun is_boolean_type T = (T = prop_T orelse T = bool_T) fun is_integer_type T = (T = nat_T orelse T = int_T) fun is_bit_type T = (T = \<^typ>\unsigned_bit\ orelse T = \<^typ>\signed_bit\) fun is_word_type (Type (\<^type_name>\word\, _)) = true | is_word_type _ = false val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type fun is_frac_type ctxt (Type (s, [])) = s |> AList.defined (op =) (#frac_types (Data.get (Context.Proof ctxt))) | is_frac_type _ _ = false fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt fun is_higher_order_type (Type (\<^type_name>\fun\, _)) = true | is_higher_order_type (Type (\<^type_name>\set\, _)) = true | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts | is_higher_order_type _ = false fun elem_type (Type (\<^type_name>\set\, [T'])) = T' | elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], []) fun pseudo_domain_type (Type (\<^type_name>\fun\, [T1, _])) = T1 | pseudo_domain_type T = elem_type T fun pseudo_range_type (Type (\<^type_name>\fun\, [_, T2])) = T2 | pseudo_range_type (Type (\<^type_name>\set\, _)) = bool_T | pseudo_range_type T = raise TYPE ("Nitpick_HOL.pseudo_range_type", [T], []) fun iterator_type_for_const gfp (s, T) = Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s, binder_types T) fun const_for_iterator_type (Type (s, Ts)) = (strip_first_name_sep s |> snd, Ts ---> bool_T) | const_for_iterator_type T = raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) fun strip_n_binders 0 T = ([], T) | strip_n_binders n (Type (\<^type_name>\fun\, [T1, T2])) = strip_n_binders (n - 1) T2 |>> cons T1 | strip_n_binders n (Type (\<^type_name>\fun_box\, Ts)) = strip_n_binders n (Type (\<^type_name>\fun\, Ts)) | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) val nth_range_type = snd oo strip_n_binders fun num_factors_in_type (Type (\<^type_name>\prod\, [T1, T2])) = fold (Integer.add o num_factors_in_type) [T1, T2] 0 | num_factors_in_type _ = 1 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types fun maybe_curried_binder_types T = (if is_pair_type (body_type T) then binder_types else curried_binder_types) T fun mk_flat_tuple _ [t] = t | mk_flat_tuple (Type (\<^type_name>\prod\, [T1, T2])) (t :: ts) = HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts) | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts) fun dest_n_tuple 1 t = [t] | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op :: fun typedef_info ctxt s = if is_frac_type ctxt (Type (s, [])) then SOME {abs_type = Type (s, []), rep_type = \<^typ>\int * int\, Abs_name = \<^const_name>\Abs_Frac\, Rep_name = \<^const_name>\Rep_Frac\, prop_of_Rep = \<^prop>\Rep_Frac x \ Collect Frac\ |> Logic.varify_global, Abs_inverse = NONE, Rep_inverse = NONE} else case Typedef.get_info ctxt s of (* When several entries are returned, it shouldn't matter much which one we take (according to Florian Haftmann). *) (* The "Logic.varifyT_global" calls are a temporary hack because these types's type variables sometimes clash with locally fixed type variables. Remove these calls once "Typedef" is fully localized. *) ({abs_type, rep_type, Abs_name, Rep_name, ...}, {Rep, Abs_inverse, Rep_inverse, ...}) :: _ => SOME {abs_type = Logic.varifyT_global abs_type, rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name, Rep_name = Rep_name, prop_of_Rep = Thm.prop_of Rep, Abs_inverse = SOME Abs_inverse, Rep_inverse = SOME Rep_inverse} | _ => NONE val is_raw_typedef = is_some oo typedef_info val is_raw_free_datatype = is_some oo Ctr_Sugar.ctr_sugar_of val is_interpreted_type = member (op =) [\<^type_name>\prod\, \<^type_name>\set\, \<^type_name>\bool\, \<^type_name>\nat\, \<^type_name>\int\, \<^type_name>\natural\, \<^type_name>\integer\] fun repair_constr_type (Type (_, Ts)) T = snd (dest_Const (Ctr_Sugar.mk_ctr Ts (Const (Name.uu, T)))) fun register_frac_type_generic frac_s ersaetze generic = let val {frac_types, ersatz_table, codatatypes} = Data.get generic val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, codatatypes = codatatypes} generic end (* TODO: Consider morphism. *) fun register_frac_type frac_s ersaetze (_ : morphism) = register_frac_type_generic frac_s ersaetze val register_frac_type_global = Context.theory_map oo register_frac_type_generic fun unregister_frac_type_generic frac_s = register_frac_type_generic frac_s [] (* TODO: Consider morphism. *) fun unregister_frac_type frac_s (_ : morphism) = unregister_frac_type_generic frac_s val unregister_frac_type_global = Context.theory_map o unregister_frac_type_generic fun register_ersatz_generic ersatz generic = let val {frac_types, ersatz_table, codatatypes} = Data.get generic val ersatz_table = AList.merge (op =) (K true) (ersatz_table, ersatz) in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, codatatypes = codatatypes} generic end (* TODO: Consider morphism. *) fun register_ersatz ersatz (_ : morphism) = register_ersatz_generic ersatz val register_ersatz_global = Context.theory_map o register_ersatz_generic fun register_codatatype_generic coT case_name constr_xs generic = let val {frac_types, ersatz_table, codatatypes} = Data.get generic val constr_xs = map (apsnd (repair_constr_type coT)) constr_xs val (co_s, coTs) = dest_Type coT val _ = if forall is_TFree coTs andalso not (has_duplicates (op =) coTs) andalso co_s <> \<^type_name>\fun\ andalso not (is_interpreted_type co_s) then () else raise TYPE ("Nitpick_HOL.register_codatatype_generic", [coT], []) val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) codatatypes in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, codatatypes = codatatypes} generic end (* TODO: Consider morphism. *) fun register_codatatype coT case_name constr_xs (_ : morphism) = register_codatatype_generic coT case_name constr_xs val register_codatatype_global = Context.theory_map ooo register_codatatype_generic fun unregister_codatatype_generic coT = register_codatatype_generic coT "" [] (* TODO: Consider morphism. *) fun unregister_codatatype coT (_ : morphism) = unregister_codatatype_generic coT val unregister_codatatype_global = Context.theory_map o unregister_codatatype_generic fun is_raw_codatatype ctxt s = Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s) = SOME BNF_Util.Greatest_FP fun is_registered_codatatype ctxt s = not (null (these (Option.map snd (AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) s)))) fun is_codatatype ctxt (Type (s, _)) = is_raw_codatatype ctxt s orelse is_registered_codatatype ctxt s | is_codatatype _ _ = false fun is_registered_type ctxt (T as Type (s, _)) = is_frac_type ctxt T orelse is_registered_codatatype ctxt s | is_registered_type _ _ = false fun is_raw_quot_type ctxt (Type (s, _)) = is_some (Quotient_Info.lookup_quotients ctxt s) | is_raw_quot_type _ _ = false fun is_quot_type ctxt T = is_raw_quot_type ctxt T andalso not (is_registered_type ctxt T) andalso T <> \<^typ>\int\ fun is_pure_typedef ctxt (T as Type (s, _)) = is_frac_type ctxt T orelse (is_raw_typedef ctxt s andalso not (is_raw_free_datatype ctxt s orelse is_raw_quot_type ctxt T orelse is_codatatype ctxt T orelse is_integer_like_type T)) | is_pure_typedef _ _ = false fun is_univ_typedef ctxt (Type (s, _)) = (case typedef_info ctxt s of SOME {prop_of_Rep, ...} => let val t_opt = try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) prop_of_Rep in case t_opt of SOME (Const (\<^const_name>\top\, _)) => true (* "Multiset.multiset" FIXME unchecked *) | SOME (Const (\<^const_name>\Collect\, _) $ Abs (_, _, Const (\<^const_name>\finite\, _) $ _)) => true (* "FinFun.finfun" FIXME unchecked *) | SOME (Const (\<^const_name>\Collect\, _) $ Abs (_, _, Const (\<^const_name>\Ex\, _) $ Abs (_, _, Const (\<^const_name>\finite\, _) $ _))) => true | _ => false end | NONE => false) | is_univ_typedef _ _ = false fun is_data_type ctxt (T as Type (s, _)) = (is_raw_typedef ctxt s orelse is_registered_type ctxt T orelse T = \<^typ>\ind\ orelse is_raw_quot_type ctxt T) andalso not (is_interpreted_type s) | is_data_type _ _ = false fun all_record_fields thy T = let val (recs, more) = Record.get_extT_fields thy T in recs @ more :: all_record_fields thy (snd more) end handle TYPE _ => [] val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields fun no_of_record_field thy s T1 = find_index (curry (op =) s o fst) (Record.get_extT_fields thy T1 ||> single |> op @) fun is_record_get thy (s, Type (\<^type_name>\fun\, [T1, _])) = exists (curry (op =) s o fst) (all_record_fields thy T1) | is_record_get _ _ = false fun is_record_update thy (s, T) = String.isSuffix Record.updateN s andalso exists (curry (op =) (unsuffix Record.updateN s) o fst) (all_record_fields thy (body_type T)) handle TYPE _ => false fun is_abs_fun ctxt (s, Type (\<^type_name>\fun\, [_, Type (s', _)])) = (case typedef_info ctxt s' of SOME {Abs_name, ...} => s = Abs_name | NONE => false) | is_abs_fun _ _ = false fun is_rep_fun ctxt (s, Type (\<^type_name>\fun\, [Type (s', _), _])) = (case typedef_info ctxt s' of SOME {Rep_name, ...} => s = Rep_name | NONE => false) | is_rep_fun _ _ = false fun is_quot_abs_fun ctxt (x as (_, Type (\<^type_name>\fun\, [_, abs_T as Type (s', _)]))) = try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s' = SOME (Const x) andalso not (is_registered_type ctxt abs_T) | is_quot_abs_fun _ _ = false fun is_quot_rep_fun ctxt (s, Type (\<^type_name>\fun\, [abs_T as Type (abs_s, _), _])) = (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of SOME (Const (s', _)) => s = s' andalso not (is_registered_type ctxt abs_T) | _ => false) | is_quot_rep_fun _ _ = false fun mate_of_rep_fun ctxt (x as (_, Type (\<^type_name>\fun\, [T1 as Type (s', _), T2]))) = (case typedef_info ctxt s' of SOME {Abs_name, ...} => (Abs_name, Type (\<^type_name>\fun\, [T2, T1])) | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])) | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]) fun rep_type_for_quot_type ctxt (T as Type (s, _)) = let val thy = Proof_Context.theory_of ctxt val {qtyp, rtyp, ...} = the (Quotient_Info.lookup_quotients ctxt s) in instantiate_type thy qtyp T rtyp end | rep_type_for_quot_type _ T = raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], []) fun equiv_relation_for_quot_type thy (Type (s, Ts)) = let val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.lookup_quotients thy s) val partial = case Thm.prop_of equiv_thm of \<^const>\Trueprop\ $ (Const (\<^const_name>\equivp\, _) $ _) => false | \<^const>\Trueprop\ $ (Const (\<^const_name>\part_equivp\, _) $ _) => true | _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \ \relation theorem" val Ts' = qtyp |> dest_Type |> snd in (subst_atomic_types (Ts' ~~ Ts) equiv_rel, partial) end | equiv_relation_for_quot_type _ T = raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) fun is_raw_free_datatype_constr ctxt (s, T) = case body_type T of dtT as Type (dt_s, _) => let val ctrs = case Ctr_Sugar.ctr_sugar_of ctxt dt_s of SOME {ctrs, ...} => map dest_Const ctrs | _ => [] in exists (fn (s', T') => s = s' andalso repair_constr_type dtT T' = T) ctrs end | _ => false fun is_registered_coconstr ctxt (s, T) = case body_type T of coT as Type (co_s, _) => let val ctrs = co_s |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) |> Option.map snd |> these in exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T) ctrs end | _ => false fun is_nonfree_constr ctxt (s, T) = member (op =) [\<^const_name>\FunBox\, \<^const_name>\PairBox\, \<^const_name>\Quot\, \<^const_name>\Zero_Rep\, \<^const_name>\Suc_Rep\] s orelse let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in is_raw_free_datatype_constr ctxt x orelse (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse is_registered_coconstr ctxt x end fun is_free_constr ctxt (s, T) = is_nonfree_constr ctxt (s, T) andalso let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in not (is_abs_fun ctxt x) orelse is_univ_typedef ctxt (range_type T) end fun is_stale_constr ctxt (x as (s, T)) = is_registered_type ctxt (body_type T) andalso is_nonfree_constr ctxt x andalso not (s = \<^const_name>\Abs_Frac\ orelse is_registered_coconstr ctxt x) fun is_constr ctxt (x as (_, T)) = is_nonfree_constr ctxt x andalso not (is_interpreted_type (fst (dest_Type (unarize_type (body_type T))))) andalso not (is_stale_constr ctxt x) val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix val is_sel_like_and_no_discr = String.isPrefix sel_prefix orf (member (op =) [\<^const_name>\fst\, \<^const_name>\snd\]) fun in_fun_lhs_for InConstr = InSel | in_fun_lhs_for _ = InFunLHS fun in_fun_rhs_for InConstr = InConstr | in_fun_rhs_for InSel = InSel | in_fun_rhs_for InFunRHS1 = InFunRHS2 | in_fun_rhs_for _ = InFunRHS1 fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T = case T of Type (\<^type_name>\fun\, _) => (boxy = InPair orelse boxy = InFunLHS) andalso not (is_boolean_type (body_type T)) | Type (\<^type_name>\prod\, Ts) => boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse ((boxy = InExpr orelse boxy = InFunLHS) andalso exists (is_boxing_worth_it hol_ctxt InPair) (map (box_type hol_ctxt InPair) Ts)) | _ => false and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z = case triple_lookup (type_match thy) boxes (Type z) of SOME (SOME box_me) => box_me | _ => is_boxing_worth_it hol_ctxt boxy (Type z) and box_type hol_ctxt boxy T = case T of Type (z as (\<^type_name>\fun\, [T1, T2])) => if boxy <> InConstr andalso boxy <> InSel andalso should_box_type hol_ctxt boxy z then Type (\<^type_name>\fun_box\, [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2]) else box_type hol_ctxt (in_fun_lhs_for boxy) T1 --> box_type hol_ctxt (in_fun_rhs_for boxy) T2 | Type (z as (\<^type_name>\prod\, Ts)) => if boxy <> InConstr andalso boxy <> InSel andalso should_box_type hol_ctxt boxy z then Type (\<^type_name>\pair_box\, map (box_type hol_ctxt InSel) Ts) else Type (\<^type_name>\prod\, map (box_type hol_ctxt (if boxy = InConstr orelse boxy = InSel then boxy else InPair)) Ts) | _ => T fun binarize_nat_and_int_in_type \<^typ>\nat\ = \<^typ>\unsigned_bit word\ | binarize_nat_and_int_in_type \<^typ>\int\ = \<^typ>\signed_bit word\ | binarize_nat_and_int_in_type (Type (s, Ts)) = Type (s, map binarize_nat_and_int_in_type Ts) | binarize_nat_and_int_in_type T = T val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T) fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) fun nth_sel_name_for_constr_name s n = if s = \<^const_name>\Pair\ then if n = 0 then \<^const_name>\fst\ else \<^const_name>\snd\ else sel_prefix_for n ^ s fun nth_sel_for_constr x ~1 = discr_for_constr x | nth_sel_for_constr (s, T) n = (nth_sel_name_for_constr_name s n, body_type T --> nth (maybe_curried_binder_types T) n) fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize = apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel) oo nth_sel_for_constr fun sel_no_from_name s = if String.isPrefix discr_prefix s then ~1 else if String.isPrefix sel_prefix s then s |> unprefix sel_prefix |> Int.fromString |> the else if s = \<^const_name>\snd\ then 1 else 0 val close_form = let fun close_up zs zs' = fold (fn (z as ((s, _), T)) => fn t' => Logic.all_const T $ Abs (s, T, abstract_over (Var z, t'))) (take (length zs' - length zs) zs') fun aux zs (\<^const>\Pure.imp\ $ t1 $ t2) = let val zs' = Term.add_vars t1 zs in close_up zs zs' (Logic.mk_implies (t1, aux zs' t2)) end | aux zs t = close_up zs (Term.add_vars t zs) t in aux [] end fun distinctness_formula T = all_distinct_unordered_pairs_of #> map (fn (t1, t2) => \<^const>\Not\ $ (HOLogic.eq_const T $ t1 $ t2)) #> List.foldr (s_conj o swap) \<^const>\True\ fun zero_const T = Const (\<^const_name>\zero_class.zero\, T) fun suc_const T = Const (\<^const_name>\Suc\, T --> T) fun uncached_data_type_constrs ({ctxt, ...} : hol_context) (T as Type (s, _)) = if is_interpreted_type s then [] else (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) s of SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs' | _ => if is_frac_type ctxt T then case typedef_info ctxt s of SOME {abs_type, rep_type, Abs_name, ...} => [(Abs_name, varify_and_instantiate_type ctxt abs_type T rep_type --> T)] | NONE => [] (* impossible *) else case Ctr_Sugar.ctr_sugar_of ctxt s of SOME {ctrs, ...} => map (apsnd (repair_constr_type T) o dest_Const) ctrs | NONE => if is_raw_quot_type ctxt T then [(\<^const_name>\Quot\, rep_type_for_quot_type ctxt T --> T)] else case typedef_info ctxt s of SOME {abs_type, rep_type, Abs_name, ...} => [(Abs_name, varify_and_instantiate_type ctxt abs_type T rep_type --> T)] | NONE => if T = \<^typ>\ind\ then [dest_Const \<^const>\Zero_Rep\, dest_Const \<^const>\Suc_Rep\] else []) | uncached_data_type_constrs _ _ = [] fun data_type_constrs (hol_ctxt as {constr_cache, ...}) T = case AList.lookup (op =) (!constr_cache) T of SOME xs => xs | NONE => let val xs = uncached_data_type_constrs hol_ctxt T in (Unsynchronized.change constr_cache (cons (T, xs)); xs) end fun binarized_and_boxed_data_type_constrs hol_ctxt binarize = map (apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InConstr)) o data_type_constrs hol_ctxt fun constr_name_for_sel_like \<^const_name>\fst\ = \<^const_name>\Pair\ | constr_name_for_sel_like \<^const_name>\snd\ = \<^const_name>\Pair\ | constr_name_for_sel_like s' = original_name s' fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') = let val s = constr_name_for_sel_like s' in AList.lookup (op =) (binarized_and_boxed_data_type_constrs hol_ctxt binarize (domain_type T')) s |> the |> pair s end fun card_of_type assigns (Type (\<^type_name>\fun\, [T1, T2])) = reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) | card_of_type assigns (Type (\<^type_name>\prod\, [T1, T2])) = card_of_type assigns T1 * card_of_type assigns T2 | card_of_type assigns (Type (\<^type_name>\set\, [T'])) = reasonable_power 2 (card_of_type assigns T') | card_of_type _ (Type (\<^type_name>\itself\, _)) = 1 | card_of_type _ \<^typ>\prop\ = 2 | card_of_type _ \<^typ>\bool\ = 2 | card_of_type assigns T = case AList.lookup (op =) assigns T of SOME k => k | NONE => if T = \<^typ>\bisim_iterator\ then 0 else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) fun bounded_card_of_type max default_card assigns (Type (\<^type_name>\fun\, [T1, T2])) = let val k1 = bounded_card_of_type max default_card assigns T1 val k2 = bounded_card_of_type max default_card assigns T2 in if k1 = max orelse k2 = max then max else Int.min (max, reasonable_power k2 k1) handle TOO_LARGE _ => max end | bounded_card_of_type max default_card assigns (Type (\<^type_name>\prod\, [T1, T2])) = let val k1 = bounded_card_of_type max default_card assigns T1 val k2 = bounded_card_of_type max default_card assigns T2 in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end | bounded_card_of_type max default_card assigns (Type (\<^type_name>\set\, [T'])) = bounded_card_of_type max default_card assigns (T' --> bool_T) | bounded_card_of_type max default_card assigns T = Int.min (max, if default_card = ~1 then card_of_type assigns T else card_of_type assigns T handle TYPE ("Nitpick_HOL.card_of_type", _, _) => default_card) (* Similar to "ATP_Util.tiny_card_of_type". *) fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card assigns T = let fun aux avoid T = (if member (op =) avoid T then 0 else if member (op =) finitizable_dataTs T then raise SAME () else case T of Type (\<^type_name>\fun\, [T1, T2]) => (case (aux avoid T1, aux avoid T2) of (_, 1) => 1 | (0, _) => 0 | (_, 0) => 0 | (k1, k2) => if k1 >= max orelse k2 >= max then max else Int.min (max, reasonable_power k2 k1)) | Type (\<^type_name>\prod\, [T1, T2]) => (case (aux avoid T1, aux avoid T2) of (0, _) => 0 | (_, 0) => 0 | (k1, k2) => if k1 >= max orelse k2 >= max then max else Int.min (max, k1 * k2)) | Type (\<^type_name>\set\, [T']) => aux avoid (T' --> bool_T) | Type (\<^type_name>\itself\, _) => 1 | \<^typ>\prop\ => 2 | \<^typ>\bool\ => 2 | Type _ => (case data_type_constrs hol_ctxt T of [] => if is_integer_type T orelse is_bit_type T then 0 else raise SAME () | constrs => let val constr_cards = map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd) constrs in if exists (curry (op =) 0) constr_cards then 0 else Int.min (max, Integer.sum constr_cards) end) | _ => raise SAME ()) handle SAME () => AList.lookup (op =) assigns T |> the_default default_card in Int.min (max, aux [] T) end val typical_atomic_card = 4 val typical_card_of_type = bounded_card_of_type 16777217 typical_atomic_card [] fun is_finite_type hol_ctxt T = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0 fun is_special_eligible_arg strict Ts t = case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of [] => true | bad_Ts => let val bad_Ts_cost = if strict then fold (curry (op *) o typical_card_of_type) bad_Ts 1 else fold (Integer.max o typical_card_of_type) bad_Ts 0 val T_cost = typical_card_of_type (fastype_of1 (Ts, t)) in (bad_Ts_cost, T_cost) |> (if strict then op < else op <=) end fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) fun let_var s = (nitpick_prefix ^ s, 999) val let_inline_threshold = 20 fun s_let Ts s n abs_T body_T f t = if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse is_special_eligible_arg false Ts t then f t else let val z = (let_var s, abs_T) in Const (\<^const_name>\Let\, abs_T --> (abs_T --> body_T) --> body_T) $ t $ abs_var z (incr_boundvars 1 (f (Var z))) end fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0 | loose_bvar1_count (t1 $ t2, k) = loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k) | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1) | loose_bvar1_count _ = 0 fun s_betapply _ (t1 as Const (\<^const_name>\Pure.eq\, _) $ t1', t2) = if t1' aconv t2 then \<^prop>\True\ else t1 $ t2 | s_betapply _ (t1 as Const (\<^const_name>\HOL.eq\, _) $ t1', t2) = if t1' aconv t2 then \<^term>\True\ else t1 $ t2 | s_betapply _ (Const (\<^const_name>\If\, _) $ \<^const>\True\ $ t1', _) = t1' | s_betapply _ (Const (\<^const_name>\If\, _) $ \<^const>\False\ $ _, t2) = t2 | s_betapply Ts (Const (\<^const_name>\Let\, Type (_, [bound_T, Type (_, [_, body_T])])) $ t12 $ Abs (s, T, t13'), t2) = let val body_T' = range_type body_T in Const (\<^const_name>\Let\, bound_T --> (bound_T --> body_T') --> body_T') $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2)) end | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) = (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1')) (curry betapply t1) t2 (* FIXME: fix all "s_betapply []" calls *) handle TERM _ => betapply (t1, t2) | General.Subscript => betapply (t1, t2)) | s_betapply _ (t1, t2) = t1 $ t2 fun s_betapplys Ts = Library.foldl (s_betapply Ts) fun s_beta_norm Ts t = let fun aux _ (Var _) = raise Same.SAME | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t') | aux Ts ((t1 as Abs _) $ t2) = Same.commit (aux Ts) (s_betapply Ts (t1, t2)) | aux Ts (t1 $ t2) = ((case aux Ts t1 of t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2)) | t1 => t1 $ Same.commit (aux Ts) t2) handle Same.SAME => t1 $ aux Ts t2) | aux _ _ = raise Same.SAME in aux Ts t handle Same.SAME => t end fun discr_term_for_constr hol_ctxt (x as (s, T)) = let val dataT = body_type T in if s = \<^const_name>\Suc\ then Abs (Name.uu, dataT, \<^const>\Not\ $ HOLogic.mk_eq (zero_const dataT, Bound 0)) else if length (data_type_constrs hol_ctxt dataT) >= 2 then Const (discr_for_constr x) else Abs (Name.uu, dataT, \<^const>\True\) end fun discriminate_value (hol_ctxt as {ctxt, ...}) x t = case head_of t of Const x' => if x = x' then \<^const>\True\ else if is_nonfree_constr ctxt x' then \<^const>\False\ else s_betapply [] (discr_term_for_constr hol_ctxt x, t) | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t) fun nth_arg_sel_term_for_constr (x as (s, T)) n = let val (arg_Ts, dataT) = strip_type T in if dataT = nat_T then \<^term>\%n::nat. n - 1\ else if is_pair_type dataT then Const (nth_sel_for_constr x n) else let fun aux m (Type (\<^type_name>\prod\, [T1, T2])) = let val (m, t1) = aux m T1 val (m, t2) = aux m T2 in (m, HOLogic.mk_prod (t1, t2)) end | aux m T = (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T) $ Bound 0) val m = fold (Integer.add o num_factors_in_type) (List.take (arg_Ts, n)) 0 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end end fun select_nth_constr_arg ctxt x t n res_T = (case strip_comb t of (Const x', args) => if x = x' then if is_free_constr ctxt x then nth args n else raise SAME () else if is_nonfree_constr ctxt x' then Const (\<^const_name>\unknown\, res_T) else raise SAME () | _ => raise SAME()) handle SAME () => s_betapply [] (nth_arg_sel_term_for_constr x n, t) fun construct_value _ x [] = Const x | construct_value ctxt (x as (s, _)) args = let val args = map Envir.eta_contract args in case hd args of Const (s', _) $ t => if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s andalso forall (fn (n, t') => select_nth_constr_arg ctxt x t n dummyT = t') (index_seq 0 (length args) ~~ args) then t else list_comb (Const x, args) | _ => list_comb (Const x, args) end fun constr_expand (hol_ctxt as {ctxt, ...}) T t = (case head_of t of Const x => if is_nonfree_constr ctxt x then t else raise SAME () | _ => raise SAME ()) handle SAME () => let val x' as (_, T') = if is_pair_type T then let val (T1, T2) = HOLogic.dest_prodT T in (\<^const_name>\Pair\, T1 --> T2 --> T) end else data_type_constrs hol_ctxt T |> hd val arg_Ts = binder_types T' in list_comb (Const x', map2 (select_nth_constr_arg ctxt x' t) (index_seq 0 (length arg_Ts)) arg_Ts) end fun coerce_bound_no f j t = case t of t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2 | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t') | Bound j' => if j' = j then f t else t | _ => t fun coerce_bound_0_in_term hol_ctxt new_T old_T = old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0 and coerce_term (hol_ctxt as {ctxt, ...}) Ts new_T old_T t = if old_T = new_T then t else case (new_T, old_T) of (Type (new_s, new_Ts as [new_T1, new_T2]), Type (\<^type_name>\fun\, [old_T1, old_T2])) => (case eta_expand Ts t 1 of Abs (s, _, t') => Abs (s, new_T1, t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2) |> Envir.eta_contract |> new_s <> \<^type_name>\fun\ ? construct_value ctxt (\<^const_name>\FunBox\, Type (\<^type_name>\fun\, new_Ts) --> new_T) o single | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])) | (Type (new_s, new_Ts as [new_T1, new_T2]), Type (old_s, old_Ts as [old_T1, old_T2])) => if old_s = \<^type_name>\fun_box\ orelse old_s = \<^type_name>\pair_box\ orelse old_s = \<^type_name>\prod\ then case constr_expand hol_ctxt old_T t of Const (old_s, _) $ t1 => if new_s = \<^type_name>\fun\ then coerce_term hol_ctxt Ts new_T (Type (\<^type_name>\fun\, old_Ts)) t1 else construct_value ctxt (old_s, Type (\<^type_name>\fun\, new_Ts) --> new_T) [coerce_term hol_ctxt Ts (Type (\<^type_name>\fun\, new_Ts)) (Type (\<^type_name>\fun\, old_Ts)) t1] | Const _ $ t1 $ t2 => construct_value ctxt (if new_s = \<^type_name>\prod\ then \<^const_name>\Pair\ else \<^const_name>\PairBox\, new_Ts ---> new_T) (@{map 3} (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] [t1, t2]) | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']) else raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 | is_ground_term (Const _) = true | is_ground_term _ = false fun special_bounds ts = fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o apply2 fst) fun is_funky_typedef_name ctxt s = member (op =) [\<^type_name>\unit\, \<^type_name>\prod\, \<^type_name>\set\, \<^type_name>\Sum_Type.sum\, \<^type_name>\int\] s orelse is_frac_type ctxt (Type (s, [])) fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s | is_funky_typedef _ _ = false fun all_defs_of thy subst = let val def_names = thy |> Theory.defs_of |> Defs.all_specifications_of |> maps snd |> map_filter #def |> Ord_List.make fast_string_ord in - Theory.nodes_of thy - |> maps Thm.axioms_of + Thm.all_axioms_of thy |> map (apsnd (subst_atomic subst o Thm.prop_of)) |> sort (fast_string_ord o apply2 fst) |> Ord_List.inter (fast_string_ord o apsnd fst) def_names |> map snd end (* Ideally we would check against "Complex_Main", not "Hilbert_Choice", but any theory will do as long as it contains all the "axioms" and "axiomatization" commands. *) fun is_built_in_theory thy_id = Context.subthy_id (thy_id, Context.theory_id \<^theory>\Hilbert_Choice\) fun all_nondefs_of ctxt subst = ctxt |> Spec_Rules.get |> filter (Spec_Rules.is_unknown o fst) |> maps (snd o snd) |> filter_out (is_built_in_theory o Thm.theory_id) |> map (subst_atomic subst o Thm.prop_of) fun arity_of_built_in_const (s, T) = if s = \<^const_name>\If\ then if nth_range_type 3 T = \<^typ>\bool\ then NONE else SOME 3 else case AList.lookup (op =) built_in_consts s of SOME n => SOME n | NONE => case AList.lookup (op =) built_in_typed_consts (s, unarize_type T) of SOME n => SOME n | NONE => case s of \<^const_name>\zero_class.zero\ => if is_iterator_type T then SOME 0 else NONE | \<^const_name>\Suc\ => if is_iterator_type (domain_type T) then SOME 0 else NONE | _ => NONE val is_built_in_const = is_some o arity_of_built_in_const (* This function is designed to work for both real definition axioms and simplification rules (equational specifications). *) fun term_under_def t = case t of \<^const>\Pure.imp\ $ _ $ t2 => term_under_def t2 | Const (\<^const_name>\Pure.eq\, _) $ t1 $ _ => term_under_def t1 | \<^const>\Trueprop\ $ t1 => term_under_def t1 | Const (\<^const_name>\HOL.eq\, _) $ t1 $ _ => term_under_def t1 | Abs (_, _, t') => term_under_def t' | t1 $ _ => term_under_def t1 | _ => t (* Here we crucially rely on "specialize_type" performing a preorder traversal of the term, without which the wrong occurrence of a constant could be matched in the face of overloading. *) fun def_props_for_const thy table (x as (s, _)) = if is_built_in_const x then [] else these (Symtab.lookup table s) |> map_filter (try (specialize_type thy x)) |> filter (curry (op =) (Const x) o term_under_def) fun normalized_rhs_of t = let fun aux (v as Var _) (SOME t) = SOME (lambda v t) | aux (c as Const (\<^const_name>\Pure.type\, _)) (SOME t) = SOME (lambda c t) | aux _ _ = NONE val (lhs, rhs) = case t of Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2 => (t1, t2) | \<^const>\Trueprop\ $ (Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) => (t1, t2) | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) val args = strip_comb lhs |> snd in fold_rev aux args (SOME rhs) end fun get_def_of_const thy table (x as (s, _)) = x |> def_props_for_const thy table |> List.last |> normalized_rhs_of |> Option.map (prefix_abs_vars s) handle List.Empty => NONE | TERM _ => NONE fun def_of_const_ext thy (unfold_table, fallback_table) (x as (s, _)) = if is_built_in_const x orelse original_name s <> s then NONE else case get_def_of_const thy unfold_table x of SOME def => SOME (true, def) | NONE => get_def_of_const thy fallback_table x |> Option.map (pair false) val def_of_const = Option.map snd ooo def_of_const_ext fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t | fixpoint_kind_of_rhs (Const (\<^const_name>\lfp\, _) $ Abs _) = Lfp | fixpoint_kind_of_rhs (Const (\<^const_name>\gfp\, _) $ Abs _) = Gfp | fixpoint_kind_of_rhs _ = NoFp fun is_mutually_inductive_pred_def thy table t = let fun is_good_arg (Bound _) = true | is_good_arg (Const (s, _)) = s = \<^const_name>\True\ orelse s = \<^const_name>\False\ orelse s = \<^const_name>\undefined\ | is_good_arg _ = false in case t |> strip_abs_body |> strip_comb of (Const x, ts as (_ :: _)) => (case def_of_const thy table x of SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts | NONE => false) | _ => false end fun unfold_mutually_inductive_preds thy table = map_aterms (fn t as Const x => (case def_of_const thy table x of SOME t' => let val t' = Envir.eta_contract t' in if is_mutually_inductive_pred_def thy table t' then t' else t end | NONE => t) | t => t) fun case_const_names ctxt = map_filter (fn {casex = Const (s, T), ...} => (case rev (binder_types T) of [] => NONE | T :: Ts => if is_data_type ctxt T then SOME (s, length Ts) else NONE)) (Ctr_Sugar.ctr_sugars_of ctxt) @ map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) fun fixpoint_kind_of_const thy table x = if is_built_in_const x then NoFp else fixpoint_kind_of_rhs (the (def_of_const thy table x)) handle Option.Option => NoFp fun is_raw_inductive_pred ({thy, def_tables, intro_table, ...} : hol_context) x = fixpoint_kind_of_const thy def_tables x <> NoFp andalso not (null (def_props_for_const thy intro_table x)) fun is_inductive_pred hol_ctxt (x as (s, _)) = String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s orelse is_raw_inductive_pred hol_ctxt x fun lhs_of_equation t = case t of Const (\<^const_name>\Pure.all\, _) $ Abs (_, _, t1) => lhs_of_equation t1 | Const (\<^const_name>\Pure.eq\, _) $ t1 $ _ => SOME t1 | \<^const>\Pure.imp\ $ _ $ t2 => lhs_of_equation t2 | \<^const>\Trueprop\ $ t1 => lhs_of_equation t1 | Const (\<^const_name>\All\, _) $ Abs (_, _, t1) => lhs_of_equation t1 | Const (\<^const_name>\HOL.eq\, _) $ t1 $ _ => SOME t1 | \<^const>\HOL.implies\ $ _ $ t2 => lhs_of_equation t2 | _ => NONE fun is_constr_pattern _ (Bound _) = true | is_constr_pattern _ (Var _) = true | is_constr_pattern ctxt t = case strip_comb t of (Const x, args) => is_nonfree_constr ctxt x andalso forall (is_constr_pattern ctxt) args | _ => false fun is_constr_pattern_lhs ctxt t = forall (is_constr_pattern ctxt) (snd (strip_comb t)) fun is_constr_pattern_formula ctxt t = case lhs_of_equation t of SOME t' => is_constr_pattern_lhs ctxt t' | NONE => false (* Similar to "specialize_type" but returns all matches rather than only the first (preorder) match. *) fun multi_specialize_type thy slack (s, T) t = let fun aux (Const (s', T')) ys = if s = s' then ys |> (if AList.defined (op =) ys T' then I else cons (T', Envir.subst_term_types (Sign.typ_match thy (T', T) Vartab.empty) t) handle Type.TYPE_MATCH => I | TERM _ => if slack then I else raise NOT_SUPPORTED ("too much polymorphism in axiom \"" ^ Syntax.string_of_term_global thy t ^ "\" involving " ^ quote s)) else ys | aux _ ys = ys in map snd (fold_aterms aux t []) end fun nondef_props_for_const thy slack table (x as (s, _)) = these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) fun unvarify_term (t1 $ t2) = unvarify_term t1 $ unvarify_term t2 | unvarify_term (Var ((s, 0), T)) = Free (s, T) | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t') | unvarify_term t = t fun axiom_for_choice_spec ctxt = unvarify_term #> Object_Logic.atomize_term ctxt #> Choice_Specification.close_form #> HOLogic.mk_Trueprop fun is_choice_spec_fun ({thy, ctxt, def_tables, nondef_table, choice_spec_table, ...} : hol_context) x = case nondef_props_for_const thy true choice_spec_table x of [] => false | ts => case def_of_const thy def_tables x of SOME (Const (\<^const_name>\Eps\, _) $ _) => true | SOME _ => false | NONE => let val ts' = nondef_props_for_const thy true nondef_table x in length ts' = length ts andalso forall (fn t => exists (curry (op aconv) (axiom_for_choice_spec ctxt t)) ts') ts end fun is_choice_spec_axiom thy choice_spec_table t = Symtab.exists (exists (curry (op aconv) t o axiom_for_choice_spec thy) o snd) choice_spec_table fun is_raw_equational_fun ({thy, simp_table, psimp_table, ...} : hol_context) x = exists (fn table => not (null (def_props_for_const thy table x))) [!simp_table, psimp_table] fun is_equational_fun hol_ctxt = is_raw_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt (** Constant unfolding **) fun constr_case_body ctxt Ts (func_t, (x as (_, T))) = let val arg_Ts = binder_types T in s_betapplys Ts (func_t, map2 (select_nth_constr_arg ctxt x (Bound 0)) (index_seq 0 (length arg_Ts)) arg_Ts) end fun add_constr_case res_T (body_t, guard_t) res_t = if res_T = bool_T then s_conj (HOLogic.mk_imp (guard_t, body_t), res_t) else Const (\<^const_name>\If\, bool_T --> res_T --> res_T --> res_T) $ guard_t $ body_t $ res_t fun optimized_case_def (hol_ctxt as {ctxt, ...}) Ts dataT res_T func_ts = let val xs = data_type_constrs hol_ctxt dataT val cases = func_ts ~~ xs |> map (fn (func_t, x) => (constr_case_body ctxt (dataT :: Ts) (incr_boundvars 1 func_t, x), discriminate_value hol_ctxt x (Bound 0))) |> AList.group (op aconv) |> map (apsnd (List.foldl s_disj \<^const>\False\)) |> sort (int_ord o apply2 (size_of_term o snd)) |> rev in if res_T = bool_T then if forall (member (op =) [\<^const>\False\, \<^const>\True\] o fst) cases then case cases of [(body_t, _)] => body_t | [_, (\<^const>\True\, head_t2)] => head_t2 | [_, (\<^const>\False\, head_t2)] => \<^const>\Not\ $ head_t2 | _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases") else \<^const>\True\ |> fold_rev (add_constr_case res_T) cases else fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases) end |> absdummy dataT fun optimized_record_get (hol_ctxt as {thy, ctxt, ...}) s rec_T res_T t = let val constr_x = hd (data_type_constrs hol_ctxt rec_T) in case no_of_record_field thy s rec_T of ~1 => (case rec_T of Type (_, Ts as _ :: _) => let val rec_T' = List.last Ts val j = num_record_fields thy rec_T - 1 in select_nth_constr_arg ctxt constr_x t j res_T |> optimized_record_get hol_ctxt s rec_T' res_T end | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T], [])) | j => select_nth_constr_arg ctxt constr_x t j res_T end fun optimized_record_update (hol_ctxt as {thy, ctxt, ...}) s rec_T fun_t rec_t = let val constr_x as (_, constr_T) = hd (data_type_constrs hol_ctxt rec_T) val Ts = binder_types constr_T val n = length Ts val special_j = no_of_record_field thy s rec_T val ts = map2 (fn j => fn T => let val t = select_nth_constr_arg ctxt constr_x rec_t j T in if j = special_j then s_betapply [] (fun_t, t) else if j = n - 1 andalso special_j = ~1 then optimized_record_update hol_ctxt s (rec_T |> dest_Type |> snd |> List.last) fun_t t else t end) (index_seq 0 n) Ts in list_comb (Const constr_x, ts) end (* Prevents divergence in case of cyclic or infinite definition dependencies. *) val unfold_max_depth = 255 (* Inline definitions or define as an equational constant? Booleans tend to benefit more from inlining, due to the polarity analysis. (However, if "total_consts" is set, the polarity analysis is likely not to be so crucial.) *) val def_inline_threshold_for_booleans = 60 val def_inline_threshold_for_non_booleans = 20 fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, whacks, total_consts, case_names, def_tables, ground_thm_table, ersatz_table, ...}) = let fun do_numeral depth Ts mult T some_t0 t1 t2 = (if is_number_type ctxt T then let val j = mult * HOLogic.dest_numeral t2 in if j = 1 then raise SAME () else let val s = numeral_prefix ^ signed_string_of_int j in if is_integer_like_type T then Const (s, T) else do_term depth Ts (Const (\<^const_name>\of_int\, int_T --> T) $ Const (s, int_T)) end end handle TERM _ => raise SAME () else raise SAME ()) handle SAME () => (case some_t0 of NONE => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2) | SOME t0 => s_betapply [] (do_term depth Ts t0, s_betapply [] (do_term depth Ts t1, do_term depth Ts t2))) and do_term depth Ts t = case t of (t0 as Const (\<^const_name>\uminus\, _) $ ((t1 as Const (\<^const_name>\numeral\, Type (\<^type_name>\fun\, [_, ran_T]))) $ t2)) => do_numeral depth Ts ~1 ran_T (SOME t0) t1 t2 | (t1 as Const (\<^const_name>\numeral\, Type (\<^type_name>\fun\, [_, ran_T]))) $ t2 => do_numeral depth Ts 1 ran_T NONE t1 t2 | Const (\<^const_name>\refl_on\, T) $ Const (\<^const_name>\top\, _) $ t2 => do_const depth Ts t (\<^const_name>\refl'\, range_type T) [t2] | (t0 as Const (\<^const_name>\Sigma\, Type (_, [T1, Type (_, [T2, T3])]))) $ t1 $ (t2 as Abs (_, _, t2')) => if loose_bvar1 (t2', 0) then s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2]) else do_term depth Ts (Const (\<^const_name>\prod\, T1 --> range_type T2 --> T3) $ t1 $ incr_boundvars ~1 t2') | Const (x as (\<^const_name>\distinct\, Type (\<^type_name>\fun\, [Type (\<^type_name>\list\, [T']), _]))) $ (t1 as _ $ _) => (t1 |> HOLogic.dest_list |> distinctness_formula T' handle TERM _ => do_const depth Ts t x [t1]) | Const (x as (\<^const_name>\If\, _)) $ t1 $ t2 $ t3 => if is_ground_term t1 andalso exists (Pattern.matches thy o rpair t1) (Inttab.lookup_list ground_thm_table (hash_term t1)) then do_term depth Ts t2 else do_const depth Ts t x [t1, t2, t3] | Const (\<^const_name>\Let\, _) $ t1 $ t2 => s_betapply Ts (apply2 (do_term depth Ts) (t2, t1)) | Const x => do_const depth Ts t x [] | t1 $ t2 => (case strip_comb t of (Const x, ts) => do_const depth Ts t x ts | _ => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)) | Bound _ => t | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body) | _ => if member (term_match thy) whacks t then Const (\<^const_name>\unknown\, fastype_of1 (Ts, t)) else t and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T = (Abs (Name.uu, body_type T, select_nth_constr_arg ctxt x (Bound 0) n res_T), []) | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T = (select_nth_constr_arg ctxt x (do_term depth Ts t) n res_T, ts) and quot_rep_of depth Ts abs_T rep_T ts = select_nth_constr_arg_with_args depth Ts (\<^const_name>\Quot\, rep_T --> abs_T) ts 0 rep_T and do_const depth Ts t (x as (s, T)) ts = if member (term_match thy) whacks (Const x) then Const (\<^const_name>\unknown\, fastype_of1 (Ts, t)) else case AList.lookup (op =) ersatz_table s of SOME s' => do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts | NONE => let fun def_inline_threshold () = if is_boolean_type (body_type T) andalso total_consts <> SOME true then def_inline_threshold_for_booleans else def_inline_threshold_for_non_booleans val (const, ts) = if is_built_in_const x then (Const x, ts) else case AList.lookup (op =) case_names s of SOME n => if length ts < n then (do_term depth Ts (eta_expand Ts t (n - length ts)), []) else let val (dataT, res_T) = nth_range_type n T |> pairf domain_type range_type in (optimized_case_def hol_ctxt Ts dataT res_T (map (do_term depth Ts) (take n ts)), drop n ts) end | _ => if is_constr ctxt x then (Const x, ts) else if is_stale_constr ctxt x then raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \ \(\"" ^ s ^ "\")") else if is_quot_abs_fun ctxt x then case T of Type (\<^type_name>\fun\, [rep_T, abs_T as Type (abs_s, _)]) => if is_interpreted_type abs_s then raise NOT_SUPPORTED ("abstraction function on " ^ quote abs_s) else (Abs (Name.uu, rep_T, Const (\<^const_name>\Quot\, rep_T --> abs_T) $ (Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T) $ Bound 0)), ts) else if is_quot_rep_fun ctxt x then case T of Type (\<^type_name>\fun\, [abs_T as Type (abs_s, _), rep_T]) => if is_interpreted_type abs_s then raise NOT_SUPPORTED ("representation function on " ^ quote abs_s) else quot_rep_of depth Ts abs_T rep_T ts else if is_record_get thy x then case length ts of 0 => (do_term depth Ts (eta_expand Ts t 1), []) | _ => (optimized_record_get hol_ctxt s (domain_type T) (range_type T) (do_term depth Ts (hd ts)), tl ts) else if is_record_update thy x then case length ts of 2 => (optimized_record_update hol_ctxt (unsuffix Record.updateN s) (nth_range_type 2 T) (do_term depth Ts (hd ts)) (do_term depth Ts (nth ts 1)), []) | n => (do_term depth Ts (eta_expand Ts t (2 - n)), []) else if is_abs_fun ctxt x andalso is_quot_type ctxt (range_type T) then let val abs_T = range_type T val rep_T = elem_type (domain_type T) val eps_fun = Const (\<^const_name>\Eps\, (rep_T --> bool_T) --> rep_T) val normal_fun = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T) val abs_fun = Const (\<^const_name>\Quot\, rep_T --> abs_T) val pred = Abs (Name.uu, rep_T, Const (\<^const_name>\Set.member\, rep_T --> domain_type T --> bool_T) $ Bound 0 $ Bound 1) in (Abs (Name.uu, HOLogic.mk_setT rep_T, abs_fun $ (normal_fun $ (eps_fun $ pred))) |> do_term (depth + 1) Ts, ts) end else if is_rep_fun ctxt x then let val x' = mate_of_rep_fun ctxt x in if is_constr ctxt x' then select_nth_constr_arg_with_args depth Ts x' ts 0 (range_type T) else if is_quot_type ctxt (domain_type T) then let val abs_T = domain_type T val rep_T = elem_type (range_type T) val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T [] val (equiv_rel, _) = equiv_relation_for_quot_type ctxt abs_T in (Abs (Name.uu, abs_T, HOLogic.Collect_const rep_T $ (equiv_rel $ (rep_fun $ Bound 0))), ts) end else (Const x, ts) end else if is_equational_fun hol_ctxt x orelse is_choice_spec_fun hol_ctxt x then (Const x, ts) else case def_of_const_ext thy def_tables x of SOME (unfold, def) => if depth > unfold_max_depth then raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term", "too many nested definitions (" ^ string_of_int depth ^ ") while expanding " ^ quote s) else if s = \<^const_name>\wfrec'\ then (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), []) else if not unfold andalso size_of_term def > def_inline_threshold () then (Const x, ts) else (do_term (depth + 1) Ts def, ts) | NONE => (Const x, ts) in s_betapplys Ts (const, map (do_term depth Ts) ts) |> s_beta_norm Ts end in do_term 0 [] end (** Axiom extraction/generation **) fun extensional_equal j T t1 t2 = if is_fun_type T then let val dom_T = pseudo_domain_type T val ran_T = pseudo_range_type T val var_t = Var (("x", j), dom_T) in extensional_equal (j + 1) ran_T (betapply (t1, var_t)) (betapply (t2, var_t)) end else Const (\<^const_name>\HOL.eq\, T --> T --> bool_T) $ t1 $ t2 (* FIXME: needed? *) fun equationalize_term ctxt tag t = let val j = maxidx_of_term t + 1 val (prems, concl) = Logic.strip_horn t in Logic.list_implies (prems, case concl of \<^const>\Trueprop\ $ (Const (\<^const_name>\HOL.eq\, Type (_, [T, _])) $ t1 $ t2) => \<^const>\Trueprop\ $ extensional_equal j T t1 t2 | \<^const>\Trueprop\ $ t' => \<^const>\Trueprop\ $ HOLogic.mk_eq (t', \<^const>\True\) | Const (\<^const_name>\Pure.eq\, Type (_, [T, _])) $ t1 $ t2 => \<^const>\Trueprop\ $ extensional_equal j T t1 t2 | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^ quote (Syntax.string_of_term ctxt t)); raise SAME ())) |> SOME end handle SAME () => NONE fun pair_for_prop t = case term_under_def t of Const (s, _) => (s, t) | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) fun def_table_for ts subst = ts |> map (pair_for_prop o subst_atomic subst) |> AList.group (op =) |> Symtab.make fun const_def_tables ctxt subst ts = (def_table_for (map Thm.prop_of (rev (Named_Theorems.get ctxt \<^named_theorems>\nitpick_unfold\))) subst, fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) (map pair_for_prop ts) Symtab.empty) fun paired_with_consts t = map (rpair t) (Term.add_const_names t []) fun const_nondef_table ts = fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make fun const_simp_table ctxt = def_table_for (map_filter (equationalize_term ctxt "nitpick_simp" o Thm.prop_of) (rev (Named_Theorems.get ctxt \<^named_theorems>\nitpick_simp\))) fun const_psimp_table ctxt = def_table_for (map_filter (equationalize_term ctxt "nitpick_psimp" o Thm.prop_of) (rev (Named_Theorems.get ctxt \<^named_theorems>\nitpick_psimp\))) fun const_choice_spec_table ctxt subst = map (subst_atomic subst o Thm.prop_of) (rev (Named_Theorems.get ctxt \<^named_theorems>\nitpick_choice_spec\)) |> const_nondef_table fun inductive_intro_table ctxt subst def_tables = let val thy = Proof_Context.theory_of ctxt in def_table_for (maps (map (unfold_mutually_inductive_preds thy def_tables o Thm.prop_of) o snd o snd) (filter ((Spec_Rules.is_inductive orf Spec_Rules.is_co_inductive) o #1) (Spec_Rules.get ctxt))) subst end fun ground_theorem_table thy = fold ((fn \<^const>\Trueprop\ $ t1 => is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) | _ => I) o Thm.prop_of o snd) (Global_Theory.all_thms_of thy true) Inttab.empty fun ersatz_table ctxt = #ersatz_table (Data.get (Context.Proof ctxt)) |> fold (append o snd) (#frac_types (Data.get (Context.Proof ctxt))) fun add_simps simp_table s eqs = Unsynchronized.change simp_table (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s))) fun inverse_axioms_for_rep_fun ctxt (x as (_, T)) = let val thy = Proof_Context.theory_of ctxt val abs_T = domain_type T in typedef_info ctxt (fst (dest_Type abs_T)) |> the |> pairf #Abs_inverse #Rep_inverse |> apply2 (specialize_type thy x o Thm.prop_of o the) ||> single |> op :: end fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) = let val thy = Proof_Context.theory_of ctxt val abs_T = Type abs_z in if is_univ_typedef ctxt abs_T then [] else case typedef_info ctxt abs_s of SOME {abs_type, rep_type, Rep_name, prop_of_Rep, ...} => let val rep_T = varify_and_instantiate_type ctxt abs_type abs_T rep_type val rep_t = Const (Rep_name, abs_T --> rep_T) val set_t = prop_of_Rep |> HOLogic.dest_Trueprop |> specialize_type thy (dest_Const rep_t) |> HOLogic.dest_mem |> snd in [HOLogic.all_const abs_T $ Abs (Name.uu, abs_T, HOLogic.mk_mem (rep_t $ Bound 0, set_t)) |> HOLogic.mk_Trueprop] end | NONE => [] end fun optimized_quot_type_axioms ctxt abs_z = let val abs_T = Type abs_z val rep_T = rep_type_for_quot_type ctxt abs_T val (equiv_rel, partial) = equiv_relation_for_quot_type ctxt abs_T val a_var = Var (("a", 0), abs_T) val x_var = Var (("x", 0), rep_T) val y_var = Var (("y", 0), rep_T) val x = (\<^const_name>\Quot\, rep_T --> abs_T) val sel_a_t = select_nth_constr_arg ctxt x a_var 0 rep_T val normal_fun = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T) val normal_x = normal_fun $ x_var val normal_y = normal_fun $ y_var val is_unknown_t = Const (\<^const_name>\is_unknown\, rep_T --> bool_T) in [Logic.mk_equals (normal_fun $ sel_a_t, sel_a_t), Logic.list_implies ([\<^const>\Not\ $ (is_unknown_t $ normal_x), \<^const>\Not\ $ (is_unknown_t $ normal_y), equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop, Logic.mk_equals (normal_x, normal_y)), Logic.list_implies ([HOLogic.mk_Trueprop (\<^const>\Not\ $ (is_unknown_t $ normal_x)), HOLogic.mk_Trueprop (\<^const>\Not\ $ HOLogic.mk_eq (normal_x, x_var))], HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))] |> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t)) end fun codatatype_bisim_axioms (hol_ctxt as {ctxt, ...}) T = let val xs = data_type_constrs hol_ctxt T val pred_T = T --> bool_T val iter_T = \<^typ>\bisim_iterator\ val bisim_max = \<^const>\bisim_iterator_max\ val n_var = Var (("n", 0), iter_T) val n_var_minus_1 = Const (\<^const_name>\safe_The\, (iter_T --> bool_T) --> iter_T) $ Abs ("m", iter_T, HOLogic.eq_const iter_T $ (suc_const iter_T $ Bound 0) $ n_var) val x_var = Var (("x", 0), T) val y_var = Var (("y", 0), T) fun bisim_const T = Const (\<^const_name>\bisim\, [iter_T, T, T] ---> bool_T) fun nth_sub_bisim x n nth_T = (if is_codatatype ctxt nth_T then bisim_const nth_T $ n_var_minus_1 else HOLogic.eq_const nth_T) $ select_nth_constr_arg ctxt x x_var n nth_T $ select_nth_constr_arg ctxt x y_var n nth_T fun case_func (x as (_, T)) = let val arg_Ts = binder_types T val core_t = discriminate_value hol_ctxt x y_var :: map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts |> foldr1 s_conj in fold_rev absdummy arg_Ts core_t end in [HOLogic.mk_imp (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T, s_betapply [] (optimized_case_def hol_ctxt [] T bool_T (map case_func xs), x_var)), bisim_const T $ n_var $ x_var $ y_var), HOLogic.eq_const pred_T $ (bisim_const T $ bisim_max $ x_var) $ Abs (Name.uu, T, HOLogic.mk_eq (x_var, Bound 0))] |> map HOLogic.mk_Trueprop end exception NO_TRIPLE of unit fun triple_for_intro_rule ctxt x t = let val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term ctxt) val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term ctxt val (main, side) = List.partition (exists_Const (curry (op =) x)) prems val is_good_head = curry (op =) (Const x) o head_of in if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE () end val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb fun wf_constraint_for rel side concl main = let val core = HOLogic.mk_mem (HOLogic.mk_prod (apply2 tuple_for_args (main, concl)), Var rel) val t = List.foldl HOLogic.mk_imp core side val vars = filter_out (curry (op =) rel) (Term.add_vars t []) in Library.foldl (fn (t', ((x, j), T)) => HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, j), T), t'))) (t, vars) end fun wf_constraint_for_triple rel (side, main, concl) = map (wf_constraint_for rel side concl) main |> foldr1 s_conj fun terminates_by ctxt timeout goal tac = can (SINGLE (Classical.safe_tac ctxt) #> the #> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt))) #> the #> Goal.finish ctxt) goal val max_cached_wfs = 50 val cached_timeout = Synchronized.var "Nitpick_HOL.cached_timeout" Time.zeroTime val cached_wf_props = Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list) val termination_tacs = [Lexicographic_Order.lex_order_tac true, ScnpReconstruct.sizechange_tac] fun uncached_is_well_founded_inductive_pred ({thy, ctxt, debug, tac_timeout, intro_table, ...} : hol_context) (x as (_, T)) = case def_props_for_const thy intro_table x of [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive", [Const x]) | intro_ts => (case map (triple_for_intro_rule ctxt x) intro_ts |> filter_out (null o #2) of [] => true | triples => let val binders_T = HOLogic.mk_tupleT (binder_types T) val rel_T = HOLogic.mk_setT (HOLogic.mk_prodT (binders_T, binders_T)) val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1 val rel = (("R", j), rel_T) val prop = Const (\<^const_name>\wf\, rel_T --> bool_T) $ Var rel :: map (wf_constraint_for_triple rel) triples |> foldr1 s_conj |> HOLogic.mk_Trueprop val _ = if debug then writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop) else () in if tac_timeout = Synchronized.value cached_timeout andalso length (Synchronized.value cached_wf_props) < max_cached_wfs then () else (Synchronized.change cached_wf_props (K []); Synchronized.change cached_timeout (K tac_timeout)); case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of SOME wf => wf | NONE => let val goal = prop |> Thm.cterm_of ctxt |> Goal.init val wf = exists (terminates_by ctxt tac_timeout goal) termination_tacs in Synchronized.change cached_wf_props (cons (prop, wf)); wf end end) handle List.Empty => false | NO_TRIPLE () => false (* The type constraint below is a workaround for a Poly/ML crash. *) fun is_well_founded_inductive_pred (hol_ctxt as {thy, wfs, def_tables, wf_cache, ...} : hol_context) (x as (s, _)) = case triple_lookup (const_match thy) wfs x of SOME (SOME b) => b | _ => s = \<^const_name>\Nats\ orelse s = \<^const_name>\fold_graph'\ orelse case AList.lookup (op =) (!wf_cache) x of SOME (_, wf) => wf | NONE => let val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp) val wf = uncached_is_well_founded_inductive_pred hol_ctxt x in Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf end fun ap_curry [_] _ t = t | ap_curry arg_Ts tuple_T t = let val n = length arg_Ts in fold_rev (Term.abs o pair "c") arg_Ts (incr_boundvars n t $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0))) end fun num_occs_of_bound_in_term j (t1 $ t2) = op + (apply2 (num_occs_of_bound_in_term j) (t1, t2)) | num_occs_of_bound_in_term j (Abs (_, _, t')) = num_occs_of_bound_in_term (j + 1) t' | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0 | num_occs_of_bound_in_term _ _ = 0 val is_linear_inductive_pred_def = let fun do_disjunct j (Const (\<^const_name>\Ex\, _) $ Abs (_, _, t2)) = do_disjunct (j + 1) t2 | do_disjunct j t = case num_occs_of_bound_in_term j t of 0 => true | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t) | _ => false fun do_lfp_def (Const (\<^const_name>\lfp\, _) $ t2) = let val (xs, body) = strip_abs t2 in case length xs of 1 => false | n => forall (do_disjunct (n - 1)) (disjuncts_of body) end | do_lfp_def _ = false in do_lfp_def o strip_abs_body end fun n_ptuple_paths 0 = [] | n_ptuple_paths 1 = [] | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1)) val ap_n_split = HOLogic.mk_ptupleabs o n_ptuple_paths val linear_pred_base_and_step_rhss = let fun aux (Const (\<^const_name>\lfp\, _) $ t2) = let val (xs, body) = strip_abs t2 val arg_Ts = map snd (tl xs) val tuple_T = HOLogic.mk_tupleT arg_Ts val j = length arg_Ts fun repair_rec j (Const (\<^const_name>\Ex\, T1) $ Abs (s2, T2, t2')) = Const (\<^const_name>\Ex\, T1) $ Abs (s2, T2, repair_rec (j + 1) t2') | repair_rec j (\<^const>\HOL.conj\ $ t1 $ t2) = \<^const>\HOL.conj\ $ repair_rec j t1 $ repair_rec j t2 | repair_rec j t = let val (head, args) = strip_comb t in if head = Bound j then HOLogic.eq_const tuple_T $ Bound j $ mk_flat_tuple tuple_T args else t end val (nonrecs, recs) = List.partition (curry (op =) 0 o num_occs_of_bound_in_term j) (disjuncts_of body) val base_body = nonrecs |> List.foldl s_disj \<^const>\False\ val step_body = recs |> map (repair_rec j) |> List.foldl s_disj \<^const>\False\ in (fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body)) |> ap_n_split (length arg_Ts) tuple_T bool_T, Abs ("y", tuple_T, fold_rev Term.abs (tl xs) step_body |> ap_n_split (length arg_Ts) tuple_T bool_T)) end | aux t = raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t]) in aux end fun predicatify T t = let val set_T = HOLogic.mk_setT T in Abs (Name.uu, T, Const (\<^const_name>\Set.member\, T --> set_T --> bool_T) $ Bound 0 $ incr_boundvars 1 t) end fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def = let val j = maxidx_of_term def + 1 val (outer, fp_app) = strip_abs def val outer_bounds = map Bound (length outer - 1 downto 0) val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer val fp_app = subst_bounds (rev outer_vars, fp_app) val (outer_Ts, rest_T) = strip_n_binders (length outer) T val tuple_arg_Ts = strip_type rest_T |> fst val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts val prod_T = HOLogic.mk_prodT (tuple_T, tuple_T) val set_T = HOLogic.mk_setT tuple_T val rel_T = HOLogic.mk_setT prod_T val pred_T = tuple_T --> bool_T val curried_T = tuple_T --> pred_T val uncurried_T = prod_T --> bool_T val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> pred_T) val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs) |> HOLogic.mk_Trueprop val _ = add_simps simp_table base_s [base_eq] val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T) val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs) |> HOLogic.mk_Trueprop val _ = add_simps simp_table step_s [step_eq] val image_const = Const (\<^const_name>\Image\, rel_T --> set_T --> set_T) val rtrancl_const = Const (\<^const_name>\rtrancl\, rel_T --> rel_T) val base_set = HOLogic.Collect_const tuple_T $ list_comb (Const base_x, outer_bounds) val step_set = HOLogic.Collect_const prod_T $ (Const (\<^const_name>\case_prod\, curried_T --> uncurried_T) $ list_comb (Const step_x, outer_bounds)) val image_set = image_const $ (rtrancl_const $ step_set) $ base_set |> predicatify tuple_T in fold_rev Term.abs outer (image_set |> ap_curry tuple_arg_Ts tuple_T) |> unfold_defs_in_term hol_ctxt end fun is_good_starred_linear_pred_type (Type (\<^type_name>\fun\, Ts)) = forall (not o (is_fun_or_set_type orf is_pair_type)) Ts | is_good_starred_linear_pred_type _ = false fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds, def_tables, simp_table, ...}) gfp (x as (s, T)) = let val iter_T = iterator_type_for_const gfp x val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T) val unrolled_const = Const x' $ zero_const iter_T val def = the (def_of_const thy def_tables x) in if is_equational_fun hol_ctxt x' then unrolled_const (* already done *) else if not gfp andalso star_linear_preds andalso is_linear_inductive_pred_def def andalso is_good_starred_linear_pred_type T then starred_linear_pred_const hol_ctxt x def else let val j = maxidx_of_term def + 1 val (outer, fp_app) = strip_abs def val outer_bounds = map Bound (length outer - 1 downto 0) val cur = Var ((iter_var_prefix, j + 1), iter_T) val next = suc_const iter_T $ cur val rhs = case fp_app of Const _ $ t => s_betapply [] (t, list_comb (Const x', next :: outer_bounds)) | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_const", [fp_app]) val (inner, naked_rhs) = strip_abs rhs val all = outer @ inner val bounds = map Bound (length all - 1 downto 0) val vars = map (fn (s, T) => Var ((s, j), T)) all val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs) |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars) val _ = add_simps simp_table s' [eq] in unrolled_const end end fun raw_inductive_pred_axiom ({thy, def_tables, ...} : hol_context) x = let val def = the (def_of_const thy def_tables x) val (outer, fp_app) = strip_abs def val outer_bounds = map Bound (length outer - 1 downto 0) val rhs = case fp_app of Const _ $ t => s_betapply [] (t, list_comb (Const x, outer_bounds)) | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom", [fp_app]) val (inner, naked_rhs) = strip_abs rhs val all = outer @ inner val bounds = map Bound (length all - 1 downto 0) val j = maxidx_of_term def + 1 val vars = map (fn (s, T) => Var ((s, j), T)) all in HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs) |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars) end fun inductive_pred_axiom hol_ctxt (x as (s, T)) = if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then let val x' = (strip_first_name_sep s |> snd, T) in raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)] end else raw_inductive_pred_axiom hol_ctxt x fun equational_fun_axioms (hol_ctxt as {thy, ctxt, def_tables, simp_table, psimp_table, ...}) x = case def_props_for_const thy (!simp_table) x of [] => (case def_props_for_const thy psimp_table x of [] => (if is_inductive_pred hol_ctxt x then [inductive_pred_axiom hol_ctxt x] else case def_of_const thy def_tables x of SOME def => \<^const>\Trueprop\ $ HOLogic.mk_eq (Const x, def) |> equationalize_term ctxt "" |> the |> single | NONE => []) | psimps => psimps) | simps => simps fun is_equational_fun_surely_complete hol_ctxt x = case equational_fun_axioms hol_ctxt x of [\<^const>\Trueprop\ $ (Const (\<^const_name>\HOL.eq\, _) $ t1 $ _)] => strip_comb t1 |> snd |> forall is_Var | _ => false (** Type preprocessing **) fun merged_type_var_table_for_terms thy ts = let fun add (s, S) table = table |> (case AList.lookup (Sign.subsort thy o swap) table S of SOME _ => I | NONE => filter_out (fn (S', _) => Sign.subsort thy (S, S')) #> cons (S, s)) val tfrees = [] |> fold Term.add_tfrees ts |> sort (string_ord o apply2 fst) in [] |> fold add tfrees |> rev end fun merge_type_vars_in_term thy merge_type_vars table = merge_type_vars ? map_types (map_atyps (fn TFree (_, S) => TFree (table |> find_first (fn (S', _) => Sign.subsort thy (S', S)) |> the |> swap) | T => T)) fun add_ground_types hol_ctxt binarize = let fun aux T accum = case T of Type (\<^type_name>\fun\, Ts) => fold aux Ts accum | Type (\<^type_name>\prod\, Ts) => fold aux Ts accum | Type (\<^type_name>\set\, Ts) => fold aux Ts accum | Type (\<^type_name>\itself\, [T1]) => aux T1 accum | Type (_, Ts) => if member (op =) (\<^typ>\prop\ :: \<^typ>\bool\ :: accum) T then accum else T :: accum |> fold aux (case binarized_and_boxed_data_type_constrs hol_ctxt binarize T of [] => Ts | xs => map snd xs) | _ => insert (op =) T accum in aux end fun ground_types_in_type hol_ctxt binarize T = add_ground_types hol_ctxt binarize T [] fun ground_types_in_terms hol_ctxt binarize ts = fold (fold_types (add_ground_types hol_ctxt binarize)) ts [] end; diff --git a/src/Pure/Thy/export_theory.ML b/src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML +++ b/src/Pure/Thy/export_theory.ML @@ -1,424 +1,424 @@ (* Title: Pure/Thy/export_theory.ML Author: Makarius Export foundational theory content and locale/class structure. *) signature EXPORT_THEORY = sig val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit val export_body: theory -> string -> XML.body -> unit end; structure Export_Theory: EXPORT_THEORY = struct (* approximative syntax *) val get_syntax = Syntax.get_approx o Proof_Context.syn_of; fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type; fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const; fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed; fun get_syntax_param ctxt loc x = let val thy = Proof_Context.theory_of ctxt in if Class.is_class thy loc then (case AList.lookup (op =) (Class.these_params thy [loc]) x of NONE => NONE | SOME (_, (c, _)) => get_syntax_const ctxt c) else get_syntax_fixed ctxt x end; val encode_syntax = XML.Encode.variant [fn NONE => ([], []), fn SOME (Syntax.Prefix delim) => ([delim], []), fn SOME (Syntax.Infix {assoc, delim, pri}) => let val ass = (case assoc of Printer.No_Assoc => 0 | Printer.Left_Assoc => 1 | Printer.Right_Assoc => 2); open XML.Encode Term_XML.Encode; in ([], triple int string int (ass, delim, pri)) end]; (* free variables: not declared in the context *) val is_free = not oo Name.is_declared; fun add_frees used = fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I); fun add_tfrees used = (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I); (* spec rules *) fun primrec_types ctxt const = Spec_Rules.retrieve ctxt (Const const) |> get_first (fn (Spec_Rules.Equational (Spec_Rules.Primrec types), _) => SOME (types, false) | (Spec_Rules.Equational (Spec_Rules.Primcorec types), _) => SOME (types, true) | _ => NONE) |> the_default ([], false); (* locales content *) fun locale_content thy loc = let val ctxt = Locale.init loc thy; val args = Locale.params_of thy loc |> map (fn ((x, T), _) => ((x, T), get_syntax_param ctxt loc x)); val axioms = let val (asm, defs) = Locale.specification_of thy loc; val cprops = map (Thm.cterm_of ctxt) (the_list asm @ defs); val (intro1, intro2) = Locale.intros_of thy loc; val intros_tac = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2) []; val res = Goal.init (Conjunction.mk_conjunction_balanced cprops) |> (ALLGOALS Goal.conjunction_tac THEN intros_tac) |> try Seq.hd; in (case res of SOME goal => Thm.prems_of goal | NONE => raise Fail ("Cannot unfold locale " ^ quote loc)) end; val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []); in {typargs = typargs, args = args, axioms = axioms} end; fun get_locales thy = Locale.get_locales thy |> map_filter (fn loc => if Experiment.is_experiment thy loc then NONE else SOME (loc, ())); fun get_dependencies prev_thys thy = Locale.dest_dependencies prev_thys thy |> map_filter (fn dep => if Experiment.is_experiment thy (#source dep) orelse Experiment.is_experiment thy (#target dep) then NONE else let val (type_params, params) = Locale.parameters_of thy (#source dep); val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params; val substT = typargs |> map_filter (fn v => let val T = TFree v; val T' = Morphism.typ (#morphism dep) T; in if T = T' then NONE else SOME (v, T') end); val subst = params |> map_filter (fn (v, _) => let val t = Free v; val t' = Morphism.term (#morphism dep) t; in if t aconv t' then NONE else SOME (v, t') end); in SOME (dep, (substT, subst)) end); (* general setup *) fun setup_presentation f = Theory.setup (Thy_Info.add_presentation (fn context => fn thy => if Options.bool (#options context) "export_theory" then f context thy else ())); fun export_buffer thy name buffer = if Buffer.is_empty buffer then () else Export.export thy (Path.binding0 (Path.make ["theory", name])) (Buffer.chunks buffer); fun export_body thy name elems = export_buffer thy name (YXML.buffer_body elems Buffer.empty); (* presentation *) val _ = setup_presentation (fn {adjust_pos, ...} => fn thy => let val parents = Theory.parents_of thy; val rep_tsig = Type.rep_tsig (Sign.tsig_of thy); val thy_ctxt = Proof_Context.init_global thy; (* entities *) fun make_entity_markup name xname pos serial = let val props = Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos @ Markup.serial_properties serial; in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end; fun entity_markup space name = let val xname = Name_Space.extern_shortest thy_ctxt space name; val {serial, pos, ...} = Name_Space.the_entry space name; in make_entity_markup name xname pos serial end; fun export_entities export_name export get_space decls = let val parent_spaces = map get_space parents; val space = get_space thy; in (decls, []) |-> fold (fn (name, decl) => if exists (fn space => Name_Space.declared space name) parent_spaces then I else (case export name decl of NONE => I | SOME body => cons (#serial (Name_Space.the_entry space name), XML.Elem (entity_markup space name, body)))) |> sort (int_ord o apply2 #1) |> map #2 |> export_body thy export_name end; (* types *) val encode_type = let open XML.Encode Term_XML.Encode in triple encode_syntax (list string) (option typ) end; fun export_type c (Type.LogicalType n) = SOME (encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE)) | export_type c (Type.Abbreviation (args, U, false)) = SOME (encode_type (get_syntax_type thy_ctxt c, args, SOME U)) | export_type _ _ = NONE; val _ = export_entities "types" export_type Sign.type_space (Name_Space.dest_table (#types rep_tsig)); (* consts *) val consts = Sign.consts_of thy; val encode_term = Term_XML.Encode.term consts; val encode_const = let open XML.Encode Term_XML.Encode in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) (pair bool (pair (list string) bool))))) end; fun export_const c (T, abbrev) = let val syntax = get_syntax_const thy_ctxt c; val U = Logic.unvarifyT_global T; val U0 = Type.strip_sorts U; val recursion = primrec_types thy_ctxt (c, U); val abbrev' = abbrev |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts); val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0)); val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0); in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end; val _ = export_entities "consts" (SOME oo export_const) Sign.const_space (#constants (Consts.dest consts)); (* axioms *) fun standard_prop used extra_shyps raw_prop raw_proof = let val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof); val args = rev (add_frees used prop []); val typargs = rev (add_tfrees used prop []); val used_typargs = fold (Name.declare o #1) typargs used; val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps; in ((sorts @ typargs, args, prop), proof) end; val encode_prop = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair string typ)) encode_term end; fun encode_axiom used prop = encode_prop (#1 (standard_prop used [] prop NONE)); val _ = - export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t)) - Theory.axiom_space (Theory.axioms_of thy); + export_entities "axioms" (K (SOME o encode_axiom Name.context)) + Theory.axiom_space (Theory.all_axioms_of thy); (* theorems and proof terms *) val export_standard_proofs = Options.default_bool @{system_option export_standard_proofs}; val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; val lookup_thm_id = Global_Theory.lookup_thm_id thy; fun proof_boxes_of thm thm_id = let val dep_boxes = thm |> Thm_Deps.proof_boxes (fn thm_id' => if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id')); in dep_boxes @ [thm_id] end; fun expand_name thm_id (header: Proofterm.thm_header) = if #serial header = #serial thm_id then "" else (case lookup_thm_id (Proofterm.thm_header_id header) of NONE => "" | SOME thm_name => Thm_Name.print thm_name); fun entity_markup_thm (serial, (name, i)) = let val space = Facts.space_of (Global_Theory.facts_of thy); val xname = Name_Space.extern_shortest thy_ctxt space name; val {pos, ...} = Name_Space.the_entry space name; in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end; fun encode_thm thm_id raw_thm = let val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); val thm = clean_thm (Thm.unconstrainT raw_thm); val boxes = proof_boxes_of thm thm_id; val proof0 = if export_standard_proofs then Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof; val (prop, SOME proof) = standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0); val _ = Proofterm.commit_proof proof; in (prop, (deps, (boxes, proof))) |> let open XML.Encode Term_XML.Encode; fun encode_box {serial, theory_name} = pair int string (serial, theory_name); val encode_proof = Proofterm.encode_standard_proof consts; in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end end; fun buffer_export_thm (thm_id, thm_name) = let val markup = entity_markup_thm (#serial thm_id, thm_name); val thm = Global_Theory.get_thm_name thy (thm_name, Position.none); val body = encode_thm thm_id thm; in YXML.buffer (XML.Elem (markup, body)) end; val _ = Buffer.empty |> fold buffer_export_thm (Global_Theory.dest_thm_names thy) |> export_buffer thy "thms"; (* type classes *) val encode_class = let open XML.Encode Term_XML.Encode in pair (list (pair string typ)) (list (encode_axiom Name.context)) end; fun export_class name = (case try (Axclass.get_info thy) name of NONE => ([], []) | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms)) |> encode_class |> SOME; val _ = export_entities "classes" (fn name => fn () => export_class name) Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig))))); (* sort algebra *) local val prop = encode_axiom Name.context o Logic.varify_global; val encode_classrel = let open XML.Encode in list (pair prop (pair string string)) end; val encode_arities = let open XML.Encode Term_XML.Encode in list (pair prop (triple string (list sort) string)) end; in val export_classrel = maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel; val export_arities = map (`Logic.mk_arity) #> encode_arities; val {classrel, arities} = Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents) (#2 (#classes rep_tsig)); end; val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel); val _ = if null arities then () else export_body thy "arities" (export_arities arities); (* locales *) fun encode_locale used = let open XML.Encode Term_XML.Encode in triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax)) (list (encode_axiom used)) end; fun export_locale loc = let val {typargs, args, axioms} = locale_content thy loc; val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context; in encode_locale used (typargs, args, axioms) end handle ERROR msg => cat_error msg ("The error(s) above occurred in locale " ^ quote (Locale.markup_name thy_ctxt loc)); val _ = export_entities "locales" (fn loc => fn () => SOME (export_locale loc)) Locale.locale_space (get_locales thy); (* locale dependencies *) fun encode_locale_dependency (dep: Locale.locale_dependency, subst) = (#source dep, (#target dep, (#prefix dep, subst))) |> let open XML.Encode Term_XML.Encode; val encode_subst = pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts))); in pair string (pair string (pair (list (pair string bool)) encode_subst)) end; val _ = get_dependencies parents thy |> map_index (fn (i, dep) => let val xname = string_of_int (i + 1); val name = Long_Name.implode [Context.theory_name thy, xname]; val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep)); val body = encode_locale_dependency dep; in XML.Elem (markup, body) end) |> export_body thy "locale_dependencies"; (* constdefs *) val constdefs = Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy) |> sort_by #1; val encode_constdefs = let open XML.Encode in list (pair string string) end; val _ = if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs); (* parents *) val _ = Export.export thy \<^path_binding>\theory/parents\ [YXML.string_of_body (XML.Encode.string (cat_lines (map Context.theory_long_name parents)))]; in () end); end; diff --git a/src/Pure/theory.ML b/src/Pure/theory.ML --- a/src/Pure/theory.ML +++ b/src/Pure/theory.ML @@ -1,350 +1,347 @@ (* Title: Pure/theory.ML Author: Lawrence C Paulson and Markus Wenzel Logical theory content: axioms, definitions, and begin/end wrappers. *) signature THEORY = sig val parents_of: theory -> theory list val ancestors_of: theory -> theory list val nodes_of: theory -> theory list val setup: (theory -> theory) -> unit val local_setup: (Proof.context -> Proof.context) -> unit val install_pure: theory -> unit val get_pure: unit -> theory val get_pure_bootstrap: unit -> theory val get_markup: theory -> Markup.T val check: {long: bool} -> Proof.context -> string * Position.T -> theory val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T - val axioms_of: theory -> (string * term) list val all_axioms_of: theory -> (string * term) list val defs_of: theory -> Defs.T val at_begin: (theory -> theory option) -> theory -> theory val at_end: (theory -> theory option) -> theory -> theory val join_theory: theory list -> theory val begin_theory: string * Position.T -> theory list -> theory val end_theory: theory -> theory val add_axiom: Proof.context -> binding * term -> theory -> theory val const_dep: theory -> string * typ -> Defs.entry val type_dep: string * typ list -> Defs.entry val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory val specify_const: (binding * typ) * mixfix -> theory -> term * theory val check_overloading: Proof.context -> bool -> string * typ -> unit end structure Theory: THEORY = struct (** theory context operations **) val parents_of = Context.parents_of; val ancestors_of = Context.ancestors_of; fun nodes_of thy = thy :: ancestors_of thy; fun setup f = Context.>> (Context.map_theory f); fun local_setup f = Context.>> (Context.map_proof f); (* implicit theory Pure *) val pure: theory Single_Assignment.var = Single_Assignment.var "pure"; fun install_pure thy = Single_Assignment.assign pure thy; fun get_pure () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => raise Fail "Theory Pure not present"); fun get_pure_bootstrap () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => Context.the_global_context ()); (** datatype thy **) type wrapper = (theory -> theory option) * stamp; fun apply_wrappers (wrappers: wrapper list) = perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); datatype thy = Thy of {pos: Position.T, id: serial, axioms: term Name_Space.table, defs: Defs.T, wrappers: wrapper list * wrapper list}; fun make_thy (pos, id, axioms, defs, wrappers) = Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers}; structure Thy = Theory_Data' ( type T = thy; - val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table; - val empty = make_thy (Position.none, 0, empty_axioms, Defs.empty, ([], [])); + val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], [])); - fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) = - make_thy (Position.none, 0, empty_axioms, defs, wrappers); + fun extend (Thy {pos = _, id = _, axioms, defs, wrappers}) = + make_thy (Position.none, 0, axioms, defs, wrappers); fun merge old_thys (thy1, thy2) = let - val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1; - val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2; + val Thy {pos = _, id = _, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1; + val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2; - val axioms' = empty_axioms; + val axioms' = Name_Space.merge_tables (axioms1, axioms2); val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2); val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); val ens' = Library.merge (eq_snd op =) (ens1, ens2); in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end; ); fun rep_theory thy = Thy.get thy |> (fn Thy args => args); fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) => make_thy (f (pos, id, axioms, defs, wrappers))); fun map_axioms f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers)); fun map_defs f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers)); fun map_wrappers f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers)); (* entity markup *) fun theory_markup def name id pos = if id = 0 then Markup.empty else Markup.properties (Position.entity_properties_of def id pos) (Markup.entity Markup.theoryN name); fun init_markup (name, pos) thy = let val id = serial (); val _ = Position.report pos (theory_markup true name id pos); in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; fun get_markup thy = let val {pos, id, ...} = rep_theory thy in theory_markup false (Context.theory_name thy) id pos end; fun check long ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt; val thy' = Context.get_theory long thy name handle ERROR msg => let val completion_report = Completion.make_report (name, pos) (fn completed => map (Context.theory_name' long) (ancestors_of thy) |> filter (completed o Long_Name.base_name) |> sort_strings |> map (fn a => (a, (Markup.theoryN, a)))); in error (msg ^ Position.here pos ^ completion_report) end; val _ = Context_Position.report ctxt pos (get_markup thy'); in thy' end; (* basic operations *) val axiom_table = #axioms o rep_theory; val axiom_space = Name_Space.space_of_table o axiom_table; -val axioms_of = Name_Space.dest_table o axiom_table; -fun all_axioms_of thy = maps axioms_of (nodes_of thy); +val all_axioms_of = Name_Space.dest_table o axiom_table; val defs_of = #defs o rep_theory; (* join theory *) fun join_theory [] = raise List.Empty | join_theory [thy] = thy | join_theory thys = foldl1 Context.join_thys thys |> Sign.restore_naming (hd thys); (* begin/end theory *) val begin_wrappers = rev o #1 o #wrappers o rep_theory; val end_wrappers = rev o #2 o #wrappers o rep_theory; fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); fun begin_theory (name, pos) imports = if name = Context.PureN then (case imports of [thy] => init_markup (name, pos) thy | _ => error "Bad bootstrapping of theory Pure") else let val thy = Context.begin_thy name imports; val wrappers = begin_wrappers thy; in thy |> init_markup (name, pos) |> Sign.local_path |> Sign.map_naming (Name_Space.set_theory_name (Long_Name.base_name name)) |> apply_wrappers wrappers |> tap (Syntax.force_syntax o Sign.syn_of) end; fun end_theory thy = thy |> apply_wrappers (end_wrappers thy) |> Sign.change_check |> Context.finish_thy; (** primitive specifications **) (* raw axioms *) fun cert_axm ctxt (b, raw_tm) = let val thy = Proof_Context.theory_of ctxt; val t = Sign.cert_prop thy raw_tm handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg; val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg; val bad_sorts = rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []); val _ = null bad_sorts orelse error ("Illegal sort constraints in primitive specification: " ^ commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts)); in (b, Sign.no_vars ctxt t) end handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b); fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms => let val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm); val context = ctxt |> Sign.inherit_naming thy |> Context_Position.set_visible_generic false; val (_, axioms') = Name_Space.define context true axm axioms; in axioms' end); (* dependencies *) fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); fun type_dep (c, args) = ((Defs.Type, c), args); fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = let fun prep (item, args) = (case fold Term.add_tvarsT args [] of [] => (item, map Logic.varifyT_global args) | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, [])); val lhs_vars = fold Term.add_tfreesT (snd lhs) []; val rhs_extras = fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v => if member (op =) lhs_vars v then I else insert (op =) v)) rhs []; val _ = if null rhs_extras then () else error ("Specification depends on extra type variables: " ^ commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ "\nThe error(s) above occurred in " ^ quote description); in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; fun cert_entry thy ((Defs.Const, c), args) = Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) |> dest_Const |> const_dep thy | cert_entry thy ((Defs.Type, c), args) = Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep; fun add_deps context a raw_lhs raw_rhs thy = let val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); val description = if a = "" then lhs_name ^ " axiom" else a; in thy |> map_defs (dependencies context false NONE description lhs rhs) end; fun add_deps_global a x y thy = add_deps (Defs.global_context thy) a x y thy; fun specify_const decl thy = let val (t, thy') = Sign.declare_const_global decl thy; in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end; (* overloading *) fun check_overloading ctxt overloaded (c, T) = let val thy = Proof_Context.theory_of ctxt; val declT = Sign.the_const_constraint thy c handle TYPE (msg, _, _) => error msg; val T' = Logic.varifyT_global T; fun message sorts txt = [Pretty.block [Pretty.str "Specification of constant ", Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)], Pretty.str txt] |> Pretty.chunks |> Pretty.string_of; in if Sign.typ_instance thy (declT, T') then () else if Type.raw_instance (declT, T') then error (message true "imposes additional sort constraints on the constant declaration") else if overloaded then () else error (message false "is strictly less general than the declared type (overloading required)") end; (* definitional axioms *) local fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; val ((lhs, rhs), _, _) = Primitive_Defs.dest_def ctxt {check_head = Term.is_Const, check_free_lhs = K true, check_free_rhs = K false, check_tfree = K false} tm handle TERM (msg, _) => error msg; val lhs_const = Term.dest_Const (Term.head_of lhs); val rhs_consts = fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs []; val rhs_types = (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs []; val rhs_deps = rhs_consts @ rhs_types; val _ = check_overloading ctxt overloaded lhs_const; in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); in fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = let val axm = cert_axm ctxt raw_axm in thy |> map_defs (check_def context thy unchecked overloaded axm) |> add_axiom ctxt axm end; end; end; diff --git a/src/Pure/thm.ML b/src/Pure/thm.ML --- a/src/Pure/thm.ML +++ b/src/Pure/thm.ML @@ -1,2335 +1,2328 @@ (* Title: Pure/thm.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Makarius The very core of Isabelle's Meta Logic: certified types and terms, derivations, theorems, inference rules (including lifting and resolution), oracles. *) infix 0 RS RSN; signature BASIC_THM = sig type ctyp type cterm exception CTERM of string * cterm list type thm type conv = cterm -> thm exception THM of string * int * thm list val RSN: thm * (int * thm) -> thm val RS: thm * thm -> thm end; signature THM = sig include BASIC_THM (*certified types*) val typ_of: ctyp -> typ val global_ctyp_of: theory -> typ -> ctyp val ctyp_of: Proof.context -> typ -> ctyp val dest_ctyp: ctyp -> ctyp list val dest_ctypN: int -> ctyp -> ctyp val dest_ctyp0: ctyp -> ctyp val dest_ctyp1: ctyp -> ctyp val make_ctyp: ctyp -> ctyp list -> ctyp (*certified terms*) val term_of: cterm -> term val typ_of_cterm: cterm -> typ val ctyp_of_cterm: cterm -> ctyp val maxidx_of_cterm: cterm -> int val global_cterm_of: theory -> term -> cterm val cterm_of: Proof.context -> term -> cterm val renamed_term: term -> cterm -> cterm val dest_comb: cterm -> cterm * cterm val dest_fun: cterm -> cterm val dest_arg: cterm -> cterm val dest_fun2: cterm -> cterm val dest_arg1: cterm -> cterm val dest_abs: string option -> cterm -> cterm * cterm val rename_tvar: indexname -> ctyp -> ctyp val var: indexname * ctyp -> cterm val apply: cterm -> cterm -> cterm val lambda_name: string * cterm -> cterm -> cterm val lambda: cterm -> cterm -> cterm val adjust_maxidx_cterm: int -> cterm -> cterm val incr_indexes_cterm: int -> cterm -> cterm val match: cterm * cterm -> ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val first_order_match: cterm * cterm -> ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list (*theorems*) val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a val terms_of_tpairs: (term * term) list -> term list val full_prop_of: thm -> term val theory_id: thm -> Context.theory_id val theory_name: thm -> string val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int val shyps_of: thm -> sort Ord_List.T val hyps_of: thm -> term list val prop_of: thm -> term val tpairs_of: thm -> (term * term) list val concl_of: thm -> term val prems_of: thm -> term list val nprems_of: thm -> int val no_prems: thm -> bool val major_prem_of: thm -> term val cprop_of: thm -> cterm val cprem_of: thm -> int -> cterm val cconcl_of: thm -> cterm val cprems_of: thm -> cterm list val chyps_of: thm -> cterm list exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option val theory_of_cterm: cterm -> theory val theory_of_thm: thm -> theory val trim_context_ctyp: ctyp -> ctyp val trim_context_cterm: cterm -> cterm val transfer_ctyp: theory -> ctyp -> ctyp val transfer_cterm: theory -> cterm -> cterm val transfer: theory -> thm -> thm val transfer': Proof.context -> thm -> thm val transfer'': Context.generic -> thm -> thm val join_transfer: theory -> thm -> thm val join_transfer_context: Proof.context * thm -> Proof.context * thm val renamed_prop: term -> thm -> thm val weaken: cterm -> thm -> thm val weaken_sorts: sort list -> cterm -> cterm val extra_shyps: thm -> sort list val proof_bodies_of: thm list -> proof_body list val proof_body_of: thm -> proof_body val proof_of: thm -> proof val consolidate: thm list -> unit val future: thm future -> cterm -> thm val thm_deps: thm -> Proofterm.thm Ord_List.T val derivation_closed: thm -> bool val derivation_name: thm -> string val derivation_id: thm -> Proofterm.thm_id option val raw_derivation_name: thm -> string val expand_name: thm -> Proofterm.thm_header -> string option val name_derivation: string * Position.T -> thm -> thm val close_derivation: Position.T -> thm -> thm val trim_context: thm -> thm val axiom: theory -> string -> thm - val axioms_of: theory -> (string * thm) list + val all_axioms_of: theory -> (string * thm) list val get_tags: thm -> Properties.T val map_tags: (Properties.T -> Properties.T) -> thm -> thm val norm_proof: thm -> thm val adjust_maxidx_thm: int -> thm -> thm (*type classes*) val the_classrel: theory -> class * class -> thm val the_arity: theory -> string * sort list * class -> thm val classrel_proof: theory -> class * class -> proof val arity_proof: theory -> string * sort list * class -> proof (*oracles*) val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory val oracle_space: theory -> Name_Space.T val pretty_oracle: Proof.context -> string -> Pretty.T val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list val check_oracle: Proof.context -> xstring * Position.T -> string (*inference rules*) val assume: cterm -> thm val implies_intr: cterm -> thm -> thm val implies_elim: thm -> thm -> thm val forall_intr: cterm -> thm -> thm val forall_elim: cterm -> thm -> thm val reflexive: cterm -> thm val symmetric: thm -> thm val transitive: thm -> thm -> thm val beta_conversion: bool -> conv val eta_conversion: conv val eta_long_conversion: conv val abstract_rule: string -> cterm -> thm -> thm val combination: thm -> thm -> thm val equal_intr: thm -> thm -> thm val equal_elim: thm -> thm -> thm val solve_constraints: thm -> thm val flexflex_rule: Proof.context option -> thm -> thm Seq.seq val generalize: string list * string list -> int -> thm -> thm val generalize_cterm: string list * string list -> int -> cterm -> cterm val generalize_ctyp: string list -> int -> ctyp -> ctyp val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> cterm -> cterm val trivial: cterm -> thm val of_class: ctyp * class -> thm val strip_shyps: thm -> thm val unconstrainT: thm -> thm val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm val varifyT_global: thm -> thm val legacy_freezeT: thm -> thm val plain_prop_of: thm -> term val dest_state: thm * int -> (term * term) list * term list * term * term val lift_rule: cterm -> thm -> thm val incr_indexes: int -> thm -> thm val assumption: Proof.context option -> int -> thm -> thm Seq.seq val eq_assumption: int -> thm -> thm val rotate_rule: int -> int -> thm -> thm val permute_prems: int -> int -> thm -> thm val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} -> bool * thm * int -> int -> thm -> thm Seq.seq val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq val thynames_of_arity: theory -> string * class -> string list val add_classrel: thm -> theory -> theory val add_arity: thm -> theory -> theory end; structure Thm: THM = struct (*** Certified terms and types ***) (** certified types **) datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T}; fun typ_of (Ctyp {T, ...}) = T; fun global_ctyp_of thy raw_T = let val T = Sign.certify_typ thy raw_T; val maxidx = Term.maxidx_of_typ T; val sorts = Sorts.insert_typ T []; in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end; val ctyp_of = global_ctyp_of o Proof_Context.theory_of; fun dest_ctyp (Ctyp {cert, T = Type (_, Ts), maxidx, sorts}) = map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); fun dest_ctypN n (Ctyp {cert, T, maxidx, sorts}) = let fun err () = raise TYPE ("dest_ctypN", [T], []) in (case T of Type (_, Ts) => Ctyp {cert = cert, T = nth Ts n handle General.Subscript => err (), maxidx = maxidx, sorts = sorts} | _ => err ()) end; val dest_ctyp0 = dest_ctypN 0; val dest_ctyp1 = dest_ctypN 1; fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert); fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts; fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx); fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs = let val As = map typ_of cargs; fun err () = raise TYPE ("make_ctyp", T :: As, []); in (case T of Type (a, args) => Ctyp { cert = fold join_certificate_ctyp cargs cert, maxidx = fold maxidx_ctyp cargs ~1, sorts = fold union_sorts_ctyp cargs [], T = if length args = length cargs then Type (a, As) else err ()} | _ => err ()) end; (** certified terms **) (*certified terms with checked typ, maxidx, and sorts*) datatype cterm = Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T}; exception CTERM of string * cterm list; fun term_of (Cterm {t, ...}) = t; fun typ_of_cterm (Cterm {T, ...}) = T; fun ctyp_of_cterm (Cterm {cert, T, maxidx, sorts, ...}) = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}; fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx; fun global_cterm_of thy tm = let val (t, T, maxidx) = Sign.certify_term thy tm; val sorts = Sorts.insert_term t []; in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; val cterm_of = global_cterm_of o Proof_Context.theory_of; fun join_certificate0 (Cterm {cert = cert1, ...}, Cterm {cert = cert2, ...}) = Context.join_certificate (cert1, cert2); fun renamed_term t' (Cterm {cert, t, T, maxidx, sorts}) = if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts} else raise TERM ("renamed_term: terms disagree", [t, t']); (* destructors *) fun dest_comb (Cterm {t = c $ a, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in (Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts}, Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts}) end | dest_comb ct = raise CTERM ("dest_comb", [ct]); fun dest_fun (Cterm {t = c $ _, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_fun ct = raise CTERM ("dest_fun", [ct]); fun dest_arg (Cterm {t = c $ a, T = _, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_arg ct = raise CTERM ("dest_arg", [ct]); fun dest_fun2 (Cterm {t = c $ _ $ _, T, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0; val B = Term.argument_type_of c 1; in Cterm {t = c, T = A --> B --> T, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]); fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) = let val (y', t') = Term.dest_abs (the_default x a, T, t) in (Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts}, Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts}) end | dest_abs _ ct = raise CTERM ("dest_abs", [ct]); (* constructors *) fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) = let val S = (case T of TFree (_, S) => S | TVar (_, S) => S | _ => raise TYPE ("rename_tvar: no variable", [T], [])); val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else (); in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end; fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) = if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)]) else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts}; fun apply (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...}) (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) = if T = dty then Cterm {cert = join_certificate0 (cf, cx), t = f $ x, T = rty, maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} else raise CTERM ("apply: types don't agree", [cf, cx]) | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]); fun lambda_name (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...}) (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) = let val t = Term.lambda_name (x, t1) t2 in Cterm {cert = join_certificate0 (ct1, ct2), t = t, T = T1 --> T2, maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} end; fun lambda t u = lambda_name ("", t) u; (* indexes *) fun adjust_maxidx_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = if maxidx = i then ct else if maxidx < i then Cterm {maxidx = i, cert = cert, t = t, T = T, sorts = sorts} else Cterm {maxidx = Int.max (maxidx_of_term t, i), cert = cert, t = t, T = T, sorts = sorts}; fun incr_indexes_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = if i < 0 then raise CTERM ("negative increment", [ct]) else if i = 0 then ct else Cterm {cert = cert, t = Logic.incr_indexes ([], [], i) t, T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; (*** Derivations and Theorems ***) (* sort constraints *) type constraint = {theory: theory, typ: typ, sort: sort}; local val constraint_ord : constraint ord = Context.theory_id_ord o apply2 (Context.theory_id o #theory) <<< Term_Ord.typ_ord o apply2 #typ <<< Term_Ord.sort_ord o apply2 #sort; val smash_atyps = map_atyps (fn TVar (_, S) => Term.aT S | TFree (_, S) => Term.aT S | T => T); in val union_constraints = Ord_List.union constraint_ord; fun insert_constraints thy (T, S) = let val ignored = S = [] orelse (case T of TFree (_, S') => S = S' | TVar (_, S') => S = S' | _ => false); in if ignored then I else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S} end; fun insert_constraints_env thy env = let val tyenv = Envir.type_env env; fun insert ([], _) = I | insert (S, T) = insert_constraints thy (Envir.norm_type tyenv T, S); in tyenv |> Vartab.fold (insert o #2) end; end; (* datatype thm *) datatype thm = Thm of deriv * (*derivation*) {cert: Context.certificate, (*background theory certificate*) tags: Properties.T, (*additional annotations/comments*) maxidx: int, (*maximum index of any Var or TVar*) constraints: constraint Ord_List.T, (*implicit proof obligations for sort constraints*) shyps: sort Ord_List.T, (*sort hypotheses*) hyps: term Ord_List.T, (*hypotheses*) tpairs: (term * term) list, (*flex-flex pairs*) prop: term} (*conclusion*) and deriv = Deriv of {promises: (serial * thm future) Ord_List.T, body: Proofterm.proof_body}; type conv = cterm -> thm; (*errors involving theorems*) exception THM of string * int * thm list; fun rep_thm (Thm (_, args)) = args; fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) = fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps; fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end; fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) = let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in (fold_terms o fold_aterms) (fn t as Const (_, T) => f (cterm t T) | t as Free (_, T) => f (cterm t T) | t as Var (_, T) => f (cterm t T) | _ => I) th end; fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs []; fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u'; fun union_tpairs ts us = Library.merge eq_tpairs (ts, us); val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u); fun attach_tpairs tpairs prop = Logic.list_implies (map Logic.mk_equals tpairs, prop); fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop; val union_hyps = Ord_List.union Term_Ord.fast_term_ord; val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord; val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord; fun join_certificate1 (Cterm {cert = cert1, ...}, Thm (_, {cert = cert2, ...})) = Context.join_certificate (cert1, cert2); fun join_certificate2 (Thm (_, {cert = cert1, ...}), Thm (_, {cert = cert2, ...})) = Context.join_certificate (cert1, cert2); (* basic components *) val cert_of = #cert o rep_thm; val theory_id = Context.certificate_theory_id o cert_of; val theory_name = Context.theory_id_name o theory_id; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); val shyps_of = #shyps o rep_thm; val hyps_of = #hyps o rep_thm; val prop_of = #prop o rep_thm; val tpairs_of = #tpairs o rep_thm; val concl_of = Logic.strip_imp_concl o prop_of; val prems_of = Logic.strip_imp_prems o prop_of; val nprems_of = Logic.count_prems o prop_of; fun no_prems th = nprems_of th = 0; fun major_prem_of th = (case prems_of th of prem :: _ => Logic.strip_assums_concl prem | [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); fun cprop_of (Thm (_, {cert, maxidx, shyps, prop, ...})) = Cterm {cert = cert, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; fun cprem_of (th as Thm (_, {cert, maxidx, shyps, prop, ...})) i = Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])}; fun cconcl_of (th as Thm (_, {cert, maxidx, shyps, ...})) = Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = concl_of th}; fun cprems_of (th as Thm (_, {cert, maxidx, shyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t}) (prems_of th); fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) = map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps; (* implicit theory context *) exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option; fun theory_of_cterm (ct as Cterm {cert, ...}) = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); fun theory_of_thm th = Context.certificate_theory (cert_of th) handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE); fun trim_context_ctyp cT = (case cT of Ctyp {cert = Context.Certificate_Id _, ...} => cT | Ctyp {cert = Context.Certificate thy, T, maxidx, sorts} => Ctyp {cert = Context.Certificate_Id (Context.theory_id thy), T = T, maxidx = maxidx, sorts = sorts}); fun trim_context_cterm ct = (case ct of Cterm {cert = Context.Certificate_Id _, ...} => ct | Cterm {cert = Context.Certificate thy, t, T, maxidx, sorts} => Cterm {cert = Context.Certificate_Id (Context.theory_id thy), t = t, T = T, maxidx = maxidx, sorts = sorts}); fun trim_context_thm th = (case th of Thm (_, {constraints = _ :: _, ...}) => raise THM ("trim_context: pending sort constraints", 0, [th]) | Thm (_, {cert = Context.Certificate_Id _, ...}) => th | Thm (der, {cert = Context.Certificate thy, tags, maxidx, constraints = [], shyps, hyps, tpairs, prop}) => Thm (der, {cert = Context.Certificate_Id (Context.theory_id thy), tags = tags, maxidx = maxidx, constraints = [], shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})); fun transfer_ctyp thy' cT = let val Ctyp {cert, T, maxidx, sorts} = cT; val _ = Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [cT], [], [], SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then cT else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts} end; fun transfer_cterm thy' ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; val _ = Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [], [ct], [], SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then ct else Cterm {cert = cert', t = t, T = T, maxidx = maxidx, sorts = sorts} end; fun transfer thy' th = let val Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) = th; val _ = Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse raise CONTEXT ("Cannot transfer: not a super theory", [], [], [th], SOME (Context.Theory thy')); val cert' = Context.join_certificate (Context.Certificate thy', cert); in if Context.eq_certificate (cert, cert') then th else Thm (der, {cert = cert', tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) end; val transfer' = transfer o Proof_Context.theory_of; val transfer'' = transfer o Context.theory_of; fun join_transfer thy th = if Context.subthy_id (Context.theory_id thy, theory_id th) then th else transfer thy th; fun join_transfer_context (ctxt, th) = if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then (Context.raw_transfer (theory_of_thm th) ctxt, th) else (ctxt, transfer' ctxt th); (* matching *) local fun gen_match match (ct1 as Cterm {t = t1, sorts = sorts1, ...}, ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = let val cert = join_certificate0 (ct1, ct2); val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE); val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) = (((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts}); fun mk_ctinst ((x, i), (U, t)) = let val T = Envir.subst_type Tinsts U in (((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts}) end; in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; in val match = gen_match Pattern.match; val first_order_match = gen_match Pattern.first_order_match; end; (*implicit alpha-conversion*) fun renamed_prop prop' (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = if prop aconv prop' then Thm (der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop'}) else raise TERM ("renamed_prop: props disagree", [prop, prop']); fun make_context ths NONE cert = (Context.Theory (Context.certificate_theory cert) handle ERROR msg => raise CONTEXT (msg, [], [], ths, NONE)) | make_context ths (SOME ctxt) cert = let val thy_id = Context.certificate_theory_id cert; val thy_id' = Context.theory_id (Proof_Context.theory_of ctxt); in if Context.subthy_id (thy_id, thy_id') then Context.Proof ctxt else raise CONTEXT ("Bad context", [], [], ths, SOME (Context.Proof ctxt)) end; fun make_context_certificate ths opt_ctxt cert = let val context = make_context ths opt_ctxt cert; val cert' = Context.Certificate (Context.theory_of context); in (context, cert') end; (*explicit weakening: maps |- B to A |- B*) fun weaken raw_ct th = let val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct; val Thm (der, {tags, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; in if T <> propT then raise THM ("weaken: assumptions must have type prop", 0, []) else if maxidxA <> ~1 then raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, []) else Thm (der, {cert = join_certificate1 (ct, th), tags = tags, maxidx = maxidx, constraints = constraints, shyps = Sorts.union sorts shyps, hyps = insert_hyps A hyps, tpairs = tpairs, prop = prop}) end; fun weaken_sorts raw_sorts ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; val thy = theory_of_cterm ct; val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); val sorts' = Sorts.union sorts more_sorts; in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; (*dangling sort constraints of a thm*) fun extra_shyps (th as Thm (_, {shyps, ...})) = Sorts.subtract (fold_terms Sorts.insert_term th []) shyps; (** derivations and promised proofs **) fun make_deriv promises oracles thms proof = Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}}; val empty_deriv = make_deriv [] [] [] MinProof; (* inference rules *) val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i); fun bad_proofs i = error ("Illegal level of detail for proof objects: " ^ string_of_int i); fun deriv_rule2 f (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}}) (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) = let val ps = Ord_List.union promise_ord ps1 ps2; val oracles = Proofterm.unions_oracles [oracles1, oracles2]; val thms = Proofterm.unions_thms [thms1, thms2]; val prf = (case ! Proofterm.proofs of 2 => f prf1 prf2 | 1 => MinProof | 0 => MinProof | i => bad_proofs i); in make_deriv ps oracles thms prf end; fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv; fun deriv_rule0 make_prf = if ! Proofterm.proofs <= 1 then empty_deriv else deriv_rule1 I (make_deriv [] [] [] (make_prf ())); fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) = make_deriv promises oracles thms (f proof); (* fulfilled proofs *) fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises; fun join_promises [] = () | join_promises promises = join_promises_of (Future.joins (map snd promises)) and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms)); fun fulfill_body (th as Thm (Deriv {promises, body}, _)) = let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises)) in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end; fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms); val proof_body_of = singleton proof_bodies_of; val proof_of = Proofterm.proof_of o proof_body_of; val consolidate = ignore o proof_bodies_of; (* future rule *) fun future_result i orig_cert orig_shyps orig_prop thm = let fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]); val Thm (Deriv {promises, ...}, {cert, constraints, shyps, hyps, tpairs, prop, ...}) = thm; val _ = Context.eq_certificate (cert, orig_cert) orelse err "bad theory"; val _ = prop aconv orig_prop orelse err "bad prop"; val _ = null constraints orelse err "bad sort constraints"; val _ = null tpairs orelse err "bad flex-flex constraints"; val _ = null hyps orelse err "bad hyps"; val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps"; val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies"; val _ = join_promises promises; in thm end; fun future future_thm ct = let val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct; val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); val _ = if Proofterm.proofs_enabled () then raise CTERM ("future: proof terms enabled", [ct]) else (); val i = serial (); val future = future_thm |> Future.map (future_result i cert sorts prop); in Thm (make_deriv [(i, future)] [] [] MinProof, {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = prop}) end; (** Axioms **) -fun axiom thy0 name = - let - fun get_ax thy = - Name_Space.lookup (Theory.axiom_table thy) name - |> Option.map (fn prop => - let - val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop); - val cert = Context.Certificate thy; - val maxidx = maxidx_of_term prop; - val shyps = Sorts.insert_term prop []; - in - Thm (der, - {cert = cert, tags = [], maxidx = maxidx, - constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop}) - end); - in - (case get_first get_ax (Theory.nodes_of thy0) of - SOME thm => thm - | NONE => raise THEORY ("No axiom " ^ quote name, [thy0])) - end; +fun axiom thy name = + (case Name_Space.lookup (Theory.axiom_table thy) name of + SOME prop => + let + val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop); + val cert = Context.Certificate thy; + val maxidx = maxidx_of_term prop; + val shyps = Sorts.insert_term prop []; + in + Thm (der, + {cert = cert, tags = [], maxidx = maxidx, + constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop}) + end + | NONE => raise THEORY ("No axiom " ^ quote name, [thy])); -(*return additional axioms of this theory node*) -fun axioms_of thy = - map (fn (name, _) => (name, axiom thy name)) (Theory.axioms_of thy); +fun all_axioms_of thy = + map (fn (name, _) => (name, axiom thy name)) (Theory.all_axioms_of thy); (* tags *) val get_tags = #tags o rep_thm; fun map_tags f (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = Thm (der, {cert = cert, tags = f tags, maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); (* technical adjustments *) fun norm_proof (th as Thm (der, args)) = Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th)) der, args); fun adjust_maxidx_thm i (th as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = if maxidx = i then th else if maxidx < i then Thm (der, {maxidx = i, cert = cert, tags = tags, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) else Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), cert = cert, tags = tags, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); (*** Theory data ***) (* type classes *) structure Aritytab = Table( type key = string * sort list * class; val ord = fast_string_ord o apply2 #1 <<< fast_string_ord o apply2 #3 <<< list_ord Term_Ord.sort_ord o apply2 #2; ); datatype classes = Classes of {classrels: thm Symreltab.table, arities: (thm * string * serial) Aritytab.table}; fun make_classes (classrels, arities) = Classes {classrels = classrels, arities = arities}; val empty_classes = make_classes (Symreltab.empty, Aritytab.empty); (*see Theory.at_begin hook for transitive closure of classrels and arity completion*) fun merge_classes (Classes {classrels = classrels1, arities = arities1}, Classes {classrels = classrels2, arities = arities2}) = let val classrels' = Symreltab.merge (K true) (classrels1, classrels2); val arities' = Aritytab.merge (K true) (arities1, arities2); in make_classes (classrels', arities') end; (* data *) structure Data = Theory_Data ( type T = unit Name_Space.table * (*oracles: authentic derivation names*) classes; (*type classes within the logic*) val empty : T = (Name_Space.empty_table "oracle", empty_classes); val extend = I; fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T = (Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2)); ); val get_oracles = #1 o Data.get; val map_oracles = Data.map o apfst; val get_classes = (fn (_, Classes args) => args) o Data.get; val get_classrels = #classrels o get_classes; val get_arities = #arities o get_classes; fun map_classes f = (Data.map o apsnd) (fn Classes {classrels, arities} => make_classes (f (classrels, arities))); fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities)); fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities)); (* type classes *) fun the_classrel thy (c1, c2) = (case Symreltab.lookup (get_classrels thy) (c1, c2) of SOME thm => transfer thy thm | NONE => error ("Unproven class relation " ^ Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2])); fun the_arity thy (a, Ss, c) = (case Aritytab.lookup (get_arities thy) (a, Ss, c) of SOME (thm, _, _) => transfer thy thm | NONE => error ("Unproven type arity " ^ Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c]))); val classrel_proof = proof_of oo the_classrel; val arity_proof = proof_of oo the_arity; (* solve sort constraints by pro-forma proof *) local fun union_digest (oracles1, thms1) (oracles2, thms2) = (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]); fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) = (oracles, thms); fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) = Sorts.of_sort_derivation (Sign.classes_of thy) {class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 => if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))), type_constructor = fn (a, _) => fn dom => fn c => let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c)) in (fold o fold) (union_digest o #1) dom arity_digest end, type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)} (typ, sort); in fun solve_constraints (thm as Thm (_, {constraints = [], ...})) = thm | solve_constraints (thm as Thm (der, args)) = let val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args; val thy = Context.certificate_theory cert; val bad_thys = constraints |> map_filter (fn {theory = thy', ...} => if Context.eq_thy (thy, thy') then NONE else SOME thy'); val () = if null bad_thys then () else raise THEORY ("solve_constraints: bad theories for theorem\n" ^ Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys); val Deriv {promises, body = PBody {oracles, thms, proof}} = der; val (oracles', thms') = (oracles, thms) |> fold (fold union_digest o constraint_digest) constraints; val body' = PBody {oracles = oracles', thms = thms', proof = proof}; in Thm (Deriv {promises = promises, body = body'}, {constraints = [], cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) end; end; (*** Closed theorems with official name ***) (*non-deterministic, depends on unknown promises*) fun derivation_closed (Thm (Deriv {body, ...}, _)) = Proofterm.compact_proof (Proofterm.proof_of body); (*non-deterministic, depends on unknown promises*) fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = Proofterm.get_approximative_name shyps hyps prop (Proofterm.proof_of body); fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = let val self_id = (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of NONE => K false | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header); fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE; in expand end; (*deterministic name of finished proof*) fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) = Proofterm.get_approximative_name shyps hyps prop (proof_of thm); (*identified PThm node*) fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) = Proofterm.get_id shyps hyps prop (proof_of thm); (*dependencies of PThm node*) fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) = (case (derivation_id thm, thms) of (SOME {serial = i, ...}, [(j, thm_node)]) => if i = j then Proofterm.thm_node_thms thm_node else thms | _ => thms) | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]); fun name_derivation name_pos = solve_constraints #> (fn thm as Thm (der, args) => let val thy = theory_of_thm thm; val Deriv {promises, body} = der; val {shyps, hyps, prop, tpairs, ...} = args; val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]); val ps = map (apsnd (Future.map fulfill_body)) promises; val (pthm, proof) = Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) name_pos shyps hyps prop ps body; val der' = make_deriv [] [] [pthm] proof; in Thm (der', args) end); fun close_derivation pos = solve_constraints #> (fn thm => if not (null (tpairs_of thm)) orelse derivation_closed thm then thm else name_derivation ("", pos) thm); val trim_context = solve_constraints #> trim_context_thm; (*** Oracles ***) fun add_oracle (b, oracle_fn) thy = let val (name, oracles') = Name_Space.define (Context.Theory thy) true (b, ()) (get_oracles thy); val thy' = map_oracles (K oracles') thy; fun invoke_oracle arg = let val Cterm {cert = cert2, t = prop, T, maxidx, sorts} = oracle_fn arg in if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else let val (oracle, prf) = (case ! Proofterm.proofs of 2 => ((name, SOME prop), Proofterm.oracle_proof name prop) | 1 => ((name, SOME prop), MinProof) | 0 => ((name, NONE), MinProof) | i => bad_proofs i); in Thm (make_deriv [] [oracle] [] prf, {cert = Context.join_certificate (Context.Certificate thy', cert2), tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = prop}) end end; in ((name, invoke_oracle), thy') end; val oracle_space = Name_Space.space_of_table o get_oracles; fun pretty_oracle ctxt = Name_Space.pretty ctxt (oracle_space (Proof_Context.theory_of ctxt)); fun extern_oracles verbose ctxt = map #1 (Name_Space.markup_table verbose ctxt (get_oracles (Proof_Context.theory_of ctxt))); fun check_oracle ctxt = Name_Space.check (Context.Proof ctxt) (get_oracles (Proof_Context.theory_of ctxt)) #> #1; (*** Meta rules ***) (** primitive rules **) (*The assumption rule A |- A*) fun assume raw_ct = let val Cterm {cert, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in if T <> propT then raise THM ("assume: prop", 0, []) else if maxidx <> ~1 then raise THM ("assume: variables", maxidx, []) else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop), {cert = cert, tags = [], maxidx = ~1, constraints = [], shyps = sorts, hyps = [prop], tpairs = [], prop = prop}) end; (*Implication introduction [A] : B ------- A \ B *) fun implies_intr (ct as Cterm {t = A, T, maxidx = maxidx1, sorts, ...}) (th as Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...})) = if T <> propT then raise THM ("implies_intr: assumptions must have type prop", 0, [th]) else Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der, {cert = join_certificate1 (ct, th), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sorts.union sorts shyps, hyps = remove_hyps A hyps, tpairs = tpairs, prop = Logic.mk_implies (A, prop)}); (*Implication elimination A \ B A ------------ B *) fun implies_elim thAB thA = let val Thm (derA, {maxidx = maxidx1, hyps = hypsA, constraints = constraintsA, shyps = shypsA, tpairs = tpairsA, prop = propA, ...}) = thA and Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...}) = thAB; fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]); in (case prop of Const ("Pure.imp", _) $ A $ B => if A aconv propA then Thm (deriv_rule2 (curry Proofterm.%%) der derA, {cert = join_certificate2 (thAB, thA), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraintsA constraints, shyps = Sorts.union shypsA shyps, hyps = union_hyps hypsA hyps, tpairs = union_tpairs tpairsA tpairs, prop = B}) else err () | _ => err ()) end; (*Forall introduction. The Free or Var x must not be free in the hypotheses. [x] : A ------ \x. A *) fun forall_intr (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...}) (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) = let fun result a = Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE) der, {cert = join_certificate1 (ct, th), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))}); fun check_occs a x ts = if exists (fn t => Logic.occs (x, t)) ts then raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a) | _ => raise THM ("forall_intr: not a variable", 0, [th])) end; (*Forall elimination \x. A ------ A[t/x] *) fun forall_elim (ct as Cterm {t, T, maxidx = maxidx1, sorts, ...}) (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) = (case prop of Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => if T <> qary then raise THM ("forall_elim: type mismatch", 0, [th]) else Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der, {cert = join_certificate1 (ct, th), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Term.betapply (A, t)}) | _ => raise THM ("forall_elim: not quantified", 0, [th])); (* Equality *) (*Reflexivity t \ t *) fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, t)}); (*Symmetry t \ u ------ u \ t *) fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = (case prop of (eq as Const ("Pure.eq", _)) $ t $ u => Thm (deriv_rule1 Proofterm.symmetric_proof der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = eq $ u $ t}) | _ => raise THM ("symmetric", 0, [th])); (*Transitivity t1 \ u u \ t2 ------------------ t1 \ t2 *) fun transitive th1 th2 = let val Thm (der1, {maxidx = maxidx1, hyps = hyps1, constraints = constraints1, shyps = shyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, hyps = hyps2, constraints = constraints2, shyps = shyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]); in case (prop1, prop2) of ((eq as Const ("Pure.eq", Type (_, [U, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) => if not (u aconv u') then err "middle term" else Thm (deriv_rule2 (Proofterm.transitive_proof U u) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = eq $ t1 $ t2}) | _ => err "premises" end; (*Beta-conversion (\x. t) u \ t[u/x] fully beta-reduces the term if full = true *) fun beta_conversion full (Cterm {cert, t, T = _, maxidx, sorts}) = let val t' = if full then Envir.beta_norm t else (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt) | _ => raise THM ("beta_conversion: not a redex", 0, [])); in Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, t')}) end; fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, Envir.eta_contract t)}); fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_equals (t, Envir.eta_long [] t)}); (*The abstraction rule. The Free or Var x must not be free in the hypotheses. The bound variable will be named "a" (since x will be something like x320) t \ u -------------- \x. t \ \x. u *) fun abstract_rule a (Cterm {t = x, T, sorts, ...}) (th as Thm (der, {cert, maxidx, hyps, constraints, shyps, tpairs, prop, ...})) = let val (t, u) = Logic.dest_equals prop handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); val result = Thm (deriv_rule1 (Proofterm.abstract_rule_proof (a, x)) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Logic.mk_equals (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))}); fun check_occs a x ts = if exists (fn t => Logic.occs (x, t)) ts then raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result) | _ => raise THM ("abstract_rule: not a variable", 0, [th])) end; (*The combination rule f \ g t \ u ------------- f t \ g u *) fun combination th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun chktypes fT tT = (case fT of Type ("fun", [T1, _]) => if T1 <> tT then raise THM ("combination: types", 0, [th1, th2]) else () | _ => raise THM ("combination: not function type", 0, [th1, th2])); in (case (prop1, prop2) of (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g, Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) => (chktypes fT tT; Thm (deriv_rule2 (Proofterm.combination_proof f g t u) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (f $ t, g $ u)})) | _ => raise THM ("combination: premises", 0, [th1, th2])) end; (*Equality introduction A \ B B \ A ---------------- A \ B *) fun equal_intr th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); in (case (prop1, prop2) of (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') => if A aconv A' andalso B aconv B' then Thm (deriv_rule2 (Proofterm.equal_intr_proof A B) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (A, B)}) else err "not equal" | _ => err "premises") end; (*The equal propositions rule A \ B A --------- B *) fun equal_elim th1 th2 = let val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1 and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); in (case prop1 of Const ("Pure.eq", _) $ A $ B => if prop2 aconv A then Thm (deriv_rule2 (Proofterm.equal_elim_proof A B) der1 der2, {cert = join_certificate2 (th1, th2), tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = B}) else err "not equal" | _ => err "major premise") end; (**** Derived rules ****) (*Smash unifies the list of term pairs leaving no flex-flex pairs. Instantiates the theorem and deletes trivial tpairs. Resulting sequence may contain multiple elements if the tpairs are not all flex-flex.*) fun flexflex_rule opt_ctxt = solve_constraints #> (fn th => let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; val (context, cert') = make_context_certificate [th] opt_ctxt cert; in Unify.smash_unifiers context tpairs (Envir.empty maxidx) |> Seq.map (fn env => if Envir.is_empty env then th else let val tpairs' = tpairs |> map (apply2 (Envir.norm_term env)) (*remove trivial tpairs, of the form t \ t*) |> filter_out (op aconv); val der' = deriv_rule1 (Proofterm.norm_proof' env) der; val constraints' = insert_constraints_env (Context.certificate_theory cert') env constraints; val prop' = Envir.norm_term env prop; val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); val shyps = Envir.insert_sorts env shyps; in Thm (der', {cert = cert', tags = [], maxidx = maxidx, constraints = constraints', shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) end) end); (*Generalization of fixed variables A -------------------- A[?'a/'a, ?x/x, ...] *) fun generalize ([], []) _ th = th | generalize (tfrees, frees) idx th = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); val bad_type = if null tfrees then K false else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false); fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x | bad_term (Var (_, T)) = bad_type T | bad_term (Const (_, T)) = bad_type T | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t | bad_term (t $ u) = bad_term t orelse bad_term u | bad_term (Bound _) = false; val _ = exists bad_term hyps andalso raise THM ("generalize: variable free in assumptions", 0, [th]); val generalize = Term_Subst.generalize (tfrees, frees) idx; val prop' = generalize prop; val tpairs' = map (apply2 generalize) tpairs; val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); in Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der, {cert = cert, tags = [], maxidx = maxidx', constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) end; fun generalize_cterm ([], []) _ ct = ct | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) = if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct]) else Cterm {cert = cert, sorts = sorts, T = Term_Subst.generalizeT tfrees idx T, t = Term_Subst.generalize (tfrees, frees) idx t, maxidx = Int.max (maxidx, idx)}; fun generalize_ctyp [] _ cT = cT | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) = if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", []) else Ctyp {cert = cert, sorts = sorts, T = Term_Subst.generalizeT tfrees idx T, maxidx = Int.max (maxidx, idx)}; (*Instantiation of schematic variables A -------------------- A[t1/v1, ..., tn/vn] *) local fun pretty_typing thy t T = Pretty.block [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T]; fun add_inst (v as (_, T), cu) (cert, sorts) = let val Cterm {t = u, T = U, cert = cert2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; val cert' = Context.join_certificate (cert, cert2); val sorts' = Sorts.union sorts_u sorts; in if T = U then ((v, (u, maxidx_u)), (cert', sorts')) else let val msg = (case cert' of Context.Certificate thy' => Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", Pretty.fbrk, pretty_typing thy' (Var v) T, Pretty.fbrk, pretty_typing thy' u U]) | Context.Certificate_Id _ => "instantiate: type conflict"); in raise TYPE (msg, [T, U], [Var v, u]) end end; fun add_instT (v as (_, S), cU) (cert, sorts) = let val Ctyp {T = U, cert = cert2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; val cert' = Context.join_certificate (cert, cert2); val thy' = Context.certificate_theory cert' handle ERROR msg => raise CONTEXT (msg, [cU], [], [], NONE); val sorts' = Sorts.union sorts_U sorts; in if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (cert', sorts')) else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) end; in (*Left-to-right replacements: ctpairs = [..., (vi, ti), ...]. Instantiates distinct Vars by terms of same type. Does NOT normalize the resulting theorem!*) fun instantiate ([], []) th = th | instantiate (instT, inst) th = let val Thm (der, {cert, hyps, constraints, shyps, tpairs, prop, ...}) = th; val (inst', (instT', (cert', shyps'))) = (cert, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT handle CONTEXT (msg, cTs, cts, ths, context) => raise CONTEXT (msg, cTs, cts, th :: ths, context); val subst = Term_Subst.instantiate_maxidx (instT', inst'); val (prop', maxidx1) = subst prop ~1; val (tpairs', maxidx') = fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; val thy' = Context.certificate_theory cert'; val constraints' = fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) instT' constraints; in Thm (deriv_rule1 (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, {cert = cert', tags = [], maxidx = maxidx', constraints = constraints', shyps = shyps', hyps = hyps, tpairs = tpairs', prop = prop'}) |> solve_constraints end handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); fun instantiate_cterm ([], []) ct = ct | instantiate_cterm (instT, inst) ct = let val Cterm {cert, t, T, sorts, ...} = ct; val (inst', (instT', (cert', sorts'))) = (cert, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT; val subst = Term_Subst.instantiate_maxidx (instT', inst'); val substT = Term_Subst.instantiateT_maxidx instT'; val (t', maxidx1) = subst t ~1; val (T', maxidx') = substT T maxidx1; in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); end; (*The trivial implication A \ A, justified by assume and forall rules. A can contain Vars, not so for assume!*) fun trivial (Cterm {cert, t = A, T, maxidx, sorts}) = if T <> propT then raise THM ("trivial: the term must have type prop", 0, []) else Thm (deriv_rule0 (fn () => Proofterm.trivial_proof), {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = sorts, hyps = [], tpairs = [], prop = Logic.mk_implies (A, A)}); (*Axiom-scheme reflecting signature contents T :: c ------------------- OFCLASS(T, c_class) *) fun of_class (cT, raw_c) = let val Ctyp {cert, T, ...} = cT; val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [cT], [], [], NONE); val c = Sign.certify_class thy raw_c; val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c)); in if Sign.of_sort thy (T, [c]) then Thm (deriv_rule0 (fn () => Proofterm.OfClass (T, c)), {cert = cert, tags = [], maxidx = maxidx, constraints = insert_constraints thy (T, [c]) [], shyps = sorts, hyps = [], tpairs = [], prop = prop}) else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, []) end |> solve_constraints; (*Remove extra sorts that are witnessed by type signature information*) fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm | strip_shyps (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = let val thy = theory_of_thm thm; val algebra = Sign.classes_of thy; val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; val extra = fold (Sorts.remove_sort o #2) present shyps; val witnessed = Sign.witness_sorts thy present extra; val extra' = fold (Sorts.remove_sort o #2) witnessed extra |> Sorts.minimal_sorts algebra; val shyps' = fold (Sorts.insert_sort o #2) present extra'; in Thm (deriv_rule_unconditional (Proofterm.strip_shyps_proof algebra present witnessed extra') der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) end; (*Internalize sort constraints of type variables*) val unconstrainT = solve_constraints #> (fn thm as Thm (der, args) => let val Deriv {promises, body} = der; val {cert, shyps, hyps, tpairs, prop, ...} = args; val thy = theory_of_thm thm; fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); val _ = null hyps orelse err "bad hyps"; val _ = null tpairs orelse err "bad flex-flex constraints"; val tfrees = rev (Term.add_tfree_names prop []); val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); val ps = map (apsnd (Future.map fulfill_body)) promises; val (pthm, proof) = Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy) shyps prop ps body; val der' = make_deriv [] [] [pthm] proof; val prop' = Proofterm.thm_node_prop (#2 pthm); in Thm (der', {cert = cert, tags = [], maxidx = maxidx_of_term prop', constraints = [], shyps = [[]], (*potentially redundant*) hyps = [], tpairs = [], prop = prop'}) end); (*Replace all TFrees not fixed or in the hyps by new TVars*) fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = let val tfrees = fold Term.add_tfrees hyps fixed; val prop1 = attach_tpairs tpairs prop; val (al, prop2) = Type.varify_global tfrees prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der, {cert = cert, tags = [], maxidx = Int.max (0, maxidx), constraints = constraints, shyps = shyps, hyps = hyps, tpairs = rev (map Logic.dest_equals ts), prop = prop3})) end; val varifyT_global = #2 o varifyT_global' []; (*Replace all TVars by TFrees that are often new*) fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) = let val prop1 = attach_tpairs tpairs prop; val prop2 = Type.legacy_freeze prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der, {cert = cert, tags = [], maxidx = maxidx_of_term prop2, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = rev (map Logic.dest_equals ts), prop = prop3}) end; fun plain_prop_of raw_thm = let val thm = strip_shyps raw_thm; fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); in if not (null (hyps_of thm)) then err "theorem may not contain hypotheses" else if not (null (extra_shyps thm)) then err "theorem may not contain sort hypotheses" else if not (null (tpairs_of thm)) then err "theorem may not contain flex-flex pairs" else prop_of thm end; (*** Inference rules for tactics ***) (*Destruct proof state into constraints, other goals, goal(i), rest *) fun dest_state (state as Thm (_, {prop,tpairs,...}), i) = (case Logic.strip_prems(i, [], prop) of (B::rBs, C) => (tpairs, rev rBs, B, C) | _ => raise THM("dest_state", i, [state])) handle TERM _ => raise THM("dest_state", i, [state]); (*Prepare orule for resolution by lifting it over the parameters and assumptions of goal.*) fun lift_rule goal orule = let val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal; val inc = gmax + 1; val lift_abs = Logic.lift_abs inc gprop; val lift_all = Logic.lift_all inc gprop; val Thm (der, {maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = orule; val (As, B) = Logic.strip_horn prop; in if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, []) else Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der, {cert = join_certificate1 (goal, orule), tags = [], maxidx = maxidx + inc, constraints = constraints, shyps = Sorts.union shyps sorts, (*sic!*) hyps = hyps, tpairs = map (apply2 lift_abs) tpairs, prop = Logic.list_implies (map lift_all As, lift_all B)}) end; fun incr_indexes i (thm as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = if i < 0 then raise THM ("negative increment", 0, [thm]) else if i = 0 then thm else Thm (deriv_rule1 (Proofterm.incr_indexes i) der, {cert = cert, tags = [], maxidx = maxidx + i, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs, prop = Logic.incr_indexes ([], [], i) prop}); (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) fun assumption opt_ctxt i state = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; val (context, cert') = make_context_certificate [state] opt_ctxt cert; val (tpairs, Bs, Bi, C) = dest_state (state, i); fun newth n (env, tpairs) = let val normt = Envir.norm_term env; fun assumption_proof prf = Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf; in Thm (deriv_rule1 (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der, {tags = [], maxidx = Envir.maxidx_of env, constraints = insert_constraints_env (Context.certificate_theory cert') env constraints, shyps = Envir.insert_sorts env shyps, hyps = hyps, tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs, prop = if Envir.is_empty env then Logic.list_implies (Bs, C) (*avoid wasted normalizations*) else normt (Logic.list_implies (Bs, C)) (*normalize the new rule fully*), cert = cert'}) end; val (close, asms, concl) = Logic.assum_problems (~1, Bi); val concl' = close concl; fun addprfs [] _ = Seq.empty | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull (Seq.mapp (newth n) (if Term.could_unify (asm, concl) then (Unify.unifiers (context, Envir.empty maxidx, (close asm, concl') :: tpairs)) else Seq.empty) (addprfs rest (n + 1)))) in addprfs asms 1 end; (*Solve subgoal Bi of proof state B1...Bn/C by assumption. Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*) fun eq_assumption i state = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val (_, asms, concl) = Logic.assum_problems (~1, Bi); in (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of ~1 => raise THM ("eq_assumption", 0, [state]) | n => Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = Logic.list_implies (Bs, C)})) end; (*For rotate_tac: fast rotation of assumptions of subgoal i*) fun rotate_rule k i state = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val params = Term.strip_all_vars Bi; val rest = Term.strip_all_body Bi; val asms = Logic.strip_imp_prems rest val concl = Logic.strip_imp_concl rest; val n = length asms; val m = if k < 0 then n + k else k; val Bi' = if 0 = m orelse m = n then Bi else if 0 < m andalso m < n then let val (ps, qs) = chop m asms in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end else raise THM ("rotate_rule", k, [state]); in Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = Logic.list_implies (Bs @ [Bi'], C)}) end; (*Rotates a rule's premises to the left by k, leaving the first j premises unchanged. Does nothing if k=0 or if k equals n-j, where n is the number of premises. Useful with eresolve_tac and underlies defer_tac*) fun permute_prems j k rl = let val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = rl; val prems = Logic.strip_imp_prems prop and concl = Logic.strip_imp_concl prop; val moved_prems = List.drop (prems, j) and fixed_prems = List.take (prems, j) handle General.Subscript => raise THM ("permute_prems: j", j, [rl]); val n_j = length moved_prems; val m = if k < 0 then n_j + k else k; val (prems', prop') = if 0 = m orelse m = n_j then (prems, prop) else if 0 < m andalso m < n_j then let val (ps, qs) = chop m moved_prems; val prems' = fixed_prems @ qs @ ps; in (prems', Logic.list_implies (prems', concl)) end else raise THM ("permute_prems: k", k, [rl]); in Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m) der, {cert = cert, tags = [], maxidx = maxidx, constraints = constraints, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop'}) end; (* strip_apply f B A strips off all assumptions/parameters from A introduced by lifting over B, and applies f to remaining part of A*) fun strip_apply f = let fun strip (Const ("Pure.imp", _) $ _ $ B1) (Const ("Pure.imp", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2) | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1)) ( Const ("Pure.all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2) | strip _ A = f A in strip end; fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1) (Const ("Pure.imp", _) $ _ $ B2) = strip_lifted B1 B2 | strip_lifted (Const ("Pure.all", _) $ Abs (_, _, t1)) (Const ("Pure.all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2 | strip_lifted _ A = A; (*Use the alist to rename all bound variables and some unknowns in a term dpairs = current disagreement pairs; tpairs = permanent ones (flexflex); Preserves unknowns in tpairs and on lhs of dpairs. *) fun rename_bvs [] _ _ _ _ = K I | rename_bvs al dpairs tpairs B As = let val add_var = fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I); val vids = [] |> fold (add_var o fst) dpairs |> fold (add_var o fst) tpairs |> fold (add_var o snd) tpairs; val vids' = fold (add_var o strip_lifted B) As []; (*unknowns appearing elsewhere be preserved!*) val al' = distinct ((op =) o apply2 fst) (filter_out (fn (x, y) => not (member (op =) vids' x) orelse member (op =) vids x orelse member (op =) vids y) al); val unchanged = filter_out (AList.defined (op =) al') vids'; fun del_clashing clash xs _ [] qs = if clash then del_clashing false xs xs qs [] else qs | del_clashing clash xs ys ((p as (x, y)) :: ps) qs = if member (op =) ys y then del_clashing true (x :: xs) (x :: ys) ps qs else del_clashing clash xs (y :: ys) ps (p :: qs); val al'' = del_clashing false unchanged unchanged al' []; fun rename (t as Var ((x, i), T)) = (case AList.lookup (op =) al'' x of SOME y => Var ((y, i), T) | NONE => t) | rename (Abs (x, T, t)) = Abs (the_default x (AList.lookup (op =) al x), T, rename t) | rename (f $ t) = rename f $ rename t | rename t = t; fun strip_ren f Ai = f rename B Ai in strip_ren end; (*Function to rename bounds/unknowns in the argument, lifted over B*) fun rename_bvars dpairs = rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs; (*** RESOLUTION ***) (** Lifting optimizations **) (*strip off pairs of assumptions/parameters in parallel -- they are identical because of lifting*) fun strip_assums2 (Const("Pure.imp", _) $ _ $ B1, Const("Pure.imp", _) $ _ $ B2) = strip_assums2 (B1,B2) | strip_assums2 (Const("Pure.all",_)$Abs(a,T,t1), Const("Pure.all",_)$Abs(_,_,t2)) = let val (B1,B2) = strip_assums2 (t1,t2) in (Abs(a,T,B1), Abs(a,T,B2)) end | strip_assums2 BB = BB; (*Faster normalization: skip assumptions that were lifted over*) fun norm_term_skip env 0 t = Envir.norm_term env t | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) = let val T' = Envir.norm_type (Envir.type_env env) T (*Must instantiate types of parameters because they are flattened; this could be a NEW parameter*) in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) = Logic.mk_implies (A, norm_term_skip env (n - 1) B) | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??"; (*unify types of schematic variables (non-lifted case)*) fun unify_var_types context (th1, th2) env = let fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types context (T, U)) Us | unify_vars _ = I; val add_vars = full_prop_of #> fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I); val vars = Vartab.empty |> add_vars th1 |> add_vars th2; in SOME (Vartab.fold (unify_vars o #2) vars env) end handle Pattern.Unif => NONE; (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) Unifies B with Bi, replacing subgoal i (1 <= i <= n) If match then forbid instantiations in proof state If lifted then shorten the dpair using strip_assums2. If eres_flg then simultaneously proves A1 by assumption. nsubgoal is the number of new subgoals (written m above). Curried so that resolution calls dest_state only once. *) local exception COMPOSE in fun bicompose_aux opt_ctxt {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted) (eres_flg, orule, nsubgoal) = let val Thm (sder, {maxidx=smax, constraints = constraints2, shyps = shyps2, hyps = hyps2, ...}) = state and Thm (rder, {maxidx=rmax, constraints = constraints1, shyps = shyps1, hyps = hyps1, tpairs=rtpairs, prop=rprop,...}) = orule (*How many hyps to skip over during normalization*) and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0) val (context, cert) = make_context_certificate [state, orule] opt_ctxt (join_certificate2 (state, orule)); (*Add new theorem with prop = "\Bs; As\ \ C" to thq*) fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) = let val normt = Envir.norm_term env; (*perform minimal copying here by examining env*) val (ntpairs, normp) = if Envir.is_empty env then (tpairs, (Bs @ As, C)) else let val ntps = map (apply2 normt) tpairs in if Envir.above env smax then (*no assignments in state; normalize the rule only*) if lifted then (ntps, (Bs @ map (norm_term_skip env nlift) As, C)) else (ntps, (Bs @ map normt As, C)) else if match then raise COMPOSE else (*normalize the new rule fully*) (ntps, (map normt (Bs @ As), normt C)) end val constraints' = union_constraints constraints1 constraints2 |> insert_constraints_env (Context.certificate_theory cert) env; fun bicompose_proof prf1 prf2 = Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) prf1 prf2 val th = Thm (deriv_rule2 (if Envir.is_empty env then bicompose_proof else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env else Proofterm.norm_proof' env oo bicompose_proof) rder' sder, {tags = [], maxidx = Envir.maxidx_of env, constraints = constraints', shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2), hyps = union_hyps hyps1 hyps2, tpairs = ntpairs, prop = Logic.list_implies normp, cert = cert}) in Seq.cons th thq end handle COMPOSE => thq; val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop) handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); (*Modify assumptions, deleting n-th if n>0 for e-resolution*) fun newAs(As0, n, dpairs, tpairs) = let val (As1, rder') = if not lifted then (As0, rder) else let val rename = rename_bvars dpairs tpairs B As0 in (map (rename strip_apply) As0, deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder) end; in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n) handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule]) end; val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); val dpairs = BBi :: (rtpairs@stpairs); (*elim-resolution: try each assumption in turn*) fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state]) | eres env (A1 :: As) = let val A = SOME A1; val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1); val concl' = close concl; fun tryasms [] _ = Seq.empty | tryasms (asm :: rest) n = if Term.could_unify (asm, concl) then let val asm' = close asm in (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of NONE => tryasms rest (n + 1) | cell as SOME ((_, tpairs), _) => Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs))) (Seq.make (fn () => cell), Seq.make (fn () => Seq.pull (tryasms rest (n + 1))))) end else tryasms rest (n + 1); in tryasms asms 1 end; (*ordinary resolution*) fun res env = (case Seq.pull (Unify.unifiers (context, env, dpairs)) of NONE => Seq.empty | cell as SOME ((_, tpairs), _) => Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs))) (Seq.make (fn () => cell), Seq.empty)); val env0 = Envir.empty (Int.max (rmax, smax)); in (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of NONE => Seq.empty | SOME env => if eres_flg then eres env (rev rAs) else res env) end; end; fun bicompose opt_ctxt flags arg i state = bicompose_aux opt_ctxt flags (state, dest_state (state,i), false) arg; (*Quick test whether rule is resolvable with the subgoal with hyps Hs and conclusion B. If eres_flg then checks 1st premise of rule also*) fun could_bires (Hs, B, eres_flg, rule) = let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs | could_reshyp [] = false; (*no premise -- illegal*) in Term.could_unify(concl_of rule, B) andalso (not eres_flg orelse could_reshyp (prems_of rule)) end; (*Bi-resolution of a state with a list of (flag,rule) pairs. Puts the rule above: rule/state. Renames vars in the rules. *) fun biresolution opt_ctxt match brules i state = let val (stpairs, Bs, Bi, C) = dest_state(state,i); val lift = lift_rule (cprem_of state i); val B = Logic.strip_assums_concl Bi; val Hs = Logic.strip_assums_hyp Bi; val compose = bicompose_aux opt_ctxt {flatten = true, match = match, incremented = true} (state, (stpairs, Bs, Bi, C), true); fun res [] = Seq.empty | res ((eres_flg, rule)::brules) = if Config.get_generic (make_context [state] opt_ctxt (cert_of state)) Pattern.unify_trace_failure orelse could_bires (Hs, B, eres_flg, rule) then Seq.make (*delay processing remainder till needed*) (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule), res brules)) else res brules in Seq.flat (res brules) end; (*Resolution: exactly one resolvent must be produced*) fun tha RSN (i, thb) = (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of ([th], _) => solve_constraints th | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb]) | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb])); (*Resolution: P \ Q, Q \ R gives P \ R*) fun tha RS thb = tha RSN (1,thb); (**** Type classes ****) fun standard_tvars thm = let val thy = theory_of_thm thm; val tvars = rev (Term.add_tvars (prop_of thm) []); val names = Name.invent Name.context Name.aT (length tvars); val tinst = map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names; in instantiate (tinst, []) thm end (* class relations *) val is_classrel = Symreltab.defined o get_classrels; fun complete_classrels thy = let fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) = let fun compl c1 c2 (finished2, thy2) = if is_classrel thy2 (c1, c2) then (finished2, thy2) else (false, thy2 |> (map_classrels o Symreltab.update) ((c1, c2), (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) |> standard_tvars |> close_derivation \<^here> |> trim_context)); val proven = is_classrel thy1; val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds []; val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs []; in fold_product compl preds succs (finished1, thy1) end; in (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of (true, _) => NONE | (_, thy') => SOME thy') end; (* type arities *) fun thynames_of_arity thy (a, c) = (get_arities thy, []) |-> Aritytab.fold (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)) |> sort (int_ord o apply2 #2) |> map #1; fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) = let val completions = Sign.super_classes thy c |> map_filter (fn c1 => if Aritytab.defined arities (t, Ss, c1) then NONE else let val th1 = (th RS the_classrel thy (c, c1)) |> standard_tvars |> close_derivation \<^here> |> trim_context; in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); val finished' = finished andalso null completions; val arities' = fold Aritytab.update completions arities; in (finished', arities') end; fun complete_arities thy = let val arities = get_arities thy; val (finished, arities') = Aritytab.fold (insert_arity_completions thy) arities (true, get_arities thy); in if finished then NONE else SOME (map_arities (K arities') thy) end; val _ = Theory.setup (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities); (* primitive rules *) fun add_classrel raw_th thy = let val th = strip_shyps (transfer thy raw_th); val prop = plain_prop_of th; val (c1, c2) = Logic.dest_classrel prop; in thy |> Sign.primitive_classrel (c1, c2) |> map_classrels (Symreltab.update ((c1, c2), th |> unconstrainT |> trim_context)) |> perhaps complete_classrels |> perhaps complete_arities end; fun add_arity raw_th thy = let val th = strip_shyps (transfer thy raw_th); val prop = plain_prop_of th; val (t, Ss, c) = Logic.dest_arity prop; val ar = ((t, Ss, c), (th |> unconstrainT |> trim_context, Context.theory_name thy, serial ())); in thy |> Sign.primitive_arity (t, Ss, [c]) |> map_arities (Aritytab.update ar #> curry (insert_arity_completions thy ar) true #> #2) end; end; structure Basic_Thm: BASIC_THM = Thm; open Basic_Thm;