isabelle: src/FOLP/ex/If.thy@ee502a9b38aa (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
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	8	schematic_lemma 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)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	12	apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
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
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	15	schematic_lemma 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)
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	22	apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
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
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	25	schematic_lemma 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
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	33	ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	34
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	35	schematic_lemma 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	36	apply (tactic {* fast_tac if_cs 1 *})
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
36319 8feb2c4bef1a mark schematic statements explicitly; wenzelm parents: 35762 diff changeset	39	schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
25991 31b38a39e589 eliminated some legacy ML files; wenzelm parents: 19796 diff changeset	40	apply (tactic {* fast_tac if_cs 1 *})
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	desharna
	Mon, 06 Oct 2014 13:32:41 +0200
changeset 58560	ee502a9b38aa
parent 36319	8feb2c4bef1a
child 58957	c9e744ea8a38
permissions	-rw-r--r--