author wenzelm Mon Jun 05 21:54:20 2006 +0200 (2006-06-05) changeset 19774 5fe7731d0836 parent 19773 ebc3b67fbd2c child 19775 06cb6743adf6
allow non-trivial schematic goals (via embedded term vars);
 src/CTT/ex/Synthesis.thy file | annotate | diff | revisions src/Pure/Isar/proof.ML file | annotate | diff | revisions src/Pure/goal.ML file | annotate | diff | revisions
```     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  reduction_rls)
1.44  apply (rule_tac  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
```