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

author	paulson
	Mon, 28 Dec 1998 16:54:01 +0100
changeset 6046	2c8a8be36c94
parent 5527	38928c4a8eb2
child 6068	2d8f3e1f1151
permissions	-rw-r--r--