author  nipkow 
Tue, 02 Jan 2001 10:27:10 +0100  
changeset 10759  994877ee68cb 
parent 9101  b643f4d7b9e9 
child 13075  d3e1d554cd6d 
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 

9101  9 
PropLog = Main + 
5184  10 

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

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

12 
'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

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

14 
thms :: 'a pl set => 'a pl set 
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 
"=" :: ['a pl set, 'a pl] => bool (infixl 50) 
9101  17 
eval :: ['a set, 'a pl] => bool ("_[[_]]" [100,0] 100) 
3120
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 
9101  32 
sat_def "H = p == (!tt. (!q:H. tt[[q]]) > tt[[p]])" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 

5184  34 
primrec 
10759  35 
"tt[[false]] = False" 
36 
"tt[[#v]] = (v:tt)" 

37 
eval_imp "tt[[p>q]] = (tt[[p]] > tt[[q]])" 

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

38 

5184  39 
primrec 
10759  40 
"hyps false tt = {}" 
41 
"hyps (#v) tt = {if v:tt then #v else #v>false}" 

42 
"hyps (p>q) tt = hyps p tt Un hyps q tt" 

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

43 

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

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

45 