isabelle: src/ZF/Resid/Redex.ML@fb28eaa07e01 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1048 diff changeset	1	(* Title: Redex.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 Redex;
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	(* redex_rec conversions *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	12	(* ------------------------------------------------------------------------- *)
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	13
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 3734 diff changeset	14	Goal "redex_rec(Var(n),b,c,d) = b(n)";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	15	by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	16	by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	17	qed "redex_rec_Var";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	18
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 3734 diff changeset	19	Goal "redex_rec(Fun(t),b,c,d) = c(t,redex_rec(t,b,c,d))";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	20	by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	21	by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	22	qed "redex_rec_Fun";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	23
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 3734 diff changeset	24	Goal "redex_rec(App(m,f,a),b,c,d) = \
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	25	\ d(m,f,a,redex_rec(f,b,c,d),redex_rec(a,b,c,d))";
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	26	by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	27	by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
3734 33f355f56f82 Much tidying including "qed" instead of result(), and even qed_spec_mp, paulson parents: 2469 diff changeset	28	qed "redex_rec_App";
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	29
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	30	Addsimps ([redex_rec_App,redex_rec_Fun,redex_rec_Var]@redexes.intrs);
1048 5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	31
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
5ba0314f8214 New example by Ole Rasmussen lcp parents: diff changeset	35

author	wenzelm
	Mon, 22 Jun 1998 17:13:09 +0200
changeset 5068	fb28eaa07e01
parent 3734	33f355f56f82
child 6046	2c8a8be36c94
permissions	-rw-r--r--