src/HOL/Induct/Exp.ML
changeset 4264 5e21f41ccd21
parent 4089 96fba19bcbe2
child 4477 b3e5857d8d99
equal deleted inserted replaced
4263:a434327aef8b 4264:5e21f41ccd21
    55 by (rtac (major RS eval.induct) 1);
    55 by (rtac (major RS eval.induct) 1);
    56 by (blast_tac (claset() addIs prems) 1);
    56 by (blast_tac (claset() addIs prems) 1);
    57 by (blast_tac (claset() addIs prems) 1);
    57 by (blast_tac (claset() addIs prems) 1);
    58 by (blast_tac (claset() addIs prems) 1);
    58 by (blast_tac (claset() addIs prems) 1);
    59 by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1);
    59 by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1);
    60 by (fast_tac (claset() addIs prems addss (simpset() addsimps [split_lemma])) 1);
    60 by (auto_tac (claset() addIs prems,simpset() addsimps [split_lemma]));
    61 qed "eval_induct";
    61 qed "eval_induct";
    62 
    62 
    63 
    63 
    64 (*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
    64 (*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
    65   using eval restricted to its functional part.  Note that the execution
    65   using eval restricted to its functional part.  Note that the execution
    85 by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
    85 by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
    86 qed "com_Unique";
    86 qed "com_Unique";
    87 
    87 
    88 
    88 
    89 (*Expression evaluation is functional, or deterministic*)
    89 (*Expression evaluation is functional, or deterministic*)
    90 goal thy "Function eval";
    90 goalw thy [Function_def] "Function eval";
    91 by (simp_tac (simpset() addsimps [Function_def]) 1);
    91 by (strip_tac 1);
    92 by (REPEAT (rtac allI 1));
    92 by (split_all_tac 1);
    93 by (rtac impI 1);
       
    94 by (etac eval_induct 1);
    93 by (etac eval_induct 1);
    95 by (dtac com_Unique 4);
    94 by (dtac com_Unique 4);
    96 by (ALLGOALS (full_simp_tac (simpset() addsimps [Unique_def])));
    95 by (ALLGOALS (full_simp_tac (simpset() addsimps [Unique_def])));
    97 by (ALLGOALS Blast_tac);
    96 by (ALLGOALS Blast_tac);
    98 qed "Function_eval";
    97 qed "Function_eval";