isabelle: src/ZF/Resid/Terms.ML@771b1f6422a8 (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
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	8	open Terms;
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	(* unmark simplifications *)
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	goalw Terms.thy [unmark_def]
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	15	"unmark(Var(n)) = Var(n)";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	16	by (Asm_simp_tac 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	17	qed "unmark_Var";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	18
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	19	goalw Terms.thy [unmark_def]
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	20	"unmark(Fun(t)) = Fun(unmark(t))";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	21	by (Asm_simp_tac 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	22	qed "unmark_Fun";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	23
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	24	goalw Terms.thy [unmark_def]
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	25	"unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	26	by (Asm_simp_tac 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	27	qed "unmark_App";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	28
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	29
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	30	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	31	(* term simplification set *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	32	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	33
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	34
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	35	Addsimps ([unmark_App, unmark_Fun, unmark_Var,
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	36	lambda.dom_subset RS subsetD] @
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	37	lambda.intrs);
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	(* unmark lemmas *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	42	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	43
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	44	goalw Terms.thy [unmark_def]
3840 e0baea4d485a fixed dots; wenzelm parents: 3734 diff changeset	45	"!!u. u:redexes ==> unmark(u):lambda";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	46	by (eresolve_tac [redexes.induct] 1);
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	47	by (ALLGOALS Asm_simp_tac);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	48	qed "unmark_type";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	49
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	50	goal Terms.thy
3840 e0baea4d485a fixed dots; wenzelm parents: 3734 diff changeset	51	"!!u. u:lambda ==> unmark(u) = u";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	52	by (eresolve_tac [lambda.induct] 1);
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	53	by (ALLGOALS Asm_simp_tac);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	54	qed "lambda_unmark";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	55
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	56
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	57	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	58	(* lift and subst preserve lambda *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	59	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	60
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	61	goal Terms.thy
3840 e0baea4d485a fixed dots; wenzelm parents: 3734 diff changeset	62	"!!u.[\|v:lambda\|]==> ALL k:nat. lift_rec(v,k):lambda";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	63	by (eresolve_tac [lambda.induct] 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	64	by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()))));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	65	qed "liftL_typea";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	66	val liftL_type =liftL_typea RS bspec ;
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	67
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	68	goal Terms.thy
3840 e0baea4d485a fixed dots; wenzelm parents: 3734 diff changeset	69	"!!n.[\|v:lambda\|]==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	70	by (eresolve_tac [lambda.induct] 1);
4091 771b1f6422a8 isatool fixclasimp; wenzelm parents: 3840 diff changeset	71	by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps [liftL_type])));
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	72	qed "substL_typea";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	73	val substL_type = substL_typea RS bspec RS bspec ;
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	74
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	75
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	76	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	77	(* type-rule for reduction definitions *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	78	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	79
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	80	val red_typechecks = [substL_type]@nat_typechecks@lambda.intrs@bool_typechecks;

author	wenzelm
	Mon, 03 Nov 1997 12:24:13 +0100
changeset 4091	771b1f6422a8
parent 3840	e0baea4d485a
child 5068	fb28eaa07e01
permissions	-rw-r--r--