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

author	wenzelm
	Fri, 25 Sep 1998 14:32:36 +0200
changeset 5570	ae1b56ef16b0
parent 5527	38928c4a8eb2
child 6046	2c8a8be36c94
permissions	-rw-r--r--