equal
deleted
inserted
replaced
1333 This will be installed by calling \texttt{setmksimps} below. Preprocessing |
1333 This will be installed by calling \texttt{setmksimps} below. Preprocessing |
1334 occurs whenever rewrite rules are added, whether by user command or |
1334 occurs whenever rewrite rules are added, whether by user command or |
1335 automatically. Preprocessing involves extracting atomic rewrites at the |
1335 automatically. Preprocessing involves extracting atomic rewrites at the |
1336 object-level, then reflecting them to the meta-level. |
1336 object-level, then reflecting them to the meta-level. |
1337 |
1337 |
1338 To start, the function \texttt{forall_elim_vars_safe} strips any meta-level |
1338 To start, the function \texttt{gen_all} strips any meta-level |
1339 quantifiers from the front of the given theorem. |
1339 quantifiers from the front of the given theorem. |
1340 |
1340 |
1341 The function \texttt{atomize} analyses a theorem in order to extract |
1341 The function \texttt{atomize} analyses a theorem in order to extract |
1342 atomic rewrite rules. The head of all the patterns, matched by the |
1342 atomic rewrite rules. The head of all the patterns, matched by the |
1343 wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}. |
1343 wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}. |
1396 | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection |
1396 | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection |
1397 | _ $ (Const("Not",_)$_) => th RS iff_reflection_F |
1397 | _ $ (Const("Not",_)$_) => th RS iff_reflection_F |
1398 | _ => th RS iff_reflection_T; |
1398 | _ => th RS iff_reflection_T; |
1399 \end{ttbox} |
1399 \end{ttbox} |
1400 The |
1400 The |
1401 three functions \texttt{forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq} |
1401 three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq} |
1402 will be composed together and supplied below to \texttt{setmksimps}. |
1402 will be composed together and supplied below to \texttt{setmksimps}. |
1403 |
1403 |
1404 |
1404 |
1405 \subsection{Making the initial simpset} |
1405 \subsection{Making the initial simpset} |
1406 |
1406 |
1425 fun mk_meta_cong rl = standard (mk_meta_eq (mk_meta_prems rl)); |
1425 fun mk_meta_cong rl = standard (mk_meta_eq (mk_meta_prems rl)); |
1426 \end{ttbox} |
1426 \end{ttbox} |
1427 % |
1427 % |
1428 The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}. It |
1428 The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}. It |
1429 preprocess rewrites using |
1429 preprocess rewrites using |
1430 {\tt forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq}. |
1430 {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}. |
1431 It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by |
1431 It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by |
1432 detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals |
1432 detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals |
1433 of conditional rewrites. |
1433 of conditional rewrites. |
1434 |
1434 |
1435 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items. |
1435 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items. |
1449 val FOL_basic_ss = |
1449 val FOL_basic_ss = |
1450 empty_ss setsubgoaler asm_simp_tac |
1450 empty_ss setsubgoaler asm_simp_tac |
1451 addsimprocs [defALL_regroup, defEX_regroup] |
1451 addsimprocs [defALL_regroup, defEX_regroup] |
1452 setSSolver safe_solver |
1452 setSSolver safe_solver |
1453 setSolver unsafe_solver |
1453 setSolver unsafe_solver |
1454 setmksimps (map mk_eq o atomize o forall_elim_vars_safe) |
1454 setmksimps (map mk_eq o atomize o gen_all) |
1455 setmkcong mk_meta_cong; |
1455 setmkcong mk_meta_cong; |
1456 |
1456 |
1457 val IFOL_ss = |
1457 val IFOL_ss = |
1458 FOL_basic_ss addsimps (IFOL_simps {\at} |
1458 FOL_basic_ss addsimps (IFOL_simps {\at} |
1459 int_ex_simps {\at} int_all_simps) |
1459 int_ex_simps {\at} int_all_simps) |