isabelle: src/HOL/UNITY/UNITY_tactics.ML@23b67731f4f0 (annotated)

13786 ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	1	(* Title: HOL/UNITY/UNITY_tactics.ML
ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	2	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	3	Copyright 2003 University of Cambridge
ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	4
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21669 diff changeset	5	Specialized UNITY tactics.
13786 ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	6	*)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	7
13797 baefae13ad37 conversion of UNITY theories to new-style paulson parents: 13796 diff changeset	8	(Combines two invariance ASSUMPTIONS into one. USEFUL??)
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 51717 diff changeset	9	fun Always_Int_tac ctxt =
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 51717 diff changeset	10	dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin}
13797 baefae13ad37 conversion of UNITY theories to new-style paulson parents: 13796 diff changeset	11
baefae13ad37 conversion of UNITY theories to new-style paulson parents: 13796 diff changeset	12	(Combines a list of invariance THEOREMS into one.)
24147 edc90be09ac1 misc cleanup of ML bindings (for multihreading); wenzelm parents: 21669 diff changeset	13	val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
13797 baefae13ad37 conversion of UNITY theories to new-style paulson parents: 13796 diff changeset	14
13812 91713a1915ee converting HOL/UNITY to use unconditional fairness paulson parents: 13798 diff changeset	15	(*Proves "co" properties when the program is specified. Any use of invariants
91713a1915ee converting HOL/UNITY to use unconditional fairness paulson parents: 13798 diff changeset	16	(from weak constrains) must have been done already.*)
42767 e6d920bea7a6 prefer Proof.context over old-style clasimpset; wenzelm parents: 37936 diff changeset	17	fun constrains_tac ctxt i =
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	18	SELECT_GOAL
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	19	(EVERY
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 51717 diff changeset	20	[REPEAT (Always_Int_tac ctxt 1),
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	21	(reduce the fancy safety properties to "constrains")
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	22	REPEAT (etac @{thm Always_ConstrainsI} 1
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	23	ORELSE
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58963 diff changeset	24	resolve_tac ctxt [@{thm StableI}, @{thm stableI},
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	25	@{thm constrains_imp_Constrains}] 1),
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	26	(for safety, the totalize operator can be ignored)
51717 9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	27	simp_tac (put_simpset HOL_ss ctxt
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	28	addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	29	rtac @{thm constrainsI} 1,
51717 9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	30	full_simp_tac ctxt 1,
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	31	REPEAT (FIRSTGOAL (etac disjE)),
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	32	ALLGOALS (clarify_tac ctxt),
51717 9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	33	ALLGOALS (asm_full_simp_tac ctxt)]) i;
13786 ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	34
ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	35	(proves "ensures/leadsTo" properties when the program is specified)
42767 e6d920bea7a6 prefer Proof.context over old-style clasimpset; wenzelm parents: 37936 diff changeset	36	fun ensures_tac ctxt sact =
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	37	SELECT_GOAL
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	38	(EVERY
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 51717 diff changeset	39	[REPEAT (Always_Int_tac ctxt 1),
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	40	etac @{thm Always_LeadsTo_Basis} 1
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	41	ORELSE (subgoal may involve LeadsTo, leadsTo or ensures)
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	42	REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	43	@{thm EnsuresI}, @{thm ensuresI}] 1),
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	44	(now there are two subgoals: co & transient)
51717 9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	45	simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
59763 56d2c357e6b5 tuned signature; wenzelm parents: 59755 diff changeset	46	Rule_Insts.res_inst_tac ctxt
59780 23b67731f4f0 support 'for' fixes in rule_tac etc.; wenzelm parents: 59763 diff changeset	47	[((("act", 0), Position.none), sact)] [] @{thm totalize_transientI} 2
59763 56d2c357e6b5 tuned signature; wenzelm parents: 59755 diff changeset	48	ORELSE Rule_Insts.res_inst_tac ctxt
59780 23b67731f4f0 support 'for' fixes in rule_tac etc.; wenzelm parents: 59763 diff changeset	49	[((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	50	(simplify the command's domain)
51717 9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	51	simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	52	constrains_tac ctxt 1,
88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 42767 diff changeset	53	ALLGOALS (clarify_tac ctxt),
51717 9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	54	ALLGOALS (asm_lr_simp_tac ctxt)]);
13796 19f50fa807ae converting more UNITY theories to new-style paulson parents: 13792 diff changeset	55
13786 ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	56
ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	57	(Composition equivalences, from Lift_prog)
ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	58
51717 9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	59	fun make_o_equivs ctxt th =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	60	[th,
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	61	th RS @{thm o_equiv_assoc} \|> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]),
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset; wenzelm parents: 46752 diff changeset	62	th RS @{thm o_equiv_apply} \|> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])];
13786 ab8f39f48a6f More conversion of UNITY to Isar new-style theories paulson parents: diff changeset	63

author	wenzelm
	Mon, 23 Mar 2015 13:30:59 +0100
changeset 59780	23b67731f4f0
parent 59763	56d2c357e6b5
child 60754	02924903a6fd
permissions	-rw-r--r--