isabelle: src/FOLP/ex/If.thy@0c51e0a6bc37 (annotated)

17480 fd19f77dcf60 converted to Isar theory format; wenzelm parents: 0 diff changeset	1	theory If
fd19f77dcf60 converted to Isar theory format; wenzelm parents: 0 diff changeset	2	imports FOLP
fd19f77dcf60 converted to Isar theory format; wenzelm parents: 0 diff changeset	3	begin
fd19f77dcf60 converted to Isar theory format; wenzelm parents: 0 diff changeset	4
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 25991 diff changeset	5	definition "if" :: "[o,o,o]=>o" where
17480 fd19f77dcf60 converted to Isar theory format; wenzelm parents: 0 diff changeset	6	"if(P,Q,R) == P&Q \| ~P&R"
fd19f77dcf60 converted to Isar theory format; wenzelm parents: 0 diff changeset	7
61337 4645502c3c64 fewer aliases for toplevel theorem statements; wenzelm parents: 60770 diff changeset	8	schematic_goal ifI:
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	9	assumes "!!x. x : P ==> f(x) : Q" "!!x. x : ~P ==> g(x) : R"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	10	shows "?p : if(P,Q,R)"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	11	apply (unfold if_def)
69593 3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 61337 diff changeset	12	apply (tactic \<open>fast_tac \<^context> (FOLP_cs addIs @{thms assms}) 1\<close>)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	13	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	14
61337 4645502c3c64 fewer aliases for toplevel theorem statements; wenzelm parents: 60770 diff changeset	15	schematic_goal ifE:
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	16	assumes 1: "p : if(P,Q,R)" and
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	17	2: "!!x y. [\| x : P; y : Q \|] ==> f(x, y) : S" and
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	18	3: "!!x y. [\| x : ~P; y : R \|] ==> g(x, y) : S"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	19	shows "?p : S"
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	20	apply (insert 1)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	21	apply (unfold if_def)
69593 3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 61337 diff changeset	22	apply (tactic \<open>fast_tac \<^context> (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1\<close>)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	23	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	24
61337 4645502c3c64 fewer aliases for toplevel theorem statements; wenzelm parents: 60770 diff changeset	25	schematic_goal if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	26	apply (rule iffI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	27	apply (erule ifE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	28	apply (erule ifE)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	29	apply (rule ifI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	30	apply (rule ifI)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	31	oops
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	32
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 58957 diff changeset	33	ML \<open>val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}]\<close>
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	34
61337 4645502c3c64 fewer aliases for toplevel theorem statements; wenzelm parents: 60770 diff changeset	35	schematic_goal if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
69593 3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 61337 diff changeset	36	apply (tactic \<open>fast_tac \<^context> if_cs 1\<close>)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	37	done
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	38
61337 4645502c3c64 fewer aliases for toplevel theorem statements; wenzelm parents: 60770 diff changeset	39	schematic_goal nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
69593 3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 61337 diff changeset	40	apply (tactic \<open>fast_tac \<^context> if_cs 1\<close>)
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	41	done
17480 fd19f77dcf60 converted to Isar theory format; wenzelm parents: 0 diff changeset	42
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	43	end

author	Simon Wimmer <wimmers@in.tum.de>
	Thu, 18 Apr 2024 17:53:14 +0200
changeset 80137	0c51e0a6bc37
parent 69593	3dda49e08b9d
permissions	-rw-r--r--