src/Pure/Isar/obtain.ML
changeset 20308 ddb7e7129481
parent 20224 9c40a144ee0e
child 20804 0e2591606867
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Aug 02 22:27:01 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Aug 02 22:27:02 2006 +0200
     1.3 @@ -40,11 +40,13 @@
     1.4  signature OBTAIN =
     1.5  sig
     1.6    val obtain: string -> (string * string option * mixfix) list ->
     1.7 -    ((string * Attrib.src list) * (string * string list) list) list
     1.8 -    -> bool -> Proof.state -> Proof.state
     1.9 +    ((string * Attrib.src list) * (string * string list) list) list ->
    1.10 +    bool -> Proof.state -> Proof.state
    1.11    val obtain_i: string -> (string * typ option * mixfix) list ->
    1.12 -    ((string * attribute list) * (term * term list) list) list
    1.13 -    -> bool -> Proof.state -> Proof.state
    1.14 +    ((string * attribute list) * (term * term list) list) list ->
    1.15 +    bool -> Proof.state -> Proof.state
    1.16 +  val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
    1.17 +    (cterm list * thm list) * Proof.context
    1.18    val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.19    val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.20    val statement: (string * ((string * 'typ option) list * 'term list)) list ->
    1.21 @@ -57,7 +59,6 @@
    1.22  structure Obtain: OBTAIN =
    1.23  struct
    1.24  
    1.25 -
    1.26  (** obtain_export **)
    1.27  
    1.28  (*
    1.29 @@ -67,22 +68,28 @@
    1.30    --------
    1.31       B
    1.32  *)
    1.33 -fun obtain_export ctxt parms rule cprops thm =
    1.34 +fun obtain_export fix_ctxt rule xs _ As thm =
    1.35    let
    1.36 -    val {thy, prop, ...} = Thm.rep_thm thm;
    1.37 -    val concl = Logic.strip_assums_concl prop;
    1.38 -    val bads = Term.fold_aterms (fn v as Free (x, _) =>
    1.39 -      if member (op =) parms x then insert (op aconv) v else I | _ => I) concl [];
    1.40 +    val thy = ProofContext.theory_of fix_ctxt;
    1.41  
    1.42 -    val thm' = thm |> Drule.implies_intr_protected cprops |> Drule.generalize ([], parms);
    1.43 -    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI);
    1.44 +    val vs = map (dest_Free o Thm.term_of) xs;
    1.45 +    val bads = Term.fold_aterms (fn t as Free v =>
    1.46 +      if member (op =) vs v then insert (op aconv) t else I | _ => I) (Thm.prop_of thm) [];
    1.47 +    val _ = null bads orelse
    1.48 +      error ("Result contains obtained parameters: " ^
    1.49 +        space_implode " " (map (ProofContext.string_of_term fix_ctxt) bads));
    1.50 +    val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
    1.51 +      error "Conclusion in obtained context must be object-logic judgment";
    1.52 +
    1.53 +    val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
    1.54 +    val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
    1.55    in
    1.56 -    if not (null bads) then
    1.57 -      error ("Conclusion contains obtained parameters: " ^
    1.58 -        space_implode " " (map (ProofContext.string_of_term ctxt) bads))
    1.59 -    else if not (ObjectLogic.is_judgment thy concl) then
    1.60 -      error "Conclusion in obtained context must be object-logic judgment"
    1.61 -    else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    1.62 +    ((Drule.implies_elim_list thm' (map Thm.assume prems)
    1.63 +        |> Drule.implies_intr_list (map Drule.norm_hhf_cterm As)
    1.64 +        |> Drule.forall_intr_list xs)
    1.65 +      COMP rule)
    1.66 +    |> Drule.implies_intr_list prems
    1.67 +    |> singleton (Variable.export ctxt' fix_ctxt)
    1.68    end;
    1.69  
    1.70  
    1.71 @@ -91,27 +98,21 @@
    1.72  
    1.73  fun bind_judgment ctxt name =
    1.74    let
    1.75 -    val (bind, _) = ProofContext.bind_fixes [name] ctxt;
    1.76 +    val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt;
    1.77      val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
    1.78 -  in (v, t) end;
    1.79 +  in ((v, t), ctxt') end;
    1.80  
    1.81  val thatN = "that";
    1.82  
    1.83  local
    1.84  
    1.85 -fun find_free t x =
    1.86 -  let
    1.87 -    exception Found of term;
    1.88 -    fun find (t as Free (x', _)) = if x = x' then raise Found t else I
    1.89 -      | find _ = I;
    1.90 -  in (fold_aterms find t (); NONE) handle Found v => SOME v end;
    1.91 -
    1.92  fun gen_obtain prep_att prep_vars prep_propp
    1.93      name raw_vars raw_asms int state =
    1.94    let
    1.95      val _ = Proof.assert_forward_or_chain state;
    1.96 +    val thy = Proof.theory_of state;
    1.97 +    val cert = Thm.cterm_of thy;
    1.98      val ctxt = Proof.context_of state;
    1.99 -    val thy = Proof.theory_of state;
   1.100      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
   1.101  
   1.102      (*obtain vars*)
   1.103 @@ -128,17 +129,17 @@
   1.104  
   1.105      (*obtain statements*)
   1.106      val thesisN = Name.variant xs AutoBind.thesisN;
   1.107 -    val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
   1.108 +    val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
   1.109  
   1.110 -    fun occs_var x = Library.get_first (fn t =>
   1.111 -      find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
   1.112 -    val parms =
   1.113 -      map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (map occs_var xs ~~ xs);
   1.114 +    val asm_frees = fold Term.add_frees asm_props [];
   1.115 +    val parms = xs |> map (fn x =>
   1.116 +      let val x' = ProofContext.get_skolem fix_ctxt x
   1.117 +      in (x', the_default propT (AList.lookup (op =) asm_frees x')) end);
   1.118  
   1.119      val that_name = if name = "" then thatN else name;
   1.120      val that_prop =
   1.121 -      Term.list_all_free (map #1 parms, Logic.list_implies (asm_props, thesis))
   1.122 -      |> Library.curry Logic.list_rename_params (map #2 parms);
   1.123 +      Term.list_all_free (parms, Logic.list_implies (asm_props, thesis))
   1.124 +      |> Library.curry Logic.list_rename_params xs;
   1.125      val obtain_prop =
   1.126        Logic.list_rename_params ([AutoBind.thesisN],
   1.127          Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
   1.128 @@ -147,7 +148,7 @@
   1.129        Proof.local_qed (NONE, false)
   1.130        #> Seq.map (`Proof.the_fact #-> (fn rule =>
   1.131          Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
   1.132 -        #> Proof.assm_i (K (obtain_export ctxt (map (#1 o #1) parms) rule)) asms));
   1.133 +        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
   1.134    in
   1.135      state
   1.136      |> Proof.enter_forward
   1.137 @@ -170,11 +171,44 @@
   1.138  
   1.139  
   1.140  
   1.141 +(** tactical result **)
   1.142 +
   1.143 +fun check_result ctxt thesis th =
   1.144 +  (case Thm.prems_of th of
   1.145 +    [prem] =>
   1.146 +      if Thm.concl_of th aconv thesis andalso
   1.147 +        Logic.strip_assums_concl prem aconv thesis then th
   1.148 +      else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
   1.149 +  | [] => error "Goal solved -- nothing guessed."
   1.150 +  | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
   1.151 +
   1.152 +fun result tac facts ctxt =
   1.153 +  let
   1.154 +    val thy = ProofContext.theory_of ctxt;
   1.155 +    val cert = Thm.cterm_of thy;
   1.156 +
   1.157 +    val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt AutoBind.thesisN;
   1.158 +    val rule =
   1.159 +      (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
   1.160 +        NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
   1.161 +      | SOME th => check_result ctxt thesis (norm_hhf (Goal.conclude th)));
   1.162 +
   1.163 +    val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
   1.164 +    val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
   1.165 +    val obtain_rule = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
   1.166 +    val ((params, stmt), fix_ctxt) = Variable.focus (Thm.cprem_of obtain_rule 1) ctxt';
   1.167 +    val (prems, ctxt'') =
   1.168 +      Assumption.add_assms (obtain_export fix_ctxt obtain_rule params)
   1.169 +        (Drule.strip_imp_prems stmt) fix_ctxt;
   1.170 +  in ((params, prems), ctxt'') end;
   1.171 +
   1.172 +
   1.173 +
   1.174  (** guess **)
   1.175  
   1.176  local
   1.177  
   1.178 -fun unify_params vars thesis_name raw_rule ctxt =
   1.179 +fun unify_params vars thesis_var raw_rule ctxt =
   1.180    let
   1.181      val thy = ProofContext.theory_of ctxt;
   1.182      val certT = Thm.ctyp_of thy;
   1.183 @@ -209,13 +243,15 @@
   1.184      val instT =
   1.185        fold (Term.add_tvarsT o #2) params []
   1.186        |> map (TVar #> (fn T => (certT T, certT (norm_type T))));
   1.187 -    val ((_, rule' :: terms'), ctxt') =
   1.188 -      Variable.import false (Thm.instantiate (instT, []) rule :: terms) ctxt;
   1.189 +    val closed_rule = rule
   1.190 +      |> Thm.forall_intr (cert (Free thesis_var))
   1.191 +      |> Thm.instantiate (instT, []);
   1.192  
   1.193 +    val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
   1.194      val vars' =
   1.195        map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
   1.196        (map snd vars @ replicate (length ys) NoSyn);
   1.197 -    val rule'' = Drule.generalize ([], [thesis_name]) rule';
   1.198 +    val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
   1.199    in ((vars', rule''), ctxt') end;
   1.200  
   1.201  fun inferred_type (x, _, mx) ctxt =
   1.202 @@ -230,25 +266,17 @@
   1.203    let
   1.204      val _ = Proof.assert_forward_or_chain state;
   1.205      val thy = Proof.theory_of state;
   1.206 +    val cert = Thm.cterm_of thy;
   1.207      val ctxt = Proof.context_of state;
   1.208      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
   1.209  
   1.210 -    val ((thesis_name, _), thesis) = bind_judgment ctxt AutoBind.thesisN;
   1.211 +    val (thesis_var, thesis) = #1 (bind_judgment ctxt AutoBind.thesisN);
   1.212      val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> fst |> polymorphic ctxt;
   1.213  
   1.214 -    fun check_result th =
   1.215 -      (case Thm.prems_of th of
   1.216 -        [prem] =>
   1.217 -          if Thm.concl_of th aconv thesis andalso
   1.218 -            Logic.strip_assums_concl prem aconv thesis then ()
   1.219 -          else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
   1.220 -      | [] => error "Goal solved -- nothing guessed."
   1.221 -      | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
   1.222 -
   1.223      fun guess_context raw_rule state' =
   1.224        let
   1.225          val ((parms, rule), ctxt') =
   1.226 -          unify_params vars thesis_name raw_rule (Proof.context_of state');
   1.227 +          unify_params vars thesis_var raw_rule (Proof.context_of state');
   1.228          val (bind, _) = ProofContext.bind_fixes (map (#1 o #1) parms) ctxt';
   1.229          val ts = map (bind o Free o #1) parms;
   1.230          val ps = map dest_Free ts;
   1.231 @@ -260,17 +288,18 @@
   1.232          state'
   1.233          |> Proof.map_context (K ctxt')
   1.234          |> Proof.fix_i (map (fn ((x, T), mx) => (x, SOME T, mx)) parms)
   1.235 -        |> Proof.assm_i (K (obtain_export ctxt' (map #1 ps) rule)) [(("", []), asms)]
   1.236 +        |> `Proof.context_of |-> (fn fix_ctxt =>
   1.237 +            Proof.assm_i (obtain_export fix_ctxt rule (map cert ts)) [(("", []), asms)])
   1.238          |> Proof.add_binds_i AutoBind.no_facts
   1.239        end;
   1.240  
   1.241      val goal = Var (("guess", 0), propT);
   1.242      fun print_result ctxt' (k, [(s, [_, th])]) =
   1.243        ProofDisplay.print_results int ctxt' (k, [(s, [th])]);
   1.244 -    val before_qed = SOME (Method.primitive_text (Goal.conclude #> (fn th =>
   1.245 -      Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
   1.246 +    val before_qed = SOME (Method.primitive_text (Goal.conclude #> norm_hhf #>
   1.247 +        (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
   1.248      fun after_qed [[_, res]] =
   1.249 -      (check_result res; Proof.end_block #> Seq.map (guess_context res));
   1.250 +      Proof.end_block #> guess_context (check_result ctxt thesis res) #> Seq.single;
   1.251    in
   1.252      state
   1.253      |> Proof.enter_forward
   1.254 @@ -279,7 +308,7 @@
   1.255      |> Proof.chain_facts chain_facts
   1.256      |> Proof.local_goal print_result (K I) (apsnd (rpair I))
   1.257        "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])]
   1.258 -    |> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis)))) |> Seq.hd
   1.259 +    |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
   1.260    end;
   1.261  
   1.262  in