37 val reconstruct_hol_model : |
37 val reconstruct_hol_model : |
38 params -> scope -> (term option * int list) list |
38 params -> scope -> (term option * int list) list |
39 -> (typ option * string list) list -> (string * typ) list -> |
39 -> (typ option * string list) list -> (string * typ) list -> |
40 (string * typ) list -> nut list -> nut list -> nut list -> |
40 (string * typ) list -> nut list -> nut list -> nut list -> |
41 nut NameTable.table -> Kodkod.raw_bound list -> Pretty.T * bool |
41 nut NameTable.table -> Kodkod.raw_bound list -> Pretty.T * bool |
42 val prove_hol_model : |
|
43 scope -> Time.time -> nut list -> nut list -> nut NameTable.table |
|
44 -> Kodkod.raw_bound list -> term -> bool option |
|
45 end; |
42 end; |
46 |
43 |
47 structure Nitpick_Model : NITPICK_MODEL = |
44 structure Nitpick_Model : NITPICK_MODEL = |
48 struct |
45 struct |
49 |
46 |
1034 else chunks), |
1031 else chunks), |
1035 bisim_depth >= 0 orelse |
1032 bisim_depth >= 0 orelse |
1036 forall (is_codatatype_wellformed codatatypes) codatatypes) |
1033 forall (is_codatatype_wellformed codatatypes) codatatypes) |
1037 end |
1034 end |
1038 |
1035 |
1039 fun term_for_name pool scope atomss sel_names rel_table bounds name = |
|
1040 let val T = type_of name in |
|
1041 tuple_list_for_name rel_table bounds name |
|
1042 |> reconstruct_term (not (is_fully_representable_set name)) false pool |
|
1043 (("", ""), ("", "")) scope atomss sel_names rel_table |
|
1044 bounds T T (rep_of name) |
|
1045 end |
|
1046 |
|
1047 fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...}, |
|
1048 card_assigns, ...}) |
|
1049 auto_timeout free_names sel_names rel_table bounds prop = |
|
1050 let |
|
1051 val pool = Unsynchronized.ref [] |
|
1052 val atomss = [(NONE, [])] |
|
1053 fun free_type_assm (T, k) = |
|
1054 let |
|
1055 fun atom j = nth_atom thy atomss pool true T j |
|
1056 fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j |
|
1057 val eqs = map equation_for_atom (index_seq 0 k) |
|
1058 val compreh_assm = |
|
1059 Const (@{const_name All}, (T --> bool_T) --> bool_T) |
|
1060 $ Abs ("x", T, foldl1 HOLogic.mk_disj eqs) |
|
1061 val distinct_assm = distinctness_formula T (map atom (index_seq 0 k)) |
|
1062 in s_conj (compreh_assm, distinct_assm) end |
|
1063 fun free_name_assm name = |
|
1064 HOLogic.mk_eq (Free (nickname_of name, type_of name), |
|
1065 term_for_name pool scope atomss sel_names rel_table bounds |
|
1066 name) |
|
1067 val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns) |
|
1068 val model_assms = map free_name_assm free_names |
|
1069 val assm = foldr1 s_conj (freeT_assms @ model_assms) |
|
1070 fun try_out negate = |
|
1071 let |
|
1072 val concl = (negate ? curry (op $) @{const Not}) |
|
1073 (Object_Logic.atomize_term ctxt prop) |
|
1074 val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl)) |
|
1075 |> map_types (map_type_tfree |
|
1076 (fn (s, []) => TFree (s, @{sort type}) |
|
1077 | x => TFree x)) |
|
1078 val _ = |
|
1079 if debug then |
|
1080 (if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^ |
|
1081 Syntax.string_of_term ctxt prop ^ "." |
|
1082 |> writeln |
|
1083 else |
|
1084 () |
|
1085 val goal = prop |> Thm.cterm_of ctxt |> Goal.init |
|
1086 in |
|
1087 (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt)) |
|
1088 |> the |> Goal.finish ctxt; true) |
|
1089 handle THM _ => false |
|
1090 | TimeLimit.TimeOut => false |
|
1091 end |
|
1092 in |
|
1093 if try_out false then SOME true |
|
1094 else if try_out true then SOME false |
|
1095 else NONE |
|
1096 end |
|
1097 |
|
1098 end; |
1036 end; |