1.1 --- a/src/Pure/Isar/proof.ML Tue May 31 11:53:36 2005 +0200
1.2 +++ b/src/Pure/Isar/proof.ML Tue May 31 11:53:37 2005 +0200
1.3 @@ -49,7 +49,8 @@
1.4 val level: state -> int
1.5 type method
1.6 val method: (thm list -> tactic) -> method
1.7 - val method_cases: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> method
1.8 + val method_cases:
1.9 + (thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq) -> method
1.10 val refine: (context -> method) -> state -> state Seq.seq
1.11 val refine_end: (context -> method) -> state -> state Seq.seq
1.12 val match_bind: (string list * string) list -> state -> state
1.13 @@ -157,7 +158,7 @@
1.14 locale_spec = NONE, ...}) = s ^ (if a = "" then "" else " " ^ a)
1.15 | kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _),
1.16 locale_spec = SOME (name, _), ...}) =
1.17 - s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
1.18 + s ^ " (in " ^ Locale.extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
1.19 | kind_name _ (Show _) = "show"
1.20 | kind_name _ (Have _) = "have";
1.21
1.22 @@ -280,10 +281,10 @@
1.23
1.24 (*
1.25 (* Jia: added here: get all goals from the state 10/01/05 *)
1.26 -fun find_all i (state as State (Node {goal = SOME goal, ...}, node::nodes)) =
1.27 +fun find_all i (state as State (Node {goal = SOME goal, ...}, node::nodes)) =
1.28 let val others = find_all (i+1) (State (node, nodes))
1.29 in
1.30 - (context_of state, (i, goal)) :: others
1.31 + (context_of state, (i, goal)) :: others
1.32 end
1.33 | find_all i (State (Node {goal = NONE, ...}, node :: nodes)) = find_all (i + 1) (State (node, nodes))
1.34 | find_all _ (state as State (_, [])) = [];
1.35 @@ -292,10 +293,10 @@
1.36
1.37 fun find_all_goals_ctxts state =
1.38 let val all_goals = find_all_goals state
1.39 - fun find_ctxt_g [] = []
1.40 - | find_ctxt_g ((ctxt, (_, ((_, (_, thm)), _)))::others) = (ctxt,thm) :: (find_ctxt_g others)
1.41 + fun find_ctxt_g [] = []
1.42 + | find_ctxt_g ((ctxt, (_, ((_, (_, thm)), _)))::others) = (ctxt,thm) :: (find_ctxt_g others)
1.43 in
1.44 - find_ctxt_g all_goals
1.45 + find_ctxt_g all_goals
1.46 end;
1.47 *)
1.48
1.49 @@ -348,16 +349,16 @@
1.50 (*Jia Meng: the modified version of enter_forward. *)
1.51 (*Jia Meng: atp: Proof.state -> unit *)
1.52 local
1.53 - fun atp state =
1.54 + fun atp state =
1.55 let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state
1.56 in
1.57 - (!atp_hook) (ctxt,thm)
1.58 + (!atp_hook) (ctxt,thm)
1.59 end;
1.60 -
1.61 +
1.62 in
1.63
1.64 - fun enter_forward state =
1.65 - if (!call_atp) then
1.66 + fun enter_forward state =
1.67 + if (!call_atp) then
1.68 ((atp state; enter_forward_aux state)
1.69 handle (STATE _) => enter_forward_aux state)
1.70 else (enter_forward_aux state);
1.71 @@ -415,7 +416,7 @@
1.72 (if mode <> Backward orelse null goal_facts then NONE else SOME goal_facts) @
1.73 [Pretty.str ("goal (" ^ kind_name (sign_of state) kind ^ prt_names names ^
1.74 levels_up (i div 2) ^ subgoals (Thm.nprems_of thm) ^ "):")] @
1.75 - pretty_goals_local ctxt begin_goal (true, !show_main_goal) (! Display.goals_limit) thm;
1.76 + pretty_goals_local ctxt begin_goal (true, ! show_main_goal) (! Display.goals_limit) thm;
1.77
1.78 val ctxt_prts =
1.79 if ! verbose orelse mode = Forward then ProofContext.pretty_context ctxt
1.80 @@ -444,7 +445,7 @@
1.81 (* datatype method *)
1.82
1.83 datatype method =
1.84 - Method of thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq;
1.85 + Method of thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq;
1.86
1.87 fun method tac = Method (fn facts => fn st => Seq.map (rpair []) (tac facts st));
1.88 val method_cases = Method;
1.89 @@ -454,25 +455,30 @@
1.90
1.91 local
1.92
1.93 +fun goalN i = "goal" ^ string_of_int i;
1.94 +fun goals st = map goalN (1 upto Thm.nprems_of st);
1.95 +
1.96 +fun no_goal_cases st = map (rpair NONE) (goals st);
1.97 +
1.98 +fun goal_cases st =
1.99 + RuleCases.make true NONE (Thm.sign_of_thm st, Thm.prop_of st) (goals st);
1.100 +
1.101 fun check_sign sg state =
1.102 if Sign.subsig (sg, sign_of state) then state
1.103 else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
1.104
1.105 -fun mk_goals_cases st =
1.106 - RuleCases.make true NONE (sign_of_thm st, prop_of st)
1.107 - (map (fn i => "goal" ^ string_of_int i) (1 upto nprems_of st));
1.108 -
1.109 fun gen_refine current_context meth_fun state =
1.110 let
1.111 - val (goal_ctxt, (_, ((result, (facts, thm)), x))) = find_goal state;
1.112 + val (goal_ctxt, (_, ((result, (facts, st)), x))) = find_goal state;
1.113 val Method meth = meth_fun (if current_context then context_of state else goal_ctxt);
1.114 -
1.115 - fun refn (thm', cases) =
1.116 + in
1.117 + meth facts st |> Seq.map (fn (st', meth_cases) =>
1.118 state
1.119 - |> check_sign (Thm.sign_of_thm thm')
1.120 - |> map_goal (ProofContext.add_cases (cases @ mk_goals_cases thm'))
1.121 - (K ((result, (facts, thm')), x));
1.122 - in Seq.map refn (meth facts thm) end;
1.123 + |> check_sign (Thm.sign_of_thm st')
1.124 + |> map_goal
1.125 + (ProofContext.add_cases (no_goal_cases st @ goal_cases st' @ meth_cases))
1.126 + (K ((result, (facts, st')), x)))
1.127 + end;
1.128
1.129 in
1.130
1.131 @@ -533,8 +539,8 @@
1.132 val ngoals = Thm.nprems_of raw_th;
1.133 val _ =
1.134 if ngoals = 0 then ()
1.135 - else (err (Pretty.string_of (Pretty.chunks (pretty_goals_local ctxt "" (true, !show_main_goal)
1.136 - (! Display.goals_limit) raw_th @
1.137 + else (err (Pretty.string_of (Pretty.chunks
1.138 + (pretty_goals_local ctxt "" (true, !show_main_goal) (! Display.goals_limit) raw_th @
1.139 [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
1.140
1.141 val {hyps, sign, ...} = Thm.rep_thm raw_th;
1.142 @@ -705,16 +711,14 @@
1.143 val (state', (lets, asms)) =
1.144 map_context_result (ProofContext.apply_case (get_case state name xs)) state;
1.145 val assumptions = asms |> map (fn (a, ts) =>
1.146 - ((if a = "" then "" else NameSpace.append name a, atts), map (rpair ([], [])) ts));
1.147 - val qnames = filter_out (equal "") (map (#1 o #1) assumptions);
1.148 + ((NameSpace.qualified name a, atts), map (rpair ([], [])) ts));
1.149 in
1.150 state'
1.151 |> add_binds_i lets
1.152 - |> map_context (ProofContext.qualified true)
1.153 + |> map_context (ProofContext.no_base_names o ProofContext.qualified_names)
1.154 |> assume_i assumptions
1.155 - |> map_context (ProofContext.hide_thms false qnames)
1.156 + |> map_context (ProofContext.restore_naming (context_of state))
1.157 |> (fn st => simple_note_thms name (the_facts st) st)
1.158 - |> map_context (ProofContext.restore_qualified (context_of state))
1.159 end;
1.160
1.161
1.162 @@ -771,7 +775,7 @@
1.163 |> map_context (ProofContext.add_cases
1.164 (if length props = 1 then
1.165 RuleCases.make true NONE (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
1.166 - else [(rule_contextN, RuleCases.empty)]))
1.167 + else [(rule_contextN, NONE)]))
1.168 |> auto_bind_goal props
1.169 |> (if is_chain state then use_facts else reset_facts)
1.170 |> new_block