isabelle: src/HOLCF/Holcfb.ML@8b24773de6db (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 892 diff changeset	1	(* Title: HOLCF/holcfb.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: 892 diff changeset	3	Author: Franz Regensburger
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	4	Changed by: David von Oheimb
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5	Copyright 1993 Technische Universitaet Muenchen
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	6	*)
243 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 Holcfb;
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	(* Some lemmas in HOL.thy *)
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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	16	(* val de_morgan1 = de_Morgan_disj RS sym; "(~a & ~b)=(~(a \| b))" *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	18	(* val de_morgan2 = de_Morgan_conj RS sym; "(~a \| ~b)=(~(a & b))" *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	19
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	21	(* val notall2ex = not_all "(~ (!x.P(x))) = (? x.~P(x))" *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	22
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	23	(* val notex2all = not_ex "(~ (? x.P(x))) = (!x.~P(x))" *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	24
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	25
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	26	(* val selectI3 = select_eq_Ex RS iffD2 "(? x. P(x)) ==> P(@ x.P(x))" *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	28	(* val selectE = select_eq_Ex RS iffD1 "P(@ x.P(x)) ==> (? x. P(x))" *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	31	(*
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 625 diff changeset	32	qed_goal "notnotI" HOL.thy "P ==> ~~P"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	33	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 892 diff changeset	34	[
6bcb44e4d6e5 expanded tabs clasohm parents: 892 diff changeset	35	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 892 diff changeset	36	(fast_tac HOL_cs 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 892 diff changeset	37	]);
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	38	*)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	39
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	40	(* val classical2 = case_split_thm; "[\|Q ==> R; ~Q ==> R\|]==>R" *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41
1832 79dd1433867c removed old version of LEAST operator oheimb parents: 1675 diff changeset	42	(* fun case_tac s = res_inst_tac [("Q",s)] classical2; *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	43
1832 79dd1433867c removed old version of LEAST operator oheimb parents: 1675 diff changeset	44	val classical3 = (notE RS notI); (* [\| ?P ==> ~ ?P1; ?P ==> ?P1 \|] ==> ~ ?P *)

author	paulson
	Wed, 21 Aug 1996 13:22:23 +0200
changeset 1933	8b24773de6db
parent 1832	79dd1433867c
child 2033	639de962ded4
permissions	-rw-r--r--