# HG changeset patch # User wenzelm # Date 1149537260 -7200 # Node ID 5fe7731d083695a7f9724e1a955babfbf398f888 # Parent ebc3b67fbd2ca81a0a7a56610aa0bc9c0199f70f allow non-trivial schematic goals (via embedded term vars); diff -r ebc3b67fbd2c -r 5fe7731d0836 src/CTT/ex/Synthesis.thy --- a/src/CTT/ex/Synthesis.thy Mon Jun 05 19:54:12 2006 +0200 +++ b/src/CTT/ex/Synthesis.thy Mon Jun 05 21:54:20 2006 +0200 @@ -11,7 +11,7 @@ begin text "discovery of predecessor function" -lemma "?a : SUM pred:?A . Eq(N, pred`0, 0) +lemma "?a : SUM pred:?A . Eq(N, pred`0, 0) * (PROD n:N. Eq(N, pred ` succ(n), n))" apply (tactic "intr_tac []") apply (tactic eqintr_tac) @@ -35,16 +35,16 @@ text "An interesting use of the eliminator, when" (*The early implementation of unification caused non-rigid path in occur check See following example.*) -lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) +lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) * Eq(?A, ?b(inr(i)), )" apply (tactic "intr_tac []") apply (tactic eqintr_tac) apply (rule comp_rls) apply (tactic "rew_tac []") -oops +done -(*Here we allow the type to depend on i. - This prevents the cycle in the first unification (no longer needed). +(*Here we allow the type to depend on i. + This prevents the cycle in the first unification (no longer needed). Requires flex-flex to preserve the dependence. Simpler still: make ?A into a constant type N*N.*) lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>) @@ -54,7 +54,7 @@ text "A tricky combination of when and split" (*Now handled easily, but caused great problems once*) lemma [folded basic_defs]: - "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl()), i) + "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl()), i) * Eq(?A, ?b(inr()), j)" apply (tactic "intr_tac []") apply (tactic eqintr_tac) @@ -63,33 +63,33 @@ apply (rule_tac [7] reduction_rls) apply (rule_tac [10] comp_rls) apply (tactic "typechk_tac []") -oops +done (*similar but allows the type to depend on i and j*) -lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl()), i) +lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl()), i) * Eq(?A(i,j), ?b(inr()), j)" oops (*similar but specifying the type N simplifies the unification problems*) -lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl()), i) +lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl()), i) * Eq(N, ?b(inr()), j)" oops text "Deriving the addition operator" lemma [folded arith_defs]: - "?c : PROD n:N. Eq(N, ?f(0,n), n) + "?c : PROD n:N. Eq(N, ?f(0,n), n) * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))" apply (tactic "intr_tac []") apply (tactic eqintr_tac) apply (rule comp_rls) apply (tactic "rew_tac []") -oops +done text "The addition function -- using explicit lambdas" lemma [folded arith_defs]: - "?c : SUM plus : ?A . - PROD x:N. Eq(N, plus`0`x, x) + "?c : SUM plus : ?A . + PROD x:N. Eq(N, plus`0`x, x) * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))" apply (tactic "intr_tac []") apply (tactic eqintr_tac) diff -r ebc3b67fbd2c -r 5fe7731d0836 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Jun 05 19:54:12 2006 +0200 +++ b/src/Pure/Isar/proof.ML Mon Jun 05 21:54:20 2006 +0200 @@ -144,7 +144,7 @@ goal: goal option} and goal = Goal of - {statement: string * term list list, (*goal kind and statement*) + {statement: string * term list list, (*goal kind and statement, starting with vars*) using: thm list, (*goal facts*) goal: thm, (*subgoals ==> statement*) before_qed: Method.text option, @@ -465,24 +465,25 @@ fun conclude_goal state goal propss = let + val thy = theory_of state; val ctxt = context_of state; + val string_of_term = ProofContext.string_of_term ctxt; + val string_of_thm = ProofContext.string_of_thm ctxt; val ngoals = Thm.nprems_of goal; - val _ = conditional (ngoals > 0) (fn () => - error (Pretty.string_of (Pretty.chunks + val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks (pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @ - [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])))); + [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))); + val _ = + (case subtract (op aconv) (ProofContext.assms_of ctxt) (#hyps (Thm.rep_thm goal)) of + [] => () + | hyps => error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term hyps))); - val {hyps, thy, ...} = Thm.rep_thm goal; - val bad_hyps = subtract (op aconv) (ProofContext.assms_of ctxt) hyps; - val _ = conditional (not (null bad_hyps)) (fn () => error ("Additional hypotheses:\n" ^ - cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps))); - - val th = Goal.conclude goal; - val _ = conditional (not (Pattern.matches thy - (Logic.mk_conjunction_list2 propss, Thm.prop_of th))) (fn () => - error ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th)); - in Conjunction.elim_precise (map length propss) th end; + val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal) + handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal); + val _ = Pattern.matches_seq thy (flat propss) (map Thm.prop_of (flat results)) orelse + error ("Proved a different theorem:\n" ^ string_of_thm th); + in results end; @@ -759,15 +760,25 @@ (* generic goals *) -fun check_tvars props state = - (case fold Term.add_tvars props [] of [] => () - | tvars => error ("Goal statement contains illegal schematic type variable(s): " ^ - commas (map (ProofContext.string_of_typ (context_of state) o TVar) tvars))); +local + +fun warn_tvars [] _ = () + | warn_tvars vs state = + warning ("Goal statement contains unbound schematic type variable(s): " ^ + commas (map (ProofContext.string_of_typ (context_of state) o TVar) vs)); -fun check_vars props state = - (case fold Term.add_vars props [] of [] => () - | vars => warning ("Goal statement contains unbound schematic variable(s): " ^ - commas (map (ProofContext.string_of_term (context_of state) o Var) vars))); +fun warn_vars [] _ = () + | warn_vars vs state = + warning ("Goal statement contains unbound schematic variable(s): " ^ + commas (map (ProofContext.string_of_term (context_of state) o Var) vs)); + +fun refine_terms n = + refine (Method.Basic (K (Method.RAW_METHOD + (K (HEADGOAL (PRECISE_CONJUNCTS n + (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))) + #> Seq.hd; + +in fun generic_goal prepp kind before_qed after_qed raw_propp state = let @@ -782,15 +793,21 @@ |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp))); val props = flat propss; - val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss)); + val dest_var = Term.dest_Var o Logic.dest_term; + val explicit_vars = map dest_var (#1 (take_prefix (can dest_var) props)); + val vars = rev ((fold o Term.fold_aterms) (fn Var v => + if member (op =) explicit_vars v then I else insert (op =) v | _ => I) props []); + + val propss' = map (Logic.mk_term o Var) vars :: propss; + val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss')); val after_qed' = after_qed |>> (fn after_local => fn results => map_context after_ctxt #> after_local results); in goal_state - |> tap (check_tvars props) - |> tap (check_vars props) + |> tap (warn_tvars (fold Term.add_tvars props [])) + |> tap (warn_vars vars) |> map_context (ProofContext.set_body true) - |> put_goal (SOME (make_goal ((kind, propss), [], goal, before_qed, after_qed'))) + |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed'))) |> map_context (ProofContext.add_cases false (AutoBind.cases thy props)) |> map_context (ProofContext.auto_bind_goal props) |> K chaining ? (`the_facts #-> using_facts) @@ -798,6 +815,7 @@ |> open_block |> put_goal NONE |> enter_backward + |> K (not (null vars)) ? refine_terms (length propss') |> K (null props) ? (refine (Method.Basic Method.assumption) #> Seq.hd) end; @@ -809,11 +827,10 @@ val outer_ctxt = context_of outer_state; val props = - flat stmt + flat (tl stmt) |> ProofContext.generalize goal_ctxt outer_ctxt; val results = - stmt - |> conclude_goal state goal + tl (conclude_goal state goal stmt) |> (Seq.map_list o Seq.map_list) (ProofContext.exports goal_ctxt outer_ctxt); in outer_state @@ -821,6 +838,8 @@ |> pair (after_qed, results) end; +end; + (* local goals *) diff -r ebc3b67fbd2c -r 5fe7731d0836 src/Pure/goal.ML --- a/src/Pure/goal.ML Mon Jun 05 19:54:12 2006 +0200 +++ b/src/Pure/goal.ML Mon Jun 05 21:54:20 2006 +0200 @@ -128,7 +128,6 @@ fun err msg = cat_error msg ("The error(s) above occurred for the goal statement:\n" ^ Sign.string_of_term thy (Term.list_all_free (params, statement))); - fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t) handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; @@ -139,19 +138,16 @@ val casms = map cert_safe asms; val prems = map (norm_hhf o Thm.assume) casms; - val cprop = cert_safe prop; - val goal = init cprop; - val goal' = case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed."; - val raw_result = finish goal' handle THM (msg, _, _) => err msg; - - val prop' = Thm.prop_of raw_result; - val _ = - if not (Pattern.matches thy (Envir.beta_norm (Thm.term_of cprop), prop')) - then err ("Proved a different theorem: " ^ Sign.string_of_term thy prop') - else (); + val res = + (case SINGLE (tac prems) (init (cert_safe prop)) of + NONE => err "Tactic failed." + | SOME res => res); + val [results] = + Conjunction.elim_precise [length props] (finish res) handle THM (msg, _, _) => err msg; + val _ = Pattern.matches_seq thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results) + orelse err ("Proved a different theorem: " ^ Sign.string_of_term thy (Thm.prop_of res)); in - hd (Conjunction.elim_precise [length props] raw_result) - |> map + results |> map (Drule.implies_intr_list casms #> Drule.forall_intr_list cparams #> norm_hhf