Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/Tactical.thy
changeset 229 abc7f90188af
parent 219 98d43270024f
child 230 8def50824320
equal deleted inserted replaced
228:fe45fbb111c5 229:abc7f90188af 
  1281 \begin{boxedminipage}{\textwidth}
 
  1281 \begin{boxedminipage}{\textwidth}
 
  1282 \begin{isabelle} *}
 
  1282 \begin{isabelle} *}
 
  1283 types  prm = "(nat \<times> nat) list"
 
  1283 types  prm = "(nat \<times> nat) list"
 
  1284 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)
 
  1284 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)
 
  1285 
  1285 
  1286 primrec (perm_nat)
 
  1286 overloading 
  1287  "[]\<bullet>c = c"
 
  1287   perm_nat \<equiv> "perm :: prm \<Rightarrow> nat \<Rightarrow> nat"
 
  1288  "(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab then snd ab 
  1288   perm_prod \<equiv> "perm :: prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"
 
  1289                else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))" 
  1289   perm_list \<equiv> "perm :: prm \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
  1290 
  1290 begin
 
  1291 primrec (perm_prod)
 
  1291 
  1292  "pi\<bullet>(x, y) = (pi\<bullet>x, pi\<bullet>y)"
 
  1292 fun swap::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 
  1293 
  1293 where
 
  1294 primrec (perm_list)
 
  1294  "swap a b c = (if c=a then b else (if c=b then a else c))"
 
  1295  "pi\<bullet>[] = []"
 
  1295 
  1296  "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
 
  1296 primrec perm_nat
 
       
  1297 where
 
       
  1298   "perm_nat [] c = c"
 
       
  1299 | "perm_nat (ab#pi) c = swap (fst ab) (snd ab) (perm_nat pi c)"
 
       
  1300 
       
  1301 fun perm_prod 
       
  1302 where
 
       
  1303  "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
 
       
  1304 
       
  1305 primrec perm_list
 
       
  1306 where
 
       
  1307   "perm_list pi [] = []"
 
       
  1308 | "perm_list pi (x#xs) = (pi\<bullet>x)#(perm_list pi xs)"
 
       
  1309 
       
  1310 end
 
  1297 
  1311 
  1298 lemma perm_append[simp]:
 
  1312 lemma perm_append[simp]:
 
  1299   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1313 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1300   shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
 
  1314 shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
 
  1301 by (induct pi\<^isub>1) (auto) 
  1315 by (induct pi\<^isub>1) (auto) 
  1302 
  1316 
  1303 lemma perm_eq[simp]:
 
  1317 lemma perm_bij[simp]:
 
  1304   fixes c::"nat" and pi::"prm"
 
  1318 fixes c d::"nat" and pi::"prm"
 
  1305   shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)" 
  1319 shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)" 
  1306 by (induct pi) (auto)
 
  1320 by (induct pi) (auto)
 
  1307 
  1321 
  1308 lemma perm_rev[simp]:
 
  1322 lemma perm_rev[simp]:
 
  1309   fixes c::"nat" and pi::"prm"
 
  1323 fixes c::"nat" and pi::"prm"
 
  1310   shows "pi\<bullet>((rev pi)\<bullet>c) = c"
 
  1324 shows "pi\<bullet>((rev pi)\<bullet>c) = c"
 
  1311 by (induct pi arbitrary: c) (auto)
 
  1325 by (induct pi arbitrary: c) (auto)
 
  1312 
  1326 
  1313 lemma perm_compose:
 
  1327 lemma perm_compose:
 
  1314   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1328 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1315   shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)" 
  1329 shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)" 
  1316 by (induct pi\<^isub>2) (auto)
 
  1330 by (induct pi\<^isub>2) (auto)
 
  1317 text_raw {*
 
  1331 text_raw {*
 
  1318 \end{isabelle}
 
  1332 \end{isabelle}
 
  1319 \end{boxedminipage}
 
  1333 \end{boxedminipage}
 
  1320 \caption{A simple theory about permutations over @{typ nat}. The point is that the
 
  1334 \caption{A simple theory about permutations over @{typ nat}s. The point is that the
 
  1321   lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
 
  1335   lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
 
  1322   it would cause the simplifier to loop. It can still be used as a simplification 
  1336   it would cause the simplifier to loop. It can still be used as a simplification 
  1323   rule if the permutation is sufficiently protected.\label{fig:perms}
 
  1337   rule if the permutation in the right-hand side is sufficiently protected.
 
  1324   (FIXME: Uses old primrec.)}
 
  1338   \label{fig:perms}}
 
  1325 \end{figure} *}
 
  1339 \end{figure} *}
 
  1326 
  1340 
  1327 
  1341 
  1328 text {*
 
  1342 text {*
 
  1329   The simplifier is often used in order to bring terms into a normal form.
 
  1343   The simplifier is often used in order to bring terms into a normal form.
 
  1339   and so causes an infinite loop. There seems to be no easy way to reformulate 
  1353   and so causes an infinite loop. There seems to be no easy way to reformulate 
  1340   this rule and so one ends up with clunky proofs like:
 
  1354   this rule and so one ends up with clunky proofs like:
 
  1341 *}
 
  1355 *}
 
  1342 
  1356 
  1343 lemma 
  1357 lemma 
  1344   fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1358 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1345   shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 
  1359 shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 
  1346 apply(simp)
 
  1360 apply(simp)
 
  1347 apply(rule trans)
 
  1361 apply(rule trans)
 
  1348 apply(rule perm_compose)
 
  1362 apply(rule perm_compose)
 
  1349 apply(simp)
 
  1363 apply(simp)
 
  1350 done 
  1364 done 
  1362   "pi \<bullet>aux c \<equiv> pi \<bullet> c"
 
  1376   "pi \<bullet>aux c \<equiv> pi \<bullet> c"
 
  1363 
  1377 
  1364 text {* Now the two lemmas *}
 
  1378 text {* Now the two lemmas *}
 
  1365 
  1379 
  1366 lemma perm_aux_expand:
 
  1380 lemma perm_aux_expand:
 
  1367   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1381 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1368   shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)" 
  1382 shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)" 
  1369 unfolding perm_aux_def by (rule refl)
 
  1383 unfolding perm_aux_def by (rule refl)
 
  1370 
  1384 
  1371 lemma perm_compose_aux:
 
  1385 lemma perm_compose_aux:
 
  1372   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1386 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1373   shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)" 
  1387 shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)" 
  1374 unfolding perm_aux_def by (rule perm_compose)
 
  1388 unfolding perm_aux_def by (rule perm_compose)
 
  1375 
  1389 
  1376 text {* 
  1390 text {* 
  1377   are simple consequence of the definition and @{thm [source] perm_compose}. 
  1391   are simple consequence of the definition and @{thm [source] perm_compose}. 
  1378   More importantly, the lemma @{thm [source] perm_compose_aux} can be safely 
  1392   More importantly, the lemma @{thm [source] perm_compose_aux} can be safely 
  1389 *}
 
  1403 *}
 
  1390 
  1404 
  1391 ML %linenosgray{*val perm_simp_tac =
 
  1405 ML %linenosgray{*val perm_simp_tac =
 
  1392 let
 
  1406 let
 
  1393   val thms1 = [@{thm perm_aux_expand}]
 
  1407   val thms1 = [@{thm perm_aux_expand}]
 
  1394   val thms2 = [@{thm perm_append}, @{thm perm_eq}, @{thm perm_rev}, 
  1408   val thms2 = [@{thm perm_append}, @{thm perm_bij}, @{thm perm_rev}, 
  1395                @{thm perm_compose_aux}] @ @{thms perm_prod.simps} @ 
  1409                @{thm perm_compose_aux}] @ @{thms perm_prod.simps} @ 
  1396                @{thms perm_list.simps} @ @{thms perm_nat.simps}
 
  1410                @{thms perm_list.simps} @ @{thms perm_nat.simps}
 
  1397   val thms3 = [@{thm perm_aux_def}]
 
  1411   val thms3 = [@{thm perm_aux_def}]
 
  1398 in
 
  1412 in
 
  1399   simp_tac (HOL_basic_ss addsimps thms1)
 
  1413   simp_tac (HOL_basic_ss addsimps thms1)
 
  1406   for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
 
  1420   for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
 
  1407   the desired results. Now we can solve the following lemma
 
  1421   the desired results. Now we can solve the following lemma
 
  1408 *}
 
  1422 *}
 
  1409 
  1423 
  1410 lemma 
  1424 lemma 
  1411   fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1425 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 
  1412   shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 
  1426 shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
 
  1413 apply(tactic {* perm_simp_tac 1 *})
 
  1427 apply(tactic {* perm_simp_tac 1 *})
 
  1414 done
 
  1428 done
 
  1415 
  1429 
  1416 
  1430 
  1417 text {*
 
  1431 text {*
isabelle-cookbook