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

author	paulson
	Thu, 11 Nov 1999 10:24:14 +0100
changeset 8004	6273f58ea2c1
parent 7499	23e090051cb8
child 8201	a81d18b0a9b1
permissions	-rw-r--r--