isabelle: src/HOLCF/Fun1.ML@0a22b9d63a18 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	1	(* Title: HOLCF/fun1.ML
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	3	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	Lemmas for fun1.thy
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9	open Fun1;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12	(* less_fun is a partial order on 'a => 'b *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	15	qed_goalw "refl_less_fun" Fun1.thy [less_fun_def] "less_fun f f"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	17	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	18	(fast_tac (HOL_cs addSIs [refl_less]) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	19	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	21	qed_goalw "antisym_less_fun" Fun1.thy [less_fun_def]
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	22	"[\|less_fun f1 f2; less_fun f2 f1\|] ==> f1 = f2"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	23	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	24	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	25	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	26	(rtac (expand_fun_eq RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	27	(fast_tac (HOL_cs addSIs [antisym_less]) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	28	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	30	qed_goalw "trans_less_fun" Fun1.thy [less_fun_def]
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	31	"[\|less_fun f1 f2; less_fun f2 f3 \|] ==> less_fun f1 f3"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	32	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	33	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	34	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	35	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	36	(rtac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	37	(etac allE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	38	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	39	((etac allE 1) THEN (atac 1))
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	40	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	42	(*
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	43	--------------------------------------------------------------------------
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	44	Since less_fun :: "['a::term=>'b::po,'a::term=>'b::po] => bool" the
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	45	lemmas refl_less_fun, antisym_less_fun, trans_less_fun justify
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	46	the class arity fun::(term,po)po !!
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	47	--------------------------------------------------------------------------
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	48	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	49

author	paulson
	Mon, 23 Sep 1996 18:18:18 +0200
changeset 2010	0a22b9d63a18
parent 1461	6bcb44e4d6e5
child 2033	639de962ded4
permissions	-rw-r--r--