29 |
29 |
30 (*code equations*) |
30 (*code equations*) |
31 val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool |
31 val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool |
32 val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option |
32 val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option |
33 val assert_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool |
33 val assert_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool |
|
34 val const_typ_eqn: thm -> string * typ |
34 val const_eqn: theory -> thm -> string |
35 val const_eqn: theory -> thm -> string |
35 val const_typ_eqn: thm -> string * typ |
|
36 val typscheme_eqn: theory -> thm -> (string * sort) list * typ |
36 val typscheme_eqn: theory -> thm -> (string * sort) list * typ |
37 val expand_eta: theory -> int -> thm -> thm |
37 val expand_eta: theory -> int -> thm -> thm |
38 val rewrite_eqn: simpset -> thm -> thm |
38 val rewrite_eqn: simpset -> thm -> thm |
39 val rewrite_head: thm list -> thm -> thm |
39 val rewrite_head: thm list -> thm -> thm |
40 val norm_args: theory -> thm list -> thm list |
40 val norm_args: theory -> thm list -> thm list |
377 |
377 |
378 fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr); |
378 fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr); |
379 |
379 |
380 val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; |
380 val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; |
381 |
381 |
382 fun typscheme_eqn thy = typscheme thy o const_typ_eqn; |
382 |
383 |
383 (*those following are permissive wrt. to overloaded constants!*) |
384 (*these are permissive wrt. to overloaded constants!*) |
384 |
385 fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o |
385 fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o |
386 apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy)); |
386 apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy)); |
387 |
387 |
388 fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) |
388 fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) |
389 o try_thm (gen_assert_eqn thy is_constr_head (K true)) |
389 o try_thm (gen_assert_eqn thy is_constr_head (K true)) |
390 o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); |
390 o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); |
391 |
391 |
392 fun const_eqn thy = AxClass.unoverload_const thy o const_typ_eqn; |
392 fun const_typ_eqn_unoverload thy thm = |
|
393 let |
|
394 val (c, ty) = const_typ_eqn thm; |
|
395 val c' = AxClass.unoverload_const thy (c, ty); |
|
396 in (c', ty) end; |
|
397 |
|
398 fun typscheme_eqn thy = typscheme thy o const_typ_eqn_unoverload thy; |
|
399 fun const_eqn thy = fst o const_typ_eqn_unoverload thy; |
393 |
400 |
394 |
401 |
395 (* case cerificates *) |
402 (* case cerificates *) |
396 |
403 |
397 fun case_certificate thm = |
404 fun case_certificate thm = |