1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory TailrecPre
8imports
9  "Word_Lib.WordSetup"
10  "Lib.Lib"
11begin
12
13definition
14  "tailrec_pre (f1 :: 'a \<Rightarrow> 'a) guard precondition (x::'a) \<equiv>
15    (\<forall>k. (\<forall>m. m < k \<longrightarrow> guard ((f1 ^^ m) x)) \<longrightarrow> precondition ((f1 ^^ k) x)) \<and>
16    (\<exists>n. \<not> guard ((f1 ^^ n) x))"
17
18definition
19  "short_tailrec_pre (f :: 'a \<Rightarrow> ('a + 'b) \<times> bool) \<equiv>
20     tailrec_pre (theLeft o fst o f) (isLeft o fst o f) (snd o f)"
21
22partial_function (tailrec)
23  tailrec :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b"
24where
25 "tailrec f1 f2 g x = (if g x then tailrec f1 f2 g (f1 x) else f2 x)"
26
27lemma tailrec_steps:
28  "g x \<Longrightarrow> tailrec f1 f2 g x = tailrec f1 f2 g (f1 x)"
29  "\<not> g x \<Longrightarrow> tailrec f1 f2 g x = f2 x"
30  by (simp_all add: tailrec.simps cong: if_weak_cong split del: if_split)
31
32definition
33  "short_tailrec (f :: 'a \<Rightarrow> ('a + 'b) \<times> bool) \<equiv>
34     tailrec (theLeft o fst o f) (theRight o fst o f) (isLeft o fst o f)"
35
36definition
37  "short_tailrec_pair stp v = (short_tailrec_pre stp v, short_tailrec stp v)"
38
39lemma tailrec_pre_lemma:
40  "!f1 g p x. tailrec_pre f1 g p (x::'a) = (p x \<and> (g x \<longrightarrow> tailrec_pre f1 g p (f1 x)))"
41  apply (clarsimp simp add: tailrec_pre_def)
42  apply (rule iffI)
43   apply (rule conjI)
44    apply auto[1]
45   apply clarsimp
46   apply (rule conjI[rotated])
47    apply (case_tac n)
48     apply simp
49    apply (clarsimp simp: funpow_swap1)
50    apply auto[1]
51   apply clarsimp
52   apply (drule_tac x="Suc n" for n in spec, simp add: funpow_swap1)
53   apply (erule mp)
54   apply clarsimp
55   apply (case_tac m, simp_all add: funpow_swap1)[1]
56  apply (case_tac "g x")
57   apply clarsimp
58   apply (rule conjI)
59    apply clarsimp
60    apply (case_tac k)
61     apply auto[1]
62    apply (simp_all add: funpow_swap1)[1]
63    apply (erule allE, erule impE)
64     prefer 2
65     apply assumption
66    apply (rule allI)
67    apply (rule impI)
68    apply (drule_tac x="Suc m" in spec, simp_all add: funpow_swap1)
69   apply (rule_tac x="Suc n" in exI)
70   apply (simp add: funpow_swap1)
71  apply (rule conjI)
72   prefer 2
73   apply (rule_tac x="0" in exI)
74   apply auto[1]
75  apply (rule allI)
76  apply (rule impI)
77  apply (case_tac k)
78  apply auto
79  done
80
81lemma tailrec_pre_lemmata:
82  "g x \<Longrightarrow> tailrec_pre f1 g p (x::'a) = (p x \<and> tailrec_pre f1 g p (f1 x))"
83  "\<not> g x \<Longrightarrow> tailrec_pre f1 g p (x::'a) = p x"
84  by (metis tailrec_pre_lemma)+
85
86theorem short_tailrec_thm:
87  "\<forall>f x. short_tailrec f x = (if isLeft (fst (f x))
88     then short_tailrec f (theLeft (fst (f x)))
89     else theRight (fst (f x))) \<and>
90   (short_tailrec_pre f x = (snd (f x)
91     \<and> (isLeft (fst (f x)) \<longrightarrow> short_tailrec_pre f (theLeft (fst (f x))))))"
92  apply (clarsimp simp add: short_tailrec_pre_def short_tailrec_def)
93  apply (simp add: tailrec_pre_lemmata tailrec_steps)
94  done
95
96lemma short_tailrec_pair_single_step:
97  "\<forall>v. \<not> isLeft (fst (f v))
98    \<Longrightarrow> short_tailrec_pair f = (\<lambda>v. let (rv, b) = (f v) in (b, theRight rv))"
99  apply (rule ext)
100  apply (simp add: short_tailrec_pair_def split_def Let_def)
101  apply (simp add: short_tailrec_thm cong: imp_cong[OF _ refl] if_weak_cong)
102  done
103
104lemma eq_true_imp:
105  "(x ==  Trueprop True) ==> PROP x"
106  apply auto
107  done
108
109lemma forall_true:
110  "(!x. True) = True"
111  apply auto
112  done
113
114lemmas split_thm = split_conv
115
116definition
117  line_number :: "word32 \<Rightarrow> bool"
118where
119  "line_number n \<equiv> True"
120
121end
122