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