340 print_theorems |
340 print_theorems |
341 |
341 |
342 |
342 |
343 section {*** lets with many assignments ***} |
343 section {*** lets with many assignments ***} |
344 |
344 |
345 datatype trm3 = |
345 datatype rtrm3 = |
346 Vr3 "name" |
346 rVr3 "name" |
347 | Ap3 "trm3" "trm3" |
347 | rAp3 "rtrm3" "rtrm3" |
348 | Lm3 "name" "trm3" --"bind (name) in (trm3)" |
348 | rLm3 "name" "rtrm3" --"bind (name) in (trm3)" |
349 | Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)" |
349 | rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)" |
350 and assigns = |
350 and rassigns = |
351 ANil |
351 rANil |
352 | ACons "name" "trm3" "assigns" |
352 | rACons "name" "rtrm3" "rassigns" |
353 |
353 |
354 (* to be given by the user *) |
354 (* to be given by the user *) |
355 primrec |
355 primrec |
356 bv3 |
356 bv3 |
357 where |
357 where |
358 "bv3 ANil = {}" |
358 "bv3 rANil = {}" |
359 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
359 | "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)" |
360 |
360 |
361 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} |
361 setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *} |
362 |
362 |
363 local_setup {* snd o define_fv_alpha "Terms.trm3" |
363 local_setup {* snd o define_fv_alpha "Terms.rtrm3" |
364 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], |
364 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], |
365 [[], [[], [], []]]] *} |
365 [[], [[], [], []]]] *} |
366 print_theorems |
366 print_theorems |
367 |
367 |
368 notation |
368 notation |
369 alpha_trm3 ("_ \<approx>3 _" [100, 100] 100) and |
369 alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and |
370 alpha_assigns ("_ \<approx>3a _" [100, 100] 100) |
370 alpha_rassigns ("_ \<approx>3a _" [100, 100] 100) |
371 thm alpha_trm3_alpha_assigns.intros |
371 thm alpha_rtrm3_alpha_rassigns.intros |
372 |
372 |
373 lemma alpha3_equivp: |
373 lemma alpha3_equivp: |
374 "equivp alpha_trm3" |
374 "equivp alpha_rtrm3" |
375 "equivp alpha_assigns" |
375 "equivp alpha_rassigns" |
376 sorry |
376 sorry |
377 |
377 |
378 quotient_type |
378 quotient_type |
379 qtrm3 = trm3 / alpha_trm3 |
379 trm3 = rtrm3 / alpha_rtrm3 |
380 and |
380 and |
381 qassigns = assigns / alpha_assigns |
381 assigns = rassigns / alpha_rassigns |
382 by (auto intro: alpha3_equivp) |
382 by (auto intro: alpha3_equivp) |
383 |
383 |
384 |
384 |
385 section {*** lam with indirect list recursion ***} |
385 section {*** lam with indirect list recursion ***} |
386 |
386 |
387 datatype trm4 = |
387 datatype rtrm4 = |
388 Vr4 "name" |
388 rVr4 "name" |
389 | Ap4 "trm4" "trm4 list" |
389 | rAp4 "rtrm4" "rtrm4 list" |
390 | Lm4 "name" "trm4" --"bind (name) in (trm)" |
390 | rLm4 "name" "rtrm4" --"bind (name) in (trm)" |
391 print_theorems |
391 |
392 |
392 thm rtrm4.recs |
393 thm trm4.recs |
|
394 |
393 |
395 (* there cannot be a clause for lists, as *) |
394 (* there cannot be a clause for lists, as *) |
396 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
395 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
397 setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *} |
396 setup {* snd o define_raw_perms ["rtrm4"] ["Terms.rtrm4"] *} |
398 |
397 |
399 (* "repairing" of the permute function *) |
398 (* "repairing" of the permute function *) |
400 lemma repaired: |
399 lemma repaired: |
401 fixes ts::"trm4 list" |
400 fixes ts::"rtrm4 list" |
402 shows "permute_trm4_list p ts = p \<bullet> ts" |
401 shows "permute_rtrm4_list p ts = p \<bullet> ts" |
403 apply(induct ts) |
402 apply(induct ts) |
404 apply(simp_all) |
403 apply(simp_all) |
405 done |
404 done |
406 |
405 |
407 thm permute_trm4_permute_trm4_list.simps |
406 thm permute_rtrm4_permute_rtrm4_list.simps |
408 thm permute_trm4_permute_trm4_list.simps[simplified repaired] |
407 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
409 |
408 |
410 local_setup {* snd o define_fv_alpha "Terms.trm4" [ |
409 local_setup {* snd o define_fv_alpha "Terms.rtrm4" [ |
411 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} |
410 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} |
412 print_theorems |
411 print_theorems |
413 |
412 |
414 notation |
413 notation |
415 alpha_trm4 ("_ \<approx>4 _" [100, 100] 100) and |
414 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
416 alpha_trm4_list ("_ \<approx>4l _" [100, 100] 100) |
415 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
417 thm alpha_trm4_alpha_trm4_list.intros |
416 thm alpha_rtrm4_alpha_rtrm4_list.intros |
418 |
417 |
419 lemma alpha4_equivp: "equivp alpha_trm4" sorry |
418 lemma alpha4_equivp: "equivp alpha_rtrm4" sorry |
420 lemma alpha4list_equivp: "equivp alpha_trm4_list" sorry |
419 lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry |
421 |
420 |
422 quotient_type |
421 quotient_type |
423 qtrm4 = trm4 / alpha_trm4 and |
422 qrtrm4 = rtrm4 / alpha_rtrm4 and |
424 qtrm4list = "trm4 list" / alpha_trm4_list |
423 qrtrm4list = "rtrm4 list" / alpha_rtrm4_list |
425 by (simp_all add: alpha4_equivp alpha4list_equivp) |
424 by (simp_all add: alpha4_equivp alpha4list_equivp) |
426 |
425 |
427 |
426 |
428 datatype rtrm5 = |
427 datatype rtrm5 = |
429 rVr5 "name" |
428 rVr5 "name" |