isabelle: src/ZF/Resid/Substitution.ML@3b6415035d1a (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	1	(* Title: Substitution.ML
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	3	Author: Ole Rasmussen
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	5	Logic Image: ZF
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	6	*)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	7
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	8	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	9	(* Arithmetic extensions *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	10	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	11
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	12	Goal "[\| p < n; n \\<in> nat\|] ==> n\\<noteq>p";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1732 diff changeset	13	by (Fast_tac 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	14	qed "gt_not_eq";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	15
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	16	Goal "[\|j \\<in> nat; i \\<in> nat\|] ==> i < j --> succ(j #- 1) = j";
9264 051592f4236a removal of batch style, and tidying paulson parents: 8201 diff changeset	17	by (induct_tac "j" 1);
051592f4236a removal of batch style, and tidying paulson parents: 8201 diff changeset	18	by (Fast_tac 1);
051592f4236a removal of batch style, and tidying paulson parents: 8201 diff changeset	19	by (Asm_simp_tac 1);
051592f4236a removal of batch style, and tidying paulson parents: 8201 diff changeset	20	qed "succ_pred";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	21
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	22	Goal "[\|succ(x)<n; n \\<in> nat; x \\<in> nat\|] ==> x < n #- 1 ";
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	23	by (rtac succ_leE 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	24	by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	25	by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	26	qed "lt_pred";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	27
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	28	Goal "[\|n < succ(x); p<n; p \\<in> nat; n \\<in> nat; x \\<in> nat\|] ==> n #- 1 < x ";
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	29	by (rtac succ_leE 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	30	by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	31	qed "gt_pred";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	32
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	33
8201 a81d18b0a9b1 tidied some proofs paulson parents: 7499 diff changeset	34	Addsimps [not_lt_iff_le, if_P, if_not_P];
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	35
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	36
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	37	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	38	(* lift_rec equality rules *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	39	(* ------------------------------------------------------------------------- *)
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	40	Goal "[\|n \\<in> nat; i \\<in> nat\|] \
6068 2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 6046 diff changeset	41	\ ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))";
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	42	by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	43	qed "lift_rec_Var";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	44
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	45	Goal "[\|n \\<in> nat; i \\<in> nat; k \\<in> nat; k le i\|] ==> lift_rec(Var(i),k) = Var(succ(i))";
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	46	by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	47	qed "lift_rec_le";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	48
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	49	Goal "[\|i \\<in> nat; k \\<in> nat; i<k \|] ==> lift_rec(Var(i),k) = Var(i)";
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	50	by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	51	qed "lift_rec_gt";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	52
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	53	Goal "[\|n \\<in> nat; k \\<in> nat\|] ==> \
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	54	\ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	55	by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	56	qed "lift_rec_Fun";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	57
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	58	Goal "[\|n \\<in> nat; k \\<in> nat\|] ==> \
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	59	\ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	60	by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	61	qed "lift_rec_App";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	62
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	63
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	64	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	65	(* substitution quality rules *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	66	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	67
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	68	Goal "[\|i \\<in> nat; k \\<in> nat; u \\<in> redexes\|] \
6068 2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 6046 diff changeset	69	\ ==> subst_rec(u,Var(i),k) = \
2d8f3e1f1151 if-then-else syntax for ZF paulson parents: 6046 diff changeset	70	\ (if k<i then Var(i #- 1) else if k=i then u else Var(i))";
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	71	by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	72	qed "subst_Var";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	73
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	74	Goal "[\|n \\<in> nat; u \\<in> redexes\|] ==> subst_rec(u,Var(n),n) = u";
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	75	by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	76	qed "subst_eq";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	77
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	78	Goal "[\|n \\<in> nat; u \\<in> redexes; p \\<in> nat; p<n\|] ==> \
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	79	\ subst_rec(u,Var(n),p) = Var(n #- 1)";
2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	80	by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	81	qed "subst_gt";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	82
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	83	Goal "[\|n \\<in> nat; u \\<in> redexes; p \\<in> nat; n<p\|] ==> \
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	84	\ subst_rec(u,Var(n),p) = Var(n)";
2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	85	by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	86	qed "subst_lt";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	87
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	88	Goal "[\|p \\<in> nat; u \\<in> redexes\|] ==> \
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	89	\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	90	by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	91	qed "subst_Fun";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	92
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	93	Goal "[\|p \\<in> nat; u \\<in> redexes\|] ==> \
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	94	\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	95	by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	96	qed "subst_App";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	97
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	98	(But not lift_rec_Var, subst_Var: too many case splits)
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	99	Addsimps [subst_Fun, subst_App];
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	100
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	101
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	102	Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. lift_rec(u,k):redexes";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	103	by (etac redexes.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	104	by (ALLGOALS
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	105	(asm_simp_tac (simpset() addsimps [lift_rec_Var,
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	106	lift_rec_Fun, lift_rec_App])));
6112 5e4871c5136b datatype package improvements paulson parents: 6070 diff changeset	107	qed_spec_mp "lift_rec_type";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	108
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	109	Goal "v \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. subst_rec(u,v,n):redexes";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	110	by (etac redexes.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	111	by (ALLGOALS(asm_simp_tac
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	112	(simpset() addsimps [subst_Var, lift_rec_type])));
6112 5e4871c5136b datatype package improvements paulson parents: 6070 diff changeset	113	qed_spec_mp "subst_type";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	114
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	115
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	116	Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1732 diff changeset	117	lift_rec_le, lift_rec_gt, lift_rec_Fun, lift_rec_App,
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1732 diff changeset	118	lift_rec_type];
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	119
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	120
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	121	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	122	(* lift and substitution proofs *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	123	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	124
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	125	Goal "u \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>i \\<in> nat. i le n --> \
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	126	\ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	127	by (etac redexes.induct 1);
2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	128	by (ALLGOALS Asm_simp_tac);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	129	by Safe_tac;
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	130	by (case_tac "n < xa" 1);
7499 23e090051cb8 isatool expandshort; wenzelm parents: 6112 diff changeset	131	by ((ftac lt_trans2 1) THEN (assume_tac 1));
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	132	by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	133	qed "lift_lift_rec";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	134
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	135	Goal "[\|u \\<in> redexes; n \\<in> nat\|] ==> \
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	136	\ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	137	by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	138	qed "lift_lift";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	139
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	140	Goal "v \\<in> redexes ==> \
8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	141	\ \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. n le m-->\
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	142	\ lift_rec(subst_rec(u,v,n),m) = \
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	143	\ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	144	by ((etac redexes.induct 1)
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	145	THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift]))));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	146	by Safe_tac;
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5116 diff changeset	147	by (excluded_middle_tac "n < x" 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	148	by (Asm_full_simp_tac 1);
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5116 diff changeset	149	by (eres_inst_tac [("j","n")] leE 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	150	by (asm_simp_tac (simpset() setloop (split_inside_tac [split_if])
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	151	addsimps [lift_rec_Var,subst_Var,
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	152	leI,gt_pred,succ_pred]) 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	153	by (hyp_subst_tac 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	154	by (Asm_simp_tac 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	155	by (forw_inst_tac [("j","x")] lt_trans2 1);
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	156	by (assume_tac 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	157	by (asm_simp_tac (simpset() addsimps [leI]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	158	qed "lift_rec_subst_rec";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	159
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	160	Goal "[\|v \\<in> redexes; u \\<in> redexes; n \\<in> nat\|] ==> \
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	161	\ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	162	by (asm_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	163	qed "lift_subst";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	164
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	165
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	166	Goal "v \\<in> redexes ==> \
8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	167	\ \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. m le n-->\
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	168	\ lift_rec(subst_rec(u,v,n),m) = \
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	169	\ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	170	by (etac redexes.induct 1
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	171	THEN ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	172	by Safe_tac;
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5116 diff changeset	173	by (excluded_middle_tac "n < x" 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	174	by (Asm_full_simp_tac 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	175	by (eres_inst_tac [("i","x")] leE 1);
7499 23e090051cb8 isatool expandshort; wenzelm parents: 6112 diff changeset	176	by (ftac lt_trans1 1 THEN assume_tac 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	177	by (ALLGOALS(asm_simp_tac
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	178	(simpset() addsimps [succ_pred,leI,gt_pred])));
771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	179	by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	180	by (case_tac "n < xa" 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	181	by (Asm_full_simp_tac 2);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	182	by (asm_simp_tac (simpset() addsimps [leI]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	183	qed "lift_rec_subst_rec_lt";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	184
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	185
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	186	Goal "u \\<in> redexes ==> \
8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	187	\ \\<forall>n \\<in> nat. \\<forall>v \\<in> redexes. subst_rec(v,lift_rec(u,n),n) = u";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	188	by (etac redexes.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	189	by Auto_tac;
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	190	by (case_tac "n < x" 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	191	by Auto_tac;
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	192	qed "subst_rec_lift_rec";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	193
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	194	Goal "v \\<in> redexes ==> \
8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	195	\ \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. \\<forall>w \\<in> redexes. m le n --> \
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	196	\ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	197	\ subst_rec(w,subst_rec(u,v,m),n)";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	198	by (etac redexes.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	199	by (ALLGOALS(asm_simp_tac (simpset() addsimps
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	200	[lift_lift RS sym,lift_rec_subst_rec_lt])));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	201	by Safe_tac;
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5116 diff changeset	202	by (excluded_middle_tac "n le succ(xa)" 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	203	by (Asm_full_simp_tac 1);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	204	by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	205	by (etac leE 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	206	by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 2);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	207	by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1);
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	208	by (forw_inst_tac [("i","x")]
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	209	(nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	210	by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1);
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5116 diff changeset	211	by (eres_inst_tac [("i","n")] leE 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	212	by (asm_simp_tac (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2);
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5116 diff changeset	213	by (excluded_middle_tac "n < x" 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	214	by (Asm_full_simp_tac 1);
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5116 diff changeset	215	by (eres_inst_tac [("j","n")] leE 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	216	by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	217	by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1);
7499 23e090051cb8 isatool expandshort; wenzelm parents: 6112 diff changeset	218	by (ftac lt_trans2 1 THEN assume_tac 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	219	by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	220	qed "subst_rec_subst_rec";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	221
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	222
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	223	Goal "[\|v \\<in> redexes; u \\<in> redexes; w \\<in> redexes; n \\<in> nat\|] ==> \
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	224	\ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)";
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	225	by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	226	qed "substitution";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	227
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	228	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	229	(* Preservation lemmas *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	230	(* Substitution preserves comp and regular *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	231	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	232
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	233
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	234	Goal "[\|n \\<in> nat; u ~ v\|] ==> \\<forall>m \\<in> nat. lift_rec(u,m) ~ lift_rec(v,m)";
1732 38776e927da8 Updated for new form of induction rules paulson parents: 1723 diff changeset	235	by (etac Scomp.induct 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	236	by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl])));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	237	qed "lift_rec_preserve_comp";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	238
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	239	Goal "u2 ~ v2 ==> \\<forall>m \\<in> nat. \\<forall>u1 \\<in> redexes. \\<forall>v1 \\<in> redexes.\
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	240	\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
1732 38776e927da8 Updated for new form of induction rules paulson parents: 1723 diff changeset	241	by (etac Scomp.induct 1);
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	242	by (ALLGOALS
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	243	(asm_simp_tac
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	244	(simpset() addsimps [subst_Var, lift_rec_preserve_comp, comp_refl])));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	245	qed "subst_rec_preserve_comp";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	246
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	247	Goal "regular(u) ==> \\<forall>m \\<in> nat. regular(lift_rec(u,m))";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	248	by (etac Sreg.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	249	by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var])));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	250	qed "lift_rec_preserve_reg";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	251
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5116 diff changeset	252	Goal "regular(v) ==> \
11319 8b84ee2cc79c X-symbols for ZF paulson parents: 9264 diff changeset	253	\ \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. regular(u)-->regular(subst_rec(u,v,m))";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	254	by (etac Sreg.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	255	by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_Var,
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5514 diff changeset	256	lift_rec_preserve_reg])));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	257	qed "subst_rec_preserve_reg";

author	wenzelm
	Wed, 15 Aug 2001 22:20:30 +0200
changeset 11501	3b6415035d1a
parent 11319	8b84ee2cc79c
child 12152	46f128d8133c
permissions	-rw-r--r--