1320 *} |
1320 *} |
1321 |
1321 |
1322 simproc_setup let_simp ("Let x f") = {* |
1322 simproc_setup let_simp ("Let x f") = {* |
1323 let |
1323 let |
1324 val (f_Let_unfold, x_Let_unfold) = |
1324 val (f_Let_unfold, x_Let_unfold) = |
1325 let val [(_$(f$x)$_)] = prems_of @{thm Let_unfold} |
1325 let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_unfold} |
1326 in (cterm_of @{theory} f, cterm_of @{theory} x) end |
1326 in (cterm_of @{theory} f, cterm_of @{theory} x) end |
1327 val (f_Let_folded, x_Let_folded) = |
1327 val (f_Let_folded, x_Let_folded) = |
1328 let val [(_$(f$x)$_)] = prems_of @{thm Let_folded} |
1328 let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_folded} |
1329 in (cterm_of @{theory} f, cterm_of @{theory} x) end; |
1329 in (cterm_of @{theory} f, cterm_of @{theory} x) end; |
1330 val g_Let_folded = |
1330 val g_Let_folded = |
1331 let val [(_$_$(g$_))] = prems_of @{thm Let_folded} in cterm_of @{theory} g end; |
1331 let val [(_ $ _ $ (g $ _))] = prems_of @{thm Let_folded} |
1332 |
1332 in cterm_of @{theory} g end; |
1333 fun proc _ ss ct = |
1333 fun count_loose (Bound i) k = if i >= k then 1 else 0 |
1334 let |
1334 | count_loose (s $ t) k = count_loose s k + count_loose t k |
1335 val ctxt = Simplifier.the_context ss; |
1335 | count_loose (Abs (_, _, t)) k = count_loose t (k + 1) |
1336 val thy = ProofContext.theory_of ctxt; |
1336 | count_loose _ _ = 0; |
1337 val t = Thm.term_of ct; |
1337 fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) = |
1338 val ([t'], ctxt') = Variable.import_terms false [t] ctxt; |
1338 case t |
1339 in Option.map (hd o Variable.export ctxt' ctxt o single) |
1339 of Abs (_, _, t') => count_loose t' 0 <= 1 |
1340 (case t' of Const ("Let",_) $ x $ f => (* x and f are already in normal form *) |
1340 | _ => true; |
1341 if is_Free x orelse is_Bound x orelse is_Const x |
1341 in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct) |
1342 then SOME @{thm Let_def} |
1342 then SOME @{thm Let_def} (*no or one ocurrenc of bound variable*) |
1343 else |
1343 else let (*Norbert Schirmer's case*) |
1344 let |
1344 val ctxt = Simplifier.the_context ss; |
1345 val n = case f of (Abs (x,_,_)) => x | _ => "x"; |
1345 val thy = ProofContext.theory_of ctxt; |
1346 val cx = cterm_of thy x; |
1346 val t = Thm.term_of ct; |
1347 val {T=xT,...} = rep_cterm cx; |
1347 val ([t'], ctxt') = Variable.import_terms false [t] ctxt; |
1348 val cf = cterm_of thy f; |
1348 in Option.map (hd o Variable.export ctxt' ctxt o single) |
1349 val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); |
1349 (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *) |
1350 val (_$_$g) = prop_of fx_g; |
1350 if is_Free x orelse is_Bound x orelse is_Const x |
1351 val g' = abstract_over (x,g); |
1351 then SOME @{thm Let_def} |
1352 in (if (g aconv g') |
1352 else |
1353 then |
1353 let |
1354 let |
1354 val n = case f of (Abs (x, _, _)) => x | _ => "x"; |
1355 val rl = |
1355 val cx = cterm_of thy x; |
1356 cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] @{thm Let_unfold}; |
1356 val {T = xT, ...} = rep_cterm cx; |
1357 in SOME (rl OF [fx_g]) end |
1357 val cf = cterm_of thy f; |
1358 else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*) |
1358 val fx_g = Simplifier.rewrite ss (Thm.capply cf cx); |
1359 else let |
1359 val (_ $ _ $ g) = prop_of fx_g; |
1360 val abs_g'= Abs (n,xT,g'); |
1360 val g' = abstract_over (x,g); |
1361 val g'x = abs_g'$x; |
1361 in (if (g aconv g') |
1362 val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x)); |
1362 then |
1363 val rl = cterm_instantiate |
1363 let |
1364 [(f_Let_folded,cterm_of thy f),(x_Let_folded,cx), |
1364 val rl = |
1365 (g_Let_folded,cterm_of thy abs_g')] |
1365 cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold}; |
1366 @{thm Let_folded}; |
1366 in SOME (rl OF [fx_g]) end |
1367 in SOME (rl OF [transitive fx_g g_g'x]) |
1367 else if Term.betapply (f, x) aconv g then NONE (*avoid identity conversion*) |
1368 end) |
1368 else let |
1369 end |
1369 val abs_g'= Abs (n,xT,g'); |
1370 | _ => NONE) |
1370 val g'x = abs_g'$x; |
1371 end |
1371 val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x)); |
1372 in proc end *} |
1372 val rl = cterm_instantiate |
1373 |
1373 [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx), |
|
1374 (g_Let_folded, cterm_of thy abs_g')] |
|
1375 @{thm Let_folded}; |
|
1376 in SOME (rl OF [transitive fx_g g_g'x]) |
|
1377 end) |
|
1378 end |
|
1379 | _ => NONE) |
|
1380 end |
|
1381 end *} |
1374 |
1382 |
1375 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
1383 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
1376 proof |
1384 proof |
1377 assume "True \<Longrightarrow> PROP P" |
1385 assume "True \<Longrightarrow> PROP P" |
1378 from this [OF TrueI] show "PROP P" . |
1386 from this [OF TrueI] show "PROP P" . |