author  bulwahn 
Fri, 22 Oct 2010 18:38:59 +0200  
changeset 40100  98d74bbe8cd8 
parent 39803  a8178a7b7b51 
child 40137  9eabcb1bfe50 
permissions  rwrr 
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1 
theory Predicate_Compile_Tests 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

2 
imports Predicate_Compile_Alternative_Defs 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

3 
begin 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

4 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

5 
subsection {* Basic predicates *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

6 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

7 
inductive False' :: "bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

8 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

9 
code_pred (expected_modes: bool) False' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

10 
code_pred [dseq] False' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

11 
code_pred [random_dseq] False' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

12 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

13 
values [expected "{}" pred] "{x. False'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

14 
values [expected "{}" dseq 1] "{x. False'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

15 
values [expected "{}" random_dseq 1, 1, 1] "{x. False'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

16 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

17 
value "False'" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

18 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

19 
inductive True' :: "bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

20 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

21 
"True ==> True'" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

22 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

23 
code_pred True' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

24 
code_pred [dseq] True' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

25 
code_pred [random_dseq] True' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

26 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

27 
thm True'.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

28 
thm True'.dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

29 
thm True'.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

30 
values [expected "{()}" ]"{x. True'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

31 
values [expected "{}" dseq 0] "{x. True'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

32 
values [expected "{()}" dseq 1] "{x. True'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

33 
values [expected "{()}" dseq 2] "{x. True'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

34 
values [expected "{}" random_dseq 1, 1, 0] "{x. True'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

35 
values [expected "{}" random_dseq 1, 1, 1] "{x. True'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

36 
values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

37 
values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

38 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

39 
inductive EmptySet :: "'a \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

40 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

41 
code_pred (expected_modes: o => bool, i => bool) EmptySet . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

42 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

43 
definition EmptySet' :: "'a \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

44 
where "EmptySet' = {}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

45 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

46 
code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

47 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

48 
inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

49 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

50 
code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

51 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

52 
inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

53 
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

54 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

55 
code_pred 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

56 
(expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

57 
(o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

58 
(i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

59 
(i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

60 
(o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

61 
(o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

62 
(i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

63 
(i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

64 
EmptyClosure . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

65 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

66 
thm EmptyClosure.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

67 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

68 
(* TODO: inductive package is broken! 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

69 
inductive False'' :: "bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

70 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

71 
"False \<Longrightarrow> False''" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

72 

40100  73 
code_pred (expected_modes: bool) False'' . 
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

74 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

75 
inductive EmptySet'' :: "'a \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

76 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

77 
"False \<Longrightarrow> EmptySet'' x" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

78 

40100  79 
code_pred (expected_modes: i => bool, o => bool) [inductify] EmptySet'' . 
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

80 
*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

81 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

82 
consts a' :: 'a 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

83 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

84 
inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

85 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

86 
"Fact a' a'" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

87 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

88 
code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

89 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

90 
inductive zerozero :: "nat * nat => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

91 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

92 
"zerozero (0, 0)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

93 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

94 
code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

95 
code_pred [dseq] zerozero . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

96 
code_pred [random_dseq] zerozero . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

97 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

98 
thm zerozero.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

99 
thm zerozero.dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

100 
thm zerozero.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

101 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

102 
text {* We expect the user to expand the tuples in the values command. 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

103 
The following values command is not supported. *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

104 
(*values "{x. zerozero x}" *) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

105 
text {* Instead, the user must type *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

106 
values "{(x, y). zerozero (x, y)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

107 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

108 
values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

109 
values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

110 
values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

111 
values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

112 
values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

113 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

114 
inductive nested_tuples :: "((int * int) * int * int) => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

115 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

116 
"nested_tuples ((0, 1), 2, 3)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

117 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

118 
code_pred nested_tuples . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

119 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

120 
inductive JamesBond :: "nat => int => code_numeral => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

121 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

122 
"JamesBond 0 0 7" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

123 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

124 
code_pred JamesBond . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

125 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

126 
values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

127 
values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

128 
values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

129 
values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

130 
values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

131 
values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

132 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

133 
values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

134 
values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

135 
values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

136 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

137 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

138 
subsection {* Alternative Rules *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

139 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

140 
datatype char = C  D  E  F  G  H 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

141 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

142 
inductive is_C_or_D 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

143 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

144 
"(x = C) \<or> (x = D) ==> is_C_or_D x" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

145 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

146 
code_pred (expected_modes: i => bool) is_C_or_D . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

147 
thm is_C_or_D.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

148 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

149 
inductive is_D_or_E 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

150 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

151 
"(x = D) \<or> (x = E) ==> is_D_or_E x" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

152 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

153 
lemma [code_pred_intro]: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

154 
"is_D_or_E D" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

155 
by (auto intro: is_D_or_E.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

156 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

157 
lemma [code_pred_intro]: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

158 
"is_D_or_E E" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

159 
by (auto intro: is_D_or_E.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

160 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

161 
code_pred (expected_modes: o => bool, i => bool) is_D_or_E 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

162 
proof  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

163 
case is_D_or_E 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

164 
from is_D_or_E.prems show thesis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

165 
proof 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

166 
fix xa 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

167 
assume x: "x = xa" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

168 
assume "xa = D \<or> xa = E" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

169 
from this show thesis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

170 
proof 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

171 
assume "xa = D" from this x is_D_or_E(1) show thesis by simp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

172 
next 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

173 
assume "xa = E" from this x is_D_or_E(2) show thesis by simp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

174 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

175 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

176 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

177 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

178 
thm is_D_or_E.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

179 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

180 
inductive is_F_or_G 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

181 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

182 
"x = F \<or> x = G ==> is_F_or_G x" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

183 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

184 
lemma [code_pred_intro]: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

185 
"is_F_or_G F" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

186 
by (auto intro: is_F_or_G.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

187 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

188 
lemma [code_pred_intro]: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

189 
"is_F_or_G G" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

190 
by (auto intro: is_F_or_G.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

191 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

192 
inductive is_FGH 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

193 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

194 
"is_F_or_G x ==> is_FGH x" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

195 
 "is_FGH H" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

196 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

197 
text {* Compilation of is_FGH requires elimination rule for is_F_or_G *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

198 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

199 
code_pred (expected_modes: o => bool, i => bool) is_FGH 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

200 
proof  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

201 
case is_F_or_G 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

202 
from is_F_or_G.prems show thesis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

203 
proof 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

204 
fix xa 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

205 
assume x: "x = xa" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

206 
assume "xa = F \<or> xa = G" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

207 
from this show thesis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

208 
proof 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

209 
assume "xa = F" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

210 
from this x is_F_or_G(1) show thesis by simp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

211 
next 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

212 
assume "xa = G" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

213 
from this x is_F_or_G(2) show thesis by simp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

214 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

215 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

216 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

217 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

218 
subsection {* Named alternative rules *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

219 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

220 
inductive appending 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

221 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

222 
nil: "appending [] ys ys" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

223 
 cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

224 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

225 
lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

226 
by (auto intro: appending.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

227 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

228 
lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

229 
by (auto intro: appending.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

230 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

231 
text {* With code_pred_intro, we can give fact names to the alternative rules, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

232 
which are used for the code_pred command. *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

233 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

234 
declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

235 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

236 
code_pred appending 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

237 
proof  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

238 
case appending 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

239 
from appending.prems show thesis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

240 
proof(cases) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

241 
case nil 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

242 
from alt_nil nil show thesis by auto 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

243 
next 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

244 
case cons 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

245 
from alt_cons cons show thesis by fastsimp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

246 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

247 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

248 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

249 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

250 
inductive ya_even and ya_odd :: "nat => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

251 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

252 
even_zero: "ya_even 0" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

253 
 odd_plus1: "ya_even x ==> ya_odd (x + 1)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

254 
 even_plus1: "ya_odd x ==> ya_even (x + 1)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

255 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

256 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

257 
declare even_zero[code_pred_intro even_0] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

258 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

259 
lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

260 
by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

261 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

262 
lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

263 
by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

264 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

265 
code_pred ya_even 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

266 
proof  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

267 
case ya_even 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

268 
from ya_even.prems show thesis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

269 
proof (cases) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

270 
case even_zero 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

271 
from even_zero even_0 show thesis by simp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

272 
next 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

273 
case even_plus1 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

274 
from even_plus1 even_Suc show thesis by simp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

275 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

276 
next 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

277 
case ya_odd 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

278 
from ya_odd.prems show thesis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

279 
proof (cases) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

280 
case odd_plus1 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

281 
from odd_plus1 odd_Suc show thesis by simp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

282 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

283 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

284 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

285 
subsection {* Preprocessor Inlining *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

286 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

287 
definition "equals == (op =)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

288 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

289 
inductive zerozero' :: "nat * nat => bool" where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

290 
"equals (x, y) (0, 0) ==> zerozero' (x, y)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

291 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

292 
code_pred (expected_modes: i => bool) zerozero' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

293 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

294 
lemma zerozero'_eq: "zerozero' x == zerozero x" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

295 
proof  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

296 
have "zerozero' = zerozero" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

297 
apply (auto simp add: mem_def) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

298 
apply (cases rule: zerozero'.cases) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

299 
apply (auto simp add: equals_def intro: zerozero.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

300 
apply (cases rule: zerozero.cases) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

301 
apply (auto simp add: equals_def intro: zerozero'.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

302 
done 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

303 
from this show "zerozero' x == zerozero x" by auto 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

304 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

305 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

306 
declare zerozero'_eq [code_pred_inline] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

307 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

308 
definition "zerozero'' x == zerozero' x" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

309 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

310 
text {* if preprocessing fails, zerozero'' will not have all modes. *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

311 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

312 
code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

313 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

314 
subsection {* Sets and Numerals *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

315 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

316 
definition 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

317 
"one_or_two = {Suc 0, (Suc (Suc 0))}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

318 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

319 
code_pred [inductify] one_or_two . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

320 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

321 
code_pred [dseq] one_or_two . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

322 
code_pred [random_dseq] one_or_two . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

323 
thm one_or_two.dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

324 
values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

325 
values [random_dseq 0,0,10] 3 "{x. one_or_two x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

326 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

327 
inductive one_or_two' :: "nat => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

328 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

329 
"one_or_two' 1" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

330 
 "one_or_two' 2" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

331 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

332 
code_pred one_or_two' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

333 
thm one_or_two'.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

334 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

335 
values "{x. one_or_two' x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

336 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

337 
definition one_or_two'': 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

338 
"one_or_two'' == {1, (2::nat)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

339 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

340 
code_pred [inductify] one_or_two'' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

341 
thm one_or_two''.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

342 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

343 
values "{x. one_or_two'' x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

344 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

345 
subsection {* even predicate *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

346 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

347 
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

348 
"even 0" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

349 
 "even n \<Longrightarrow> odd (Suc n)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

350 
 "odd n \<Longrightarrow> even (Suc n)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

351 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

352 
code_pred (expected_modes: i => bool, o => bool) even . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

353 
code_pred [dseq] even . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

354 
code_pred [random_dseq] even . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

355 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

356 
thm odd.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

357 
thm even.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

358 
thm odd.dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

359 
thm even.dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

360 
thm odd.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

361 
thm even.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

362 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

363 
values "{x. even 2}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

364 
values "{x. odd 2}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

365 
values 10 "{n. even n}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

366 
values 10 "{n. odd n}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

367 
values [expected "{}" dseq 2] "{x. even 6}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

368 
values [expected "{}" dseq 6] "{x. even 6}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

369 
values [expected "{()}" dseq 7] "{x. even 6}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

370 
values [dseq 2] "{x. odd 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

371 
values [dseq 6] "{x. odd 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

372 
values [dseq 7] "{x. odd 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

373 
values [expected "{()}" dseq 8] "{x. odd 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

374 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

375 
values [expected "{}" dseq 0] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

376 
values [expected "{0::nat}" dseq 1] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

377 
values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

378 
values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

379 
values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

380 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

381 
values [random_dseq 1, 1, 0] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

382 
values [random_dseq 1, 1, 1] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

383 
values [random_dseq 1, 1, 2] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

384 
values [random_dseq 1, 1, 3] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

385 
values [random_dseq 1, 1, 6] 8 "{x. even x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

386 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

387 
values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

388 
values [random_dseq 1, 1, 8] "{x. odd 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

389 
values [random_dseq 1, 1, 9] "{x. odd 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

390 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

391 
definition odd' where "odd' x == \<not> even x" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

392 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

393 
code_pred (expected_modes: i => bool) [inductify] odd' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

394 
code_pred [dseq inductify] odd' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

395 
code_pred [random_dseq inductify] odd' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

396 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

397 
values [expected "{}" dseq 2] "{x. odd' 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

398 
values [expected "{()}" dseq 9] "{x. odd' 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

399 
values [expected "{}" dseq 2] "{x. odd' 8}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

400 
values [expected "{}" dseq 10] "{x. odd' 8}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

401 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

402 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

403 
inductive is_even :: "nat \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

404 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

405 
"n mod 2 = 0 \<Longrightarrow> is_even n" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

406 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

407 
code_pred (expected_modes: i => bool) is_even . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

408 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

409 
subsection {* append predicate *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

410 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

411 
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

412 
"append [] xs xs" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

413 
 "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

414 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

415 
code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

416 
i => o => i => bool as suffix, i => i => i => bool) append . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

417 
code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as "concat", o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as "slice", o \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool as prefix, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

418 
i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

419 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

420 
code_pred [dseq] append . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

421 
code_pred [random_dseq] append . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

422 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

423 
thm append.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

424 
thm append.dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

425 
thm append.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

426 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

427 
values "{(ys, xs). append xs ys [0, Suc 0, 2]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

428 
values "{zs. append [0, Suc 0, 2] [17, 8] zs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

429 
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

430 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

431 
values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

432 
values [expected "{(([]::nat list), [Suc 0, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

433 
values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

434 
values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

435 
values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

436 
values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

437 
values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

438 
values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

439 
values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

440 
values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

441 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

442 
value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

443 
value [code] "Predicate.the (slice ([]::int list))" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

444 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

445 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

446 
text {* tricky case with alternative rules *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

447 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

448 
inductive append2 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

449 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

450 
"append2 [] xs xs" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

451 
 "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

452 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

453 
lemma append2_Nil: "append2 [] (xs::'b list) xs" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

454 
by (simp add: append2.intros(1)) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

455 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

456 
lemmas [code_pred_intro] = append2_Nil append2.intros(2) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

457 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

458 
code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

459 
i => o => i => bool, i => i => i => bool) append2 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

460 
proof  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

461 
case append2 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

462 
from append2.prems show thesis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

463 
proof 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

464 
fix xs 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

465 
assume "xa = []" "xb = xs" "xc = xs" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

466 
from this append2(1) show thesis by simp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

467 
next 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

468 
fix xs ys zs x 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

469 
assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

470 
from this append2(2) show thesis by fastsimp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

471 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

472 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

473 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

474 
inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

475 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

476 
"tupled_append ([], xs, xs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

477 
 "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

478 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

479 
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

480 
i * o * i => bool, i * i * i => bool) tupled_append . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

481 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

482 
code_pred (expected_modes: i \<times> i \<times> o \<Rightarrow> bool, o \<times> o \<times> i \<Rightarrow> bool, o \<times> i \<times> i \<Rightarrow> bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

483 
i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

484 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

485 
code_pred [random_dseq] tupled_append . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

486 
thm tupled_append.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

487 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

488 
values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

489 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

490 
inductive tupled_append' 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

491 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

492 
"tupled_append' ([], xs, xs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

493 
 "[ ys = fst (xa, y); x # zs = snd (xa, y); 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

494 
tupled_append' (xs, ys, zs) ] ==> tupled_append' (x # xs, xa, y)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

495 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

496 
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

497 
i * o * i => bool, i * i * i => bool) tupled_append' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

498 
thm tupled_append'.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

499 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

500 
inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

501 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

502 
"tupled_append'' ([], xs, xs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

503 
 "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

504 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

505 
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

506 
i * o * i => bool, i * i * i => bool) tupled_append'' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

507 
thm tupled_append''.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

508 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

509 
inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

510 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

511 
"tupled_append''' ([], xs, xs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

512 
 "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

513 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

514 
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

515 
i * o * i => bool, i * i * i => bool) tupled_append''' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

516 
thm tupled_append'''.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

517 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

518 
subsection {* map_ofP predicate *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

519 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

520 
inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

521 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

522 
"map_ofP ((a, b)#xs) a b" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

523 
 "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

524 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

525 
code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

526 
thm map_ofP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

527 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

528 
subsection {* filter predicate *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

529 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

530 
inductive filter1 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

531 
for P 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

532 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

533 
"filter1 P [] []" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

534 
 "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

535 
 "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

536 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

537 
code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

538 
code_pred [dseq] filter1 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

539 
code_pred [random_dseq] filter1 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

540 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

541 
thm filter1.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

542 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

543 
values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

544 
values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

545 
values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

546 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

547 
inductive filter2 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

548 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

549 
"filter2 P [] []" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

550 
 "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

551 
 "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

552 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

553 
code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

554 
code_pred [dseq] filter2 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

555 
code_pred [random_dseq] filter2 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

556 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

557 
thm filter2.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

558 
thm filter2.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

559 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

560 
inductive filter3 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

561 
for P 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

562 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

563 
"List.filter P xs = ys ==> filter3 P xs ys" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

564 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

565 
code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

566 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

567 
code_pred filter3 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

568 
thm filter3.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

569 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

570 
(* 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

571 
inductive filter4 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

572 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

573 
"List.filter P xs = ys ==> filter4 P xs ys" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

574 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

575 
code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

576 
(*code_pred [depth_limited] filter4 .*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

577 
(*code_pred [random] filter4 .*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

578 
*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

579 
subsection {* reverse predicate *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

580 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

581 
inductive rev where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

582 
"rev [] []" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

583 
 "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

584 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

585 
code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

586 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

587 
thm rev.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

588 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

589 
values "{xs. rev [0, 1, 2, 3::nat] xs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

590 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

591 
inductive tupled_rev where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

592 
"tupled_rev ([], [])" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

593 
 "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

594 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

595 
code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

596 
thm tupled_rev.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

597 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

598 
subsection {* partition predicate *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

599 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

600 
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

601 
for f where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

602 
"partition f [] [] []" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

603 
 "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

604 
 "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

605 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

606 
code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

607 
(i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

608 
partition . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

609 
code_pred [dseq] partition . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

610 
code_pred [random_dseq] partition . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

611 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

612 
values 10 "{(ys, zs). partition is_even 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

613 
[0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

614 
values 10 "{zs. partition is_even zs [0, 2] [3, 5]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

615 
values 10 "{zs. partition is_even zs [0, 7] [3, 5]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

616 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

617 
inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

618 
for f where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

619 
"tupled_partition f ([], [], [])" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

620 
 "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

621 
 "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

622 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

623 
code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

624 
(i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

625 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

626 
thm tupled_partition.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

627 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

628 
lemma [code_pred_intro]: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

629 
"r a b \<Longrightarrow> tranclp r a b" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

630 
"r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

631 
by auto 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

632 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

633 
subsection {* transitive predicate *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

634 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

635 
text {* Also look at the tabled transitive closure in the Library *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

636 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

637 
code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

638 
(o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

639 
(o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

640 
proof  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

641 
case tranclp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

642 
from this converse_tranclpE[OF tranclp.prems] show thesis by metis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

643 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

644 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

645 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

646 
code_pred [dseq] tranclp . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

647 
code_pred [random_dseq] tranclp . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

648 
thm tranclp.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

649 
thm tranclp.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

650 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

651 
inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

652 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

653 
"rtrancl' x x r" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

654 
 "r x y ==> rtrancl' y z r ==> rtrancl' x z r" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

655 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

656 
code_pred [random_dseq] rtrancl' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

657 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

658 
thm rtrancl'.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

659 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

660 
inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

661 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

662 
"rtrancl'' (x, x, r)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

663 
 "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

664 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

665 
code_pred rtrancl'' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

666 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

667 
inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

668 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

669 
"rtrancl''' (x, (x, x), r)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

670 
 "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

671 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

672 
code_pred rtrancl''' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

673 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

674 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

675 
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

676 
"succ 0 1" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

677 
 "succ m n \<Longrightarrow> succ (Suc m) (Suc n)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

678 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

679 
code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

680 
code_pred [random_dseq] succ . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

681 
thm succ.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

682 
thm succ.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

683 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

684 
values 10 "{(m, n). succ n m}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

685 
values "{m. succ 0 m}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

686 
values "{m. succ m 0}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

687 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

688 
text {* values command needs mode annotation of the parameter succ 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

689 
to disambiguate which mode is to be chosen. *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

690 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

691 
values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

692 
values [mode: o => i => bool] 10 "{n. tranclp succ n 10}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

693 
values 20 "{(n, m). tranclp succ n m}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

694 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

695 
inductive example_graph :: "int => int => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

696 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

697 
"example_graph 0 1" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

698 
 "example_graph 1 2" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

699 
 "example_graph 1 3" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

700 
 "example_graph 4 7" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

701 
 "example_graph 4 5" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

702 
 "example_graph 5 6" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

703 
 "example_graph 7 6" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

704 
 "example_graph 7 8" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

705 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

706 
inductive not_reachable_in_example_graph :: "int => int => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

707 
where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

708 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

709 
code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

710 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

711 
thm not_reachable_in_example_graph.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

712 
thm tranclp.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

713 
value "not_reachable_in_example_graph 0 3" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

714 
value "not_reachable_in_example_graph 4 8" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

715 
value "not_reachable_in_example_graph 5 6" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

716 
text {* rtrancl compilation is strange! *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

717 
(* 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

718 
value "not_reachable_in_example_graph 0 4" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

719 
value "not_reachable_in_example_graph 1 6" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

720 
value "not_reachable_in_example_graph 8 4"*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

721 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

722 
code_pred [dseq] not_reachable_in_example_graph . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

723 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

724 
values [dseq 6] "{x. tranclp example_graph 0 3}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

725 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

726 
values [dseq 0] "{x. not_reachable_in_example_graph 0 3}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

727 
values [dseq 0] "{x. not_reachable_in_example_graph 0 4}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

728 
values [dseq 20] "{x. not_reachable_in_example_graph 0 4}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

729 
values [dseq 6] "{x. not_reachable_in_example_graph 0 3}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

730 
values [dseq 3] "{x. not_reachable_in_example_graph 4 2}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

731 
values [dseq 6] "{x. not_reachable_in_example_graph 4 2}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

732 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

733 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

734 
inductive not_reachable_in_example_graph' :: "int => int => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

735 
where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

736 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

737 
code_pred not_reachable_in_example_graph' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

738 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

739 
value "not_reachable_in_example_graph' 0 3" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

740 
(* value "not_reachable_in_example_graph' 0 5" would not terminate *) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

741 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

742 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

743 
(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

744 
(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

745 
(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

746 
(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

747 
(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

748 
(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

749 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

750 
code_pred [dseq] not_reachable_in_example_graph' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

751 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

752 
(*thm not_reachable_in_example_graph'.dseq_equation*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

753 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

754 
(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

755 
(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

756 
(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

757 
values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

758 
(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

759 
(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

760 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

761 
subsection {* Free function variable *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

762 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

763 
inductive FF :: "nat => nat => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

764 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

765 
"f x = y ==> FF x y" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

766 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

767 
code_pred FF . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

768 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

769 
subsection {* IMP *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

770 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

771 
types 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

772 
var = nat 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

773 
state = "int list" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

774 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

775 
datatype com = 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

776 
Skip  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

777 
Ass var "state => int"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

778 
Seq com com  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

779 
IF "state => bool" com com  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

780 
While "state => bool" com 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

781 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

782 
inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

783 
"tupled_exec (Skip, s, s)"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

784 
"tupled_exec (Ass x e, s, s[x := e(s)])"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

785 
"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

786 
"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

787 
"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

788 
"~b s ==> tupled_exec (While b c, s, s)"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

789 
"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

790 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

791 
code_pred tupled_exec . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

792 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

793 
values "{s. tupled_exec (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0  1)) (Ass 1 (%s. s!1 + 1))), [3, 5], s)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

794 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

795 
subsection {* CCS *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

796 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

797 
text{* This example formalizes finite CCS processes without communication or 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

798 
recursion. For simplicity, labels are natural numbers. *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

799 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

800 
datatype proc = nil  pre nat proc  or proc proc  par proc proc 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

801 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

802 
inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

803 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

804 
"tupled_step (pre n p, n, p)"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

805 
"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

806 
"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

807 
"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)"  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

808 
"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

809 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

810 
code_pred tupled_step . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

811 
thm tupled_step.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

812 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

813 
subsection {* divmod *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

814 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

815 
inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

816 
"k < l \<Longrightarrow> divmod_rel k l 0 k" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

817 
 "k \<ge> l \<Longrightarrow> divmod_rel (k  l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

818 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

819 
code_pred divmod_rel . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

820 
thm divmod_rel.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

821 
value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

822 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

823 
subsection {* Transforming predicate logic into logic programs *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

824 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

825 
subsection {* Transforming functions into logic programs *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

826 
definition 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

827 
"case_f xs ys = (case (xs @ ys) of [] => []  (x # xs) => xs)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

828 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

829 
code_pred [inductify, skip_proof] case_f . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

830 
thm case_fP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

831 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

832 
fun fold_map_idx where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

833 
"fold_map_idx f i y [] = (y, [])" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

834 
 "fold_map_idx f i y (x # xs) = 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

835 
(let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

836 
in (y'', x' # xs'))" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

837 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

838 
code_pred [inductify] fold_map_idx . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

839 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

840 
subsection {* Minimum *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

841 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

842 
definition Min 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

843 
where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

844 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

845 
code_pred [inductify] Min . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

846 
thm Min.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

847 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

848 
subsection {* Lexicographic order *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

849 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

850 
declare lexord_def[code_pred_def] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

851 
code_pred [inductify] lexord . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

852 
code_pred [random_dseq inductify] lexord . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

853 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

854 
thm lexord.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

855 
thm lexord.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

856 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

857 
inductive less_than_nat :: "nat * nat => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

858 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

859 
"less_than_nat (0, x)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

860 
 "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

861 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

862 
code_pred less_than_nat . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

863 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

864 
code_pred [dseq] less_than_nat . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

865 
code_pred [random_dseq] less_than_nat . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

866 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

867 
inductive test_lexord :: "nat list * nat list => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

868 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

869 
"lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

870 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

871 
code_pred test_lexord . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

872 
code_pred [dseq] test_lexord . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

873 
code_pred [random_dseq] test_lexord . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

874 
thm test_lexord.dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

875 
thm test_lexord.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

876 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

877 
values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

878 
(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

879 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

880 
lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

881 
(* 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

882 
code_pred [inductify] lexn . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

883 
thm lexn.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

884 
*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

885 
(* 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

886 
code_pred [random_dseq inductify] lexn . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

887 
thm lexn.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

888 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

889 
values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

890 
*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

891 
inductive has_length 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

892 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

893 
"has_length [] 0" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

894 
 "has_length xs i ==> has_length (x # xs) (Suc i)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

895 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

896 
lemma has_length: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

897 
"has_length xs n = (length xs = n)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

898 
proof (rule iffI) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

899 
assume "has_length xs n" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

900 
from this show "length xs = n" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

901 
by (rule has_length.induct) auto 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

902 
next 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

903 
assume "length xs = n" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

904 
from this show "has_length xs n" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

905 
by (induct xs arbitrary: n) (auto intro: has_length.intros) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

906 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

907 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

908 
lemma lexn_intros [code_pred_intro]: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

909 
"has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

910 
"lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

911 
proof  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

912 
assume "has_length xs i" "has_length ys i" "r (x, y)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

913 
from this has_length show "lexn r (Suc i) (x # xs, y # ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

914 
unfolding lexn_conv Collect_def mem_def 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

915 
by fastsimp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

916 
next 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

917 
assume "lexn r i (xs, ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

918 
thm lexn_conv 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

919 
from this show "lexn r (Suc i) (x#xs, x#ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

920 
unfolding Collect_def mem_def lexn_conv 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

921 
apply auto 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

922 
apply (rule_tac x="x # xys" in exI) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

923 
by auto 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

924 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

925 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

926 
code_pred [random_dseq] lexn 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

927 
proof  
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

928 
fix r n xs ys 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

929 
assume 1: "lexn r n (xs, ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

930 
assume 2: "\<And>r' i x xs' y ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', y # ys') ==> has_length xs' i ==> has_length ys' i ==> r' (x, y) ==> thesis" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

931 
assume 3: "\<And>r' i x xs' ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r' i (xs', ys') ==> thesis" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

932 
from 1 2 3 show thesis 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

933 
unfolding lexn_conv Collect_def mem_def 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

934 
apply (auto simp add: has_length) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

935 
apply (case_tac xys) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

936 
apply auto 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

937 
apply fastsimp 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

938 
apply fastsimp done 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

939 
qed 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

940 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

941 
values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

942 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

943 
code_pred [inductify, skip_proof] lex . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

944 
thm lex.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

945 
thm lex_def 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

946 
declare lenlex_conv[code_pred_def] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

947 
code_pred [inductify, skip_proof] lenlex . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

948 
thm lenlex.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

949 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

950 
code_pred [random_dseq inductify] lenlex . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

951 
thm lenlex.random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

952 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

953 
values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

954 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

955 
thm lists.intros 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

956 
code_pred [inductify] lists . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

957 
thm lists.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

958 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

959 
subsection {* AVL Tree *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

960 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

961 
datatype 'a tree = ET  MKT 'a "'a tree" "'a tree" nat 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

962 
fun height :: "'a tree => nat" where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

963 
"height ET = 0" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

964 
 "height (MKT x l r h) = max (height l) (height r) + 1" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

965 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

966 
primrec avl :: "'a tree => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

967 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

968 
"avl ET = True" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

969 
 "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

970 
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

971 
(* 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

972 
code_pred [inductify] avl . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

973 
thm avl.equation*) 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

974 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

975 
code_pred [new_random_dseq inductify] avl . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

976 
thm avl.new_random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

977 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

978 
values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

979 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

980 
fun set_of 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

981 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

982 
"set_of ET = {}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

983 
 "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

984 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

985 
fun is_ord :: "nat tree => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

986 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

987 
"is_ord ET = True" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

988 
 "is_ord (MKT n l r h) = 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

989 
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

990 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

991 
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

992 
thm set_of.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

993 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

994 
code_pred (expected_modes: i => bool) [inductify] is_ord . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

995 
thm is_ord_aux.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

996 
thm is_ord.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

997 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

998 
subsection {* Definitions about Relations *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

999 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1000 
term "converse" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1001 
code_pred (modes: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1002 
(i * i => bool) => i * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1003 
(i * o => bool) => o * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1004 
(i * o => bool) => i * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1005 
(o * i => bool) => i * o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1006 
(o * i => bool) => i * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1007 
(o * o => bool) => o * o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1008 
(o * o => bool) => i * o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1009 
(o * o => bool) => o * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1010 
(o * o => bool) => i * i => bool) [inductify] converse . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1011 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1012 
thm converse.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1013 
code_pred [inductify] rel_comp . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1014 
thm rel_comp.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1015 
code_pred [inductify] Image . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1016 
thm Image.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1017 
declare singleton_iff[code_pred_inline] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1018 
declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1019 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1020 
code_pred (expected_modes: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1021 
(o => bool) => o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1022 
(o => bool) => i * o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1023 
(o => bool) => o * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1024 
(o => bool) => i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1025 
(i => bool) => i * o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1026 
(i => bool) => o * i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1027 
(i => bool) => i => bool) [inductify] Id_on . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1028 
thm Id_on.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1029 
thm Domain_def 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1030 
code_pred (modes: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1031 
(o * o => bool) => o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1032 
(o * o => bool) => i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1033 
(i * o => bool) => i => bool) [inductify] Domain . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1034 
thm Domain.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1035 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1036 
thm Range_def 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1037 
code_pred (modes: 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1038 
(o * o => bool) => o => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1039 
(o * o => bool) => i => bool, 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1040 
(o * i => bool) => i => bool) [inductify] Range . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1041 
thm Range.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1042 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1043 
code_pred [inductify] Field . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1044 
thm Field.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1045 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1046 
thm refl_on_def 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1047 
code_pred [inductify] refl_on . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1048 
thm refl_on.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1049 
code_pred [inductify] total_on . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1050 
thm total_on.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1051 
code_pred [inductify] antisym . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1052 
thm antisym.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1053 
code_pred [inductify] trans . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1054 
thm trans.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1055 
code_pred [inductify] single_valued . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1056 
thm single_valued.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1057 
thm inv_image_def 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1058 
code_pred [inductify] inv_image . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1059 
thm inv_image.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1060 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1061 
subsection {* Inverting list functions *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1062 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1063 
code_pred [inductify] size_list . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1064 
code_pred [new_random_dseq inductify] size_list . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1065 
thm size_listP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1066 
thm size_listP.new_random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1067 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1068 
values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1069 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1070 
code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1071 
thm concatP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1072 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1073 
values "{ys. concatP [[1, 2], [3, (4::int)]] ys}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1074 
values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1075 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1076 
code_pred [dseq inductify] List.concat . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1077 
thm concatP.dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1078 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1079 
values [dseq 3] 3 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1080 
"{xs. concatP xs ([0] :: nat list)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1081 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1082 
values [dseq 5] 3 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1083 
"{xs. concatP xs ([1] :: int list)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1084 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1085 
values [dseq 5] 3 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1086 
"{xs. concatP xs ([1] :: nat list)}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1087 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1088 
values [dseq 5] 3 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1089 
"{xs. concatP xs [(1::int), 2]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1090 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1091 
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1092 
thm hdP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1093 
values "{x. hdP [1, 2, (3::int)] x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1094 
values "{(xs, x). hdP [1, 2, (3::int)] 1}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1095 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1096 
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1097 
thm tlP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1098 
values "{x. tlP [1, 2, (3::nat)] x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1099 
values "{x. tlP [1, 2, (3::int)] [3]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1100 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1101 
code_pred [inductify, skip_proof] last . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1102 
thm lastP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1103 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1104 
code_pred [inductify, skip_proof] butlast . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1105 
thm butlastP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1106 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1107 
code_pred [inductify, skip_proof] take . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1108 
thm takeP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1109 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1110 
code_pred [inductify, skip_proof] drop . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1111 
thm dropP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1112 
code_pred [inductify, skip_proof] zip . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1113 
thm zipP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1114 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1115 
code_pred [inductify, skip_proof] upt . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1116 
code_pred [inductify, skip_proof] remdups . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1117 
thm remdupsP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1118 
code_pred [dseq inductify] remdups . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1119 
values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1120 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1121 
code_pred [inductify, skip_proof] remove1 . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1122 
thm remove1P.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1123 
values "{xs. remove1P 1 xs [2, (3::int)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1124 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1125 
code_pred [inductify, skip_proof] removeAll . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1126 
thm removeAllP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1127 
code_pred [dseq inductify] removeAll . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1128 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1129 
values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1130 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1131 
code_pred [inductify] distinct . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1132 
thm distinct.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1133 
code_pred [inductify, skip_proof] replicate . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1134 
thm replicateP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1135 
values 5 "{(n, xs). replicateP n (0::int) xs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1136 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1137 
code_pred [inductify, skip_proof] splice . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1138 
thm splice.simps 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1139 
thm spliceP.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1140 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1141 
values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1142 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1143 
code_pred [inductify, skip_proof] List.rev . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1144 
code_pred [inductify] map . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1145 
code_pred [inductify] foldr . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1146 
code_pred [inductify] foldl . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1147 
code_pred [inductify] filter . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1148 
code_pred [random_dseq inductify] filter . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1149 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1150 
section {* Function predicate replacement *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1151 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1152 
text {* 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1153 
If the mode analysis uses the functional mode, we 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1154 
replace predicates that resulted from functions again by their functions. 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1155 
*} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1156 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1157 
inductive test_append 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1158 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1159 
"List.append xs ys = zs ==> test_append xs ys zs" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1160 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1161 
code_pred [inductify, skip_proof] test_append . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1162 
thm test_append.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1163 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1164 
text {* If append is not turned into a predicate, then the mode 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1165 
o => o => i => bool could not be inferred. *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1166 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1167 
values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1168 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1169 
text {* If appendP is not reverted back to a function, then mode i => i => o => bool 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1170 
fails after deleting the predicate equation. *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1171 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1172 
declare appendP.equation[code del] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1173 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1174 
values "{xs::int list. test_append [1,2] [3,4] xs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1175 
values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1176 
values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1177 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1178 
text {* Redeclaring append.equation as code equation *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1179 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1180 
declare appendP.equation[code] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1181 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1182 
subsection {* Function with tuples *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1183 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1184 
fun append' 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1185 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1186 
"append' ([], ys) = ys" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1187 
 "append' (x # xs, ys) = x # append' (xs, ys)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1188 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1189 
inductive test_append' 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1190 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1191 
"append' (xs, ys) = zs ==> test_append' xs ys zs" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1192 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1193 
code_pred [inductify, skip_proof] test_append' . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1194 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1195 
thm test_append'.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1196 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1197 
values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1198 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1199 
declare append'P.equation[code del] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1200 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1201 
values "{zs :: int list. test_append' [1,2,3] [4,5] zs}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1202 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1203 
section {* Arithmetic examples *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1204 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1205 
subsection {* Examples on nat *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1206 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1207 
inductive plus_nat_test :: "nat => nat => nat => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1208 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1209 
"x + y = z ==> plus_nat_test x y z" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1210 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1211 
code_pred [inductify, skip_proof] plus_nat_test . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1212 
code_pred [new_random_dseq inductify] plus_nat_test . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1213 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1214 
thm plus_nat_test.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1215 
thm plus_nat_test.new_random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1216 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1217 
values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1218 
values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1219 
values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1220 
values [expected "{}"] "{y. plus_nat_test 9 y 8}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1221 
values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1222 
values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1223 
values [expected "{}"] "{x. plus_nat_test x 9 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1224 
values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1225 
values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1226 
values [expected "{(0, 5), (4, Suc 0), (3, 2), (2, 3), (Suc 0, 4), (5, 0)}"] 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1227 
"{(x, y). plus_nat_test x y 5}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1228 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1229 
inductive minus_nat_test :: "nat => nat => nat => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1230 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1231 
"x  y = z ==> minus_nat_test x y z" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1232 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1233 
code_pred [inductify, skip_proof] minus_nat_test . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1234 
code_pred [new_random_dseq inductify] minus_nat_test . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1235 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1236 
thm minus_nat_test.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1237 
thm minus_nat_test.new_random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1238 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1239 
values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1240 
values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1241 
values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1242 
values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1243 
values [expected "{0, Suc 0, 2, 3}"] "{x. minus_nat_test x 3 0}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1244 
values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1245 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1246 
subsection {* Examples on int *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1247 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1248 
inductive plus_int_test :: "int => int => int => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1249 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1250 
"a + b = c ==> plus_int_test a b c" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1251 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1252 
code_pred [inductify, skip_proof] plus_int_test . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1253 
code_pred [new_random_dseq inductify] plus_int_test . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1254 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1255 
thm plus_int_test.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1256 
thm plus_int_test.new_random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1257 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1258 
values [expected "{1::int}"] "{a. plus_int_test a 6 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1259 
values [expected "{1::int}"] "{b. plus_int_test 6 b 7}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1260 
values [expected "{11::int}"] "{c. plus_int_test 5 6 c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1261 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1262 
inductive minus_int_test :: "int => int => int => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1263 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1264 
"a  b = c ==> minus_int_test a b c" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1265 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1266 
code_pred [inductify, skip_proof] minus_int_test . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1267 
code_pred [new_random_dseq inductify] minus_int_test . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1268 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1269 
thm minus_int_test.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1270 
thm minus_int_test.new_random_dseq_equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1271 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1272 
values [expected "{4::int}"] "{c. minus_int_test 9 5 c}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1273 
values [expected "{9::int}"] "{a. minus_int_test a 4 5}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1274 
values [expected "{ 1::int}"] "{b. minus_int_test 4 b 5}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1275 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1276 
subsection {* minus on bool *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1277 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1278 
inductive All :: "nat => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1279 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1280 
"All x" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1281 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1282 
inductive None :: "nat => bool" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1283 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1284 
definition "test_minus_bool x = (None x  All x)" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1285 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1286 
code_pred [inductify] test_minus_bool . 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1287 
thm test_minus_bool.equation 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1288 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1289 
values "{x. test_minus_bool x}" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1290 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1291 
subsection {* Functions *} 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1292 

8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1293 
fun partial_hd :: "'a list => 'a option" 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1294 
where 
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
diff
changeset

1295 
"partial_hd [] = Option.None" 
