isabelle: src/ZF/Resid/Terms.ML@2c8a8be36c94 (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])));
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	33	bind_thm ("liftL_type", result() RS bspec);
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])));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	38	qed "substL_typea";
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 5527 diff changeset	39	bind_thm ("substL_type", result() RS bspec RS bspec);
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	(* type-rule for reduction definitions *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	44	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	45
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	46	val red_typechecks = [substL_type]@nat_typechecks@lambda.intrs@bool_typechecks;

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