Changeset 2681 for src/joint/Joint.ma


Ignore:
Timestamp:
Feb 19, 2013, 6:48:32 PM (7 years ago)
Author:
tranquil
Message:
  • improvements to the graph translation function
  • fixed passes up to LTL
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2655 r2681  
    416416}.
    417417
     418definition code_in_universe : ∀p,globals.
     419  codeT p globals → universe LabelTag → Prop ≝
     420  λp,globals,c,u.∀l.code_has_label … c l → fresh_for_univ … l u.
     421
     422lemma memb_to_present : ∀tag,A.∀i : identifier tag.∀m.
     423  i ∈ m → present tag A m i.
     424#tag #A #i #m whd in ⊢ (?%→%); cases (lookup tag A m i)
     425[ * | #x #_ % #ABS destruct ]
     426qed.
     427
     428lemma present_to_memb : ∀tag,A.∀i : identifier tag.∀m.
     429  present tag A m i → bool_to_Prop (i∈m).
     430#tag #A #i #m whd in ⊢ (%→?%); cases (lookup tag A m i)
     431[ * #ABS cases (ABS (refl …)) | #x #_ % ]
     432qed.
     433
     434lemma graph_code_in_universe_if : ∀p : graph_params.∀globals.
     435  ∀c : codeT p globals.∀u.fresh_map_for_univ … c u → code_in_universe … c u ≝
     436λp,g,c,u,H,l,G.H ? (memb_to_present … G).
     437
     438lemma graph_code_in_universe_only_if : ∀p : graph_params.∀globals.
     439  ∀c : codeT p globals.∀u.
     440  code_in_universe … c u → fresh_map_for_univ … c u ≝
     441λp,g,c,u,H,l,G.H ? (present_to_memb … G).
     442
     443include alias "basics/logic.ma".
     444
     445record good_if
     446(p : params) (globals : list ident) (def : joint_internal_function p globals)
     447: Prop ≝
     448{ unique_cost_labels :
     449  ∀l1,l2,c,nxt1,nxt2.
     450        stmt_at … (joint_if_code … def) l1 =
     451          Some … (sequential … (COST_LABEL … c) nxt1) →
     452        stmt_at … (joint_if_code … def) l2 =
     453          Some … (sequential … (COST_LABEL … c) nxt2) →
     454        l1 = l2
     455; entry_costed :
     456  ∃l,nxt.
     457        stmt_at … (joint_if_code … def) (joint_if_entry … def) =
     458          Some … (sequential … (COST_LABEL … l) nxt)
     459; code_is_closed : code_closed … (joint_if_code … def)
     460; code_is_in_universe :
     461  code_in_universe … (joint_if_code … def) (joint_if_luniverse … def)
     462}.
     463 
    418464definition joint_closed_internal_function ≝
    419465  λp,globals.
    420     Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def).
     466    Σdef : joint_internal_function p globals.good_if … def.
    421467
    422468unification hint 0 ≔ p,g ⊢
    423469  joint_closed_internal_function p g ≡
    424   Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)).
     470  Sig (joint_internal_function p g) (λdef.good_if … def).
    425471
    426472definition set_joint_code ≝
Note: See TracChangeset for help on using the changeset viewer.