src/HOLCF/IOA/ex/TrivEx.ML
author nipkow
Tue Mar 28 17:31:36 2000 +0200 (2000-03-28)
changeset 8600 a466c687c726
parent 6470 f3015fd68d66
child 12218 6597093b77e7
permissions -rw-r--r--
mods because of weak_case_cong
mueller@6470
     1
(*  Title:      HOLCF/IOA/TrivEx.thy
mueller@6470
     2
    ID:         $Id$
mueller@6470
     3
    Author:     Olaf Mueller
mueller@6470
     4
    Copyright   1995  TU Muenchen
mueller@6470
     5
mueller@6470
     6
Trivial Abstraction Example
mueller@6470
     7
*)
mueller@6470
     8
mueller@6470
     9
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
mueller@6470
    10
  by (fast_tac (claset() addDs prems) 1);
mueller@6470
    11
qed "imp_conj_lemma";
mueller@6470
    12
mueller@6470
    13
mueller@6470
    14
Goalw [is_abstraction_def] 
mueller@6470
    15
"is_abstraction h_abs C_ioa A_ioa";
mueller@6470
    16
by (rtac conjI 1);
mueller@6470
    17
(* ------------- start states ------------ *)
mueller@6470
    18
by (simp_tac (simpset() addsimps 
mueller@6470
    19
    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
mueller@6470
    20
(* -------------- step case ---------------- *)
mueller@6470
    21
by (REPEAT (rtac allI 1));
mueller@6470
    22
by (rtac imp_conj_lemma 1);
mueller@6470
    23
by (simp_tac (simpset() addsimps [trans_of_def,
mueller@6470
    24
        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
nipkow@8600
    25
by (induct_tac "a" 1);
mueller@6470
    26
by (simp_tac (simpset() addsimps [h_abs_def]) 1);
mueller@6470
    27
qed"h_abs_is_abstraction";
mueller@6470
    28
mueller@6470
    29
mueller@6470
    30
Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
mueller@6470
    31
by (rtac AbsRuleT1 1);
mueller@6470
    32
by (rtac h_abs_is_abstraction 1);
mueller@6470
    33
by (rtac MC_result 1);
mueller@6470
    34
by (abstraction_tac 1);
mueller@6470
    35
by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
mueller@6470
    36
qed"TrivEx_abstraction";
mueller@6470
    37
mueller@6470
    38