1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory ML_Goal_Test 8imports 9 ML_Goal 10 MLUtils 11begin 12experiment begin 13 14\<comment>\<open> 15 Basic usage. 16\<close> 17ML_goal test: \<open> 18 [@{term "(P \<longrightarrow> Q) \<and> P \<longrightarrow> Q"}] 19\<close> 20 apply clarsimp 21 done 22 23thm test 24 25\<comment>\<open> 26 A goal that we definitely don't want to write out by hand. 27 28 In this case, we're going to show that if x is less than 10, 29 we "only" need to consider the cases when x = 0, or x = 1, or... 30\<close> 31ML_goal big_goal: \<open> 32 let 33 val var_x = Free ("x", @{typ nat}); 34 val var_P = Free ("P", @{typ bool}); 35 val max = 10; 36 37 \<comment>\<open> 38 @{ML "HOLogic.mk_nat"} produces nested Suc's, which are pretty 39 ugly, so we use this instead. 40 \<close> 41 val mk_nat = HOLogic.mk_number @{typ nat}; 42 43 \<comment>\<open> 44 Turns (i: int) into @{term "x = i \<Longrightarrow> P"}. 45 \<close> 46 fun mk_case i = 47 let 48 val prem = HOLogic.mk_eq (var_x, mk_nat i) |> HOLogic.mk_Trueprop; 49 val conc = var_P |> HOLogic.mk_Trueprop; 50 in Logic.mk_implies (prem, conc) end 51 52 val x_cases = 53 ListExtras.range 0 max 54 |> map mk_case; 55 56 val assm = 57 HOLogic.mk_binrel @{const_name "less"} 58 (var_x, 59 (mk_nat max)) 60 |> HOLogic.mk_Trueprop; 61 62 val goal = 63 Logic.list_implies (assm :: x_cases, var_P |> HOLogic.mk_Trueprop) 64 65 in [goal] end 66\<close> 67 by force 68 69\<comment>\<open> 70 Names are optional. 71\<close> 72ML_goal \<open> 73 [@{term "True"}] 74\<close> 75 by (rule TrueI) 76 77\<comment>\<open> 78 Multiple goals are supported, and result in similar 79 "list of fact" lemmas 80\<close> 81ML_goal multiple_goals: \<open> 82 [@{term "(P \<Longrightarrow> Q \<Longrightarrow> P)"}, @{term "(P \<Longrightarrow> Q \<Longrightarrow> Q)"}] 83\<close> 84 by simp+ 85 86thm multiple_goals[OF TrueI] 87 88\<comment>\<open> 89 Handles mixes of @{typ bool} and @{typ prop}. 90\<close> 91ML_goal \<open> 92 [@{term "PROP A \<Longrightarrow> PROP A"}, @{term "B \<longrightarrow> B"}] 93\<close> 94 by simp+ 95 96\<comment>\<open> 97 Turns out a lemma name can refer to nothing as well! 98\<close> 99ML_goal nothing: \<open>[]\<close> 100 done 101 102thm nothing[OF TrueI] 103 104\<comment>\<open> 105 Attributes can be applied, just like normal lemmas. 106\<close> 107definition magic where "magic = (5 :: nat)" 108 109ML_goal declared_with_an_attribute[folded magic_def, simp]: \<open> 110 [@{term "(5 :: nat) = 2 + 3"}] 111\<close> 112 by simp 113 114lemma uses_our_new_magic_simp_rule: 115 "magic = 1 + 4" 116 by simp 117 118end 119 120end