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

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 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
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	15	qed_goalw "refl_less_fun" thy [less_fun_def] "(f::'a::term =>'b::po) << 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]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	22	"[\|(f1::'a::term =>'b::po) << f2; 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),
2033 639de962ded4 Ran expandshort; used stac instead of ssubst paulson parents: 1461 diff changeset	26	(stac expand_fun_eq 1),
1461 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]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	31	"[\|(f1::'a::term =>'b::po) << f2; f2 << f3 \|] ==> 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	]);

author	paulson
	Mon, 23 Jun 1997 10:42:03 +0200
changeset 3457	a8ab7c64817c
parent 3323	194ae2e0c193
child 9245	428385c4bc50
permissions	-rw-r--r--