allow non-trivial schematic goals (via embedded term vars);
authorwenzelm
Mon Jun 05 21:54:20 2006 +0200 (2006-06-05)
changeset 197745fe7731d0836
parent 19773 ebc3b67fbd2c
child 19775 06cb6743adf6
allow non-trivial schematic goals (via embedded term vars);
src/CTT/ex/Synthesis.thy
src/Pure/Isar/proof.ML
src/Pure/goal.ML
     1.1 --- a/src/CTT/ex/Synthesis.thy	Mon Jun 05 19:54:12 2006 +0200
     1.2 +++ b/src/CTT/ex/Synthesis.thy	Mon Jun 05 21:54:20 2006 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  begin
     1.5  
     1.6  text "discovery of predecessor function"
     1.7 -lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)    
     1.8 +lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
     1.9                    *  (PROD n:N. Eq(N, pred ` succ(n), n))"
    1.10  apply (tactic "intr_tac []")
    1.11  apply (tactic eqintr_tac)
    1.12 @@ -35,16 +35,16 @@
    1.13  text "An interesting use of the eliminator, when"
    1.14  (*The early implementation of unification caused non-rigid path in occur check
    1.15    See following example.*)
    1.16 -lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)   
    1.17 +lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
    1.18                     * Eq(?A, ?b(inr(i)), <succ(0), i>)"
    1.19  apply (tactic "intr_tac []")
    1.20  apply (tactic eqintr_tac)
    1.21  apply (rule comp_rls)
    1.22  apply (tactic "rew_tac []")
    1.23 -oops
    1.24 +done
    1.25  
    1.26 -(*Here we allow the type to depend on i.  
    1.27 - This prevents the cycle in the first unification (no longer needed).  
    1.28 +(*Here we allow the type to depend on i.
    1.29 + This prevents the cycle in the first unification (no longer needed).
    1.30   Requires flex-flex to preserve the dependence.
    1.31   Simpler still: make ?A into a constant type N*N.*)
    1.32  lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
    1.33 @@ -54,7 +54,7 @@
    1.34  text "A tricky combination of when and split"
    1.35  (*Now handled easily, but caused great problems once*)
    1.36  lemma [folded basic_defs]:
    1.37 -  "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)    
    1.38 +  "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
    1.39                             *  Eq(?A, ?b(inr(<i,j>)), j)"
    1.40  apply (tactic "intr_tac []")
    1.41  apply (tactic eqintr_tac)
    1.42 @@ -63,33 +63,33 @@
    1.43  apply (rule_tac [7] reduction_rls)
    1.44  apply (rule_tac [10] comp_rls)
    1.45  apply (tactic "typechk_tac []")
    1.46 -oops
    1.47 +done
    1.48  
    1.49  (*similar but allows the type to depend on i and j*)
    1.50 -lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)  
    1.51 +lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
    1.52                            *   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
    1.53  oops
    1.54  
    1.55  (*similar but specifying the type N simplifies the unification problems*)
    1.56 -lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)   
    1.57 +lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
    1.58                            *   Eq(N, ?b(inr(<i,j>)), j)"
    1.59  oops
    1.60  
    1.61  
    1.62  text "Deriving the addition operator"
    1.63  lemma [folded arith_defs]:
    1.64 -  "?c : PROD n:N. Eq(N, ?f(0,n), n)   
    1.65 +  "?c : PROD n:N. Eq(N, ?f(0,n), n)
    1.66                    *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
    1.67  apply (tactic "intr_tac []")
    1.68  apply (tactic eqintr_tac)
    1.69  apply (rule comp_rls)
    1.70  apply (tactic "rew_tac []")
    1.71 -oops
    1.72 +done
    1.73  
    1.74  text "The addition function -- using explicit lambdas"
    1.75  lemma [folded arith_defs]:
    1.76 -  "?c : SUM plus : ?A .   
    1.77 -         PROD x:N. Eq(N, plus`0`x, x)   
    1.78 +  "?c : SUM plus : ?A .
    1.79 +         PROD x:N. Eq(N, plus`0`x, x)
    1.80                  *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
    1.81  apply (tactic "intr_tac []")
    1.82  apply (tactic eqintr_tac)
     2.1 --- a/src/Pure/Isar/proof.ML	Mon Jun 05 19:54:12 2006 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Mon Jun 05 21:54:20 2006 +0200
     2.3 @@ -144,7 +144,7 @@
     2.4      goal: goal option}
     2.5  and goal =
     2.6    Goal of
     2.7 -   {statement: string * term list list,     (*goal kind and statement*)
     2.8 +   {statement: string * term list list,     (*goal kind and statement, starting with vars*)
     2.9      using: thm list,                        (*goal facts*)
    2.10      goal: thm,                              (*subgoals ==> statement*)
    2.11      before_qed: Method.text option,
    2.12 @@ -465,24 +465,25 @@
    2.13  
    2.14  fun conclude_goal state goal propss =
    2.15    let
    2.16 +    val thy = theory_of state;
    2.17      val ctxt = context_of state;
    2.18 +    val string_of_term = ProofContext.string_of_term ctxt;
    2.19 +    val string_of_thm = ProofContext.string_of_thm ctxt;
    2.20  
    2.21      val ngoals = Thm.nprems_of goal;
    2.22 -    val _ = conditional (ngoals > 0) (fn () =>
    2.23 -      error (Pretty.string_of (Pretty.chunks
    2.24 +    val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
    2.25          (pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @
    2.26 -          [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
    2.27 +          [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
    2.28 +    val _ =
    2.29 +      (case subtract (op aconv) (ProofContext.assms_of ctxt) (#hyps (Thm.rep_thm goal)) of
    2.30 +        [] => ()
    2.31 +      | hyps => error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term hyps)));
    2.32  
    2.33 -    val {hyps, thy, ...} = Thm.rep_thm goal;
    2.34 -    val bad_hyps = subtract (op aconv) (ProofContext.assms_of ctxt) hyps;
    2.35 -    val _ = conditional (not (null bad_hyps)) (fn () => error ("Additional hypotheses:\n" ^
    2.36 -        cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps)));
    2.37 -
    2.38 -    val th = Goal.conclude goal;
    2.39 -    val _ = conditional (not (Pattern.matches thy
    2.40 -        (Logic.mk_conjunction_list2 propss, Thm.prop_of th))) (fn () =>
    2.41 -      error ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th));
    2.42 -  in Conjunction.elim_precise (map length propss) th end;
    2.43 +    val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal)
    2.44 +      handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal);
    2.45 +    val _ = Pattern.matches_seq thy (flat propss) (map Thm.prop_of (flat results)) orelse
    2.46 +      error ("Proved a different theorem:\n" ^ string_of_thm th);
    2.47 +  in results end;
    2.48  
    2.49  
    2.50  
    2.51 @@ -759,15 +760,25 @@
    2.52  
    2.53  (* generic goals *)
    2.54  
    2.55 -fun check_tvars props state =
    2.56 -  (case fold Term.add_tvars props [] of [] => ()
    2.57 -  | tvars => error ("Goal statement contains illegal schematic type variable(s): " ^
    2.58 -      commas (map (ProofContext.string_of_typ (context_of state) o TVar) tvars)));
    2.59 +local
    2.60 +
    2.61 +fun warn_tvars [] _ = ()
    2.62 +  | warn_tvars vs state =
    2.63 +      warning ("Goal statement contains unbound schematic type variable(s): " ^
    2.64 +        commas (map (ProofContext.string_of_typ (context_of state) o TVar) vs));
    2.65  
    2.66 -fun check_vars props state =
    2.67 -  (case fold Term.add_vars props [] of [] => ()
    2.68 -  | vars => warning ("Goal statement contains unbound schematic variable(s): " ^
    2.69 -      commas (map (ProofContext.string_of_term (context_of state) o Var) vars)));
    2.70 +fun warn_vars [] _ = ()
    2.71 +  | warn_vars vs state =
    2.72 +      warning ("Goal statement contains unbound schematic variable(s): " ^
    2.73 +        commas (map (ProofContext.string_of_term (context_of state) o Var) vs));
    2.74 +
    2.75 +fun refine_terms n =
    2.76 +  refine (Method.Basic (K (Method.RAW_METHOD
    2.77 +    (K (HEADGOAL (PRECISE_CONJUNCTS n
    2.78 +      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
    2.79 +  #> Seq.hd;
    2.80 +
    2.81 +in
    2.82  
    2.83  fun generic_goal prepp kind before_qed after_qed raw_propp state =
    2.84    let
    2.85 @@ -782,15 +793,21 @@
    2.86        |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
    2.87      val props = flat propss;
    2.88  
    2.89 -    val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss));
    2.90 +    val dest_var = Term.dest_Var o Logic.dest_term;
    2.91 +    val explicit_vars = map dest_var (#1 (take_prefix (can dest_var) props));
    2.92 +    val vars = rev ((fold o Term.fold_aterms) (fn Var v =>
    2.93 +      if member (op =) explicit_vars v then I else insert (op =) v | _ => I) props []);
    2.94 +
    2.95 +    val propss' = map (Logic.mk_term o Var) vars :: propss;
    2.96 +    val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss'));
    2.97      val after_qed' = after_qed |>> (fn after_local =>
    2.98        fn results => map_context after_ctxt #> after_local results);
    2.99    in
   2.100      goal_state
   2.101 -    |> tap (check_tvars props)
   2.102 -    |> tap (check_vars props)
   2.103 +    |> tap (warn_tvars (fold Term.add_tvars props []))
   2.104 +    |> tap (warn_vars vars)
   2.105      |> map_context (ProofContext.set_body true)
   2.106 -    |> put_goal (SOME (make_goal ((kind, propss), [], goal, before_qed, after_qed')))
   2.107 +    |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
   2.108      |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
   2.109      |> map_context (ProofContext.auto_bind_goal props)
   2.110      |> K chaining ? (`the_facts #-> using_facts)
   2.111 @@ -798,6 +815,7 @@
   2.112      |> open_block
   2.113      |> put_goal NONE
   2.114      |> enter_backward
   2.115 +    |> K (not (null vars)) ? refine_terms (length propss')
   2.116      |> K (null props) ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   2.117    end;
   2.118  
   2.119 @@ -809,11 +827,10 @@
   2.120      val outer_ctxt = context_of outer_state;
   2.121  
   2.122      val props =
   2.123 -      flat stmt
   2.124 +      flat (tl stmt)
   2.125        |> ProofContext.generalize goal_ctxt outer_ctxt;
   2.126      val results =
   2.127 -      stmt
   2.128 -      |> conclude_goal state goal
   2.129 +      tl (conclude_goal state goal stmt)
   2.130        |> (Seq.map_list o Seq.map_list) (ProofContext.exports goal_ctxt outer_ctxt);
   2.131    in
   2.132      outer_state
   2.133 @@ -821,6 +838,8 @@
   2.134      |> pair (after_qed, results)
   2.135    end;
   2.136  
   2.137 +end;
   2.138 +
   2.139  
   2.140  (* local goals *)
   2.141  
     3.1 --- a/src/Pure/goal.ML	Mon Jun 05 19:54:12 2006 +0200
     3.2 +++ b/src/Pure/goal.ML	Mon Jun 05 21:54:20 2006 +0200
     3.3 @@ -128,7 +128,6 @@
     3.4      fun err msg = cat_error msg
     3.5        ("The error(s) above occurred for the goal statement:\n" ^
     3.6          Sign.string_of_term thy (Term.list_all_free (params, statement)));
     3.7 -
     3.8      fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
     3.9        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    3.10  
    3.11 @@ -139,19 +138,16 @@
    3.12      val casms = map cert_safe asms;
    3.13      val prems = map (norm_hhf o Thm.assume) casms;
    3.14  
    3.15 -    val cprop = cert_safe prop;
    3.16 -    val goal = init cprop;
    3.17 -    val goal' = case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.";
    3.18 -    val raw_result = finish goal' handle THM (msg, _, _) => err msg;
    3.19 -
    3.20 -    val prop' = Thm.prop_of raw_result;
    3.21 -    val _ =
    3.22 -      if not (Pattern.matches thy (Envir.beta_norm (Thm.term_of cprop), prop'))
    3.23 -      then err ("Proved a different theorem: " ^ Sign.string_of_term thy prop')
    3.24 -      else ();
    3.25 +    val res =
    3.26 +      (case SINGLE (tac prems) (init (cert_safe prop)) of
    3.27 +        NONE => err "Tactic failed."
    3.28 +      | SOME res => res);
    3.29 +    val [results] =
    3.30 +      Conjunction.elim_precise [length props] (finish res) handle THM (msg, _, _) => err msg;
    3.31 +    val _ = Pattern.matches_seq thy (map (Thm.term_of o cert_safe) props) (map Thm.prop_of results)
    3.32 +      orelse err ("Proved a different theorem: " ^ Sign.string_of_term thy (Thm.prop_of res));
    3.33    in
    3.34 -    hd (Conjunction.elim_precise [length props] raw_result)
    3.35 -    |> map
    3.36 +    results |> map
    3.37        (Drule.implies_intr_list casms
    3.38          #> Drule.forall_intr_list cparams
    3.39          #> norm_hhf