1open HolKernel Parse boolLib bossLib; 2 3val _ = new_theory "oneline"; 4 5Definition ZIP2: 6 (ZIP2 ([],[]) z = []) /\ 7 (ZIP2 (x::xs,y::ys) z = (x,y) :: ZIP2 (xs, ys) (5:num)) 8Termination 9 WF_REL_TAC ���measure (\p. LENGTH (FST (FST p)) + LENGTH (SND (FST p)))��� >> 10 simp[] 11End 12 13fun is_oneline th = 14 let val cs = th |> concl |> strip_conj 15 in 16 length cs = 1 andalso is_eq (hd cs) 17 end 18 19val oneline_zip2 = DefnBase.one_line_ify NONE ZIP2 20val _ = assert 21 (fn l => length l = 1 andalso is_disj (hd l)) 22 (hyp oneline_zip2) 23val _ = assert is_oneline oneline_zip2 24 25Definition AEVERY_AUX_def: 26 (AEVERY_AUX aux P [] <=> T) /\ 27 (AEVERY_AUX aux P ((x:'a,y:'b)::xs) <=> 28 if MEM x aux then AEVERY_AUX aux P xs 29 else 30 P (x,y) /\ AEVERY_AUX (x::aux) P xs) 31End 32 33Theorem oneline_aevery_aux[local] = DefnBase.one_line_ify NONE AEVERY_AUX_def 34val _ = assert (null o hyp) oneline_aevery_aux 35val _ = assert is_oneline oneline_aevery_aux 36 37Definition incomplete_literal: 38 incomplete_literal 1 = 10 /\ 39 incomplete_literal 2 = 11 /\ 40 incomplete_literal 3 = 30 41End 42 43val oneline_incomplete = DefnBase.one_line_ify NONE incomplete_literal 44val (theta, _) = match_term 45 ���incomplete_literal svar = 46 case svar of 1 => 10 | 2 => 11 | 3 => 30 | _ => ARB��� 47 (concl oneline_incomplete) 48val _ = length (hyp oneline_incomplete) = 1 andalso 49 aconv (hd (hyp oneline_incomplete)) 50 (subst theta ���svar = 1 \/ svar = 2 \/ svar = 3���) orelse 51 raise Fail "incomplete_literal test fails" 52 53Definition complete_literal0: 54 complete_literal0 1 = 10 /\ 55 complete_literal0 2 = 12 /\ 56 complete_literal0 _ = 15 57End 58 59Theorem oneline_complete0[local] = DefnBase.one_line_ify NONE complete_literal0 60val _ = assert is_oneline oneline_complete0 61val _ = assert (null o hyp) oneline_complete0 62 63Definition complete_literal1a: 64 complete_literal1a [] 1 = 10 /\ 65 complete_literal1a (3::t) 2 = 16 /\ 66 complete_literal1a (h::t) 2 = 12 + h /\ 67 complete_literal1a _ _ = 15 68End 69 70Theorem oneline_complete1a[local] = 71 DefnBase.one_line_ify NONE complete_literal1a 72 73val _ = assert null (hyp oneline_complete1a) 74val _ = assert is_oneline oneline_complete1a 75 76Definition complete_literal1b: 77 complete_literal1b ([], 1) = 10 /\ 78 complete_literal1b (3::t, 2) = 16 /\ 79 complete_literal1b (h::t, 2) = 12 + h /\ 80 complete_literal1b _ = 15 81End 82 83Theorem oneline_complete1b[local] = 84 DefnBase.one_line_ify NONE complete_literal1b 85 86val _ = assert (null o hyp) oneline_complete1b 87val _ = assert is_oneline oneline_complete1b 88 89Definition complete_literal2: 90 complete_literal2 (3, [], 2) = 10 /\ 91 complete_literal2 (5, h::t, x) = 12 + h + x /\ 92 complete_literal2 _ = 15 93End 94 95Theorem oneline_complete2[local] = DefnBase.one_line_ify NONE complete_literal2 96val _ = assert (null o hyp) oneline_complete2 97val _ = assert is_oneline oneline_complete2 98 99Definition ADEL_def: 100 (ADEL [] z = []) /\ 101 (ADEL ((x:'a,y:'b)::xs) z = if x = z then ADEL xs z else (x,y)::ADEL xs z) 102End 103 104Theorem oneline_ADEL[local] = DefnBase.one_line_ify NONE ADEL_def 105val _ = assert (null o hyp) oneline_ADEL 106val _ = assert is_oneline oneline_ADEL 107 108Definition bar_def: 109 bar = [] : 'a list 110End 111 112Theorem oneline_bar[local] = DefnBase.one_line_ify NONE bar_def 113val _ = assert (null o hyp) oneline_bar 114val _ = assert is_oneline oneline_bar 115 116Definition foo1_def: 117 foo1 = if bar = []:'a list then []:'a list else [] 118End 119 120Theorem oneline_foo1[local] = DefnBase.one_line_ify NONE foo1_def 121val _ = assert (null o hyp) oneline_foo1 122val _ = assert is_oneline oneline_foo1 123 124Datatype: 125 tt = A1 126 | B1 tt 127 | C1 (tt option) 128 | D1 (tt list) 129 | E1 (tt # tt) 130End 131 132Definition test_def: 133 test A1 = [()] /\ 134 test (B1 x) = test x ++ [()] /\ 135 test (C1 NONE) = [] /\ 136 test (C1 (SOME x)) = test x ++ REVERSE (test x) /\ 137 test (D1 tts) = (case tts of [] => [(); ()] 138 | (tt :: tts) => test (D1 tts) ++ test tt) /\ 139 test (E1 (x, y)) = REVERSE (test x) ++ test y 140End 141 142Theorem oneline_test[local] = DefnBase.one_line_ify NONE test_def 143 144 145val _ = export_theory(); 146