equal
deleted
inserted
replaced
42 |
42 |
43 instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *) |
43 instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *) |
44 instance bool :: ml_equiv .. |
44 instance bool :: ml_equiv .. |
45 instance list :: (ml_equiv) ml_equiv .. |
45 instance list :: (ml_equiv) ml_equiv .. |
46 |
46 |
47 ML {* |
|
48 structure Eval_Witness_Method = |
|
49 struct |
|
50 |
|
51 val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE; |
|
52 |
|
53 end; |
|
54 *} |
|
55 |
|
56 oracle eval_witness_oracle = {* fn (cgoal, ws) => |
47 oracle eval_witness_oracle = {* fn (cgoal, ws) => |
57 let |
48 let |
58 val thy = Thm.theory_of_cterm cgoal; |
49 val thy = Thm.theory_of_cterm cgoal; |
59 val goal = Thm.term_of cgoal; |
50 val goal = Thm.term_of cgoal; |
60 fun check_type T = |
51 fun check_type T = |
66 | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = |
57 | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) = |
67 Abs (v, check_type T, dest_exs (n - 1) b) |
58 Abs (v, check_type T, dest_exs (n - 1) b) |
68 | dest_exs _ _ = sys_error "dest_exs"; |
59 | dest_exs _ _ = sys_error "dest_exs"; |
69 val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); |
60 val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal); |
70 in |
61 in |
71 if Code_Eval.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws |
62 if Code_Eval.eval NONE (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t ws |
72 then Thm.cterm_of thy goal |
63 then Thm.cterm_of thy goal |
73 else @{cprop True} (*dummy*) |
64 else @{cprop True} (*dummy*) |
74 end |
65 end |
75 *} |
66 *} |
76 |
67 |