Jak założyć drugi przypadek dowodu Isabelle/Isar w konkretnych przypadkach?

Question

Mam dowód Isabelle następującą strukturę:

proof (cases "n = 0") 
    case True 
    (* lots of stuff here *) 
    show ?thesis sorry 
next 
    case False 
    (* lots of stuff here too *) 
    show ?thesis sorry 
qed 

Pierwszy przypadek jest rzeczywiście kilka stron, więc podczas czytania drugim przypadku nie jest już jasne, do przypadkowego czytelnika, nawet do siebie, co False odnosi się do. (Cóż, w rzeczywistości jest to jest, ale nie z czytania, tylko w środowisku interaktywnym: Jeśli, na przykład, w Isabelle/jEdit, umieścisz kursor po case False, zobaczysz n ≠ 0 pod "to" w panelu Wyjście.)

A więc istnieje składnia, która pozwala jednoznacznie przypisać założenie sprawy "Fałszywe", aby czytelnik nie musiał wchodzić w interakcję z IDE, ani przewijać słowa kluczowego proof, ale widzi założenie na miejscu?

Answer 1

W tym przypadku dowód staje się bardziej czytelny, stwierdzając założenie każdorazowo wyraźnie:

proof cases 
    assume "n = 0" 
    show ?thesis sorry 
next 
    assume "n ≠ 0" 
    show ?thesis sorry 
qed 

Answer 2

Jeśli sprawa False jest krótszy, wystarczy umieścić go w pierwszej kolejności. Kolejność prób w bloku Isar nie ma znaczenia:

proof (cases "n = 0") 
    case False 
    show ?thesis sorry 
next 
    case True 
    show ?thesis sorry 
qed 

Answer 3

Isar pozwala na wiele wariantów tego samego tematu. Z zachowaniem oryginalnego zarysu, można dokonać faktów pośrednich wyraźne tak:

proof (cases "n = 0") 
    case True 
    (* lots of stuff here *) 
    from `n = 0` show ?thesis sorry 
next 
    case False 
    (* lots of stuff here too *) 
    from `n ≠ 0` show ?thesis sorry 
qed 

Jest to konserwatywny rozszerzenie oryginalnego dowodu zarysie, to znaczy nie wprowadza żadnych zmian w polityce sprawdzenie, unifikacji, wyszukiwania itd.

ogół postać

note `prop` 

odpowiada

have "prop" by fact