--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed May 08 12:06:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 09 02:42:51 2013 +0200
@@ -93,6 +93,8 @@
val morN: string
val nchotomyN: string
val recN: string
+ val rel_coinductN: string
+ val rel_inductN: string
val rel_injectN: string
val rel_distinctN: string
val rvN: string
@@ -310,6 +312,8 @@
val rel_distinctN = relN ^ "_" ^ distinctN
val injectN = "inject"
val rel_injectN = relN ^ "_" ^ injectN
+val rel_coinductN = relN ^ "_" ^ coinductN
+val rel_inductN = relN ^ "_" ^ inductN
val selN = "sel"
val sel_unfoldN = selN ^ "_" ^ unfoldN
val sel_corecN = selN ^ "_" ^ corecN
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed May 08 12:06:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu May 09 02:42:51 2013 +0200
@@ -1366,6 +1366,13 @@
fun mk_ctor_Irel_DEADID_thm ctor_inject bnf =
trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
+ val IphiTs = map2 mk_pred2T passiveAs passiveBs;
+ val activeIphiTs = map2 mk_pred2T Ts Ts';
+ val ((Iphis, activeIphis), names_lthy) = names_lthy
+ |> mk_Frees "R" IphiTs
+ ||>> mk_Frees "IR" activeIphiTs;
+ val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
+
(*register new datatypes as BNFs*)
val (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
if m = 0 then
@@ -1383,10 +1390,9 @@
val AXTs = map HOLogic.mk_setT passiveXs;
val XTs = mk_Ts passiveXs;
val YTs = mk_Ts passiveYs;
- val IphiTs = map2 mk_pred2T passiveAs passiveBs;
- val ((((((((((((((fs, fs'), fs_copy), us),
- B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), Iphis),
+ val (((((((((((((fs, fs'), fs_copy), us),
+ B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')),
names_lthy) = names_lthy
|> mk_Frees' "f" fTs
||>> mk_Frees "f" fTs
@@ -1399,8 +1405,7 @@
||>> mk_Frees "f2" f2Ts
||>> mk_Frees "p1" p1Ts
||>> mk_Frees "p2" p2Ts
- ||>> mk_Frees' "y" passiveAs
- ||>> mk_Frees "R" IphiTs;
+ ||>> mk_Frees' "y" passiveAs;
val map_FTFT's = map2 (fn Ds =>
mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
@@ -1746,7 +1751,6 @@
val timer = time (timer "registered new datatypes as BNFs");
- val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels;
@@ -1803,9 +1807,33 @@
lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
end;
+ val Irel_induct_thm =
+ let
+ val relphis = map (fn rel => Term.list_comb (rel, Iphis @ activeIphis)) rels;
+ fun mk_prem relphi phi x y ctor ctor' =
+ fold_rev Logic.all [x, y] (Logic.mk_implies (HOLogic.mk_Trueprop (relphi $ x $ y),
+ HOLogic.mk_Trueprop (phi $ (ctor $ x) $ (ctor' $ y))));
+ val prems = map6 mk_prem relphis activeIphis xFs yFs ctors ctor's;
+
+ val Irels = if m = 0 then map HOLogic.eq_const Ts
+ else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
+ val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels;
+ val concl =
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq Irelphis activeIphis));
+ in
+ Goal.prove_sorry lthy [] []
+ (fold_rev Logic.all (Iphis @ activeIphis) (Logic.list_implies (prems, concl)))
+ (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms
+ (map rel_mono_strong_of_bnf bnfs))
+ |> Thm.close_derivation
+ end;
+
+ val timer = time (timer "relator induction");
+
val common_notes =
[(ctor_inductN, [ctor_induct_thm]),
- (ctor_induct2N, [ctor_induct2_thm])]
+ (ctor_induct2N, [ctor_induct2_thm]),
+ (rel_inductN, [Irel_induct_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed May 08 12:06:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu May 09 02:42:51 2013 +0200
@@ -64,6 +64,8 @@
val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
thm list -> tactic
val mk_mor_str_tac: 'a list -> thm -> tactic
+ val mk_rel_induct_tac: int -> thm -> int list -> thm list -> thm list ->
+ {prems: 'a, context: Proof.context} -> tactic
val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
tactic
@@ -844,4 +846,19 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
+fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = _} =
+ let val n = length ks;
+ in
+ unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN
+ EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
+ EVERY' (map3 (fn i => fn ctor_rel => fn rel_mono_strong =>
+ EVERY' [rtac impI, dtac (ctor_rel RS iffD1), select_prem_tac n (dtac @{thm meta_spec2}) i,
+ etac meta_mp, etac rel_mono_strong,
+ REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
+ EVERY' (map (fn j =>
+ EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]},
+ Goal.assume_rule_tac ctxt]) ks)])
+ ks ctor_rels rel_mono_strongs)] 1
+ end;
+
end;
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 08 12:06:04 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 09 02:42:51 2013 +0200
@@ -551,7 +551,7 @@
in ary oo robust_const_type end
(* This function only makes sense if "T" is as general as possible. *)
-fun robust_const_typargs thy (s, T) =
+fun robust_const_type_args thy (s, T) =
if s = app_op_name then
let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
else if String.isPrefix old_skolem_const_prefix s then
@@ -573,7 +573,7 @@
in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
| iterm_from_term thy type_enc _ (Const (c, T)) =
(IConst (`(make_fixed_const (SOME type_enc)) c, T,
- robust_const_typargs thy (c, T)),
+ robust_const_type_args thy (c, T)),
atomic_types_of T)
| iterm_from_term _ _ _ (Free (s, T)) =
(IConst (`make_fixed_var s, T, []), atomic_types_of T)
@@ -870,7 +870,7 @@
T
else
dummyT
- val U_args = (s, U) |> robust_const_typargs thy
+ val U_args = (s, U) |> robust_const_type_args thy
in map (filt o apfst dest_TVar) (U_args ~~ T_args) end
handle TYPE _ => T_args
val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary)
@@ -1087,11 +1087,14 @@
fun unmangled_const_name s =
(s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
+
fun unmangled_const s =
let val ss = unmangled_const_name s in
(hd ss, map unmangled_type (tl ss))
end
+val unmangled_invert_const = invert_const o hd o unmangled_const_name
+
fun introduce_proxies_in_iterm type_enc =
let
fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
@@ -1174,7 +1177,8 @@
if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
else T_args
| SOME s'' =>
- filter_type_args thy constrs type_enc (invert_const s'') ary T_args
+ filter_type_args thy constrs type_enc (unmangled_invert_const s'') ary
+ T_args
fun filter_type_args_in_iterm thy constrs type_enc =
let
fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
@@ -1341,8 +1345,8 @@
(case unprefix_and_unascii const_prefix s of
SOME s =>
let fun tvars_of T = [] |> Term.add_tvarsT T |> map fst in
- s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
- |> map tvars_of
+ s |> unmangled_invert_const |> robust_const_type thy |> chop_fun ary
+ |> fst |> map tvars_of
end
| NONE => [])
handle TYPE _ => []
@@ -1551,8 +1555,7 @@
(if String.isSubstring uncurried_alias_sep s then
ary
else case try (robust_const_ary thy
- o invert_const o hd
- o unmangled_const_name) s of
+ o unmangled_invert_const) s of
SOME ary0 => Int.min (ary0, ary)
| NONE => ary)
| NONE => ary
@@ -1595,7 +1598,7 @@
| NONE =>
case unprefix_and_unascii const_prefix s of
SOME s =>
- let val s = s |> unmangled_const_name |> hd |> invert_const in
+ let val s = s |> unmangled_invert_const in
if s = predicator_name then 1
else if s = app_op_name then 2
else if s = type_guard_name then 1
@@ -1642,21 +1645,42 @@
completish =
let
fun do_app arg head = mk_app_op type_enc head arg
- fun list_app_ops head args = fold do_app args head
+ fun list_app_ops (head, args) = fold do_app args head
fun introduce_app_ops tm =
let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
case head of
IConst (name as (s, _), T, T_args) =>
- if uncurried_aliases andalso String.isPrefix const_prefix s then
- let
- val ary = length args
- val name =
- name |> ary > min_ary_of sym_tab s ? aliased_uncurried ary
- in list_app (IConst (name, T, T_args)) args end
- else
- args |> chop (min_ary_of sym_tab s)
- |>> list_app head |-> list_app_ops
- | _ => list_app_ops head args
+ let
+ val min_ary = min_ary_of sym_tab s
+ val ary =
+ if uncurried_aliases andalso String.isPrefix const_prefix s then
+ let
+ val ary = length args
+ (* In polymorphic native type encodings, it is impossible to
+ declare a fully polymorphic symbol that takes more arguments
+ than its signature (even though such concrete instances, where
+ a type variable is instantiated by a function type, are
+ possible.) *)
+ val official_ary =
+ if is_type_enc_polymorphic type_enc then
+ case unprefix_and_unascii const_prefix s of
+ SOME s' =>
+ (case try (robust_const_ary thy) (invert_const s') of
+ SOME ary => ary
+ | NONE => min_ary)
+ | NONE => min_ary
+ else
+ 1000000000 (* irrealistically big arity *)
+ in Int.min (ary, official_ary) end
+ else
+ min_ary
+ val head =
+ if ary = min_ary then head
+ else IConst (aliased_uncurried ary name, T, T_args)
+ in
+ args |> chop ary |>> list_app head |> list_app_ops
+ end
+ | _ => list_app_ops (head, args)
end
fun introduce_predicators tm =
case strip_iterm_comb tm of
@@ -1859,7 +1883,7 @@
fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
| add (t $ u) = add t #> add u
| add (Const x) =
- x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
+ x |> robust_const_type_args thy |> fold (fold_type_constrs set_insert)
| add (Abs (_, _, u)) = add u
| add _ = I
in add end
@@ -2387,9 +2411,9 @@
else case unprefix_and_unascii const_prefix s of
SOME s' =>
let
- val s' = s' |> invert_const
+ val s' = s' |> unmangled_invert_const
val T = s' |> robust_const_type thy
- in (T, robust_const_typargs thy (s', T)) end
+ in (T, robust_const_type_args thy (s', T)) end
| NONE => raise Fail "unexpected type arguments"
in
Sym_Decl (sym_decl_prefix ^ s, (s, s'),
@@ -2522,7 +2546,7 @@
val (role, maybe_negate) = honor_conj_sym_role in_conj
val base_name = base_s0 |> `(make_fixed_const (SOME type_enc))
val T = case types of [T] => T | _ => robust_const_type thy base_s0
- val T_args = robust_const_typargs thy (base_s0, T)
+ val T_args = robust_const_type_args thy (base_s0, T)
val (base_name as (base_s, _), T_args) =
mangle_type_args_in_const type_enc base_name T_args
val base_ary = min_ary_of sym_tab0 base_s
@@ -2564,7 +2588,7 @@
SOME mangled_s =>
if String.isSubstring uncurried_alias_sep mangled_s then
let
- val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
+ val base_s0 = mangled_s |> unmangled_invert_const
in
do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
sym_tab base_s0 types in_conj min_ary
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed May 08 12:06:04 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu May 09 02:42:51 2013 +0200
@@ -610,7 +610,7 @@
(* Not really a prover: Experimental Polymorphic THF and DFG output *)
-fun dummy_config prem_role format type_enc : atp_config =
+fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
{exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
arguments = K (K (K (K (K (K ""))))),
proof_delims = [],
@@ -619,19 +619,19 @@
best_slices =
K [(1.0, (((200, ""), format, type_enc,
if is_format_higher_order format then keep_lamsN
- else combsN, false), ""))],
+ else combsN, uncurried_aliases), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
val dummy_thf_format =
THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
val dummy_thf_config =
- dummy_config Hypothesis dummy_thf_format "poly_native_higher"
+ dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
val spass_poly_format = DFG Polymorphic
val spass_poly_config =
- dummy_config (#prem_role spass_config) spass_poly_format "tc_native"
+ dummy_config (#prem_role spass_config) spass_poly_format "tc_native" true
val spass_poly = (spass_polyN, fn () => spass_poly_config)
(* Remote ATP invocation via SystemOnTPTP *)