353 |
353 |
354 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>" |
354 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>" |
355 by simp |
355 by simp |
356 |
356 |
357 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>" |
357 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>" |
358 apply (tactic {* simp_tac |
358 apply (tactic \<open>simp_tac |
359 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.upd_simproc]) 1*}) |
359 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.upd_simproc]) 1\<close>) |
360 done |
360 done |
361 |
361 |
362 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)" |
362 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)" |
363 apply (tactic {* simp_tac |
363 apply (tactic \<open>simp_tac |
364 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*}) |
364 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1\<close>) |
365 apply simp |
365 apply simp |
366 done |
366 done |
367 |
367 |
368 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)" |
368 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)" |
369 apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) |
369 apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) |
370 apply simp |
370 apply simp |
371 done |
371 done |
372 |
372 |
373 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)" |
373 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)" |
374 apply (tactic {* simp_tac |
374 apply (tactic \<open>simp_tac |
375 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*}) |
375 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1\<close>) |
376 apply simp |
376 apply simp |
377 done |
377 done |
378 |
378 |
379 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)" |
379 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)" |
380 apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) |
380 apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) |
381 apply simp |
381 apply simp |
382 done |
382 done |
383 |
383 |
384 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
384 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
385 apply (tactic {* simp_tac |
385 apply (tactic \<open>simp_tac |
386 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*}) |
386 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1\<close>) |
387 apply auto |
387 apply auto |
388 done |
388 done |
389 |
389 |
390 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
390 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
391 apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) |
391 apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) |
392 apply auto |
392 apply auto |
393 done |
393 done |
394 |
394 |
395 lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
395 lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
396 apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) |
396 apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) |
397 apply auto |
397 apply auto |
398 done |
398 done |
399 |
399 |
400 lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
400 lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
401 apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) |
401 apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) |
402 apply auto |
402 apply auto |
403 done |
403 done |
404 |
404 |
405 |
405 |
406 notepad |
406 notepad |
407 begin |
407 begin |
408 fix P r |
408 fix P r |
409 assume "P (A155 r)" |
409 assume "P (A155 r)" |
410 then have "\<exists>x. P x" |
410 then have "\<exists>x. P x" |
411 apply - |
411 apply - |
412 apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) |
412 apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) |
413 apply auto |
413 apply auto |
414 done |
414 done |
415 end |
415 end |
416 |
416 |
417 |
417 |
418 lemma "\<exists>r. A155 r = x" |
418 lemma "\<exists>r. A155 r = x" |
419 apply (tactic {*simp_tac |
419 apply (tactic \<open>simp_tac |
420 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.ex_sel_eq_simproc]) 1*}) |
420 (put_simpset HOL_basic_ss @{context} addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>) |
421 done |
421 done |
422 |
422 |
423 print_record many_A |
423 print_record many_A |
424 |
424 |
425 print_record many_B |
425 print_record many_B |