forked from wimmers/explore-subgoal
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Explorer.thy
594 lines (520 loc) · 20.6 KB
/
Explorer.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
(* Title: Explorer
Initial author: Florian Haftmann
Initial author: Fabian Immler
Maintainer: Mathias Fleury
License: ?
From: The isabelle-dev mailing list. "Re: [isabelle-dev] The coming release of Isabelle2017"
Link: http://www.mail-archive.com/[email protected]/msg07448.html
Remark that a similar version (with fewer variants) is now in Isabelle in the theory
"HOL-ex.Sketch_and_Explore".
*)
theory Explorer
imports Main
keywords "explore" "explore_have" "explore_lemma" "explore_context" "explore_subgoal" :: diag
begin
subsection \<open>Explore command\<close>
text \<open>This theory contains the definition of four tactics that work on goals
and put them in an Isar proof:
\<^item> \<open>explore\<close> generates an assume-show proof block
\<^item> \<open>explore_have\<close> generates an have-if-for block
\<^item> \<open>lemma\<close> generates a lemma-fixes-assumes-shows block
\<^item> \<open>explore_context\<close> is mostly meaningful on several goals: it combines assumptions and variables
between the goals to generate a context-fixes-begin-end bloc with lemmas in the middle. This
tactic is mostly useful when a lot of assumption and proof steps would be shared.
If you use any of those tactic or have an idea how to improve it, please send an email to the
current maintainer!
\<close>
ML \<open>
signature EXPLORER_LIB =
sig
datatype explorer_quote = QUOTES | GUILLEMOTS
val set_default_raw_param: theory -> theory
val default_raw_params: theory -> string * explorer_quote
val switch_to_cartouches: theory -> theory
val switch_to_quotes: theory -> theory
end
structure Explorer_Lib : EXPLORER_LIB =
struct
datatype explorer_quote = QUOTES | GUILLEMOTS
type raw_param = string * explorer_quote
val default_params = ("explorer_quotes", QUOTES)
structure Data = Theory_Data
(
type T = raw_param list
val empty = single default_params
val extend = I
fun merge data : T = AList.merge (op =) (K true) data
)
fun set_default_raw_param thy =
thy |> Data.map (AList.update (op =) default_params)
fun switch_to_quotes thy =
thy |> Data.map (AList.update (op =) ("explorer_quotes", QUOTES))
fun switch_to_cartouches thy =
thy |> Data.map (AList.update (op =) ("explorer_quotes", GUILLEMOTS))
fun default_raw_params thy =
Data.get thy |> hd
end
\<close>
setup Explorer_Lib.set_default_raw_param
ML \<open>
Explorer_Lib.default_raw_params @{theory}
\<close>
ML \<open>
signature EXPLORER =
sig
datatype explore_kind = HAVE_IF | ASSUME_SHOW | ASSUMES_SHOWS | CONTEXT | SUBGOAL
val explore: explore_kind -> Toplevel.state -> Proof.state
val enclose: Proof.context -> theory -> string -> string
end
structure Explorer: EXPLORER =
struct
datatype explore_kind = HAVE_IF | ASSUME_SHOW | ASSUMES_SHOWS | CONTEXT | SUBGOAL
fun split_clause t =
let
val (fixes, horn) = funpow_yield (length (Term.strip_all_vars t)) Logic.dest_all_global t;
val assms = Logic.strip_imp_prems horn;
val shows = Logic.strip_imp_concl horn;
in (fixes, assms, shows) end;
fun space_implode_with_line_break l =
if length l > 1 then
"\n " ^ space_implode " and\n " l
else
space_implode " and\n " l
fun keyword_fix HAVE_IF = " for "
| keyword_fix ASSUME_SHOW = " fix "
| keyword_fix ASSUMES_SHOWS = " fixes "
fun keyword_assume HAVE_IF = " if "
| keyword_assume ASSUME_SHOW = " assume "
| keyword_assume ASSUMES_SHOWS = " assumes "
fun keyword_goal HAVE_IF = ""
| keyword_goal ASSUME_SHOW = " show "
| keyword_goal ASSUMES_SHOWS = " shows "
fun subgoal_text ctxt aim enclosure (fixes, _, _) =
let
val kw_subgoal = "subgoal"
val kw_premises = "premises prems"
val kw_fix = "for"
val kw_goal = "using prems apply -"
val kw_sorry = "sorry"
val fixes_s = if null fixes then ""
else kw_fix ^ " " ^ space_implode " "
(map (fn (v, _) => v) fixes)
val lines = map (space_implode " ")
[
[kw_subgoal, kw_premises] @ (if fixes_s = "" then [] else [fixes_s]),
[kw_goal],
[kw_sorry]
]
in space_implode "\n " lines end;
fun isar_skeleton ctxt aim enclosure (fixes, assms, shows) =
let
val kw_fix = keyword_fix aim
val kw_assume = keyword_assume aim
val kw_goal = keyword_goal aim
val fixes_s = if null fixes then NONE
else SOME (kw_fix ^ space_implode " and "
(map (fn (v, T) => v ^ " :: " ^ enclosure (Syntax.string_of_typ ctxt T)) fixes));
val (_, ctxt') = Variable.add_fixes (map fst fixes) ctxt;
val assumes_s = if null assms then NONE
else SOME (kw_assume ^ space_implode_with_line_break
(map (enclosure o Syntax.string_of_term ctxt') assms))
val shows_s = (kw_goal ^ (enclosure o Syntax.string_of_term ctxt') shows)
val s =
(case aim of
HAVE_IF => (map_filter I [fixes_s], map_filter I [assumes_s], shows_s)
| ASSUME_SHOW => (map_filter I [fixes_s], map_filter I [assumes_s], shows_s ^" sorry")
| ASSUMES_SHOWS => (map_filter I [fixes_s], map_filter I [assumes_s], shows_s));
in
s
end;
fun generate_text ASSUME_SHOW context enclosure clauses =
let val lines = clauses
|> map (isar_skeleton context ASSUME_SHOW enclosure)
|> map (fn (a, b, c) => a @ b @ [c])
|> map cat_lines
in
("proof -" :: separate "next" lines @ ["qed"])
end
| generate_text HAVE_IF context enclosure clauses =
let
val raw_lines = map (isar_skeleton context HAVE_IF enclosure) clauses
fun treat_line (fixes_s, assumes_s, shows_s) =
let val combined_line = [shows_s] @ assumes_s @ fixes_s |> cat_lines
in
"have " ^ combined_line ^ "\nproof -\n show ?thesis sorry\nqed"
end
val raw_lines_with_proof_body = map treat_line raw_lines
in
separate "\n" raw_lines_with_proof_body
end
| generate_text ASSUMES_SHOWS context enclosure clauses =
let
val raw_lines = map (isar_skeleton context ASSUMES_SHOWS enclosure) clauses
fun treat_line (fixes_s, assumes_s, shows_s) =
let val combined_line = fixes_s @ assumes_s @ [shows_s] |> cat_lines
in
"lemma\n" ^ combined_line ^ "\nproof -\n show ?thesis sorry\nqed"
end
val raw_lines_with_lemma_and_proof_body = map treat_line raw_lines
in
separate "\n" raw_lines_with_lemma_and_proof_body
end
| generate_text SUBGOAL context enclosure clauses =
let
val lines = map (subgoal_text context SUBGOAL enclosure) clauses
in (separate "" lines @ ["done"]) end;
datatype proof_step = ASSUMPTION of term | FIXES of (string * typ) | GOAL of term
| Step of (proof_step * proof_step)
| Branch of (proof_step list)
datatype cproof_step = cASSUMPTION of term list | cFIXES of ((string * typ) list) | cGOAL of term
| cStep of (cproof_step * cproof_step)
| cBranch of (cproof_step list)
| cLemma of ((string * typ) list * term list * term)
fun explore_context_init (FIXES var :: cgoal) =
Step ((FIXES var), explore_context_init cgoal)
| explore_context_init (ASSUMPTION assm :: cgoal) =
Step ((ASSUMPTION assm), explore_context_init cgoal)
| explore_context_init ([GOAL show]) =
GOAL show
| explore_context_init (GOAL show :: cgoal) =
Step (GOAL show, explore_context_init cgoal)
fun branch_hd_fixes_is P (Step (FIXES var, _)) = P var
| branch_hd_fixes_is P _ = false
fun branch_hd_assms_is P (Step (ASSUMPTION var, _)) = P var
| branch_hd_assms_is P (Step (GOAL var, _)) = P var
| branch_hd_assms_is P (GOAL var) = P var
| branch_hd_assms_is _ _ = false
fun find_find_pos P brs =
let
fun f accs (br :: brs) = if P br then SOME (accs, br, brs)
else f (accs @ [br]) brs
| f _ [] = NONE
in f [] brs end
(* Term.exists_subterm (curry (op =) t) *)
fun explore_context_merge (FIXES var :: cgoal) (Step (FIXES var', steps)) =
if var = var' then
Step (FIXES var',
explore_context_merge cgoal steps)
else
Step (FIXES var', explore_context_merge cgoal steps)
| explore_context_merge (FIXES var :: cgoal) (Branch brs) =
(case find_find_pos (branch_hd_fixes_is (curry (op =) var)) brs of
SOME (b, (Step (fixe, st)), after) =>
Branch (b @ Step (fixe, explore_context_merge cgoal st) :: after)
| NONE =>
Branch (brs @ [Step (FIXES var, explore_context_init cgoal)]))
| explore_context_merge (FIXES var :: cgoal) steps =
Branch (steps :: [Step (FIXES var, explore_context_init cgoal)])
| explore_context_merge (ASSUMPTION assm :: cgoal) (Step (ASSUMPTION assm', steps)) =
if assm = assm' then
Step (ASSUMPTION assm', explore_context_merge cgoal steps)
else
Branch [Step (ASSUMPTION assm', steps), explore_context_init (ASSUMPTION assm :: cgoal)]
| explore_context_merge (ASSUMPTION assm :: cgoal) (Step (GOAL assm', steps)) =
if assm = assm' then
Step (GOAL assm', explore_context_merge cgoal steps)
else
Branch [Step (GOAL assm', steps), explore_context_init (ASSUMPTION assm :: cgoal)]
| explore_context_merge (ASSUMPTION assm :: cgoal) (GOAL assm') =
if assm = assm' then
Step (GOAL assm', explore_context_init cgoal)
else
Branch [GOAL assm', explore_context_init (ASSUMPTION assm :: cgoal)]
| explore_context_merge (ASSUMPTION assm :: cgoal) (Branch brs) =
(case find_find_pos (branch_hd_assms_is (fn t => assm = (t))) brs of
SOME (b, (Step (assm, st)), after) =>
Branch (b @ Step (assm, explore_context_merge cgoal st) :: after)
| SOME (b, (GOAL goal), after) =>
Branch (b @ Step (GOAL goal, explore_context_init cgoal) :: after)
| NONE =>
Branch (brs @ [Step (ASSUMPTION assm, explore_context_init cgoal)]))
| explore_context_merge (GOAL show :: []) (Step (GOAL show', steps)) =
if show = show' then
GOAL show'
else
Branch [Step (GOAL show', steps), GOAL show]
| explore_context_merge clause ps =
Branch [ps, explore_context_init clause]
fun explore_context_all (clause :: clauses) =
fold explore_context_merge clauses (explore_context_init clause)
fun convert_proof (ASSUMPTION a) = cASSUMPTION [a]
| convert_proof (FIXES a) = cFIXES [a]
| convert_proof (GOAL a) = cGOAL a
| convert_proof (Step (a, b)) = cStep (convert_proof a, convert_proof b)
| convert_proof (Branch brs) = cBranch (map convert_proof brs)
fun compress_proof (cStep (cASSUMPTION a, cStep (cASSUMPTION b, step))) =
compress_proof (cStep (cASSUMPTION (a @ b), compress_proof step))
| compress_proof (cStep (cFIXES a, cStep (cFIXES b, step))) =
compress_proof (cStep (cFIXES (a @ b), compress_proof step))
| compress_proof (cStep (cFIXES a, cStep (cASSUMPTION b,
cStep (cFIXES a', step)))) =
compress_proof (cStep (cFIXES (a @ a'), compress_proof (cStep (cASSUMPTION b, step))))
| compress_proof (cStep (a, b)) =
let
val a' = compress_proof a
val b' = compress_proof b
in
if a = a' andalso b = b' then cStep (a', b')
else compress_proof (cStep (a', b'))
end
| compress_proof (cBranch brs) =
cBranch (map compress_proof brs)
| compress_proof a = a
fun compress_proof2 (cStep (cFIXES a, cStep (cASSUMPTION b, cGOAL g))) =
cLemma (a, b, g)
| compress_proof2 (cStep (cASSUMPTION b, cGOAL g)) =
cLemma ([], b, g)
| compress_proof2 (cStep (cFIXES b, cGOAL g)) =
cLemma (b, [], g)
| compress_proof2 (cStep (a, b)) =
cStep (compress_proof2 a, compress_proof2 b)
| compress_proof2 (cBranch brs) =
cBranch (map compress_proof2 brs)
| compress_proof2 a = a
fun reorder_assumptions_wrt_fixes (fixes, assms, goal) =
let
fun depends_on t (fix) = Term.exists_subterm (curry (op =) (Term.Free fix)) t
fun depends_on_any t (fix :: fixes) = depends_on t fix orelse depends_on_any t fixes
| depends_on_any _ [] = false
fun insert_all_assms [] assms = map ASSUMPTION assms
| insert_all_assms fixes [] = map FIXES fixes
| insert_all_assms (fix :: fixes) (assm :: assms) =
if depends_on_any assm (fix :: fixes) then
FIXES fix :: insert_all_assms fixes (assm :: assms)
else
ASSUMPTION assm :: insert_all_assms (fix :: fixes) assms
in
insert_all_assms fixes assms @ [GOAL goal]
end
fun generate_context_proof ctxt enclosure (cFIXES fixes) =
let
val kw_fix = " fixes "
val fixes_s = if null fixes then NONE
else SOME (kw_fix ^ space_implode " and "
(map (fn (v, T) => v ^ " :: " ^ enclosure (Syntax.string_of_typ ctxt T)) fixes));
in the_default "" fixes_s end
| generate_context_proof ctxt enclosure (cASSUMPTION assms) =
let
val kw_assume = " assumes "
val assumes_s = if null assms then NONE
else SOME (kw_assume ^ space_implode_with_line_break
(map (enclosure o Syntax.string_of_term ctxt) assms))
in the_default "" assumes_s end
| generate_context_proof ctxt enclosure (cGOAL shows) =
hd (generate_text ASSUMES_SHOWS ctxt enclosure [([], [], shows)])
| generate_context_proof ctxt enclosure (cStep (cFIXES f, cStep (cASSUMPTION assms, st))) =
let val (_, ctxt') = Variable.add_fixes (map fst f) ctxt in
["context" ,
generate_context_proof ctxt enclosure (cFIXES f),
generate_context_proof ctxt' enclosure (cASSUMPTION assms),
"begin",
generate_context_proof ctxt' enclosure st,
"end"]
|> cat_lines
end
| generate_context_proof ctxt enclosure (cStep (cFIXES f, st)) =
let val (_, ctxt') = Variable.add_fixes (map fst f) ctxt in
["context" ,
generate_context_proof ctxt enclosure (cFIXES f),
"begin",
generate_context_proof ctxt' enclosure st,
"end"]
|> cat_lines
end
| generate_context_proof ctxt enclosure (cStep (cASSUMPTION assms, st)) =
["context" ,
generate_context_proof ctxt enclosure (cASSUMPTION assms),
"begin",
generate_context_proof ctxt enclosure st,
"end"]
|> cat_lines
| generate_context_proof ctxt enclosure (cStep (st, st')) =
[generate_context_proof ctxt enclosure st,
generate_context_proof ctxt enclosure st']
|> cat_lines
| generate_context_proof ctxt enclosure (cBranch st) =
separate "\n" (map (generate_context_proof ctxt enclosure) st)
|> cat_lines
| generate_context_proof ctxt enclosure (cLemma (fixes, assms, shows)) =
hd (generate_text ASSUMES_SHOWS ctxt enclosure [(fixes, assms, shows)])
(*
We cannot reuse ATP_Util.maybe_quote because it does not support selecting the
quoting function. But, this is a copy-paste of that function.
*)
val unquote_tvar = perhaps (try (unprefix "'"))
val unquery_var = perhaps (try (unprefix "?"))
val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
fun maybe_quote_with keywords quote y =
let val s = YXML.content_of y in
y |> ((not (is_long_identifier (unquote_tvar s)) andalso
not (is_long_identifier (unquery_var s))) orelse
Keyword.is_literal keywords s) ? quote
end
fun enclose ctxt thy =
let
val quote_type = Explorer_Lib.default_raw_params thy |> snd
in
(case quote_type of
Explorer_Lib.GUILLEMOTS => maybe_quote_with (Thy_Header.get_keywords' ctxt) cartouche
| Explorer_Lib.QUOTES => maybe_quote_with (Thy_Header.get_keywords' ctxt) quote)
end
fun explore aim st =
let
val thy = Toplevel.theory_of st
val quote_type = Explorer_Lib.default_raw_params thy |> snd
val ctxt = Toplevel.presentation_context st
val enclosure = enclose ctxt thy
val st = Toplevel.proof_of st
val { context, facts = _, goal } = Proof.goal st;
val goal_props = Logic.strip_imp_prems (Thm.prop_of goal);
val clauses = map split_clause goal_props;
val text =
if aim = CONTEXT then
(clauses
|> map reorder_assumptions_wrt_fixes
|> explore_context_all
|> convert_proof
|> compress_proof
|> compress_proof2
|> generate_context_proof context enclosure)
else cat_lines (generate_text aim context enclosure clauses);
val message = Active.sendback_markup_properties [] text;
in
st
|> tap (fn _ => Output.information ("Proof outline with cases:\n" ^ message))
end
end
val explore_cmd =
Toplevel.keep_proof (K () o Explorer.explore Explorer.ASSUME_SHOW)
val _ =
Outer_Syntax.command @{command_keyword "explore"}
"explore current goal state as Isar proof"
(Scan.succeed (explore_cmd))
val explore_have_cmd =
Toplevel.keep_proof (K () o Explorer.explore Explorer.HAVE_IF)
val _ =
Outer_Syntax.command @{command_keyword "explore_have"}
"explore current goal state as Isar proof with have, if and for"
(Scan.succeed explore_have_cmd)
val explore_lemma_cmd =
Toplevel.keep_proof (K () o Explorer.explore Explorer.ASSUMES_SHOWS)
val _ =
Outer_Syntax.command @{command_keyword "explore_lemma"}
"explore current goal state as Isar proof with lemma, fixes, assumes, and shows"
(Scan.succeed explore_lemma_cmd)
val explore_ctxt_cmd =
Toplevel.keep_proof (K () o Explorer.explore Explorer.CONTEXT)
val _ =
Outer_Syntax.command @{command_keyword "explore_context"}
"explore current goal state as Isar proof with context and lemmas"
(Scan.succeed explore_ctxt_cmd)
val explore_subgoal_cmd =
Toplevel.keep_proof (K () o Explorer.explore Explorer.SUBGOAL)
val _ =
Outer_Syntax.command @{command_keyword "explore_subgoal"}
"explore current goal state as apply-style subgoals"
(Scan.succeed explore_subgoal_cmd)
\<close>
subsection \<open>Examples\<close>
text \<open>You can choose cartouches\<close>
setup Explorer_Lib.switch_to_cartouches
lemma
"distinct xs \<Longrightarrow> P xs \<Longrightarrow> length (filter (\<lambda>x. x = y) xs) \<le> 1" for xs
apply (induct xs)
(* apply simp_all
apply auto *)
explore
(*
proof -
assume
\<open>distinct []\<close> and
\<open>P []\<close>
show \<open>length (filter (\<lambda>x. x = y) []) \<le> 1\<close> sorry
next
fix a :: \<open>'a\<close> and xs :: \<open>'a list\<close>
assume
\<open>distinct xs \<Longrightarrow> P xs \<Longrightarrow> length (filter (\<lambda>x. x = y) xs) \<le> 1\<close> and
\<open>distinct (a # xs)\<close> and
\<open>P (a # xs)\<close>
show \<open>length (filter (\<lambda>x. x = y) (a # xs)) \<le> 1\<close> sorry
qed
*)
explore_have
(*
have \<open>length (filter (\<lambda>x. x = y) []) \<le> 1\<close>
if
\<open>distinct []\<close> and
\<open>P []\<close>
proof -
show ?thesis sorry
qed
have \<open>length (filter (\<lambda>x. x = y) (a # xs)) \<le> 1\<close>
if
\<open>distinct xs \<Longrightarrow> P xs \<Longrightarrow> length (filter (\<lambda>x. x = y) xs) \<le> 1\<close> and
\<open>distinct (a # xs)\<close> and
\<open>P (a # xs)\<close>
for a :: \<open>'a\<close> and xs :: \<open>'a list\<close>
proof -
show ?thesis sorry
qed
*)
explore_lemma
(*
lemma
assumes
\<open>distinct []\<close> and
\<open>P []\<close>
shows \<open>length (filter (\<lambda>x. x = y) []) \<le> 1\<close>
proof -
show ?thesis sorry
qed
lemma
fixes a :: \<open>'a\<close> and xs :: \<open>'a list\<close>
assumes
\<open>distinct xs \<Longrightarrow> P xs \<Longrightarrow> length (filter (\<lambda>x. x = y) xs) \<le> 1\<close> and
\<open>distinct (a # xs)\<close> and
\<open>P (a # xs)\<close>
shows \<open>length (filter (\<lambda>x. x = y) (a # xs)) \<le> 1\<close>
proof -
show ?thesis sorry
qed
*)
explore_subgoal
oops
lemma
"\<And>x. A1 x \<Longrightarrow> A2"
"\<And>x y. A1 x \<Longrightarrow> B2 y"
"\<And>x y z s. B2 y \<Longrightarrow> A1 x \<Longrightarrow> C2 z \<Longrightarrow> C3 s"
"\<And>x y z s. B2 y \<Longrightarrow> A1 x \<Longrightarrow> C2 z \<Longrightarrow> C4 s"
"\<And>x y z s t. B2 y \<Longrightarrow> A1 x \<Longrightarrow> C2 z \<Longrightarrow> C4 s \<Longrightarrow> C3' t"
"\<And>x y z s t. B2 y \<Longrightarrow> A1 x \<Longrightarrow> C2 z \<Longrightarrow> C4 s \<Longrightarrow> C4' t"
"\<And>x y z s t. B2 y \<Longrightarrow> A1 x \<Longrightarrow> C2 z \<Longrightarrow> C4 s \<Longrightarrow> C5' t"
(* apply simp_all
apply auto *)
explore_context
explore_have
explore_lemma
oops
text \<open>You can also choose quotes\<close>
setup Explorer_Lib.switch_to_quotes
lemma
"distinct xs \<Longrightarrow> P xs \<Longrightarrow> length (filter (\<lambda>x. x = y) xs) \<le> 1" for xs
apply (induct xs)
(* apply simp_all
apply auto *)
explore
explore_have
explore_lemma
oops
text \<open>And switch back\<close>
setup Explorer_Lib.switch_to_cartouches
lemma
"distinct xs \<Longrightarrow> P xs \<Longrightarrow> sh \<Longrightarrow> length (filter (\<lambda>x. x = y) xs) \<le> 1" for xs
apply (induct xs)
(* apply simp_all
apply auto *)
explore
explore_have
explore_lemma
oops
end