21 spark_vc procedure_g_c_d_4 (*..select 1st VC for proof: *) |
21 spark_vc procedure_g_c_d_4 (*..select 1st VC for proof: *) |
22 proof - |
22 proof - |
23 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign) |
23 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign) |
24 (*^^^^^^^^^^^^-Syntax.read_props..Output.report |
24 (*^^^^^^^^^^^^-Syntax.read_props..Output.report |
25 ^^^^^^^^^^^^^^^^^-Proof.gen_have..Output.report 2x |
25 ^^^^^^^^^^^^^^^^^-Proof.gen_have..Output.report 2x |
26 ^^^^^^^^^^^^^^^^^^^^^^-have 0 \<le> c mod d*) |
26 ^^^^^^^^^^^^^^^^^^^^^^-"have 0 \<le> c mod d"*) |
27 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1 |
27 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1 |
28 (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-Proof.gen_show....Output.report 2x |
28 (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-Syntax.read_props..Output.report 2x |
29 ^^^^^^^^-Proof.gen_show..Output.report 2x*) |
29 ^^^^^^^^-Proof.gen_show..Output.report 2x*) |
30 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric]) |
30 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric]) |
31 (* ^^^ Successful attempt to solve goal by exported rule: 0 < c - c sdiv d * d*) |
31 (* ^^^ Successful attempt to solve goal by exported rule: 0 < c - c sdiv d * d*) |
32 next |
32 next |
33 from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2 |
33 from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2 |
53 # Specific traces seem to be extended by the subsequent one, |
53 # Specific traces seem to be extended by the subsequent one, |
54 e.g. from \<open>0 < d\<close> extended by have "0 \<le> c mod d" |
54 e.g. from \<open>0 < d\<close> extended by have "0 \<le> c mod d" |
55 but both NOT by ... by (rule pos_mod_sign) |
55 but both NOT by ... by (rule pos_mod_sign) |
56 # Private_Output.report seems to have "" as argument frequently |
56 # Private_Output.report seems to have "" as argument frequently |
57 # Output.report provided semantic annotations in Naproche; |
57 # Output.report provided semantic annotations in Naproche; |
58 thus ALL calls of Output.report (in src/Pure) are traced an show up at these elements: |
58 thus ALL calls of Output.report (in src/Pure) are traced and show up at these elements: |
59 proof x x . . . |
59 proof x x . . . |
60 from \<open>0 < d\<close> x . x x x |
60 from \<open>0 < d\<close> x . x x x |
61 have "0 \<le> c mod d" x . x x . |
61 have "0 \<le> c mod d" x . x x . |
62 by (rule pos_mod_sign) x x . . . |
62 by (rule pos_mod_sign) x x . . . |
63 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> x . x x x |
63 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> x . x x x |
73 | Token.syntax_generic |
73 | Token.syntax_generic |
74 Private_Output.report |
74 Private_Output.report |
75 \<close> |
75 \<close> |
76 |
76 |
77 subsection \<open>tracing calls of Output.report\<close> |
77 subsection \<open>tracing calls of Output.report\<close> |
78 text \<open> |
78 subsubsection \<open>click on "proof -"\<close> |
79 (*--------- click on "proof -" -------- |
79 text \<open> |
80 ### Private_Output.report keyword1 |
80 ### Private_Output.report keyword1 |
81 ### Private_Output.report language |
81 ### Private_Output.report language |
82 ### Private_Output.report entityo |
82 ### Private_Output.report entityo |
83 ### Private_Output.report operator |
83 ### Private_Output.report operator |
84 ### Token.syntax_generic, Scan.error |
84 ### Token.syntax_generic, Scan.error |
85 ### Private_Output.report |
85 ### Private_Output.report |
86 ### Token.syntax_generic, Scan.error |
86 ### Token.syntax_generic, Scan.error |
87 \<close> |
87 \<close> |
88 text \<open> |
88 subsubsection \<open>click on "from \<open>0 < d\<close>"\<close> |
89 (*--------- click on "from \<open>0 < d\<close>" -------- |
89 text \<open> |
90 ### Private_Output.report keyword1 |
90 ### Private_Output.report keyword1 |
91 ### Private_Output.report cartouch |
91 ### Private_Output.report cartouch |
92 ### Private_Output.report delimite |
92 ### Private_Output.report delimite |
93 ### Private_Output.report entityo |
93 ### Private_Output.report entityo |
94 ##### Syntax.read_props |
94 ##### Syntax.read_props |
99 ## calling Output.report |
99 ## calling Output.report |
100 ### Private_Output.report typingo ===== |
100 ### Private_Output.report typingo ===== |
101 ### Context_Position.report_generic //--- different to subsequent part below |
101 ### Context_Position.report_generic //--- different to subsequent part below |
102 ### Private_Output.report entityo |
102 ### Private_Output.report entityo |
103 \<close> |
103 \<close> |
104 text \<open> |
104 subsubsection \<open>click on "have "0 \<le> c mod d""\<close> |
105 (*--------- click on "have "0 \<le> c mod d"" -------- |
105 text \<open> |
106 ### Private_Output.report keyword1 |
106 ### Private_Output.report keyword1 |
107 ### Private_Output.report |
107 ### Private_Output.report |
108 ### Private_Output.report cartouch |
108 ### Private_Output.report cartouch |
109 ### Private_Output.report delimite |
109 ### Private_Output.report delimite |
110 ### Private_Output.report entityo |
110 ### Private_Output.report entityo |
111 ####-# Proof.gen_have |
111 ####-# Proof.gen_have |
|
112 ###-# Proof_Context.prep_statement |
|
113 ###-# Proof_Context.prep_stmt |
112 ##### Syntax.read_props |
114 ##### Syntax.read_props |
113 #### Syntax_Phases.check_props |
115 #### Syntax_Phases.check_props |
114 ### Syntax_Phases.check_terms |
116 ### Syntax_Phases.check_terms |
115 ### Syntax_Phases.check_typs |
117 ### Syntax_Phases.check_typs |
116 ### Syntax_Phases.check_typs |
118 ### Syntax_Phases.check_typs |
118 ### Private_Output.report typingo =====//--- different to previous part above |
120 ### Private_Output.report typingo =====//--- different to previous part above |
119 ##### Syntax.read_props |
121 ##### Syntax.read_props |
120 #### Syntax_Phases.check_props |
122 #### Syntax_Phases.check_props |
121 ### Syntax_Phases.check_terms |
123 ### Syntax_Phases.check_terms |
122 ### Syntax_Phases.check_typs |
124 ### Syntax_Phases.check_typs |
123 ## calling Output.report\<close> |
125 ## calling Output.report |
|
126 \<close> |
|
127 subsubsection \<open>click on "with \<open>0 \<le> c\<close> \<open>0 < d\<close> .."\<close> |
|
128 text \<open> |
|
129 ##### Syntax.read_props |
|
130 #### Syntax_Phases.check_props |
|
131 ### Syntax_Phases.check_terms |
|
132 ### Syntax_Phases.check_typs |
|
133 ### Syntax_Phases.check_typs |
|
134 ## calling Output.report |
|
135 ##### Syntax.read_props |
|
136 #### Syntax_Phases.check_props |
|
137 ### Syntax_Phases.check_terms |
|
138 ### Syntax_Phases.check_typs |
|
139 ### Syntax_Phases.check_typs |
|
140 ## calling Output.report |
|
141 ##### Syntax.read_props |
|
142 #### Syntax_Phases.check_props |
|
143 ### Syntax_Phases.check_terms |
|
144 ### Syntax_Phases.check_typs |
|
145 ### Syntax_Phases.check_typs |
|
146 ## calling Output.report |
|
147 \<close> |
|
148 subsubsection \<open>click on "show ?C1"\<close> |
|
149 text \<open> |
|
150 ###### Proof.gen_show |
|
151 ##### Syntax.read_props |
|
152 #### Syntax_Phases.check_props |
|
153 ### Syntax_Phases.check_terms |
|
154 ### Syntax_Phases.check_typs |
|
155 ### Syntax_Phases.check_typs |
|
156 ## calling Output.report |
|
157 ##### Syntax.read_props |
|
158 #### Syntax_Phases.check_props |
|
159 ### Syntax_Phases.check_terms |
|
160 ### Syntax_Phases.check_typs |
|
161 ## calling Output.report |
|
162 \<close> |
|
163 |
|
164 subsection \<open>fill gaps in traces \<close> |
|
165 subsubsection \<open>at beginning of "have "0 \<le> c mod d""\<close> |
|
166 text \<open> |
|
167 WHAT HAS BEEN OBSERVED / DONE |
|
168 click on "have "0 \<le> c mod d"" traces ####-# Proof.gen_have. |
|
169 "gen_have" occurs only in proof.ML, there is NO "open Proof" in src/Pure |
|
170 "gen_have" is ONLY called by Proof.have, Proof.have_cmd |
|
171 Proof.have, Proof.have_cmd are not re-used in proof.ML; |
|
172 Proof.have is ONLY called by Obtain.gen_consider, Obtain.gen_obtain |
|
173 Obtain.gen_consider, Obtain.gen_obtain DO NOT SHOW UP IN traces ?!? |
|
174 TODO |
|
175 TODO |
|
176 TODO |
|
177 TODO |
|
178 \<close> |
|
179 |
|
180 subsubsection \<open>between Proof.gen_have .. Syntax.read_props\<close> |
|
181 text \<open> |
|
182 WHAT HAS BEEN OBSERVED / DONE (search bottom up..) |
|
183 Syntax.read_props callers.. |
|
184 in Syntax.: |
|
185 read_prop |
|
186 read_prop_global: not in trace--// |
|
187 in src/Pure (NO "open Syntax") |
|
188 Expression.read_full_context_statement not in trace--// |
|
189 Proof_Context.read_propp not in trace--// |
|
190 ML_Thms: val _ = Theory.setup..thm_binding "lemma"..propss: |
|
191 ?in trace ?!? |
|
192 TODO ?!? |
|
193 TODO ?!? |
|
194 TODO ?!? |
|
195 TODO |
|
196 TODO ^v^v^v^v^v^v^v^v^--- gap to be closed (by insertion into above) |
|
197 TODO |
|
198 Proof_Context.prep_statement callers.. |
|
199 in Proof_Context.: |
|
200 cert_statement not in trace--// |
|
201 read_statement not in trace--// |
|
202 in src/Pure (NO "open Proof_Context") ..\<nexists> ----------// |
|
203 TODO ?!? |
|
204 TODO ?!? |
|
205 TODO ?!? |
|
206 \<close> |
124 |
207 |
125 subsection \<open>signatures of the traced callers of Private_Output.report\<close> |
208 subsection \<open>signatures of the traced callers of Private_Output.report\<close> |
126 declare [[ML_print_depth = 99999]] |
209 (** )declare [[ML_print_depth = 99999]]( **) |
127 ML \<open> |
210 ML \<open> |
128 \<close> ML \<open> |
211 \<close> ML \<open> |
129 Token.syntax_generic : 'a Token.context_parser -> Token.src -> Context.generic -> |
212 (*'a \<rightarrow> term, *) |
130 'a * Context.generic; |
213 Token.syntax_generic : 'a Token.context_parser -> |
|
214 Token.src -> Context.generic -> 'a * Context.generic; |
|
215 Token.syntax_generic : (Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)) -> |
|
216 Token.src -> Context.generic -> 'a * Context.generic; |
131 Context_Position.report_generic: Context.generic -> Position.T -> Markup.T -> unit; |
217 Context_Position.report_generic: Context.generic -> Position.T -> Markup.T -> unit; |
132 Private_Output.report : string(*= markup*) list -> unit; |
218 Private_Output.report : string(*= markup*) list -> unit; |
133 (*Syntax_Phases.check_typs : Proof.context -> typ list -> typ list; ..local*) |
219 (*Syntax_Phases.check_typs : Proof.context -> typ list -> typ list; ..local*) |
134 (*Syntax_Phases.check_terms : Proof.context -> term list -> term list; ..local*) |
220 (*Syntax_Phases.check_terms : Proof.context -> term list -> term list; ..local*) |
135 Syntax.check_typs : Proof.context -> typ list -> typ list; |
221 Syntax.check_typs : Proof.context -> typ list -> typ list; |
195 Syntax.read_prop_global |
282 Syntax.read_prop_global |
196 ML_Thms Theory.setup ML_Antiquotation.declaration |
283 ML_Thms Theory.setup ML_Antiquotation.declaration |
197 Proof_Context.read_propp |
284 Proof_Context.read_propp |
198 Expression.read_full_context_statement |
285 Expression.read_full_context_statement |
199 |
286 |
200 ??? where else might Syntax.read_props be called ??? |
287 ??? where else might Syntax.read_props be called: found ####-# Proof.gen_have |
201 |
288 |
202 search top down |
289 search top down |
203 "from" :: prf_chain % "proof" only def.in Pure.thy: "from" "with" |
290 "from" :: prf_chain % "proof" only def.in Pure.thy, \<notin> src/Pure |
|
291 "with" :: prf_chain % "proof" only def.in Pure.thy, \<in> src/Pure in ml_lex.ML/scala |
204 "have" :: prf_goal % "proof" -"- + Proof.have |
292 "have" :: prf_goal % "proof" -"- + Proof.have |
205 "show" :: prf_asm_goal % "proof" -"- + Proof.show |
293 "show" :: prf_asm_goal % "proof" -"- + Proof.show |
206 \<close> |
|
207 |
|
208 subsection \<open>TODO: fill gap Syntax.read_props .. Proof.gen_have\<close> |
|
209 text \<open> |
|
210 TODO: fill the gap in the trace between Syntax.read_props .. Proof.gen_have. |
|
211 \<close> |
|
212 |
|
213 subsection \<open>lookup calls of Proof.have.."have"\<close> |
|
214 text \<open> |
|
215 Proof.have |
|
216 Proof.have_cmd |
|
217 Proof.show |
|
218 Proof.show_cmd |
|
219 Obtain.gen_consider |
|
220 Obtain.gen_obtain |
|
221 |
|
222 ??? where else might Proof.have (current hd of trace) be called ??? |
|
223 NO "open Proof" in src/Pure |
|
224 !!! there are new trace elements Proof.* (found in other parts of spark_vc procedure_g_c_d_4) |
|
225 |
|
226 \<close> |
294 \<close> |
227 |
295 |
228 subsubsection \<open>TODO\<close> |
296 subsubsection \<open>TODO\<close> |
229 text \<open> |
297 text \<open> |
230 TODO |
298 TODO |