obtain_export: Thm.generalize;
authorwenzelm
Mon Jul 03 19:33:09 2006 +0200 (2006-07-03)
changeset 19978df19a7876183
parent 19977 ac1b062c81ac
child 19979 a0846edbe8b0
obtain_export: Thm.generalize;
guess: fixed handling of mixfixes of vars;
tuned;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Mon Jul 03 19:33:07 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Mon Jul 03 19:33:09 2006 +0200
     1.3 @@ -69,24 +69,21 @@
     1.4  *)
     1.5  fun obtain_export ctxt parms rule cprops thm =
     1.6    let
     1.7 -    val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
     1.8 -    val cparms = map (Thm.cterm_of thy) parms;
     1.9 +    val {thy, prop, ...} = Thm.rep_thm thm;
    1.10 +    val concl = Logic.strip_assums_concl prop;
    1.11 +    val bads = Term.fold_aterms (fn v as Free (x, _) =>
    1.12 +      if member (op =) parms x then insert (op aconv) v else I | _ => I) concl [];
    1.13  
    1.14 -    val thm' = thm
    1.15 -      |> Drule.implies_intr_protected cprops
    1.16 -      |> Drule.forall_intr_list cparms
    1.17 -      |> Drule.forall_elim_vars (maxidx + 1);
    1.18 +    val thm' = thm |> Drule.implies_intr_protected cprops;
    1.19 +    val thm'' = thm' |> Thm.generalize ([], parms) (Thm.maxidx_of thm' + 1);
    1.20      val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI);
    1.21 -
    1.22 -    val concl = Logic.strip_assums_concl prop;
    1.23 -    val bads = parms inter (Term.term_frees concl);
    1.24    in
    1.25      if not (null bads) then
    1.26        error ("Conclusion contains obtained parameters: " ^
    1.27          space_implode " " (map (ProofContext.string_of_term ctxt) bads))
    1.28      else if not (ObjectLogic.is_judgment thy concl) then
    1.29 -      error "Conclusion in obtained context must be object-logic judgments"
    1.30 -    else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    1.31 +      error "Conclusion in obtained context must be object-logic judgment"
    1.32 +    else (Tactic.rtac thm'' THEN' RANGE elim_tacs) 1 rule
    1.33    end;
    1.34  
    1.35  
    1.36 @@ -129,15 +126,13 @@
    1.37  
    1.38      fun occs_var x = Library.get_first (fn t =>
    1.39        Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
    1.40 -    val raw_parms = map occs_var xs;
    1.41 -    val parms = map_filter I raw_parms;
    1.42 -    val parm_names =
    1.43 -      map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
    1.44 +    val parms =
    1.45 +      map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (map occs_var xs ~~ xs);
    1.46  
    1.47      val that_name = if name = "" then thatN else name;
    1.48      val that_prop =
    1.49 -      Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, thesis))
    1.50 -      |> Library.curry Logic.list_rename_params (map #2 parm_names);
    1.51 +      Term.list_all_free (map #1 parms, Logic.list_implies (asm_props, thesis))
    1.52 +      |> Library.curry Logic.list_rename_params (map #2 parms);
    1.53      val obtain_prop =
    1.54        Logic.list_rename_params ([AutoBind.thesisN],
    1.55          Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
    1.56 @@ -146,7 +141,7 @@
    1.57        Proof.local_qed (NONE, false)
    1.58        #> Seq.map (`Proof.the_fact #-> (fn rule =>
    1.59          Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
    1.60 -        #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
    1.61 +        #> Proof.assm_i (K (obtain_export ctxt (map (#1 o #1) parms) rule)) asms));
    1.62    in
    1.63      state
    1.64      |> Proof.enter_forward
    1.65 @@ -173,15 +168,17 @@
    1.66  
    1.67  local
    1.68  
    1.69 -fun unify_params ctxt vars raw_rule =
    1.70 +fun unify_params vars thesis_name raw_rule ctxt =
    1.71    let
    1.72      val thy = ProofContext.theory_of ctxt;
    1.73 +    val certT = Thm.ctyp_of thy;
    1.74 +    val cert = Thm.cterm_of thy;
    1.75      val string_of_typ = ProofContext.string_of_typ ctxt;
    1.76      val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
    1.77  
    1.78      fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
    1.79  
    1.80 -    val maxidx = fold (Term.maxidx_typ o snd) vars ~1;
    1.81 +    val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
    1.82      val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
    1.83  
    1.84      val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
    1.85 @@ -194,26 +191,26 @@
    1.86          err ("Failed to unify variable " ^
    1.87            string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
    1.88            string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
    1.89 -    val (tyenv, _) = fold unify (vars ~~ Library.take (m, params))
    1.90 +    val (tyenv, _) = fold unify (map #1 vars ~~ Library.take (m, params))
    1.91        (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
    1.92      val norm_type = Envir.norm_type tyenv;
    1.93  
    1.94 -    val xs = map (apsnd norm_type) vars;
    1.95 +    val xs = map (apsnd norm_type o fst) vars;
    1.96      val ys = map (apsnd norm_type) (Library.drop (m, params));
    1.97      val ys' = map Term.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys;
    1.98 +    val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
    1.99  
   1.100      val instT =
   1.101        fold (Term.add_tvarsT o #2) params []
   1.102 -      |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T))));
   1.103 -    val rule' = rule |> Thm.instantiate (instT, []);
   1.104 +      |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
   1.105 +    val (rule' :: terms', ctxt') =
   1.106 +      Variable.import false (Thm.instantiate (instT, []) rule :: terms) ctxt;
   1.107  
   1.108 -    val tvars = Drule.tvars_of rule';
   1.109 -    val vars = subtract (op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
   1.110 -    val _ =
   1.111 -      if null tvars andalso null vars then ()
   1.112 -      else err ("Illegal schematic variable(s) " ^
   1.113 -        commas (map (string_of_typ o TVar) tvars @ map (string_of_term o Var) vars) ^ " in") rule';
   1.114 -  in (xs @ ys', rule') end;
   1.115 +    val vars' =
   1.116 +      map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
   1.117 +      (map snd vars @ replicate (length ys) NoSyn);
   1.118 +    val rule'' = Thm.generalize ([], [thesis_name]) (Thm.maxidx_of rule' + 1) rule';
   1.119 +  in ((vars', rule''), ctxt') end;
   1.120  
   1.121  fun inferred_type (x, _, mx) ctxt =
   1.122    let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
   1.123 @@ -230,7 +227,7 @@
   1.124      val ctxt = Proof.context_of state;
   1.125      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
   1.126  
   1.127 -    val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
   1.128 +    val ((thesis_name, _), thesis) = bind_judgment ctxt AutoBind.thesisN;
   1.129      val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> polymorphic;
   1.130  
   1.131      fun check_result th =
   1.132 @@ -242,20 +239,23 @@
   1.133        | [] => error "Goal solved -- nothing guessed."
   1.134        | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
   1.135  
   1.136 -    fun guess_context [_, raw_rule] =
   1.137 +    fun guess_context raw_rule state' =
   1.138        let
   1.139 -        val (parms, rule) = unify_params ctxt (map #1 vars) raw_rule;
   1.140 -        val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt;
   1.141 -        val ts = map (bind o Free) parms;
   1.142 +        val ((parms, rule), ctxt') =
   1.143 +          unify_params vars thesis_name raw_rule (Proof.context_of state');
   1.144 +        val (bind, _) = ProofContext.bind_fixes (map (#1 o #1) parms) ctxt';
   1.145 +        val ts = map (bind o Free o #1) parms;
   1.146          val ps = map dest_Free ts;
   1.147          val asms =
   1.148            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
   1.149            |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
   1.150          val _ = not (null asms) orelse error "Trivial result -- nothing guessed";
   1.151        in
   1.152 -        Proof.fix_i (map2 (fn (x, T) => fn (_, mx) => (x, SOME T, mx)) parms vars)
   1.153 -        #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)]
   1.154 -        #> Proof.add_binds_i AutoBind.no_facts
   1.155 +        state'
   1.156 +        |> Proof.map_context (K ctxt')
   1.157 +        |> Proof.fix_i (map (fn ((x, T), mx) => (x, SOME T, mx)) parms)
   1.158 +        |> Proof.assm_i (K (obtain_export ctxt' (map #1 ps) rule)) [(("", []), asms)]
   1.159 +        |> Proof.add_binds_i AutoBind.no_facts
   1.160        end;
   1.161  
   1.162      val goal = Var (("guess", 0), propT);
   1.163 @@ -264,7 +264,7 @@
   1.164      val before_qed = SOME (Method.primitive_text (Goal.conclude #> (fn th =>
   1.165        Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
   1.166      fun after_qed [[_, res]] =
   1.167 -      (check_result res; Proof.end_block #> Seq.map (`Proof.the_facts #-> guess_context));
   1.168 +      (check_result res; Proof.end_block #> Seq.map (guess_context res));
   1.169    in
   1.170      state
   1.171      |> Proof.enter_forward