isabelle: src/ZF/Resid/Terms.ML@85d62ecb950d (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
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5068 diff changeset	14	Goalw [unmark_def] "unmark(Var(n)) = Var(n)";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	15	by (Asm_simp_tac 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	16	qed "unmark_Var";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	17
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5068 diff changeset	18	Goalw [unmark_def] "unmark(Fun(t)) = Fun(unmark(t))";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	19	by (Asm_simp_tac 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	20	qed "unmark_Fun";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	21
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5068 diff changeset	22	Goalw [unmark_def] "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	23	by (Asm_simp_tac 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	24	qed "unmark_App";
1048 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	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	28	(* term simplification set *)
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
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	32	Addsimps ([unmark_App, unmark_Fun, unmark_Var,
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	33	lambda.dom_subset RS subsetD] @
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	34	lambda.intrs);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	35
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	36
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	37	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	38	(* unmark lemmas *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	39	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	40
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4091 diff changeset	41	Goalw [unmark_def]
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5068 diff changeset	42	"u:redexes ==> unmark(u):lambda";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	43	by (etac redexes.induct 1);
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	44	by (ALLGOALS Asm_simp_tac);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	45	qed "unmark_type";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	46
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5068 diff changeset	47	Goal "u:lambda ==> unmark(u) = u";
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	48	by (etac lambda.induct 1);
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	49	by (ALLGOALS Asm_simp_tac);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	50	qed "lambda_unmark";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	51
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	52
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	53	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	54	(* lift and subst preserve lambda *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	55	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	56
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	57	Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda";
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	58	by (etac lambda.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	59	by (ALLGOALS (asm_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	60	qed "liftL_typea";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	61	val liftL_type =liftL_typea RS bspec ;
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	62
5527 38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	63	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	64	by (etac lambda.induct 1);
38928c4a8eb2 big tidying of simpsets, etc paulson parents: 5147 diff changeset	65	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	66	qed "substL_typea";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	67	val substL_type = substL_typea RS bspec RS bspec ;
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	68
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	69
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	70	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	71	(* type-rule for reduction definitions *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	72	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	73
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	74	val red_typechecks = [substL_type]@nat_typechecks@lambda.intrs@bool_typechecks;

author	wenzelm
	Wed, 18 Nov 1998 10:56:53 +0100
changeset 5922	85d62ecb950d
parent 5527	38928c4a8eb2
child 6046	2c8a8be36c94
permissions	-rw-r--r--