src/HOLCF/IOA/ex/TrivEx.ML
author mueller
Thu Apr 22 11:06:35 1999 +0200 (1999-04-22)
changeset 6470 f3015fd68d66
child 8600 a466c687c726
permissions -rw-r--r--
moved this trivial example to new ex dir;
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);
mueller@6470
    25
by (simp_tac (simpset() addsimps [h_abs_def]) 1);
mueller@6470
    26
by (induct_tac "a" 1);
mueller@6470
    27
by Auto_tac;
mueller@6470
    28
qed"h_abs_is_abstraction";
mueller@6470
    29
mueller@6470
    30
mueller@6470
    31
Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
mueller@6470
    32
by (rtac AbsRuleT1 1);
mueller@6470
    33
by (rtac h_abs_is_abstraction 1);
mueller@6470
    34
by (rtac MC_result 1);
mueller@6470
    35
by (abstraction_tac 1);
mueller@6470
    36
by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
mueller@6470
    37
qed"TrivEx_abstraction";
mueller@6470
    38
mueller@6470
    39