isabelle: src/Sequents/Washing.thy@f241e9cd26ca (annotated)

21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	1
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	2	(* $Id$ *)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	3
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	4	(* code by Sara Kalvala, based on Paulson's LK
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	5	and Moore's tisl.ML *)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	6
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	7	theory Washing
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	8	imports ILL
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	9	begin
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	10
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	11	consts
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	12	dollar :: o
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	13	quarter :: o
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	14	loaded :: o
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	15	dirty :: o
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	16	wet :: o
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	17	clean :: o
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	18
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	19	axioms
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	20	change:
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	21	"dollar \|- (quarter >< quarter >< quarter >< quarter)"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	22
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	23	load1:
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	24	"quarter , quarter , quarter , quarter , quarter \|- loaded"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	25
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	26	load2:
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	27	"dollar , quarter \|- loaded"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	28
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	29	wash:
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	30	"loaded , dirty \|- wet"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	31
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	32	dry:
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	33	"wet, quarter , quarter , quarter \|- clean"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	34
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	35
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	36	(* "activate" definitions for use in proof *)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	37
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	38	ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	39	ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	40	ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	41	ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	42
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	43	(* a load of dirty clothes and two dollars gives you clean clothes *)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	44
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	45	lemma "dollar , dollar , dirty \|- clean"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	46	apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	47	done
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	48
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	49	(* order of premises doesn't matter *)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	50
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	51	lemma "dollar , dirty , dollar \|- clean"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	52	apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	53	done
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	54
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	55	(* alternative formulation *)
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	56
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	57	lemma "dollar , dollar \|- dirty -o clean"
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	58	apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	59	done
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	60
87ac12bed1ab converted legacy ML scripts; wenzelm parents: diff changeset	61	end

author	wenzelm
	Thu, 28 Dec 2006 14:30:41 +0100
changeset 21921	f241e9cd26ca
parent 21426	87ac12bed1ab
child 26480	544cef16045b
permissions	-rw-r--r--