author  paulson 
Wed, 07 May 1997 12:50:26 +0200  
changeset 3120  c58423c20740 
child 3842  b55686a7b22c 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/PropLog.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

2 
ID: $Id$ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

3 
Author: Tobias Nipkow 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 
Copyright 1994 TU Muenchen 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

5 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

6 
Inductive definition of propositional logic. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 
*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

8 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 
PropLog = Finite + 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

10 
datatype 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 
'a pl = false  var 'a ("#_" [1000])  ">" ('a pl) ('a pl) (infixr 90) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
consts 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

13 
thms :: 'a pl set => 'a pl set 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
"" :: ['a pl set, 'a pl] => bool (infixl 50) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 
"=" :: ['a pl set, 'a pl] => bool (infixl 50) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
eval2 :: ['a pl, 'a set] => bool 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 
eval :: ['a set, 'a pl] => bool ("_[_]" [100,0] 100) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 
hyps :: ['a pl, 'a set] => 'a pl set 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

19 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

20 
translations 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 
"H  p" == "p : thms(H)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 
inductive "thms(H)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
intrs 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 
H "p:H ==> H  p" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

26 
K "H  p>q>p" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

27 
S "H  (p>q>r) > (p>q) > p>r" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

28 
DN "H  ((p>false) > false) > p" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

29 
MP "[ H  p>q; H  p ] ==> H  q" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

31 
defs 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

32 
sat_def "H = p == (!tt. (!q:H. tt[q]) > tt[p])" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 
eval_def "tt[p] == eval2 p tt" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

34 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

35 
primrec eval2 pl 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 
"eval2(false) = (%x.False)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
"eval2(#v) = (%tt.v:tt)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 
"eval2(p>q) = (%tt.eval2 p tt>eval2 q tt)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

40 
primrec hyps pl 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

41 
"hyps(false) = (%tt.{})" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
"hyps(#v) = (%tt.{if v:tt then #v else #v>false})" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
"hyps(p>q) = (%tt.hyps p tt Un hyps q tt)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

45 
end 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

46 