# HG changeset patch # User steckerm # Date 1410093563 -7200 # Node ID d95055489fce4febed663838d4af7702d92fc0d3 # Parent 5fbe474b5da81ee6c7df3498bb4a595e4ba6645d Added translation for lambda expressions in terms. diff -r 5fbe474b5da8 -r d95055489fce src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Sep 07 09:49:05 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Sep 07 14:39:23 2014 +0200 @@ -100,6 +100,7 @@ val type_enc_of_string : strictness -> string -> type_enc val adjust_type_enc : atp_format -> type_enc -> type_enc val is_lambda_free : term -> bool + val do_cheaply_conceal_lambdas : typ list -> term -> term val mk_aconns : atp_connective -> ('a, 'b, 'c, 'd) atp_formula list -> ('a, 'b, 'c, 'd) atp_formula diff -r 5fbe474b5da8 -r d95055489fce src/HOL/Tools/ATP/atp_waldmeister.ML --- a/src/HOL/Tools/ATP/atp_waldmeister.ML Sun Sep 07 09:49:05 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Sun Sep 07 14:39:23 2014 +0200 @@ -228,6 +228,7 @@ val waldmeister_true = "true" val waldmeister_false = "false" val waldmeister_skolemize_rule = "waldmeister_skolemize" +val lam_lift_waldmeister_prefix = "lambda_wm" val factsN = "Relevant facts" val helpersN = "Helper facts" @@ -245,13 +246,19 @@ fun mk_eq_true (trm as (Const (@{const_name HOL.eq}, _) $ _ $ _)) = (NONE,trm) | mk_eq_true trm = (SOME trm,HOLogic.mk_eq (trm, @{term True})) +val is_lambda_name = String.isPrefix lam_lifted_poly_prefix + +fun lookup table k = + List.find (fn (key, _) => key = k) table + (* Translation from Isabelle theorms and terms to ATP terms. *) fun trm_to_atp'' thy (Const (x, ty)) args = let - val ty_args = Sign.const_typargs thy (x,ty) + val ty_args = if is_lambda_name x then + [] else Sign.const_typargs thy (x,ty) in [ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x,ty_args)), []), args)] end @@ -285,7 +292,7 @@ (* Translation from ATP terms to Isabelle terms. *) -fun construct_term (name, args) = +fun construct_term thy (name, args) = let val prefix = String.sub (name, 0) val encoded_name = String.extract(name,1,NONE) @@ -294,8 +301,18 @@ if prefix = const_prefix then let val (const_name,ty_args) = decode_const encoded_name + val const_trans_name = + if is_lambda_name const_name then + lam_lift_waldmeister_prefix ^ + String.extract(const_name,size lam_lifted_poly_prefix,NONE) + else + const_name in - Const (const_name,Sign.const_instance @{theory } (* FIXME? *) (const_name, ty_args)) + Const (const_trans_name, + if is_lambda_name const_name then + dummyT + else + Sign.const_instance thy (const_name, ty_args)) end else if prefix = free_prefix then Free (encoded_name, dummy_fun_type ()) @@ -303,36 +320,35 @@ Var ((name, 0), dummy_fun_type ()) (* Use name instead of encoded_name because Waldmeister renames free variables. *) else if name = waldmeister_equals then - case args of - [_, _] => - eq_const dummyT + (case args of + [_, _] => eq_const dummyT | _ => raise FailureMessage (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ - Int.toString (length args)) + Int.toString (length args))) else if name = waldmeister_true then - @{term "True"} + @{term True} else if name = waldmeister_false then - @{term "False"} + @{term False} else raise FailureMessage (WM_ERROR_MSG ^ "Unknown name prefix when parsing Waldmeister proof: name = " ^ name) end -and atp_to_trm' (ATerm ((name,_), args)) = +and atp_to_trm' thy (ATerm ((name,_), args)) = (case args of - [] => construct_term (name, args) - | _ => Term.list_comb (construct_term (name, args), map atp_to_trm' args)) - | atp_to_trm' _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm' expects ATerm") + [] => construct_term thy (name, args) + | _ => Term.list_comb (construct_term thy (name, args), map (atp_to_trm' thy) args)) + | atp_to_trm' _ _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm' expects ATerm") -fun atp_to_trm (ATerm (("equal", _), [lhs, rhs])) = - mk_eq (atp_to_trm' lhs, atp_to_trm' rhs) - | atp_to_trm (ATerm (("$true", _), _)) = @{term True} - | atp_to_trm _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm expects ATerm") +fun atp_to_trm thy (ATerm (("equal", _), [lhs, rhs])) = + mk_eq (atp_to_trm' thy lhs, atp_to_trm' thy rhs) + | atp_to_trm _ (ATerm (("$true", _), _)) = @{term True} + | atp_to_trm _ _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm expects ATerm") -fun formula_to_trm (AAtom aterm) = aterm |> atp_to_trm - | formula_to_trm (AConn (ANot, [aterm])) = - mk_not (formula_to_trm aterm) - | formula_to_trm _ = raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn") +fun formula_to_trm thy (AAtom aterm) = aterm |> atp_to_trm thy + | formula_to_trm thy (AConn (ANot, [aterm])) = + mk_not (formula_to_trm thy aterm) + | formula_to_trm _ _ = raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn") (* Abstract translation *) @@ -389,13 +405,15 @@ val (ctxt'',sko_conditions) = map_ctxt (skolemize false) ctxt' conditions : Proof.context * (term list * term) list - val sko_eq_facts = map (apsnd (apsnd mk_eq_true)) sko_facts : + val post_skolem = do_cheaply_conceal_lambdas [] + + val sko_eq_facts = map (apsnd (apsnd (mk_eq_true #> apsnd post_skolem))) sko_facts : (string * (term list * (term option * term))) list - val sko_eq_conditions = map (apsnd mk_eq_true) sko_conditions + val sko_eq_conditions = map (apsnd (mk_eq_true #> apsnd post_skolem)) sko_conditions |> name_list conjecture_condition_name : (string * (term list * (term option * term))) list val (_,eq_conseq as (_,(non_eq_consequence,eq_consequence))) = - skolemize false ctxt'' consequence |> apsnd (apsnd mk_eq_true) : + skolemize false ctxt'' consequence |> apsnd (apsnd (mk_eq_true #> apsnd post_skolem)) : (Proof.context * (term list * (term option * term))) val sko_eq_info = @@ -428,14 +446,15 @@ val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])] - val (nice_problem, pool) = make_nice (@{print} problem) + val (nice_problem, pool) = make_nice problem in (nice_problem, Option.map snd pool |> the_default Symtab.empty, [], Symtab.empty, sko_eq_info) end fun termify_line ctxt (name, role, u, rule, deps) = let - val t = u |> formula_to_trm + val thy = Proof_Context.theory_of ctxt + val t = u |> formula_to_trm thy |> singleton (infer_formulas_types ctxt) |> HOLogic.mk_Trueprop in @@ -447,9 +466,7 @@ #> map (termify_line ctxt) #> repair_waldmeister_endgame -fun lookup table k = - List.find (fn (key, _) => key = k) table - + fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of SOME x => x | NONE => NONE @@ -461,24 +478,31 @@ name fun skolemization_steps info - (proof_step as ((waldmeister_name,isabelle_names), _, trm, rule, _)) = - case get_skolem_info info (map fix_name isabelle_names |> @{print}) of + (proof_step as ((waldmeister_name,isabelle_names), role, trm, rule, _)) = + case get_skolem_info info (map fix_name isabelle_names) of NONE => [proof_step] | SOME (_,([],_)) => [proof_step] | SOME (_,(step :: steps,_)) => let + val is_conjecture = String.isPrefix "1.0.0.0" waldmeister_name + fun mk_steps _ [] = [] | mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^ Int.toString i),[]),Plain, - mk_Trueprop x,waldmeister_skolemize_rule,[(waldmeister_name ^ "_" ^ Int.toString (i-1),if i = 1 then isabelle_names else [])]) :: mk_steps (i+1) xs - val skolem_steps = ((waldmeister_name ^ "_0",isabelle_names),Unknown,mk_Trueprop step,rule,[]) :: + mk_Trueprop (if is_conjecture then mk_not x else x),waldmeister_skolemize_rule, + [(waldmeister_name ^ "_" ^ Int.toString (i-1),if i = 1 then isabelle_names else [])]) + :: mk_steps (i+1) xs + val skolem_steps = ((waldmeister_name ^ "_0",isabelle_names),Unknown, + mk_Trueprop (if is_conjecture then mk_not step else step),rule,[]) :: mk_steps 1 steps in - skolem_steps @ [((waldmeister_name,[]), Unknown, trm, waldmeister_skolemize_rule, + if role = Conjecture then + [proof_step] + else + skolem_steps @ [((waldmeister_name,[]), Unknown, trm, waldmeister_skolemize_rule, [(waldmeister_name ^ "_" ^ Int.toString (length skolem_steps - 1),if length skolem_steps = 1 then isabelle_names else [])])] end -fun introduce_waldmeister_skolems info (proof_steps : (term, string) atp_step list) = (@{print} info; proof_steps |> tap (map @{print}) - |> map (skolemization_steps info) |> List.concat |> tap (map @{print})) - +fun introduce_waldmeister_skolems info (proof_steps : (term, string) atp_step list) = proof_steps + |> map (skolemization_steps info) |> List.concat end; \ No newline at end of file