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