29 val unregister_term_postprocessor : typ -> theory -> theory |
29 val unregister_term_postprocessor : typ -> theory -> theory |
30 val tuple_list_for_name : |
30 val tuple_list_for_name : |
31 nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list |
31 nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list |
32 val dest_plain_fun : term -> bool * (term list * term list) |
32 val dest_plain_fun : term -> bool * (term list * term list) |
33 val reconstruct_hol_model : |
33 val reconstruct_hol_model : |
34 params -> scope -> (term option * int list) list -> styp list -> nut list |
34 params -> scope -> (term option * int list) list |
35 -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list |
35 -> (typ option * string list) list -> styp list -> nut list -> nut list |
|
36 -> nut list -> nut NameTable.table -> Kodkod.raw_bound list |
36 -> Pretty.T * bool |
37 -> Pretty.T * bool |
37 val prove_hol_model : |
38 val prove_hol_model : |
38 scope -> Time.time option -> nut list -> nut list -> nut NameTable.table |
39 scope -> Time.time option -> nut list -> nut list -> nut NameTable.table |
39 -> Kodkod.raw_bound list -> term -> bool option |
40 -> Kodkod.raw_bound list -> term -> bool option |
40 end; |
41 end; |
101 ProofContext.transfer_syntax thy ctxt) |
102 ProofContext.transfer_syntax thy ctxt) |
102 end |
103 end |
103 |
104 |
104 (** Term reconstruction **) |
105 (** Term reconstruction **) |
105 |
106 |
106 fun nth_atom_suffix pool s j k = |
107 fun nth_atom_number pool T j = |
107 (case AList.lookup (op =) (!pool) (s, k) of |
108 case AList.lookup (op =) (!pool) T of |
108 SOME js => |
109 SOME js => |
109 (case find_index (curry (op =) j) js of |
110 (case find_index (curry (op =) j) js of |
110 ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js)); |
111 ~1 => (Unsynchronized.change pool (cons (T, j :: js)); |
111 length js + 1) |
112 length js + 1) |
112 | n => length js - n) |
113 | n => length js - n) |
113 | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1)) |
114 | NONE => (Unsynchronized.change pool (cons (T, [j])); 1) |
114 |> nat_subscript |
115 fun atom_suffix s = |
115 |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s))) |
116 nat_subscript |
|
117 #> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s))) |
116 ? prefix "\<^isub>," |
118 ? prefix "\<^isub>," |
117 fun nth_atom_name pool prefix (Type (s, _)) j k = |
119 fun nth_atom_name thy atomss pool prefix T j = |
118 let val s' = shortest_name s in |
120 let |
119 prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^ |
121 val ss = these (triple_lookup (type_match thy) atomss T) |
120 nth_atom_suffix pool s j k |
122 val m = nth_atom_number pool T j |
121 end |
123 in |
122 | nth_atom_name pool prefix (TFree (s, _)) j k = |
124 if m <= length ss then |
123 prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k |
125 nth ss (m - 1) |
124 | nth_atom_name _ _ T _ _ = |
126 else case T of |
125 raise TYPE ("Nitpick_Model.nth_atom_name", [T], []) |
127 Type (s, _) => |
126 fun nth_atom pool for_auto T j k = |
128 let val s' = shortest_name s in |
|
129 prefix ^ |
|
130 (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^ |
|
131 atom_suffix s m |
|
132 end |
|
133 | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m |
|
134 | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], []) |
|
135 end |
|
136 fun nth_atom thy atomss pool for_auto T j = |
127 if for_auto then |
137 if for_auto then |
128 Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T) |
138 Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix)) |
|
139 T j, T) |
129 else |
140 else |
130 Const (nth_atom_name pool "" T j k, T) |
141 Const (nth_atom_name thy atomss pool "" T j, T) |
131 |
142 |
132 fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) = |
143 fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) = |
133 real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2)) |
144 real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2)) |
134 | extract_real_number t = real (snd (HOLogic.dest_number t)) |
145 | extract_real_number t = real (snd (HOLogic.dest_number t)) |
135 fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2) |
146 fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2) |
298 |
309 |
299 fun varified_type_match thy (candid_T, pat_T) = |
310 fun varified_type_match thy (candid_T, pat_T) = |
300 strict_type_match thy (candid_T, Logic.varifyT_global pat_T) |
311 strict_type_match thy (candid_T, Logic.varifyT_global pat_T) |
301 |
312 |
302 fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope) |
313 fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope) |
303 sel_names rel_table bounds card T = |
314 atomss sel_names rel_table bounds card T = |
304 let |
315 let |
305 val card = if card = 0 then card_of_type card_assigns T else card |
316 val card = if card = 0 then card_of_type card_assigns T else card |
306 fun nth_value_of_type n = |
317 fun nth_value_of_type n = |
307 let |
318 let |
308 fun term unfold = |
319 fun term unfold = |
309 reconstruct_term unfold pool wacky_names scope sel_names rel_table |
320 reconstruct_term unfold pool wacky_names scope atomss sel_names |
310 bounds T T (Atom (card, 0)) [[n]] |
321 rel_table bounds T T (Atom (card, 0)) [[n]] |
311 in |
322 in |
312 case term false of |
323 case term false of |
313 t as Const (s, _) => |
324 t as Const (s, _) => |
314 if String.isPrefix cyclic_const_prefix s then |
325 if String.isPrefix cyclic_const_prefix s then |
315 HOLogic.mk_eq (t, term true) |
326 HOLogic.mk_eq (t, term true) |
318 | t => t |
329 | t => t |
319 end |
330 end |
320 in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end |
331 in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end |
321 and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _)) |
332 and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _)) |
322 (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, |
333 (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, |
323 bits, datatypes, ofs, ...}) sel_names rel_table bounds = |
334 bits, datatypes, ofs, ...}) |
|
335 atomss sel_names rel_table bounds = |
324 let |
336 let |
325 val for_auto = (maybe_name = "") |
337 val for_auto = (maybe_name = "") |
326 fun value_of_bits jss = |
338 fun value_of_bits jss = |
327 let |
339 let |
328 val j0 = offset_of_type ofs @{typ unsigned_bit} |
340 val j0 = offset_of_type ofs @{typ unsigned_bit} |
330 in |
342 in |
331 fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~)) |
343 fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~)) |
332 js 0 |
344 js 0 |
333 end |
345 end |
334 val all_values = |
346 val all_values = |
335 all_values_of_type pool wacky_names scope sel_names rel_table bounds 0 |
347 all_values_of_type pool wacky_names scope atomss sel_names rel_table |
|
348 bounds 0 |
336 fun postprocess_term (Type (@{type_name fun}, _)) = I |
349 fun postprocess_term (Type (@{type_name fun}, _)) = I |
337 | postprocess_term T = |
350 | postprocess_term T = |
338 if null (Data.get thy) then |
351 if null (Data.get thy) then |
339 I |
352 I |
340 else case AList.lookup (varified_type_match thy) (Data.get thy) T of |
353 else case AList.lookup (varified_type_match thy) (Data.get thy) T of |
469 else if is_fp_iterator_type T then |
482 else if is_fp_iterator_type T then |
470 HOLogic.mk_number nat_T (k - j - 1) |
483 HOLogic.mk_number nat_T (k - j - 1) |
471 else if T = @{typ bisim_iterator} then |
484 else if T = @{typ bisim_iterator} then |
472 HOLogic.mk_number nat_T j |
485 HOLogic.mk_number nat_T j |
473 else case datatype_spec datatypes T of |
486 else case datatype_spec datatypes T of |
474 NONE => nth_atom pool for_auto T j k |
487 NONE => nth_atom thy atomss pool for_auto T j |
475 | SOME {deep = false, ...} => nth_atom pool for_auto T j k |
488 | SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j |
476 | SOME {co, standard, constrs, ...} => |
489 | SOME {co, standard, constrs, ...} => |
477 let |
490 let |
478 fun tuples_for_const (s, T) = |
491 fun tuples_for_const (s, T) = |
479 tuple_list_for_name rel_table bounds (ConstName (s, T, Any)) |
492 tuple_list_for_name rel_table bounds (ConstName (s, T, Any)) |
480 fun cyclic_atom () = |
493 fun cyclic_atom () = |
481 nth_atom pool for_auto (Type (cyclic_type_name, [])) j k |
494 nth_atom thy atomss pool for_auto (Type (cyclic_type_name, [])) j |
482 fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T) |
495 fun cyclic_var () = |
483 |
496 Var ((nth_atom_name thy atomss pool "" T j, 0), T) |
484 val discr_jsss = map (tuples_for_const o discr_for_constr o #const) |
497 val discr_jsss = map (tuples_for_const o discr_for_constr o #const) |
485 constrs |
498 constrs |
486 val real_j = j + offset_of_type ofs T |
499 val real_j = j + offset_of_type ofs T |
487 val constr_x as (constr_s, constr_T) = |
500 val constr_x as (constr_s, constr_T) = |
488 get_first (fn (jss, {const, ...}) => |
501 get_first (fn (jss, {const, ...}) => |
610 | term_for_rep _ seen T T' (Opt R) jss = |
623 | term_for_rep _ seen T T' (Opt R) jss = |
611 if null jss then Const (unknown, T) |
624 if null jss then Const (unknown, T) |
612 else term_for_rep true seen T T' R jss |
625 else term_for_rep true seen T T' R jss |
613 | term_for_rep _ _ T _ R jss = |
626 | term_for_rep _ _ T _ R jss = |
614 raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", |
627 raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", |
615 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^ |
628 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ |
616 string_of_int (length jss)) |
629 string_of_int (length jss)) |
617 in |
630 in |
618 postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term |
631 postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term |
619 oooo term_for_rep true [] |
632 oooo term_for_rep true [] |
620 end |
633 end |
809 else |
822 else |
810 "=" |
823 "=" |
811 |
824 |
812 (** Model reconstruction **) |
825 (** Model reconstruction **) |
813 |
826 |
814 fun term_for_name pool scope sel_names rel_table bounds name = |
827 fun term_for_name pool scope atomss sel_names rel_table bounds name = |
815 let val T = type_of name in |
828 let val T = type_of name in |
816 tuple_list_for_name rel_table bounds name |
829 tuple_list_for_name rel_table bounds name |
817 |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names |
830 |> reconstruct_term false pool (("", ""), ("", "")) scope atomss sel_names |
818 rel_table bounds T T (rep_of name) |
831 rel_table bounds T T (rep_of name) |
819 end |
832 end |
820 |
833 |
821 fun unfold_outer_the_binders (t as Const (@{const_name The}, _) |
834 fun unfold_outer_the_binders (t as Const (@{const_name The}, _) |
822 $ Abs (s, T, Const (@{const_name "op ="}, _) |
835 $ Abs (s, T, Const (@{const_name "op ="}, _) |
846 case_names, def_table, nondef_table, user_nondefs, |
859 case_names, def_table, nondef_table, user_nondefs, |
847 simp_table, psimp_table, choice_spec_table, intro_table, |
860 simp_table, psimp_table, choice_spec_table, intro_table, |
848 ground_thm_table, ersatz_table, skolems, special_funs, |
861 ground_thm_table, ersatz_table, skolems, special_funs, |
849 unrolled_preds, wf_cache, constr_cache}, |
862 unrolled_preds, wf_cache, constr_cache}, |
850 binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope) |
863 binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope) |
851 formats all_frees free_names sel_names nonsel_names rel_table bounds = |
864 formats atomss all_frees free_names sel_names nonsel_names rel_table |
|
865 bounds = |
852 let |
866 let |
853 val pool = Unsynchronized.ref [] |
867 val pool = Unsynchronized.ref [] |
854 val (wacky_names as (_, base_step_names), ctxt) = |
868 val (wacky_names as (_, base_step_names), ctxt) = |
855 add_wacky_syntax ctxt |
869 add_wacky_syntax ctxt |
856 val hol_ctxt = |
870 val hol_ctxt = |
869 constr_cache = constr_cache} |
883 constr_cache = constr_cache} |
870 val scope = |
884 val scope = |
871 {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns, |
885 {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns, |
872 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs} |
886 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs} |
873 fun term_for_rep unfold = |
887 fun term_for_rep unfold = |
874 reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds |
888 reconstruct_term unfold pool wacky_names scope atomss sel_names rel_table |
|
889 bounds |
875 fun nth_value_of_type card T n = |
890 fun nth_value_of_type card T n = |
876 let |
891 let fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]] in |
877 fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]] |
|
878 in |
|
879 case aux false of |
892 case aux false of |
880 t as Const (s, _) => |
893 t as Const (s, _) => |
881 if String.isPrefix cyclic_const_prefix s then |
894 if String.isPrefix cyclic_const_prefix s then |
882 HOLogic.mk_eq (t, aux true) |
895 HOLogic.mk_eq (t, aux true) |
883 else |
896 else |
884 t |
897 t |
885 | t => t |
898 | t => t |
886 end |
899 end |
887 val all_values = |
900 val all_values = |
888 all_values_of_type pool wacky_names scope sel_names rel_table bounds |
901 all_values_of_type pool wacky_names scope atomss sel_names rel_table |
|
902 bounds |
889 fun is_codatatype_wellformed (cos : dtype_spec list) |
903 fun is_codatatype_wellformed (cos : dtype_spec list) |
890 ({typ, card, ...} : dtype_spec) = |
904 ({typ, card, ...} : dtype_spec) = |
891 let |
905 let |
892 val ts = all_values card typ |
906 val ts = all_values card typ |
893 val max_depth = Integer.sum (map #card cos) |
907 val max_depth = Integer.sum (map #card cos) |
994 fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...}, |
1008 fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...}, |
995 card_assigns, ...}) |
1009 card_assigns, ...}) |
996 auto_timeout free_names sel_names rel_table bounds prop = |
1010 auto_timeout free_names sel_names rel_table bounds prop = |
997 let |
1011 let |
998 val pool = Unsynchronized.ref [] |
1012 val pool = Unsynchronized.ref [] |
|
1013 val atomss = [(NONE, [])] |
999 fun free_type_assm (T, k) = |
1014 fun free_type_assm (T, k) = |
1000 let |
1015 let |
1001 fun atom j = nth_atom pool true T j k |
1016 fun atom j = nth_atom thy atomss pool true T j |
1002 fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j |
1017 fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j |
1003 val eqs = map equation_for_atom (index_seq 0 k) |
1018 val eqs = map equation_for_atom (index_seq 0 k) |
1004 val compreh_assm = |
1019 val compreh_assm = |
1005 Const (@{const_name All}, (T --> bool_T) --> bool_T) |
1020 Const (@{const_name All}, (T --> bool_T) --> bool_T) |
1006 $ Abs ("x", T, foldl1 HOLogic.mk_disj eqs) |
1021 $ Abs ("x", T, foldl1 HOLogic.mk_disj eqs) |
1007 val distinct_assm = distinctness_formula T (map atom (index_seq 0 k)) |
1022 val distinct_assm = distinctness_formula T (map atom (index_seq 0 k)) |
1008 in s_conj (compreh_assm, distinct_assm) end |
1023 in s_conj (compreh_assm, distinct_assm) end |
1009 fun free_name_assm name = |
1024 fun free_name_assm name = |
1010 HOLogic.mk_eq (Free (nickname_of name, type_of name), |
1025 HOLogic.mk_eq (Free (nickname_of name, type_of name), |
1011 term_for_name pool scope sel_names rel_table bounds name) |
1026 term_for_name pool scope atomss sel_names rel_table bounds |
|
1027 name) |
1012 val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns) |
1028 val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns) |
1013 val model_assms = map free_name_assm free_names |
1029 val model_assms = map free_name_assm free_names |
1014 val assm = foldr1 s_conj (freeT_assms @ model_assms) |
1030 val assm = foldr1 s_conj (freeT_assms @ model_assms) |
1015 fun try_out negate = |
1031 fun try_out negate = |
1016 let |
1032 let |