88 val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list |
88 val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list |
89 -> state -> state |
89 -> state -> state |
90 val def: string -> context attribute list -> string * (string * string list) -> state -> state |
90 val def: string -> context attribute list -> string * (string * string list) -> state -> state |
91 val def_i: string -> context attribute list -> string * (term * term list) -> state -> state |
91 val def_i: string -> context attribute list -> string * (term * term list) -> state -> state |
92 val invoke_case: string * string option list * context attribute list -> state -> state |
92 val invoke_case: string * string option list * context attribute list -> state -> state |
93 val multi_theorem: |
93 val multi_theorem: string -> (theory -> theory) -> |
94 string -> (theory -> theory) -> |
|
95 (cterm list -> context -> context -> thm -> thm) -> |
94 (cterm list -> context -> context -> thm -> thm) -> |
96 (xstring * (Locale.multi_attribute list * Locale.multi_attribute list list)) option |
95 (xstring * (Attrib.src list * Attrib.src list list)) option -> |
97 -> bstring * theory attribute list -> Locale.multi_attribute Locale.element Locale.elem_expr list |
96 bstring * theory attribute list -> Locale.element Locale.elem_expr list |
98 -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list |
97 -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list |
99 -> theory -> state |
98 -> theory -> state |
100 val multi_theorem_i: |
99 val multi_theorem_i: string -> (theory -> theory) -> |
101 string -> (theory -> theory) -> |
|
102 (cterm list -> context -> context -> thm -> thm) -> |
100 (cterm list -> context -> context -> thm -> thm) -> |
103 (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option |
101 (string * (Attrib.src list * Attrib.src list list)) option |
104 -> bstring * theory attribute list |
102 -> bstring * theory attribute list |
105 -> Locale.multi_attribute Locale.element_i Locale.elem_expr list |
103 -> Locale.element_i Locale.elem_expr list |
106 -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list |
104 -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list |
107 -> theory -> state |
105 -> theory -> state |
108 val chain: state -> state |
106 val chain: state -> state |
109 val from_facts: thm list -> state -> state |
107 val from_facts: thm list -> state -> state |
110 val show: (bool -> state -> state) -> (state -> state Seq.seq) -> bool |
108 val show: (bool -> state -> state) -> (state -> state Seq.seq) -> bool |
117 -> ((string * context attribute list) * (string * (string list * string list)) list) list |
115 -> ((string * context attribute list) * (string * (string list * string list)) list) list |
118 -> state -> state |
116 -> state -> state |
119 val have_i: (state -> state Seq.seq) -> bool |
117 val have_i: (state -> state Seq.seq) -> bool |
120 -> ((string * context attribute list) * (term * (term list * term list)) list) list |
118 -> ((string * context attribute list) * (term * (term list * term list)) list) list |
121 -> state -> state |
119 -> state -> state |
122 val interpret: (context -> context) -> (state -> state Seq.seq) -> bool |
|
123 -> ((string * context attribute list) * (string * (string list * string list)) list) list |
|
124 -> state -> state |
|
125 val interpret_i: (context -> context) -> (state -> state Seq.seq) -> bool |
|
126 -> ((string * context attribute list) * (term * (term list * term list)) list) list |
|
127 -> state -> state |
|
128 val at_bottom: state -> bool |
120 val at_bottom: state -> bool |
129 val local_qed: (state -> state Seq.seq) |
121 val local_qed: (state -> state Seq.seq) |
130 -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit) |
122 -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit) |
131 -> state -> state Seq.seq |
123 -> state -> state Seq.seq |
132 val global_qed: (state -> state Seq.seq) -> state |
124 val global_qed: (state -> state Seq.seq) -> state |
150 |
140 |
151 type context = ProofContext.context; |
141 type context = ProofContext.context; |
152 |
142 |
153 |
143 |
154 (* type goal *) |
144 (* type goal *) |
155 |
|
156 (* CB: four kinds of Isar goals are distinguished: |
|
157 - Theorem: global goal in a theory, corresponds to Isar commands theorem, |
|
158 lemma and corollary, |
|
159 - Have: local goal in a proof, Isar command have |
|
160 - Show: local goal in a proof, Isar command show |
|
161 - Interpret: local goal in a proof, Isar command interpret |
|
162 *) |
|
163 |
145 |
164 datatype kind = |
146 datatype kind = |
165 Theorem of {kind: string, |
147 Theorem of {kind: string, |
166 theory_spec: (bstring * theory attribute list) * theory attribute list list, |
148 theory_spec: (bstring * theory attribute list) * theory attribute list list, |
167 locale_spec: (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option, |
149 locale_spec: (string * (Attrib.src list * Attrib.src list list)) option, |
168 view: cterm list * cterm list, (* target view and includes view *) |
150 view: cterm list * cterm list, (* target view and includes view *) |
169 thy_mod: theory -> theory, (* used in finish_global to modify final |
151 export: cterm list -> context -> context -> thm -> thm} | |
170 theory, normally set to I; used by |
|
171 registration command to activate |
|
172 registrations *) |
|
173 export: cterm list -> context -> context -> thm -> thm } | |
|
174 (* exporter to be used in finish_global *) |
152 (* exporter to be used in finish_global *) |
175 Show of context attribute list list | |
153 Show of context attribute list list | |
176 Have of context attribute list list | |
154 Have of context attribute list list; |
177 Interpret of {attss: context attribute list list, |
|
178 ctxt_mod: context -> context}; (* used in finish_local to modify final |
|
179 context *) |
|
180 |
|
181 (* CB: this function prints the goal kind (Isar command), name and target in |
|
182 the proof state *) |
|
183 |
155 |
184 fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _), |
156 fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _), |
185 locale_spec = NONE, ...}) = s ^ (if a = "" then "" else " " ^ a) |
157 locale_spec = NONE, ...}) = s ^ (if a = "" then "" else " " ^ a) |
186 | kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _), |
158 | kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _), |
187 locale_spec = SOME (name, _), ...}) = |
159 locale_spec = SOME (name, _), ...}) = |
188 s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a) |
160 s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a) |
189 | kind_name _ (Show _) = "show" |
161 | kind_name _ (Show _) = "show" |
190 | kind_name _ (Have _) = "have" |
162 | kind_name _ (Have _) = "have"; |
191 | kind_name _ (Interpret _) = "interpret"; |
|
192 |
163 |
193 type goal = |
164 type goal = |
194 (kind * (*result kind*) |
165 (kind * (*result kind*) |
195 string list * (*result names*) |
166 string list * (*result names*) |
196 term list list) * (*result statements*) |
167 term list list) * (*result statements*) |
209 datatype node = |
180 datatype node = |
210 Node of |
181 Node of |
211 {context: context, |
182 {context: context, |
212 facts: thm list option, |
183 facts: thm list option, |
213 mode: mode, |
184 mode: mode, |
214 goal: (goal * ((state -> state Seq.seq) * bool)) option} |
185 goal: (goal * (after_qed * bool)) option} |
215 and state = |
186 and state = |
216 State of |
187 State of |
217 node * (*current*) |
188 node * (*current*) |
218 node list; (*parents wrt. block structure*) |
189 node list (*parents wrt. block structure*) |
|
190 and after_qed = |
|
191 AfterQed of (state -> state Seq.seq) * (theory -> theory); |
219 |
192 |
220 fun make_node (context, facts, mode, goal) = |
193 fun make_node (context, facts, mode, goal) = |
221 Node {context = context, facts = facts, mode = mode, goal = goal}; |
194 Node {context = context, facts = facts, mode = mode, goal = goal}; |
222 |
195 |
223 |
196 |
772 |> enter_forward |
747 |> enter_forward |
773 |> opt_block |
748 |> opt_block |
774 |> map_context_result (fn ctxt => prepp (ctxt, raw_propp)); |
749 |> map_context_result (fn ctxt => prepp (ctxt, raw_propp)); |
775 val sign' = sign_of state'; |
750 val sign' = sign_of state'; |
776 |
751 |
|
752 val AfterQed (after_local, after_global) = after_qed; |
|
753 val after_qed' = AfterQed (after_local o map_context gen_binds, after_global); |
|
754 |
777 val props = List.concat propss; |
755 val props = List.concat propss; |
778 val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props); |
756 val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props); |
779 val goal = Drule.mk_triv_goal cprop; |
757 val goal = Drule.mk_triv_goal cprop; |
780 |
758 |
781 val tvars = foldr Term.add_term_tvars [] props; |
759 val tvars = foldr Term.add_term_tvars [] props; |
787 if null vars then () |
765 if null vars then () |
788 else warning ("Goal statement contains unbound schematic variable(s): " ^ |
766 else warning ("Goal statement contains unbound schematic variable(s): " ^ |
789 commas (map (ProofContext.string_of_term (context_of state')) vars)); |
767 commas (map (ProofContext.string_of_term (context_of state')) vars)); |
790 state' |
768 state' |
791 |> map_context (autofix props) |
769 |> map_context (autofix props) |
792 |> put_goal (SOME (((kind, names, propss), ([], goal)), |
770 |> put_goal (SOME (((kind, names, propss), ([], goal)), (after_qed', pr))) |
793 (after_qed o map_context gen_binds, pr))) |
|
794 |> map_context (ProofContext.add_cases |
771 |> map_context (ProofContext.add_cases |
795 (if length props = 1 then |
772 (if length props = 1 then |
796 RuleCases.make true NONE (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN] |
773 RuleCases.make true NONE (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN] |
797 else [(rule_contextN, RuleCases.empty)])) |
774 else [(rule_contextN, RuleCases.empty)])) |
798 |> auto_bind_goal props |
775 |> auto_bind_goal props |
800 |> new_block |
777 |> new_block |
801 |> enter_backward |
778 |> enter_backward |
802 end; |
779 end; |
803 |
780 |
804 (*global goals*) |
781 (*global goals*) |
805 fun global_goal prep kind thy_mod export raw_locale a elems concl thy = |
782 fun global_goal prep kind after_global export raw_locale a elems concl thy = |
806 let |
783 let |
807 val init = init_state thy; |
784 val init = init_state thy; |
808 val (opt_name, view, locale_ctxt, elems_ctxt, propp) = |
785 val (opt_name, view, locale_ctxt, elems_ctxt, propp) = |
809 prep (Option.map fst raw_locale) elems (map snd concl) (context_of init); |
786 prep (Option.map fst raw_locale) elems (map snd concl) (context_of init); |
810 in |
787 in |
811 init |
788 init |
812 |> open_block |
789 |> open_block |
813 |> map_context (K locale_ctxt) |
790 |> map_context (K locale_ctxt) |
814 |> open_block |
791 |> open_block |
815 |> map_context (K elems_ctxt) |
792 |> map_context (K elems_ctxt) |
816 (* CB: elems_ctxt is an extension of locale_ctxt, see prep_context_statement |
|
817 in locale.ML, naming there: ctxt and import_ctxt. *) |
|
818 |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees |
793 |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees |
819 (Theorem {kind = kind, |
794 (Theorem {kind = kind, |
820 theory_spec = (a, map (snd o fst) concl), |
795 theory_spec = (a, map (snd o fst) concl), |
821 locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)), |
796 locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)), |
822 view = view, |
797 view = view, |
823 thy_mod = thy_mod, |
|
824 export = export}) |
798 export = export}) |
825 Seq.single true (map (fst o fst) concl) propp |
799 (AfterQed (Seq.single, after_global)) |
|
800 true (map (fst o fst) concl) propp |
826 end; |
801 end; |
827 |
802 |
828 val multi_theorem = global_goal Locale.read_context_statement; |
803 val multi_theorem = global_goal Locale.read_context_statement; |
829 val multi_theorem_i = global_goal Locale.cert_context_statement; |
804 val multi_theorem_i = global_goal Locale.cert_context_statement; |
830 |
805 |
831 |
806 |
832 (*local goals*) |
807 (*local goals*) |
833 fun local_goal' prepp kind (check: bool -> state -> state) f pr args int state = |
808 fun local_goal' prepp kind (check: bool -> state -> state) after_local pr args int state = |
834 state |
809 state |
835 |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args)) |
810 |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args)) |
836 f pr (map (fst o fst) args) (map snd args) |
811 (AfterQed (after_local, I)) pr (map (fst o fst) args) (map snd args) |
837 |> warn_extra_tfrees state |
812 |> warn_extra_tfrees state |
838 |> check int; |
813 |> check int; |
839 |
814 |
840 fun local_goal prepp kind f pr args = local_goal' prepp kind (K I) f pr args false; |
815 fun local_goal prepp kind f pr args = local_goal' prepp kind (K I) f pr args false; |
841 |
816 |
842 val show = local_goal' ProofContext.bind_propp Show; |
817 val show = local_goal' ProofContext.bind_propp Show; |
843 val show_i = local_goal' ProofContext.bind_propp_i Show; |
818 val show_i = local_goal' ProofContext.bind_propp_i Show; |
844 val have = local_goal ProofContext.bind_propp Have; |
819 val have = local_goal ProofContext.bind_propp Have; |
845 val have_i = local_goal ProofContext.bind_propp_i Have; |
820 val have_i = local_goal ProofContext.bind_propp_i Have; |
846 fun interpret ctxt_mod = local_goal ProofContext.bind_propp |
821 |
847 (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod}); |
|
848 fun interpret_i ctxt_mod = local_goal ProofContext.bind_propp_i |
|
849 (fn attss => Interpret {attss = attss, ctxt_mod = ctxt_mod}); |
|
850 |
822 |
851 |
823 |
852 (** conclusions **) |
824 (** conclusions **) |
853 |
825 |
854 (* current goal *) |
826 (* current goal *) |
882 |
854 |
883 (* local_qed *) |
855 (* local_qed *) |
884 |
856 |
885 fun finish_local (print_result, print_rule) state = |
857 fun finish_local (print_result, print_rule) state = |
886 let |
858 let |
887 val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (after_qed, pr))) = current_goal state; |
859 val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (AfterQed (after_local, _), pr))) = |
|
860 current_goal state; |
888 val outer_state = state |> close_block; |
861 val outer_state = state |> close_block; |
889 val outer_ctxt = context_of outer_state; |
862 val outer_ctxt = context_of outer_state; |
890 |
863 |
891 val ts = List.concat tss; |
864 val ts = List.concat tss; |
892 val results = prep_result state ts raw_thm; |
865 val results = prep_result state ts raw_thm; |
893 val resultq = |
866 val resultq = |
894 results |> map (ProofContext.export false goal_ctxt outer_ctxt) |
867 results |> map (ProofContext.export false goal_ctxt outer_ctxt) |
895 |> Seq.commute |> Seq.map (Library.unflat tss); |
868 |> Seq.commute |> Seq.map (Library.unflat tss); |
896 |
869 |
897 val (attss, opt_solve, ctxt_mod) = |
870 val (attss, opt_solve) = |
898 (case kind of |
871 (case kind of |
899 Show attss => (attss, |
872 Show attss => (attss, |
900 export_goals goal_ctxt (if pr then print_rule else (K (K ()))) |
873 export_goals goal_ctxt (if pr then print_rule else (K (K ()))) results) |
901 results, I) |
874 | Have attss => (attss, Seq.single) |
902 | Have attss => (attss, Seq.single, I) |
|
903 | Interpret {attss, ctxt_mod} => (attss, Seq.single, ctxt_mod) |
|
904 | _ => err_malformed "finish_local" state); |
875 | _ => err_malformed "finish_local" state); |
905 in |
876 in |
906 conditional pr (fn () => print_result goal_ctxt |
877 conditional pr (fn () => print_result goal_ctxt |
907 (kind_name (sign_of state) kind, names ~~ Library.unflat tss results)); |
878 (kind_name (sign_of state) kind, names ~~ Library.unflat tss results)); |
908 outer_state |
879 outer_state |
909 |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts) |
880 |> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts) |
910 (* original version |
|
911 |> (fn st => Seq.map (fn res => |
881 |> (fn st => Seq.map (fn res => |
912 note_thmss_i ((names ~~ attss) ~~ |
882 note_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq) |
913 map (single o Thm.no_attributes) res) st) resultq) |
|
914 *) |
|
915 |> (fn st => Seq.map (fn res => |
|
916 st |> note_thmss_i ((names ~~ attss) ~~ |
|
917 map (single o Thm.no_attributes) res) |
|
918 |> map_context ctxt_mod) resultq) |
|
919 |> (Seq.flat o Seq.map opt_solve) |
883 |> (Seq.flat o Seq.map opt_solve) |
920 |> (Seq.flat o Seq.map after_qed) |
884 |> (Seq.flat o Seq.map after_local) |
921 end; |
885 end; |
922 |
886 |
923 fun local_qed finalize print state = |
887 fun local_qed finalize print state = |
924 state |
888 state |
925 |> end_proof false |
889 |> end_proof false |
929 |
893 |
930 (* global_qed *) |
894 (* global_qed *) |
931 |
895 |
932 fun finish_global state = |
896 fun finish_global state = |
933 let |
897 let |
934 val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state; |
898 val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (AfterQed (_, after_global), _))) = |
|
899 current_goal state; |
935 val locale_ctxt = context_of (state |> close_block); |
900 val locale_ctxt = context_of (state |> close_block); |
936 val theory_ctxt = context_of (state |> close_block |> close_block); |
901 val theory_ctxt = context_of (state |> close_block |> close_block); |
937 val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view), thy_mod, export} = |
902 val {kind = k, theory_spec = ((name, atts), attss), |
|
903 locale_spec, view = (target_view, elems_view), export} = |
938 (case kind of Theorem x => x | _ => err_malformed "finish_global" state); |
904 (case kind of Theorem x => x | _ => err_malformed "finish_global" state); |
|
905 val locale_name = Option.map fst locale_spec; |
939 |
906 |
940 val ts = List.concat tss; |
907 val ts = List.concat tss; |
941 val locale_results = map (export elems_view goal_ctxt locale_ctxt) |
908 val locale_results = map (export elems_view goal_ctxt locale_ctxt) |
942 (prep_result state ts raw_thm); |
909 (prep_result state ts raw_thm); |
943 |
910 |
954 |> Locale.add_thmss k loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss) |
921 |> Locale.add_thmss k loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss) |
955 |> (fn ((thy', ctxt'), res) => |
922 |> (fn ((thy', ctxt'), res) => |
956 if name = "" andalso null loc_atts then thy' |
923 if name = "" andalso null loc_atts then thy' |
957 else (thy', ctxt') |
924 else (thy', ctxt') |
958 |> (#1 o #1 o Locale.add_thmss k loc [((name, List.concat (map #2 res)), loc_atts)]))) |
925 |> (#1 o #1 o Locale.add_thmss k loc [((name, List.concat (map #2 res)), loc_atts)]))) |
959 |> Locale.smart_note_thmss k locale_spec |
926 |> Locale.smart_note_thmss k locale_name |
960 ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results)) |
927 ((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results)) |
961 |> (fn (thy, res) => (thy, res) |
928 |> (fn (thy, res) => (thy, res) |
962 |>> (#1 o Locale.smart_note_thmss k locale_spec |
929 |>> (#1 o Locale.smart_note_thmss k locale_name |
963 [((name, atts), [(List.concat (map #2 res), [])])])); |
930 [((name, atts), [(List.concat (map #2 res), [])])])); |
964 in (thy_mod theory', ((k, name), results')) end; |
931 in (after_global theory', ((k, name), results')) end; |
965 |
932 |
966 |
933 |
967 (*note: clients should inspect first result only, as backtracking may destroy theory*) |
934 (*note: clients should inspect first result only, as backtracking may destroy theory*) |
968 fun global_qed finalize state = |
935 fun global_qed finalize state = |
969 state |
936 state |