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

author	nipkow
	Wed, 13 Nov 2024 23:11:06 +0100
changeset 81442	6097eaaee6ee
parent 60774	6c28d8ed2488
permissions	-rw-r--r--