isabelle: src/ZF/AC/recfunAC16.ML@08e1610c1dcb (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	1	(* Title: ZF/AC/recfunAC16.ML
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	3	Author: Krzysztof Grabczewski
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	4
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	5	Properties of the recursive definition used in the proof of WO2 ==> AC16
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	6	*)
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	7
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	8	(* ********************************************************************** *)
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	9	(* Basic properties of recfunAC16 *)
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	10	(* ********************************************************************** *)
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	11
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4091 diff changeset	12	Goalw [recfunAC16_def] "recfunAC16(f,fa,0,a) = 0";
1208 bc3093616ba4 Ran expandshort and corrected spelling of Grabczewski paulson parents: 1196 diff changeset	13	by (rtac transrec2_0 1);
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	14	qed "recfunAC16_0";
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	15
6068 2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 5137 diff changeset	16	Goalw [recfunAC16_def]
2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 5137 diff changeset	17	"recfunAC16(f,fa,succ(i),a) = \
2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 5137 diff changeset	18	\ (if (EX y:recfunAC16(f,fa,i,a). fa ` i <= y) then recfunAC16(f,fa,i,a) \
2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 5137 diff changeset	19	\ else recfunAC16(f,fa,i,a) Un \
2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 5137 diff changeset	20	\ {f ` (LEAST j. fa ` i <= f ` j & \
2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 5137 diff changeset	21	\ (ALL b<a. (fa`b <= f`j \
2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 5137 diff changeset	22	\ --> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})";
1208 bc3093616ba4 Ran expandshort and corrected spelling of Grabczewski paulson parents: 1196 diff changeset	23	by (rtac transrec2_succ 1);
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	24	qed "recfunAC16_succ";
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	25
5137 60205b0de9b9 Huge tidy-up: removal of leading \!\! paulson parents: 5116 diff changeset	26	Goalw [recfunAC16_def] "Limit(i) \
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	27	\ ==> recfunAC16(f,fa,i,a) = (UN j<i. recfunAC16(f,fa,j,a))";
1208 bc3093616ba4 Ran expandshort and corrected spelling of Grabczewski paulson parents: 1196 diff changeset	28	by (etac transrec2_Limit 1);
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	29	qed "recfunAC16_Limit";
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	30
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	31	(* ********************************************************************** *)
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	32	(* Monotonicity of transrec2 *)
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	33	(* ********************************************************************** *)
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	34
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	35	val [prem1, prem2] = goal thy
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	36	"[\| !!g r. r <= B(g,r); Ord(i) \|] \
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	37	\ ==> j<i --> transrec2(j, 0, B) <= transrec2(i, 0, B)";
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	38	by (resolve_tac [prem2 RS trans_induct] 1);
1208 bc3093616ba4 Ran expandshort and corrected spelling of Grabczewski paulson parents: 1196 diff changeset	39	by (rtac Ord_cases 1 THEN (REPEAT (assume_tac 1)));
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	40	by (Fast_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	41	by (Asm_simp_tac 1);
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	42	by (fast_tac (FOL_cs addSIs [succI1, prem1]
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	43	addSEs [ballE, leE, prem1 RSN (2, subset_trans)]) 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	44	by (fast_tac (claset() addIs [OUN_I, ltI]
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	45	addSEs [Limit_has_succ RS ltE, succI1 RSN (2, Ord_in_Ord) RS le_refl,
6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	46	transrec2_Limit RS ssubst]) 1);
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	47	qed "transrec2_mono_lemma";
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	48
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	49	val [prem1, prem2] = goal thy "[\| !!g r. r <= B(g,r); j le i \|] \
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	50	\ ==> transrec2(j, 0, B) <= transrec2(i, 0, B)";
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	51	by (resolve_tac [prem2 RS leE] 1);
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	52	by (resolve_tac [transrec2_mono_lemma RS impE] 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3731 diff changeset	53	by (TRYALL (fast_tac (claset() addSIs [prem1, prem2, lt_Ord2])));
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	54	qed "transrec2_mono";
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	55
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	56	(* ********************************************************************** *)
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	57	(* Monotonicity of recfunAC16 *)
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	58	(* ********************************************************************** *)
d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	59
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4091 diff changeset	60	Goalw [recfunAC16_def]
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1208 diff changeset	61	"!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)";
1208 bc3093616ba4 Ran expandshort and corrected spelling of Grabczewski paulson parents: 1196 diff changeset	62	by (rtac transrec2_mono 1);
5116 8eb343ab5748 Renamed expand_if to split_if and setloop split_tac to addsplits, paulson parents: 5068 diff changeset	63	by (REPEAT (fast_tac (claset() addIs [split_if RS iffD2]) 1));
3731 71366483323b result() -> qed; Step_tac -> Safe_tac paulson parents: 2469 diff changeset	64	qed "recfunAC16_mono";
1196 d43c1f7a53fe Numerous small improvements by KG and LCP lcp parents: diff changeset	65

author	oheimb
	Tue, 02 Jan 2001 22:41:17 +0100
changeset 10763	08e1610c1dcb
parent 6068	2d8f3e1f1151
child 11317	7f9e4c389318
permissions	-rw-r--r--