--- 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)), <succ(0), 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,j>)), i)
+ "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
* Eq(?A, ?b(inr(<i,j>)), 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,j>)), i)
+lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
* Eq(?A(i,j), ?b(inr(<i,j>)), 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,j>)), i)
+lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
* Eq(N, ?b(inr(<i,j>)), 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)
--- 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 *)
--- 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