Commit 803606ff authored by Sylvain Dailler's avatar Sylvain Dailler

Added intros n which introduce n times.

parent 31c951c3
......@@ -476,6 +476,72 @@ let destruct pr : Task.task Trans.tlist =
end
| _ -> [[d]]) None
(* TODO to be done ... *)
open Ident
open Ty
open Term
open Decl
(* TODO temporary for intros *)
let rec intros n pr f =
if n = 0 then [create_prop_decl Pgoal pr f] else
match f.t_node with
(* (f2 \/ True) => _ *)
| Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },_)
when Slab.mem Term.asym_label f2.t_label ->
[create_prop_decl Pgoal pr f]
| Tbinop (Timplies,f1,f2) ->
(* split f1 *)
(* f is going to be removed, preserve its labels and location in f2 *)
let f2 = t_label_copy f f2 in
let l = Split_goal.split_intro_right f1 in
List.fold_right
(fun f acc ->
let id = create_prsymbol (id_fresh "H") in
let d = create_prop_decl Paxiom id f in
d :: acc)
l
(intros (n-1) pr f2)
| Tquant (Tforall,fq) ->
let vsl,_trl,f_t = t_open_quant fq in
let intro_var subst vs =
let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
Mvs.add vs (fs_app ls [] vs.vs_ty) subst,
create_param_decl ls
in
let subst, decl = intro_var Mvs.empty (List.hd vsl) in
if List.length vsl = 1 then
begin
let f = t_label_copy f (t_subst subst f_t) in
decl :: intros (n-1) pr f
end
else
let f = t_quant Tforall
(t_close_quant (List.tl vsl) [] (t_subst subst f_t)) in
decl :: intros (n-1) pr f
| Tlet (t,fb) ->
let vs,f = t_open_bound fb in
let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
let f = t_subst_single vs (fs_app ls [] vs.vs_ty) f in
let d = create_logic_decl [make_ls_defn ls [] t] in
d :: intros (n-1) pr f
| _ -> [create_prop_decl Pgoal pr f]
let intros n pr f =
let tvs = t_ty_freevars Stv.empty f in
let mk_ts tv () = create_tysymbol (id_clone tv.tv_name) [] NoDef in
let tvm = Mtv.mapi mk_ts tvs in
let decls = Mtv.map create_ty_decl tvm in
let subst = Mtv.map (fun ts -> ty_app ts []) tvm in
Mtv.values decls @ intros n pr (t_ty_subst subst Mvs.empty f)
let introduce_premises n = Trans.goal (intros n)
let () = wrap_and_register ~desc:"intros n"
"intros"
(Tint Ttrans) introduce_premises
let use_th th =
Trans.add_tdecls [Theory.create_use th]
......
......@@ -133,4 +133,3 @@ let rec chop_last = function
| [] -> invalid_arg "Util.chop_last"
| [r] -> [], r
| x :: s -> let s, r = chop_last s in x :: s, r
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment