isabelle: src/ZF/Resid/Terms.ML@793b33191ce3 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	1	(* Title: Terms.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
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	8	Addsimps ([lambda.dom_subset RS subsetD] @ lambda.intrs);
1048 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	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	12	(* unmark lemmas *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	13	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	14
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	15	Goal "u:redexes ==> unmark(u):lambda";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	16	by (etac redexes.induct 1);
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	17	by (ALLGOALS Asm_simp_tac);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	18	qed "unmark_type";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	19
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5068 diff changeset	20	Goal "u:lambda ==> unmark(u) = u";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	21	by (etac lambda.induct 1);
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	22	by (ALLGOALS Asm_simp_tac);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	23	qed "lambda_unmark";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	24
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	25
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	26	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	27	(* lift and subst preserve lambda *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	28	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	29
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	30	Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda";
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	31	by (etac lambda.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	32	by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
6112 5e4871c5136b datatype package improvements paulson parents: 6046 diff changeset	33	qed_spec_mp "liftL_type";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	34
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	35	Goal "v:lambda ==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	36	by (etac lambda.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	37	by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
6112 5e4871c5136b datatype package improvements paulson parents: 6046 diff changeset	38	qed_spec_mp "substL_type";
1048 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	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	42	(* type-rule for reduction definitions *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	43	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	44
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	45	val red_typechecks = [substL_type]@nat_typechecks@lambda.intrs@bool_typechecks;

author	wenzelm
	Mon, 03 May 1999 10:47:32 +0200
changeset 6561	793b33191ce3
parent 6112	5e4871c5136b
child 11319	8b84ee2cc79c
permissions	-rw-r--r--