35 and undefined_fast_Eps :: 'a |
35 and undefined_fast_Eps :: 'a |
36 and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
36 and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
37 and bisim_iterator_max :: bisim_iterator |
37 and bisim_iterator_max :: bisim_iterator |
38 and Quot :: "'a \<Rightarrow> 'b" |
38 and Quot :: "'a \<Rightarrow> 'b" |
39 and quot_normal :: "'a \<Rightarrow> 'a" |
39 and quot_normal :: "'a \<Rightarrow> 'a" |
40 and Silly :: "'a \<Rightarrow> 'b" |
|
41 and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" |
40 and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" |
42 |
41 |
43 datatype ('a, 'b) pair_box = PairBox 'a 'b |
42 datatype ('a, 'b) pair_box = PairBox 'a 'b |
44 datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)" |
43 datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)" |
45 |
44 |
46 typedecl unsigned_bit |
45 typedecl unsigned_bit |
47 typedecl signed_bit |
46 typedecl signed_bit |
48 typedecl \<xi> |
|
49 |
47 |
50 datatype 'a word = Word "('a set)" |
48 datatype 'a word = Word "('a set)" |
51 |
49 |
52 text {* |
50 text {* |
53 Alternative definitions. |
51 Alternative definitions. |
252 use "Tools/Nitpick/minipick.ML" |
250 use "Tools/Nitpick/minipick.ML" |
253 |
251 |
254 setup {* Nitpick_Isar.setup *} |
252 setup {* Nitpick_Isar.setup *} |
255 |
253 |
256 hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim |
254 hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim |
257 bisim_iterator_max Quot quot_normal Silly Tha PairBox FunBox Word refl' wf' |
255 bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf' |
258 wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd |
256 wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd |
259 int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac |
257 int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac |
260 plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac |
258 plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac |
261 of_frac |
259 of_frac |
262 hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit \<xi> word |
260 hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word |
263 hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def |
261 hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def |
264 wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def |
262 wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def |
265 The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def |
263 The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def |
266 nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def |
264 nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def |
267 num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def |
265 num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def |