author  wenzelm 
Wed, 21 Jun 2000 18:09:09 +0200  
changeset 9101  b643f4d7b9e9 
parent 5184  9b8547a9496a 
child 10759  994877ee68cb 
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) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

20 

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

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

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

23 

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

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

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

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

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

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

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

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

31 

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

32 
defs 
9101  33 
sat_def "H = p == (!tt. (!q:H. tt[[q]]) > tt[[p]])" 
34 
eval_def "tt[[p]] == eval2 p tt" 

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

35 

5184  36 
primrec 
3842  37 
"eval2(false) = (%x. False)" 
38 
"eval2(#v) = (%tt. v:tt)" 

39 
"eval2(p>q) = (%tt. eval2 p tt>eval2 q tt)" 

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

40 

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

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

43 
"hyps(#v) = (%tt.{if v:tt then #v else #v>false})" 
3842  44 
"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

45 

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

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

47 